Handle non-racy MCPA for non-unique threads

Author: michael-schwarz

src/analyses/pthreadBarriers.ml

@@ -108,17 +108,27 @@ struct
                     in
                     let can_proceed = exists_k can_proceed_pred (min_cap - 1) relevant_waiters in
                     if not can_proceed then raise Analyses.Deadcode;
-                    (* All TIDs are definite here, they may have other MCPA stuff but that is irrelevant. *)
-                    let tids = waiters |> List.map snd |> List.sort_uniq TID.compare in
-                    (* limit to this case to avoid having to construct all permutations above *)
-                    if BatList.compare_length_with tids (min_cap - 1) = 0 then
-                      List.fold_left (fun acc tid ->
-                          let curr = MustObserved.find tid acc in
-                          let must' = MustObserved.add tid (Barriers.add addr curr) acc in
-                          must'
-                        ) must tids
-                    else
+                    let exists_non_unique = List.exists (function
+                        | _, `Lifted tid -> not @@ ThreadIdDomain.Thread.is_unique tid
+                        | _ -> true
+                      ) waiters
+                    in
+                    if exists_non_unique then
+                      (* There can be non-unique threads that don't race with themselves because of mutexes etc *)
+                      (* We do nothing for those cases *)
                       must
+                    else
+                      (* All TIDs are definite here, they may have other MCPA stuff but that is irrelevant. *)
+                      let tids = waiters |> List.map snd |> List.sort_uniq TID.compare in
+                      (* limit to this case to avoid having to construct all permutations above *)
+                      if BatList.compare_length_with tids (min_cap - 1) = 0 then
+                        List.fold_left (fun acc tid ->
+                            let curr = MustObserved.find tid acc in
+                            let must' = MustObserved.add tid (Barriers.add addr curr) acc in
+                            must'
+                          ) must tids
+                      else
+                        must
                   in
                   (may, must)
                 else