Unexpected behavior of __VERIFIER_assume in multithreaded contexts

[41968]

CBMC version: 6.3.1 (cbmc-6.3.1-10-g83922b2f54-dirty)

Operating system: macOS 15.0

Exact command line resulting in the issue:

cbmc --no-pointer-primitive-check --no-pointer-check --no-standard-checks multithreaded_assume.c

To allow the above command to execute successfully, I added the following line before line 110 (if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)) in src/goto-symex/goto_symex_state.cpp:

allow_pointer_unsoundness = true;

with multithreaded_assume.c:

// file: multithreaded_assume.c
#include <assert.h>
#include <pthread.h>

int x;

void* thread_function1(void* arg)
{
    __VERIFIER_atomic_begin();
    x = __VERIFIER_nondet_int(); // s1
    __VERIFIER_assume(x == 42);  // s2
    __VERIFIER_atomic_end();
    assert(x == 42);             // s3
}

void* thread_function2(void* arg)
{
    __VERIFIER_atomic_begin();
    x = __VERIFIER_nondet_int(); // s4
    __VERIFIER_assume(x == 42);  // s5
    __VERIFIER_atomic_end();
    assert(x == 42);             // s6
}

int main()
{
    pthread_t t_id1, t_id2;
    pthread_create(&t_id1, 0, thread_function1, 0);
    pthread_create(&t_id2, 0, thread_function2, 0);
    pthread_join(t_id1, 0);
    pthread_join(t_id2, 0);
    return 0;
}

What behaviour did you expect:

The two assertions in multithreaded_assume.c have been proven to hold.

What happened instead:

CBMC reported that the two assertions were violated, with the output below:

** Results:
<builtin-library-__spawned_thread> function __spawned_thread
[__spawned_thread.pointer_dereference.1] line 41 dereferenced function pointer must be one of [thread_function2, thread_function1]: SUCCESS

examples/multithreaded_assume.c function thread_function1
[thread_function1.assertion.1] line 13 assertion x == 42: FAILURE

examples/multithreaded_assume.c function thread_function2
[thread_function2.assertion.1] line 23 assertion x == 42: FAILURE

** 2 of 3 failed (3 iterations)
VERIFICATION FAILED

I used the option --trace to identify the counterexample causing the violation:

cbmc --trace --no-pointer-primitive-check --no-pointer-check --no-standard-checks multithreaded_assume.c

The trace that violates the assertion in thread_function1 proceeds as follows (with key statements in the program labeled s1,s2,...,s6):

1. s1 is executed, assigning x the value 42
2. s2 is executed and passes the assumption
3. context switches to thread_function2
4. s4 is executed, assigning x the value 40
5. s5 is executed but fails the assumption
6. context switches to thread_function1
7. s3 is executed and fails the assertion

The unexpected behavior is that execution continues even after an assumption is voilated (step 5 in the trace). Here, __VERIFIER_assume appears to act like a thread-local assume, allowing other threads to proceed even when an fails in one thread. However, I expected __VERIFIER_assume to function as a global assume, where execution would block for all threads upon any assumption failure.

Thank you very much for your assistance!