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

We take inspiration from the efficient computation of register
read-from (see PR #1704): atomic effects are ordered according
to (extended by iico) program order and an atomic load is paired
with the closest atomic effect that follows it, if this effect
is a write.

Author: maranget

herd/mem.ml

@@ -864,28 +864,45 @@ and get_written e = match E.written_of e with
 (* Compute rfmap for registers *)
 (*******************************)
 
-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
+
+(* Event set ordered by to (generalised) program order *)
+
+module
+  EvtSetByPo
+    (I:sig val es : S.event_structure end) =
+struct
+
+  let is_before_strict = U.is_before_strict I.es
+
+  include Set.Make
+      (struct
+
+        type t = E.event
+
+        let compare e1 e2 =
+          if is_before_strict e1 e2 then -1
+          else if is_before_strict e2 e1 then 1
+          else
+            let () =
+              Printf.eprintf "Not ordered stores %a and %a\n" E.debug_event e1
+                E.debug_event e2
+            in
+            assert false
+
+      end)
+
+  let find_last_before set e =
+    find_last_opt (fun e' -> is_before_strict e' e) set
+
+  let find_first_after e set =
+    find_first_opt (fun e' -> is_before_strict e e') set
+
+end
 
 let match_reg_events add_eq es csn =
   let loc_loads_stores = U.collect_reg_loads_stores es in
-  let is_before_strict = U.is_before_strict es in
-  let compare e1 e2 =
-    if is_before_strict e1 e2 then -1
-    else if is_before_strict e2 e1 then 1
-    else
-      let () =
-        Printf.eprintf "Not ordered stores %a and %a\n" E.debug_event e1
-          E.debug_event e2
-      in
-      assert false
-  in
-  let module StoreSet = Set.Make (struct
-    type t = E.event
-
-    let compare = compare
-  end) in
+  let module StoreSet = EvtSetByPo(struct let es = es end) in
   let add wt rf (rfm, csn) = (S.RFMap.add wt rf rfm, add_eq rfm wt rf csn) in
   (* For all loads find the right store, the one "just before" the load *)
   U.LocEnv.fold
@@ -901,9 +918,7 @@ let match_reg_events add_eq es csn =
       (* Add the corresponding store for each load *)
       List.fold_left
         (fun k load ->
-          let f e = is_before_strict e load in
-          let rf =
-            match StoreSet.find_last_opt f stores with
+          let rf = match StoreSet.find_last_before stores load with
             | Some store -> S.Store store
             | None -> S.Init
           in
@@ -1804,37 +1819,51 @@ let get_rf_value test read =
 (* Reconstruct load/store atomic pairs *)
 
     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 =
@@ -1929,12 +1958,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,25 @@ 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