[Question] Mismatch Between pthread_create Declarations Causes Type Error

[bob-boberman]

Dear CBMC developers,

I'm running into an issue using CBMC 6.6.0 to verify a basic multi-threaded Cpp program. When including <pthread.h>, CBMC reports a type mismatch for pthread_create due to a difference in the parameter types for pthread_attr_t.

Minimal Reproducible Example

#include <pthread.h>
#include <assert.h>

int shared_variable = 0;

void* increment(void* arg) {
    int temp = shared_variable;
    shared_variable = temp + 1;
    return 0;
}

void* decrement(void* arg) {
    int temp = shared_variable;
    shared_variable = temp - 1;
    return 0;
}

int main() {
    pthread_t thread1, thread2;

    pthread_create(&thread1, 0, increment, 0);
    pthread_create(&thread2, 0, decrement, 0);

    pthread_join(thread1, 0);
    pthread_join(thread2, 0);

    __CPROVER_assert(shared_variable == 0, "Race condition detected: shared_variable ");

    return 0;
}

CBMC Output

CBMC version 6.6.0 (cbmc-6.6.0) 64-bit x86_64 linux
Type-checking test_unsafe
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_create> line 27: pointer parameter types differ between declaration and definition 'pthread_create(pthread_t *, const union pthread_attr_t *, auto (*)(void *) -> void *, void *)'
old definition in module test_unsafe file /usr/include/pthread.h line 202
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 27
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
pointer handling for concurrency is unsound

Question

Is there a way to resolve this mismatch cleanly without ignoring pointer checks?

Ideally, I would like to:

• Use pthread without redefining or using work around like __CPROVER_ASYNC
• Allow CBMC to simulate threads or analyze races.
• Still be able to perform standard checks

Thank you in advance :)

[tautschnig]

Can you please provide the operating system (and maybe: GCC version) that you are using and the exact CBMC command line that you were using? Thank you!

[bob-boberman]

Thanks for the fast reply!

I am using Manjaro 25.0.1 Zetar (Arch based distro).

cbmc test.cpp 

Using this version resulted in the output above.

cbmc --no-pointer-primitive-check --no-pointer-check test.cpp 

Without the pointer checks disabled, I get a result and this output here:

CBMC version 6.6.0 (cbmc-6.6.0) 64-bit x86_64 linux
Type-checking test_unsafe
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_create> line 27: pointer parameter types differ between declaration and definition 'pthread_create(pthread_t *, const union pthread_attr_t *, auto (*)(void *) -> void *, void *)'
old definition in module test_unsafe file /usr/include/pthread.h line 202
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 27
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to propositional reduction
converting SSA
Running propositional reduction
SAT checker: instance is SATISFIABLE
Running propositional reduction
SAT checker inconsistent: instance is UNSATISFIABLE

** Results:
/usr/include/pthread.h function ~__pthread_cleanup_class
[~__pthread_cleanup_class.pointer_dereference.1] line 578 dereferenced function pointer must be one of [decrement(ptr_void), increment(ptr_void)]: SUCCESS

<builtin-library-__spawned_thread> function __spawned_thread
[__spawned_thread.pointer_dereference.1] line 41 dereferenced function pointer must be one of [decrement(ptr_void), increment(ptr_void)]: SUCCESS

test_unsafe.cpp function decrement
[decrement.overflow.1] line 24 arithmetic overflow on signed - in temp - 1: SUCCESS

test_unsafe.cpp function increment
[increment.overflow.1] line 18 arithmetic overflow on signed + in temp + 1: SUCCESS

test_unsafe.cpp function main
[main.assertion.1] line 42 Race condition detected: shared_variable : FAILURE

** 1 of 5 failed (2 iterations)
VERIFICATION FAILED

[tautschnig]

I believe you can avoid the initial warning that were seeing about mismatched types by naming your file with a .c suffix instead of .cpp (there is no C++-only code in there).

We still need to review whether our warning about unsoundness in pointer handling is actually warranted for this sort of example. It is possible that we can fix this problem by making some of our instrumentation variables thread-local.

[bob-boberman]

Thanks for the response!

I’m planning to use other C++ features later, so I’d prefer to avoid switching to .c.

Do you think that there’s a way to fix the type mismatch in the current version of CBMC?