Expand some NORACE annotations

goblint · Jan 20, 2022 · a9e03d8 · a9e03d8
1 parent 814cd11
commit a9e03d8
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/tests/regression/04-mutex/27-base_rc.c b/tests/regression/04-mutex/27-base_rc.c
@@ -9,7 +9,7 @@ void bad() {
 }
 void good() {
   pthread_mutex_lock(&gm);
-  global++; // NORACE (MHP)
+  global++; // NORACE (same unique thread with bad, same lock with main)
   pthread_mutex_unlock(&gm);
 }
 

diff --git a/tests/regression/04-mutex/35-trylock_rc.c b/tests/regression/04-mutex/35-trylock_rc.c
@@ -49,7 +49,7 @@ void *monitor_thread (void *arg) {
     if (status != EBUSY) {
       if (status != 0)
         err_abort (status, "Trylock mutex");
-      printf ("Counter is %ld\n", counter/SPIN); // NORACE (MHP)
+      printf ("Counter is %ld\n", counter/SPIN); // NORACE (same lock with counter_thread, same unique thread with monitor_thread)
       status = pthread_mutex_unlock (&mutex);
       if (status != 0)
         err_abort (status, "Unlock mutex");

diff --git a/tests/regression/10-synch/12-join_rc.c b/tests/regression/10-synch/12-join_rc.c
@@ -18,7 +18,7 @@ int main(void) {
   for (i=0; i<10; i++)
     pthread_create(&id[i], NULL, t_fun, NULL);
   pthread_mutex_lock(&mutex);
-  myglobal=myglobal+1; // NORACE (MHP)
+  myglobal=myglobal+1; // NORACE (same lock with t_fun, same unique thread with main)
   pthread_mutex_unlock(&mutex);
   for (i=0; i<9; i++)
     pthread_join(id[i], NULL);

diff --git a/tests/regression/53-races-mhp/03-not-created_rc.c b/tests/regression/53-races-mhp/03-not-created_rc.c
@@ -19,7 +19,7 @@ void *t_fun2(void *arg) {
 int main(void) {
   pthread_t id, id2;
   pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
-  myglobal = 5; // NORACE
+  myglobal = 5; // NORACE (MHP, t_fun2 not yet created, same unique thread with main)
 
   pthread_create(&id2, NULL, t_fun2, NULL);
   pthread_mutex_lock(&mutex2);