From e140813e925dc863a7b585e5f52debb2e3eb5724 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 21 Sep 2023 10:53:21 +0300 Subject: [PATCH] Use cond vars instead of busy loops in race challenges --- .../31-thread-alive-counter-inner.c | 17 +++++++---------- .../34-thread-alive-counter-outer.c | 10 +++++----- .../03-practical/38-value-barrier-norace.c | 9 ++++----- .../49-symbolic-thread-array-alive-counter.c | 10 +++++----- 4 files changed, 21 insertions(+), 25 deletions(-) diff --git a/tests/regression/03-practical/31-thread-alive-counter-inner.c b/tests/regression/03-practical/31-thread-alive-counter-inner.c index 43002ee19a..0a694d2c30 100644 --- a/tests/regression/03-practical/31-thread-alive-counter-inner.c +++ b/tests/regression/03-practical/31-thread-alive-counter-inner.c @@ -7,6 +7,7 @@ extern int __VERIFIER_nondet_int(); int threads_alive = 0; pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_cond_t threads_alive_cond = PTHREAD_COND_INITIALIZER; bool keep_alive = true; pthread_mutex_t keep_alive_mutex = PTHREAD_MUTEX_INITIALIZER; @@ -17,6 +18,7 @@ pthread_mutex_t data_mutex = PTHREAD_MUTEX_INITIALIZER; void *thread(void *arg) { pthread_mutex_lock(&threads_alive_mutex); threads_alive++; // NORACE + pthread_cond_signal(&threads_alive_cond); pthread_mutex_unlock(&threads_alive_mutex); pthread_mutex_lock(&keep_alive_mutex); @@ -33,6 +35,7 @@ void *thread(void *arg) { pthread_mutex_lock(&threads_alive_mutex); threads_alive--; // NORACE + pthread_cond_signal(&threads_alive_cond); pthread_mutex_unlock(&threads_alive_mutex); return NULL; } @@ -50,11 +53,8 @@ int main() { // 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); - } + while (threads_alive != threads_total) // NORACE + pthread_cond_wait(&threads_alive_cond, &threads_alive_mutex); pthread_mutex_unlock(&threads_alive_mutex); // stop threads @@ -64,11 +64,8 @@ int main() { // 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); - } + while (threads_alive) // NORACE + pthread_cond_wait(&threads_alive_cond, &threads_alive_mutex); pthread_mutex_unlock(&threads_alive_mutex); return data; // NORACE (all threads stopped) diff --git a/tests/regression/03-practical/34-thread-alive-counter-outer.c b/tests/regression/03-practical/34-thread-alive-counter-outer.c index 7208a3c09d..7e108a25fe 100644 --- a/tests/regression/03-practical/34-thread-alive-counter-outer.c +++ b/tests/regression/03-practical/34-thread-alive-counter-outer.c @@ -6,6 +6,7 @@ extern int __VERIFIER_nondet_int(); int threads_alive = 0; pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_cond_t threads_alive_cond = PTHREAD_COND_INITIALIZER; int data = 0; pthread_mutex_t data_mutex = PTHREAD_MUTEX_INITIALIZER; @@ -17,6 +18,7 @@ void *thread(void *arg) { pthread_mutex_lock(&threads_alive_mutex); threads_alive--; // NORACE + pthread_cond_signal(&threads_alive_cond); pthread_mutex_unlock(&threads_alive_mutex); return NULL; } @@ -29,6 +31,7 @@ int main() { for (int i = 0; i < threads_total; i++) { pthread_mutex_lock(&threads_alive_mutex); threads_alive++; // NORACE + // no need to signal, because nobody is waiting pthread_mutex_unlock(&threads_alive_mutex); pthread_t tid; @@ -38,11 +41,8 @@ int main() { // 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); - } + while (threads_alive) // NORACE + pthread_cond_wait(&threads_alive_cond, &threads_alive_mutex); pthread_mutex_unlock(&threads_alive_mutex); return data; // NORACE (all threads stopped) diff --git a/tests/regression/03-practical/38-value-barrier-norace.c b/tests/regression/03-practical/38-value-barrier-norace.c index 6fa388bf39..e28c5843bb 100644 --- a/tests/regression/03-practical/38-value-barrier-norace.c +++ b/tests/regression/03-practical/38-value-barrier-norace.c @@ -8,17 +8,15 @@ extern int __VERIFIER_nondet_int(); bool ready = false; pthread_mutex_t ready_mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_cond_t ready_cond = PTHREAD_COND_INITIALIZER; int data = 0; void *thread(void *arg) { // wait for main thread to be ready pthread_mutex_lock(&ready_mutex); - while (!ready) { // NORACE - pthread_mutex_unlock(&ready_mutex); - // busy loop for simplicity - pthread_mutex_lock(&ready_mutex); - } + while (!ready) // NORACE + pthread_cond_wait(&ready_cond, &ready_mutex); pthread_mutex_unlock(&ready_mutex); int x = data; // NORACE (main thread wrote before ready) @@ -41,6 +39,7 @@ int main() { // become ready pthread_mutex_lock(&ready_mutex); ready = true; // NORACE + pthread_cond_broadcast(&ready_cond); pthread_mutex_unlock(&ready_mutex); // join threads diff --git a/tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c b/tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c index 79cb823ac4..da61efb6fa 100644 --- a/tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c +++ b/tests/regression/03-practical/49-symbolic-thread-array-alive-counter.c @@ -12,6 +12,7 @@ extern int __VERIFIER_nondet_int(); int threads_total; int threads_alive = 0; pthread_mutex_t threads_alive_mutex = PTHREAD_MUTEX_INITIALIZER; +pthread_cond_t threads_alive_cond = PTHREAD_COND_INITIALIZER; pthread_t *tids; bool *datas; @@ -33,6 +34,7 @@ void *cleaner(void *arg) { pthread_join(tids[i], NULL); // NORACE pthread_mutex_lock(&threads_alive_mutex); threads_alive--; // NORACE + pthread_cond_signal(&threads_alive_cond); pthread_mutex_unlock(&threads_alive_mutex); datas[i] = false; // NORACE } @@ -62,16 +64,14 @@ int main() { pthread_mutex_lock(&threads_alive_mutex); threads_alive++; // NORACE + pthread_cond_signal(&threads_alive_cond); pthread_mutex_unlock(&threads_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); - } + while (threads_alive) // NORACE + pthread_cond_wait(&threads_alive_cond, &threads_alive_mutex); pthread_mutex_unlock(&threads_alive_mutex); free(tids);