More involved MHP check

Author: michael-schwarz

src/analyses/pthreadBarriers.ml

@@ -53,7 +53,26 @@ struct
             let count = Waiters.cardinal relevant_waiters in
             match capacity with
             | `Lifted c -> 
-              Z.geq (Z.of_int count) (BatOption.default Z.zero (Capacity.I.minimal c)) 
+              (* Add 1 as the thread calling wait at the moment will not be MHP with itself *)
+              let min_cap = (BatOption.default Z.zero (Capacity.I.minimal c)) in
+              if Z.leq min_cap Z.one then
+                true
+              else if min_cap = Z.of_int 2 && count = 1 then
+                true
+              else if Z.geq (Z.of_int (count + 1)) min_cap then
+                (* This is quite a cute problem: Do (min_cap-1) elements exist in the set such that 
+                  MHP is pairwise true? This solution is a sledgehammer, there should be something much
+                  better algorithmically (beyond just laziness) *)
+                let waiters = Waiters.elements relevant_waiters in
+                let min_cap = Z.to_int min_cap in
+                let lists = List.init (min_cap - 1) (fun _ -> waiters) in
+                let candidates = BatList.n_cartesian_product lists in
+                List.exists (fun candidate ->
+                  let pairwise = BatList.cartesian_product candidate candidate in
+                  List.for_all (fun (a,b) -> MHP.may_happen_in_parallel a b) pairwise
+                ) candidates
+              else
+                false
             | _ -> true
         in
         if may_run then

tests/regression/82-barrier/02-more.c

@@ -38,10 +38,6 @@ int main(int argc, char const *argv[])
         i = 1;
     }
 
-    // Created too late to have any effect
-    pthread_t t2;
-    pthread_create(&t2,NULL,f1,NULL);
-
     __goblint_check(i == 0);
 
 

tests/regression/82-barrier/03-problem.c

@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 2);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Live!
+        i = 1;
+    }
+
+    __goblint_check(i == 0); //UNKNOWN!
+
+
+    return 0;
+}

tests/regression/82-barrier/04-challenge.c

@@ -0,0 +1,49 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+void* f2(void* ptr) {
+    pthread_barrier_wait(&barrier);
+    return NULL;
+}
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This is past the barrier, so it will not be reached
+    pthread_t t2;
+    pthread_create(&t2,NULL,f2,NULL);
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    }
+
+    // Created too late to have any effect
+    pthread_t t2;
+    pthread_create(&t2,NULL,f1,NULL);
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}

tests/regression/82-barrier/05-mhp-not-enough.c

@@ -0,0 +1,45 @@
+// PARAM: --set ana.activated[+] 'pthreadBarriers'
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+
+int g;
+
+pthread_barrier_t barrier;
+
+
+void* f1(void* ptr) {
+    pthread_barrier_wait(&barrier);
+
+    // This should not be reached as either main calls wait or the other thread is created
+    // -> In the concrete, there never are three threads calling wait
+
+    return NULL;
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    int top2;
+    int i = 0;
+    
+    pthread_barrier_init(&barrier, NULL, 3);
+
+    pthread_t t1;
+    pthread_create(&t1,NULL,f1,NULL);
+    
+    if(top) {
+        pthread_barrier_wait(&barrier);
+        // Unreachable
+        i = 1;
+    } else {
+        pthread_t t2;
+        pthread_create(&t2,NULL,f1,NULL);    
+    }
+
+
+    __goblint_check(i == 0);
+
+
+    return 0;
+}