[herd,asl] Optimise computation of relation "loc" in the ASL case

herd/machModelChecker.ml

@@ -180,6 +180,65 @@ module Make
     module Equiv = EquivSpec.Make(S)
     module E = S.E
 
+    (* Fast "loc" relation computation *)
+
+    module NameEnv = StringMap
+
+    let loc_as_fault_base loc =
+      let (>>=) = Option.bind in
+      S.A.global loc >>= S.A.V.as_constant
+      >>=  Constant.as_fault_base
+
+    let comp_loc evts =
+      let mlocs,mfaults =
+        E.EventSet.fold
+          (fun e (mlocs,mfaults as k)  ->
+             match E.location_of e with
+             | None -> k
+             | Some loc ->
+                 if E.is_fault e then
+                   match loc_as_fault_base loc with
+                   | None -> k
+                   | Some name ->
+                       mlocs,NameEnv.accumulate name e mfaults
+                  else
+                   U.LocEnv.accumulate loc e mlocs,mfaults)
+          evts (U.LocEnv.empty,NameEnv.empty) in
+      let rel_locs =
+        U.LocEnv.fold
+          (fun _ es k ->
+             let es = E.EventSet.of_list es in
+             E.EventRel.cartesian es es::k)
+          mlocs [] |> E.EventRel.unions
+      and rel_faults =
+        if NameEnv.is_empty mfaults then E.EventRel.empty
+        else
+          let mnames =
+            U.LocEnv.fold
+              (fun loc es mnames ->
+                 match loc_as_fault_base loc with
+                 | None -> mnames
+                 | Some name ->
+                     begin
+                       match
+                         NameEnv.safe_find [] name mfaults with
+                       | [] -> mnames
+                       | _ ->
+                           let old = NameEnv.safe_find [] name mnames in
+                           NameEnv.add name (es@old) mnames
+                     end)
+              mlocs NameEnv.empty in
+          NameEnv.fold
+            (fun name es k ->
+               let fs = E.EventSet.of_list es in
+               let es =
+                 NameEnv.safe_find [] name mnames
+                 |> E.EventSet.of_list in
+               E.EventRel.cartesian es fs::
+               E.EventRel.cartesian fs fs::k)
+            mfaults [] |> E.EventRel.unions in
+      E.EventRel.union rel_locs rel_faults
+
 (* Local utility: bell event selection *)
     let add_bell_events m pred evts annots =
       I.add_sets m
@@ -260,7 +319,7 @@ module Make
                (fun e -> e,e)
                (E.EventSet.elements evts))
         end in
-      let unv = lazy begin E.EventRel.cartesian evts evts  end in
+      let unv = lazy (E.EventRel.cartesian evts evts) in
       let ks = { I.id; unv; evts; conc; po;} in
       let calc_si sca =
         let r =
@@ -287,6 +346,7 @@ module Make
           E.EventRel.unions rs
         end in
       let rf_reg = lazy (U.make_rf_regs conc) in
+
 (* Initial env *)
       let m =
         I.add_rels
@@ -304,11 +364,7 @@ module Make
                ("data", lazy (Lazy.force pr).S.data)::
                ("ctrl", lazy (Lazy.force pr).S.ctrl)::k)
              ["id",id;
-              "loc", lazy begin
-                E.EventRel.restrict_rel
-                  E.same_location_with_faults
-                  (Lazy.force unv)
-              end;
+              "loc", lazy (comp_loc evts);
               "same-low-order-bits", lazy begin
                 E.EventRel.restrict_rel
                   E.same_low_order_bits
@@ -600,5 +656,8 @@ module Make
         U.apply_process_co test  conc process_co res
       else
 (*        let m = I.add_rels m ["co0",lazy  conc.S.pco] in *)
+        let kont x y z t u =
+          if O.debug then prerr_endline "Cat over" ;
+          kont x y z t u in
         run_interpret test kfail ks m vb_pp kont res
   end

lib/constant.ml

@@ -452,6 +452,11 @@ let as_symbol = function
   | Symbolic sym -> Some sym
   | _ -> None
 
+let as_fault_base = function
+  | Symbolic (Virtual {name;_}) -> Some name
+  | Symbolic (System (PTE,name)) -> Some (Misc.add_pte name)
+  | _ -> None
+
 let as_symbolic_data =function
 | Symbolic (Virtual sym) -> Some sym
 | _ -> None

lib/constant.mli

@@ -145,6 +145,7 @@ val check_sym : ('a,'pte,'instr) t -> ('b,'pte,'instr) t
 val is_virtual : ('scalar,'pte,'instr) t -> bool
 val as_virtual : ('scalar,'pte,'instr) t -> string option
 val as_symbol : ('scalar,'pte,'instr) t -> symbol option
+val as_fault_base :  ('scalar,'pte,'instr) t -> string option
 val as_symbolic_data : ('scalar,'pte,'instr) t -> symbolic_data option
 val of_symbolic_data : symbolic_data -> ('scalar,'pte,'instr) t
 

lib/myMap.ml

@@ -44,6 +44,9 @@ module type S = sig
   val from_bindings :  (key * 'a) list -> 'a t
 
   val fold_values : ('a -> 'acc -> 'acc) -> 'a t -> 'acc -> 'acc
+
+(* Bind keys to list of values *)
+  val accumulate : key -> 'a -> 'a list t -> 'a list t
 end
 
 module Make(O:Set.OrderedType) : S with type key = O.t =
@@ -93,4 +96,9 @@ module Make(O:Set.OrderedType) : S with type key = O.t =
     let fold_values fold_value =
       let fold_binding _key v acc = fold_value v acc in
       fun t acc -> fold fold_binding t acc
+
+    let accumulate k v m =
+      let vs = safe_find [] k m in
+      add k (v::vs) m
+
   end