diff --git a/tests/regression/03-practical/31-thread-alive-counter.c b/tests/regression/03-practical/31-thread-alive-counter.c new file mode 100644 index 0000000000..6537ec2856 --- /dev/null +++ b/tests/regression/03-practical/31-thread-alive-counter.c @@ -0,0 +1,75 @@ +// Thread pool joining via threads alive counter. +// Extracted from concrat/C-Thread-Pool. +#include +#include +#include +extern int __VERIFIER_nondet_int(); + +int threads_alive = 0; +pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER; + +bool keep_alive = true; +pthread_mutex_t keep_alive_mutex = PTHREAD_MUTEX_INITIALIZER; + +int data = 0; +pthread_mutex_t data_mutex = PTHREAD_MUTEX_INITIALIZER; + +void *thread(void *arg) { + pthread_mutex_lock(&threads_alive_mutex); + threads_alive++; // NORACE + pthread_mutex_unlock(&threads_alive_mutex); + + pthread_mutex_lock(&keep_alive_mutex); + while (keep_alive) { // NORACE + pthread_mutex_unlock(&keep_alive_mutex); + + pthread_mutex_lock(&data_mutex); + data = __VERIFIER_nondet_int(); // NORACE + pthread_mutex_unlock(&data_mutex); + + pthread_mutex_lock(&keep_alive_mutex); + } + pthread_mutex_unlock(&keep_alive_mutex); + + pthread_mutex_lock(&threads_alive_mutex); + threads_alive--; // NORACE + pthread_mutex_unlock(&threads_alive_mutex); + return NULL; +} + +int main() { + int threads_total = __VERIFIER_nondet_int(); + __goblint_assume(threads_total >= 0); + + // create threads + for (int i = 0; i < threads_total; i++) { + pthread_t tid; + pthread_create(&tid, NULL, &thread, NULL); // may fail but doesn't matter + pthread_detach(tid); + } + + // wait for all threads to come alive + pthread_mutex_lock(&threads_alive_mutex); + while (threads_alive != threads_total) { // NORACE + pthread_mutex_unlock(&threads_alive_mutex); + // busy loop for simplicity + pthread_mutex_lock(&threads_alive_mutex); + } + pthread_mutex_unlock(&threads_alive_mutex); + + // stop threads + pthread_mutex_lock(&keep_alive_mutex); + keep_alive = false; // NORACE + pthread_mutex_unlock(&keep_alive_mutex); + + // wait for all threads to stop + pthread_mutex_lock(&threads_alive_mutex); + while (threads_alive) { // NORACE + pthread_mutex_unlock(&threads_alive_mutex); + // busy loop for simplicity + pthread_mutex_lock(&threads_alive_mutex); + } + pthread_mutex_unlock(&threads_alive_mutex); + + return data; // NORACE (all threads stopped) +}