Use cond vars instead of busy loops in race challenges

goblint · Sep 21, 2023 · e140813 · e140813
1 parent 28644ca
commit e140813
Show file tree

Hide file tree

Showing 4 changed files with 21 additions and 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
@@ -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
@@ -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
@@ -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
@@ -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);