[herd] More efficient computation of atomic load X stores pairs

herd/mem.ml

@@ -901,12 +901,10 @@ struct
 
   let find_first_after e set =
     find_first_opt (fun e' -> is_before_strict e e') set
-  [@@warning "-32"]
+
 end
 
-let map_loc_find loc m =
-  try U.LocEnv.find loc m
-  with Not_found -> []
+let map_loc_find loc m = U.LocEnv.safe_find [] loc m
 
 let match_reg_events add_eq es csn =
   let loc_loads_stores = U.collect_reg_loads_stores es in
@@ -1827,40 +1825,74 @@ let get_rf_value test read =
         | _,_ -> k)
         rfm E.EventRel.empty
 
-(* Reconstruct load/store atomic pairs *)
+(*
+ * Reconstruct load/store atomic pairs,
+ *   By definition such a pair exists when the
+ * store precedes the load in generalised program order
+ * (_i.e._ the union of program order and of iico), and
+ * that there is no atomic effect to the same location
+ * in-between (w.r.t generalised po) the load and the store.
+ *   Computation proceeds as follows:
+ *   First, atomic events are grouped first by thread
+ * and then by location. Then, to each atomic load, we
+ * associate the closest generalised po successor store,
+ * by using a set of stores ordered by generalised po.
+ * We additionally check that no atomic load exists
+ * between the load and store. Notice that it is not possible
+ * to use a set of all atomic events (by a given thread and
+ * with a given location) ordered by po because some atomic loads
+ * may be unrelated.
+ *   Finally, such atomic pairs can be spurious, that is not performed
+ * by a specific thread. In that case, pairs are given
+ * simply by the intra causality data relation.
+ *)
 
     let make_atomic_load_store es =
-      let all = E.atomics_of es.E.events in
-      let atms = U.collect_atomics es in
-      U.LocEnv.fold
-        (fun _loc atms k ->
-          let atms =
-            List.filter
-              (fun e -> not (E.is_load e && E.is_store e))
-              atms in (* get rid of C RMW *)
-          let rs,ws = List.partition E.is_load atms in
-          List.fold_left
-            (fun k r ->
-              let exp = E.is_explicit r in
-              List.fold_left
-                (fun k w ->
-                  if
-                    S.atomic_pair_allowed r w &&
-                    U.is_before_strict es r w &&
-                    E.is_explicit w = exp &&
-                    not
-                      (E.EventSet.exists
-                         (fun e ->
-                           E.is_explicit e = exp &&
-                           U.is_before_strict es r e &&
-                           U.is_before_strict es e w)
-                         all)
-                  then E.EventRel.add (r,w) k
-                  else k)
-                k ws)
-            k rs)
-        atms E.EventRel.empty
-
+      let atms,spurious = U.collect_atomics es in
+      let module StoreSet = EvtSetByPo(struct let es = es end) in
+      let make_atomic_pairs es k =
+        let rs,ws = List.partition E.is_load es in
+        let ws = StoreSet.of_list ws
+        and intervening_read er ew =
+          List.exists
+            (fun e ->
+              StoreSet.is_before_strict er e
+              && StoreSet.is_before_strict e ew)
+            rs in
+        List.fold_left
+          (fun k er ->
+             match StoreSet.find_first_after er ws with
+             | Some ew ->
+                if
+                  S.atomic_pair_allowed er ew
+                  && not (intervening_read er ew)
+                 then
+                   E.EventRel.add (er,ew) k
+                 else k
+             | None -> k)
+          k rs in
+      let r1 =
+        List.map
+          (fun (_,m) ->
+           U.LocEnv.fold
+             (fun _loc es k ->
+                let exps,nexps = List.partition E.is_explicit es in
+                make_atomic_pairs exps @@ make_atomic_pairs nexps k)
+             m E.EventRel.empty)
+        atms |> E.EventRel.unions
+      and r2 =
+        let iico = es.E.intra_causality_data in
+        List.map
+          (fun e ->
+             if E.is_load e then
+               match
+                 E.EventRel.succs iico e |> E.EventSet.as_singleton
+               with
+               | None -> assert false (* spurious updates are by pairs *)
+               | Some w -> E.EventRel.singleton (e,w)
+             else E.EventRel.empty)
+          spurious |> E.EventRel.unions in
+      E.EventRel.union r1 r2
 
 (* Retrieve last store from rfmap *)
     let get_max_store _test _es rfm loc =
@@ -1955,12 +1987,9 @@ let get_rf_value test read =
           if C.debug.Debug_herd.mem then begin
             eprintf "Observed locs: {%s}\n" (pp_locations observed_locs)
           end ;
-          U.LocEnv.fold
-            (fun loc ws k ->
-              if keep_observed_loc loc observed_locs then
-                U.LocEnv.add loc ws k
-              else k)
-            loc_stores U.LocEnv.empty
+          U.LocEnv.filter
+            (fun loc _ ->  keep_observed_loc loc observed_locs)
+            loc_stores
         else loc_stores in
 
       let possible_finals =

herd/memUtils.ml

@@ -387,9 +387,26 @@ let lift_proc_info i evts =
   and collect_stores es = collect_by_loc es E.is_store
   and collect_loads_non_spec es = collect_by_loc es (fun e -> E.is_load e && not_speculated es e)
   and collect_stores_non_spec es = collect_by_loc es (fun e -> E.is_store e && not_speculated es e)
-  and collect_atomics es = collect_by_loc es E.is_atomic
   and collect_reg_loads_stores es = collect_by_loc2 es E.is_reg_load_any E.is_reg_store_any
 
+  let accumulate_loc_proc proc loc e =
+    IntMap.update proc @@
+      function
+      | None -> Some (LocEnv.singleton loc [e])
+      | Some m -> Some (LocEnv.accumulate loc e m)
+
+  let collect_atomics es =
+    let m,sp =
+      E.EventSet.fold
+        (fun e (m,sp as k) ->
+           if E.is_atomic e then
+             match E.proc_of e with
+             | None -> if E.is_spurious e then (m, e::sp) else k
+             | Some proc -> accumulate_loc_proc proc (get_loc e) e m, sp
+           else k)
+        es.E.events (IntMap.empty,[]) in
+    IntMap.bindings m,sp
+
   let partition_events es =
     let env =
       E.EventSet.fold

herd/memUtils.mli

@@ -70,7 +70,7 @@ module Make : functor (S: SemExtra.S) -> sig
    relation *)
   val make_fr : S.concrete -> S.event_rel -> S.event_rel
 
-(* Mapping from locations *)
+(* Mapping from locations, a.k.a. location maps *)
   module LocEnv : MyMap.S with type key = S.location
 
 (* Collect various events, indexed by location *)
@@ -85,7 +85,19 @@ module Make : functor (S: SemExtra.S) -> sig
   val collect_stores : S.event_structure -> S.event list LocEnv.t
   val collect_stores_non_spec : S.event_structure -> S.event list LocEnv.t
   val collect_loads_non_spec : S.event_structure -> S.event list LocEnv.t
-  val collect_atomics : S.event_structure -> S.event list LocEnv.t
+
+  (*
+   * Collect atomic effects indexed by threads and by locations.
+   * When given an event structure as argument, the function
+   * returns a pair [(maps,evts)], where:
+   *  + [maps] is a list of location maps, one per thread.
+   *    The values of this map are the atomic effects
+        of the given thread.
+   *  + [evts] is the list of spurious (atomic) effects.
+   *)
+
+  val collect_atomics :
+    S.event_structure -> (Proc.t * S.event list LocEnv.t) list * S.event list
 
 (* Partition by location *)
   val partition_events : S.event_set -> S.event_set list