[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 stores by a given thread and
to a given location are ordered according to (extended by iico)
program order and an atomic load is paired
with the closest atomic store that follows it.
Additionaly it is checked that there is no atomic load
in-between. That is, the next effect in (generalised) po
indeed 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
@@ -1801,40 +1816,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 exist 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 =
@@ -1929,12 +1978,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