diff --git a/tests/regression/03-practical/31-thread-alive-counter.c b/tests/regression/03-practical/31-thread-alive-counter-inner.c similarity index 96% rename from tests/regression/03-practical/31-thread-alive-counter.c rename to tests/regression/03-practical/31-thread-alive-counter-inner.c index 6537ec2856..43002ee19a 100644 --- a/tests/regression/03-practical/31-thread-alive-counter.c +++ b/tests/regression/03-practical/31-thread-alive-counter-inner.c @@ -1,4 +1,4 @@ -// Thread pool joining via threads alive counter. +// Thread pool joining via threads alive counter incremented inside of thread. // Extracted from concrat/C-Thread-Pool. #include #include diff --git a/tests/regression/03-practical/34-thread-alive-counter-outer.c b/tests/regression/03-practical/34-thread-alive-counter-outer.c new file mode 100644 index 0000000000..7208a3c09d --- /dev/null +++ b/tests/regression/03-practical/34-thread-alive-counter-outer.c @@ -0,0 +1,49 @@ +// Thread pool joining via threads alive counter incremented outside of thread. +// Extracted from concrat/nnn. +#include +#include +extern int __VERIFIER_nondet_int(); + +int threads_alive = 0; +pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER; + +int data = 0; +pthread_mutex_t data_mutex = PTHREAD_MUTEX_INITIALIZER; + +void *thread(void *arg) { + pthread_mutex_lock(&data_mutex); + data = __VERIFIER_nondet_int(); // NORACE + pthread_mutex_unlock(&data_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_mutex_lock(&threads_alive_mutex); + threads_alive++; // NORACE + pthread_mutex_unlock(&threads_alive_mutex); + + pthread_t tid; + pthread_create(&tid, NULL, &thread, NULL); // may fail but doesn't matter + pthread_detach(tid); + } + + // 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) +}