Group racing accesses into disjoint components

src/domains/access.ml

@@ -391,27 +391,59 @@ let may_race (conf,w,loc,e,a) (conf2,w2,loc2,e2,a2) =
   else
     true
 
-let filter_may_race accs =
-  let accs = AS.elements accs in
-  let cart = List.cartesian_product accs accs in
-  List.fold_left (fun acc (x, y) ->
-      if A.compare x y <= 0 && may_race x y then
-        AS.add y (AS.add x acc)
-      else
-        acc
-    ) (AS.empty ()) cart
+let group_may_race accs =
+  (* DFS to traverse one component with may_race edges *)
+  let rec dfs accs visited acc =
+    if AS.mem acc visited then
+      (accs, visited)
+    else (
+      let accs' = AS.remove acc accs in
+      let visited' = AS.add acc visited in
+      AS.fold (fun acc' (accs', visited') ->
+          if may_race acc acc' then
+            dfs accs' visited' acc'
+          else
+            (accs', visited')
+        ) accs' (accs', visited')
+    )
+  in
+  (* repeat DFS to find all components *)
+  let rec components comps accs =
+    if AS.is_empty accs then
+      comps
+    else (
+      let acc = AS.choose accs in
+      let (accs', comp) = dfs accs (AS.empty ()) acc in
+      let comps' = comp :: comps in
+      components comps' accs'
+    )
+  in
+  components [] accs
+
+let race_conf accs =
+  assert (not (AS.is_empty accs)); (* group_may_race should only construct non-empty components *)
+  if AS.cardinal accs = 1 then ( (* singleton component *)
+    let acc = AS.choose accs in
+    if may_race acc acc then (* self-race *)
+      Some (A.conf acc)
+    else
+      None
+  )
+  else
+    Some (AS.max_conf accs)
 
 let is_all_safe = ref true
 
 (* Commenting your code is for the WEAK! *)
 let incr_summary safe vulnerable unsafe (lv, ty) accs =
   (* ignore(printf "Checking safety of %a:\n" d_memo (ty,lv)); *)
-  let race_accs = filter_may_race accs in
   let safety =
-    if AS.is_empty race_accs then
-      None
-    else
-      Some (AS.max_conf race_accs)
+    group_may_race accs
+    |> List.filter_map race_conf
+    |> (function
+        | [] -> None
+        | confs -> Some (List.max confs)
+      )
   in
   match safety with
   | None -> incr safe
@@ -436,10 +468,16 @@ let print_accesses (lv, ty) accs =
     AS.elements race_accs
     |> List.map h
   in
-  match filter_may_race accs with
-  | race_accs when AS.is_empty race_accs ->
-    if allglobs then
-      M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs accs)
-  | race_accs ->
-    let conf = AS.max_conf race_accs in
-    M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) conf (msgs (if allglobs then accs else race_accs))
+  group_may_race accs
+  |> List.fold_left (fun safe_accs accs ->
+      match race_conf accs with
+      | None ->
+        AS.union safe_accs accs (* group all safe accs together for allglobs *)
+      | Some conf ->
+        M.msg_group Warning ~category:Race "Memory location %a (race with conf. %d)" d_memo (ty,lv) conf (msgs accs);
+        safe_accs
+    ) (AS.empty ())
+  |> (fun safe_accs ->
+      if allglobs && not (AS.is_empty safe_accs) then
+        M.msg_group Success ~category:Race "Memory location %a (safe)" d_memo (ty,lv) (msgs safe_accs)
+    )

tests/regression/10-synch/05-two_unique_two_lock.c

@@ -0,0 +1,34 @@
+// PARAM: --set ana.activated[+] thread
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t B = PTHREAD_MUTEX_INITIALIZER;
+
+void *f1(void *arg) {
+  pthread_mutex_lock(&A);
+  myglobal=1; // RACE! (with just 4)
+  pthread_mutex_unlock(&A);
+  pthread_mutex_lock(&B);
+  myglobal=2; // RACE! (with just 3)
+  pthread_mutex_unlock(&B);
+  return NULL;
+}
+
+void *f2(void *arg) {
+  pthread_mutex_lock(&A);
+  myglobal=3; // RACE! (with just 2)
+  pthread_mutex_unlock(&A);
+  pthread_mutex_lock(&B);
+  myglobal=4; // RACE! (with just 1)
+  pthread_mutex_unlock(&B);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t t1, t2;
+  pthread_create(&t1, NULL, f1, NULL);
+  pthread_create(&t2, NULL, f2, NULL);
+  return 0;
+}

tests/regression/10-synch/06-thread_nonunique_plain.c

@@ -0,0 +1,20 @@
+// PARAM: --set ana.activated[+] thread --set ana.thread.domain plain
+#include <pthread.h>
+#include <stdio.h>
+
+int myglobal;
+
+void *t_fun(void *arg) {
+  myglobal=42; // RACE!
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id[10];
+  int i;
+  for (i=0; i<10; i++)
+    pthread_create(&id[i], NULL, t_fun, NULL);
+  for (i=0; i<10; i++)
+    pthread_join (id[i], NULL);
+  return 0;
+}