Port undefined behavior fixes from #1164 to goblint-regression races-as-reachability benchmarks

sim642 · sim642 · commit 4eb3b2cef73d · 2020-10-17T13:28:24.000+03:00
diff --git a/c/goblint-regression/28-race_reach_23-sound_unlock_racing.c b/c/goblint-regression/28-race_reach_23-sound_unlock_racing.c
@@ -2,8 +2,9 @@
 #include "racemacros.h"
 
 int global = 0;
-pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutexattr_t mutexattr;
+pthread_mutex_t mutex1;
+pthread_mutex_t mutex2;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex1);
@@ -13,14 +14,19 @@ void *t_fun(void *arg) {
 }
 
 int main(void) {
+  pthread_mutexattr_init(&mutexattr);
+  pthread_mutexattr_settype(&mutexattr, PTHREAD_MUTEX_ERRORCHECK);
+  pthread_mutex_init(&mutex1, &mutexattr);
+  pthread_mutex_init(&mutex2, &mutexattr);
+
   int i = __VERIFIER_nondet_int();
   pthread_mutex_t *m = &mutex1;
   if (i) m = &mutex2;
   create_threads(t);
   pthread_mutex_lock(&mutex1);
-  pthread_mutex_unlock(m);
+  pthread_mutex_unlock(m); // no UB because ERRORCHECK
   assert_racefree(global); // UNKNOWN
-  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(&mutex1); // no UB because ERRORCHECK
   join_threads(t);
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_23-sound_unlock_racing.i b/c/goblint-regression/28-race_reach_23-sound_unlock_racing.i
@@ -688,15 +688,20 @@ void assume_abort_if_not(int cond) {
 }
 pthread_mutex_t __global_lock = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
 int global = 0;
-pthread_mutex_t mutex1 = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
-pthread_mutex_t mutex2 = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
+pthread_mutexattr_t mutexattr;
+pthread_mutex_t mutex1;
+pthread_mutex_t mutex2;
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex1);
   do { do { pthread_mutex_lock(&__global_lock); (global)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (global)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
   pthread_mutex_unlock(&mutex1);
   return ((void *)0);
 }
 int main(void) {
+  pthread_mutexattr_init(&mutexattr);
+  pthread_mutexattr_settype(&mutexattr, PTHREAD_MUTEX_ERRORCHECK);
+  pthread_mutex_init(&mutex1, &mutexattr);
+  pthread_mutex_init(&mutex2, &mutexattr);
   int i = __VERIFIER_nondet_int();
   pthread_mutex_t *m = &mutex1;
   if (i) m = &mutex2;
diff --git a/c/goblint-regression/28-race_reach_36-indirect_racefree.c b/c/goblint-regression/28-race_reach_36-indirect_racefree.c
@@ -10,7 +10,7 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
   access(*g1);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   return NULL;
 }
 
@@ -20,7 +20,7 @@ int main(void) {
   create_threads(t);
   pthread_mutex_lock(&mutex);
   assert_racefree(*g2);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   join_threads(t);
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_36-indirect_racefree.i b/c/goblint-regression/28-race_reach_36-indirect_racefree.i
@@ -694,15 +694,15 @@ pthread_mutex_t mutex = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
   do { do { pthread_mutex_lock(&__global_lock); (*g1)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (*g1)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   return ((void *)0);
 }
 int main(void) {
   g1 = g2 = &g;
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   pthread_mutex_lock(&mutex);
   do { pthread_mutex_lock(&__global_lock); __VERIFIER_assert((*g2) == 0); pthread_mutex_unlock(&__global_lock); } while (0);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   for (int i=0; i < 10000; i++) pthread_join (t_ids[i], ((void *)0));
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_37-indirect_racing.c b/c/goblint-regression/28-race_reach_37-indirect_racing.c
@@ -10,7 +10,7 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
   access(*g1);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   return NULL;
 }
 
diff --git a/c/goblint-regression/28-race_reach_37-indirect_racing.i b/c/goblint-regression/28-race_reach_37-indirect_racing.i
@@ -694,7 +694,7 @@ pthread_mutex_t mutex = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
   do { do { pthread_mutex_lock(&__global_lock); (*g1)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (*g1)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
-  pthread_mutex_lock(&mutex);
+  pthread_mutex_unlock(&mutex);
   return ((void *)0);
 }
 int main(void) {
diff --git a/c/goblint-regression/28-race_reach_40-trylock_racing.c b/c/goblint-regression/28-race_reach_40-trylock_racing.c
@@ -2,7 +2,8 @@
 #include "racemacros.h"
 
 int global;
-pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutexattr_t mutexattr;
+pthread_mutex_t mutex;
 
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
@@ -13,11 +14,15 @@ void *t_fun(void *arg) {
 }
 
 int main(void) {
+  pthread_mutexattr_init(&mutexattr);
+  pthread_mutexattr_settype(&mutexattr, PTHREAD_MUTEX_ERRORCHECK);
+  pthread_mutex_init(&mutex, &mutexattr);
+
   create_threads(t);
 
   pthread_mutex_trylock(&mutex);
   assert_racefree(global); // UNKNOWN
-  pthread_mutex_unlock(&mutex);
+  pthread_mutex_unlock(&mutex); // no UB because ERRORCHECK
   join_threads(t);
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_40-trylock_racing.i b/c/goblint-regression/28-race_reach_40-trylock_racing.i
@@ -688,14 +688,18 @@ void assume_abort_if_not(int cond) {
 }
 pthread_mutex_t __global_lock = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
 int global;
-pthread_mutex_t mutex = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };
+pthread_mutexattr_t mutexattr;
+pthread_mutex_t mutex;
 void *t_fun(void *arg) {
   pthread_mutex_lock(&mutex);
   do { do { pthread_mutex_lock(&__global_lock); (global)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (global)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
   pthread_mutex_unlock(&mutex);
   return ((void *)0);
 }
 int main(void) {
+  pthread_mutexattr_init(&mutexattr);
+  pthread_mutexattr_settype(&mutexattr, PTHREAD_MUTEX_ERRORCHECK);
+  pthread_mutex_init(&mutex, &mutexattr);
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   pthread_mutex_trylock(&mutex);
   do { pthread_mutex_lock(&__global_lock); __VERIFIER_assert((global) == 0); pthread_mutex_unlock(&__global_lock); } while (0);
diff --git a/c/goblint-regression/28-race_reach_70-funloop_racefree.c b/c/goblint-regression/28-race_reach_70-funloop_racefree.c
@@ -21,6 +21,9 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
   int i;
   create_threads(t);
 
diff --git a/c/goblint-regression/28-race_reach_70-funloop_racefree.i b/c/goblint-regression/28-race_reach_70-funloop_racefree.i
@@ -941,6 +941,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, ((void *)0));
   int i;
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   for(i=0; i<10; i++)
diff --git a/c/goblint-regression/28-race_reach_71-funloop_racing.c b/c/goblint-regression/28-race_reach_71-funloop_racing.c
@@ -21,9 +21,12 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
   int i;
   create_threads(t);
-  
+
   for(i=0; i<10; i++)
     cache_entry_addref(&cache[i]);
   access_or_assert_racefree(cache[5].refs); // UNKNOWN
diff --git a/c/goblint-regression/28-race_reach_71-funloop_racing.i b/c/goblint-regression/28-race_reach_71-funloop_racing.i
@@ -941,6 +941,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, ((void *)0));
   int i;
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   for(i=0; i<10; i++)
diff --git a/c/goblint-regression/28-race_reach_72-funloop_hard_racing.c b/c/goblint-regression/28-race_reach_72-funloop_hard_racing.c
@@ -20,14 +20,17 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
   int i;
   create_threads(t);
 
   for(i=0; i<10; i++) cache_entry_addref(&cache[i]);
 
   pthread_mutex_lock(&cache[4].refs_mutex);
   access_or_assert_racefree(cache[5].refs); // UNKNOWN
-  pthread_mutex_lock(&cache[4].refs_mutex);
+  pthread_mutex_unlock(&cache[4].refs_mutex);
 
   join_threads(t);
   return 0;
diff --git a/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i b/c/goblint-regression/28-race_reach_72-funloop_hard_racing.i
@@ -940,12 +940,14 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, ((void *)0));
   int i;
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   for(i=0; i<10; i++) cache_entry_addref(&cache[i]);
   pthread_mutex_lock(&cache[4].refs_mutex);
   do { if (__VERIFIER_nondet_int()) do { do { pthread_mutex_lock(&__global_lock); (cache[5].refs)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (cache[5].refs)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0); else do { pthread_mutex_lock(&__global_lock); __VERIFIER_assert((cache[5].refs) == 0); pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
-  pthread_mutex_lock(&cache[4].refs_mutex);
+  pthread_mutex_unlock(&cache[4].refs_mutex);
   for (int i=0; i < 10000; i++) pthread_join (t_ids[i], ((void *)0));
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_73-funloop_hard_racefree.c b/c/goblint-regression/28-race_reach_73-funloop_hard_racefree.c
@@ -20,14 +20,17 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
   int i;
   create_threads(t);
 
   for(i=0; i<10; i++) cache_entry_addref(&cache[i]);
 
   pthread_mutex_lock(&cache[5].refs_mutex);
   access_or_assert_racefree(cache[5].refs); // TODO
-  pthread_mutex_lock(&cache[5].refs_mutex);
+  pthread_mutex_unlock(&cache[5].refs_mutex);
 
   join_threads(t);
   return 0;
diff --git a/c/goblint-regression/28-race_reach_73-funloop_hard_racefree.i b/c/goblint-regression/28-race_reach_73-funloop_hard_racefree.i
@@ -940,12 +940,14 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, ((void *)0));
   int i;
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
   for(i=0; i<10; i++) cache_entry_addref(&cache[i]);
   pthread_mutex_lock(&cache[5].refs_mutex);
   do { if (__VERIFIER_nondet_int()) do { do { pthread_mutex_lock(&__global_lock); (cache[5].refs)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (cache[5].refs)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0); else do { pthread_mutex_lock(&__global_lock); __VERIFIER_assert((cache[5].refs) == 0); pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
-  pthread_mutex_lock(&cache[5].refs_mutex);
+  pthread_mutex_unlock(&cache[5].refs_mutex);
   for (int i=0; i < 10000; i++) pthread_join (t_ids[i], ((void *)0));
   return 0;
 }
diff --git a/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.c b/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.c
@@ -18,6 +18,9 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, NULL);
+
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   create_threads(t);
diff --git a/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i b/c/goblint-regression/28-race_reach_74-tricky_address1_racefree.i
@@ -939,6 +939,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, ((void *)0));
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
diff --git a/c/goblint-regression/28-race_reach_75-tricky_address2_racefree.c b/c/goblint-regression/28-race_reach_75-tricky_address2_racefree.c
@@ -18,6 +18,9 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, NULL);
+
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   create_threads(t);
diff --git a/c/goblint-regression/28-race_reach_75-tricky_address2_racefree.i b/c/goblint-regression/28-race_reach_75-tricky_address2_racefree.i
@@ -939,6 +939,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, ((void *)0));
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
diff --git a/c/goblint-regression/28-race_reach_76-tricky_address3_racefree.c b/c/goblint-regression/28-race_reach_76-tricky_address3_racefree.c
@@ -19,6 +19,9 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, NULL);
+
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   create_threads(t);
diff --git a/c/goblint-regression/28-race_reach_76-tricky_address3_racefree.i b/c/goblint-regression/28-race_reach_76-tricky_address3_racefree.i
@@ -940,6 +940,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, ((void *)0));
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
diff --git a/c/goblint-regression/28-race_reach_77-tricky_address4_racing.c b/c/goblint-regression/28-race_reach_77-tricky_address4_racing.c
@@ -19,6 +19,9 @@ void *t_fun(void *arg) {
 }
 
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, NULL);
+
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   create_threads(t);
diff --git a/c/goblint-regression/28-race_reach_77-tricky_address4_racing.i b/c/goblint-regression/28-race_reach_77-tricky_address4_racing.i
@@ -940,6 +940,8 @@ void *t_fun(void *arg) {
   return ((void *)0);
 }
 int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&a[i].mutex, ((void *)0));
   int i = __VERIFIER_nondet_int();
   assume_abort_if_not(0 <= i && i < 10);
   pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void *)0), t_fun, ((void *)0));
diff --git a/c/goblint-regression/28-race_reach_78-equ_racing.c b/c/goblint-regression/28-race_reach_78-equ_racing.c
@@ -12,11 +12,14 @@ struct s {
 void *t_fun(void *arg) {
   pthread_mutex_lock(&A.mutex);
   access_or_assert_racefree(B.datum); // UNKNOWN
-  pthread_mutex_lock(&A.mutex);
+  pthread_mutex_unlock(&A.mutex);
   return NULL;
 }
 
 int main () {
+  pthread_mutex_init(&A.mutex, NULL);
+  pthread_mutex_init(&B.mutex, NULL);
+
   int x = __VERIFIER_nondet_int();
 
   // struct s *s = malloc(sizeof(struct s));
diff --git a/c/goblint-regression/28-race_reach_78-equ_racing.i b/c/goblint-regression/28-race_reach_78-equ_racing.i
@@ -1004,10 +1004,12 @@ struct s {
 void *t_fun(void *arg) {
   pthread_mutex_lock(&A.mutex);
   do { if (__VERIFIER_nondet_int()) do { do { pthread_mutex_lock(&__global_lock); (B.datum)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (B.datum)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0); else do { pthread_mutex_lock(&__global_lock); __VERIFIER_assert((B.datum) == 0); pthread_mutex_unlock(&__global_lock); } while (0); } while (0);
-  pthread_mutex_lock(&A.mutex);
+  pthread_mutex_unlock(&A.mutex);
   return ((void *)0);
 }
 int main () {
+  pthread_mutex_init(&A.mutex, ((void *)0));
+  pthread_mutex_init(&B.mutex, ((void *)0));
   int x = __VERIFIER_nondet_int();
   struct s *s;
   int *d;
diff --git a/c/goblint-regression/28-race_reach_79-equ_racefree.c b/c/goblint-regression/28-race_reach_79-equ_racefree.c
@@ -12,11 +12,14 @@ struct s {
 void *t_fun(void *arg) {
   pthread_mutex_lock(&A.mutex);
   access_or_assert_racefree(A.datum); // TODO
-  pthread_mutex_lock(&A.mutex);
+  pthread_mutex_unlock(&A.mutex);
   return NULL;
 }
 
 int main () {
+  pthread_mutex_init(&A.mutex, NULL);
+  pthread_mutex_init(&B.mutex, NULL);
+
   int x = __VERIFIER_nondet_int();
 
   // struct s *s = malloc(sizeof(struct s));
diff --git a/c/goblint-regression/28-race_reach_79-equ_racefree.i b/c/goblint-regression/28-race_reach_79-equ_racefree.i

Original file line number	Diff line number	Diff line change
`@@ -10,7 +10,7 @@ pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;`
`10`	`10`	`void t_fun(void arg) {`
`11`	`11`	`pthread_mutex_lock(&mutex);`
`12`	`12`	`access(*g1);`
`13`		`- pthread_mutex_lock(&mutex);`
	`13`	`+ pthread_mutex_unlock(&mutex);`
`14`	`14`	`return NULL;`
`15`	`15`	`}`
`16`	`16`
Original file line number	Diff line number	Diff line change
`@@ -694,7 +694,7 @@ pthread_mutex_t mutex = { { 0, 0, 0, 0, 0, { { 0, 0 } } } };`
`694`	`694`	`void t_fun(void arg) {`
`695`	`695`	`pthread_mutex_lock(&mutex);`
`696`	`696`	`do { do { pthread_mutex_lock(&__global_lock); (g1)++; pthread_mutex_unlock(&__global_lock); } while (0); do { pthread_mutex_lock(&__global_lock); (g1)--; pthread_mutex_unlock(&__global_lock); } while (0); } while (0);`
`697`		`- pthread_mutex_lock(&mutex);`
	`697`	`+ pthread_mutex_unlock(&mutex);`
`698`	`698`	`return ((void *)0);`
`699`	`699`	`}`
`700`	`700`	`int main(void) {`
Original file line number	Diff line number	Diff line change
`@@ -21,6 +21,9 @@ void t_fun(void arg) {`
`21`	`21`	`}`
`22`	`22`
`23`	`23`	`int main () {`
	`24`	`+ for (int i = 0; i < 10; i++)`
	`25`	`+ pthread_mutex_init(&cache[i].refs_mutex, NULL);`
	`26`	`+`
`24`	`27`	`int i;`
`25`	`28`	`create_threads(t);`
`26`	`29`
Original file line number	Diff line number	Diff line change
`@@ -941,6 +941,8 @@ void t_fun(void arg) {`
`941`	`941`	`return ((void *)0);`
`942`	`942`	`}`
`943`	`943`	`int main () {`
	`944`	`+ for (int i = 0; i < 10; i++)`
	`945`	`+ pthread_mutex_init(&cache[i].refs_mutex, ((void *)0));`
`944`	`946`	`int i;`
`945`	`947`	`pthread_t t_ids[10000]; for (int i=0; i<10000; i++) pthread_create(&t_ids[i], ((void )0), t_fun, ((void )0));`
`946`	`948`	`for(i=0; i<10; i++)`