Merge pull request #430 from herd/optace-explicit

[herd] Limits sc-per-location inner check to explicit accesses
That way, using optimisation `-optace true` should not changes output for models that include the `sc per-location` on explicit accesses and not on some non-explicit accesses.

herd/libdir/cos-no-opt.cat

@@ -0,0 +1,18 @@
+"Generate co's"
+
+include "cross.cat"
+
+let invrf = rf^-1
+let cobase = co0
+with co from generate_cos(cobase)
+
+(* From now, co is a coherence order *)
+let coi = co & int
+let coe = co \ coi
+
+(* Compute fr *)
+let fr = (invrf ; co) \ id
+let fri = fr & int
+let fre = fr \ fri
+
+show co,fr

herd/libdir/cos-opt.cat

@@ -3,21 +3,28 @@
 (* generates possible co's, optimized version *)
 
 (* co observations in test *)
+
 let invrf = rf^-1
 
+(* Relation pco is computed by herd7 code
+
 let obsco =
+  let po-loc = [Exp];po-loc;[Exp] in
   let ww = po-loc & (W * W)
   and rw = rf ; (po-loc & (R * W))
   and wr = ((po-loc & (W * R)) ; invrf) \ id
   and rr = (rf ; (po-loc & (R * R)) ; invrf) \ id in
   (ww|rw|wr|rr)
 
+let pco = obsco|co0
+*)
+
 (* The following applies to C only, where RMW is both R and W *)
 let rmwco =
   let _RMW = R & W in
   rf & (W * _RMW) (* co observation by atomicity *)
 
-let cobase = obsco|rmwco|co0
+let cobase = rmwco|pco
 
 (* Catch uniproc violations early *)
 acyclic cobase as ConsCo

herd/libdir/cos.cat

@@ -1,18 +1,7 @@
 "Generate co's"
 
-include "cross.cat"
-
-let invrf = rf^-1
-let cobase = co0
-with co from generate_cos(cobase)
-
-(* From now, co is a coherence order *)
-let coi = co & int
-let coe = co \ coi
-
-(* Compute fr *)
-let fr = (invrf ; co) \ id
-let fri = fr & int
-let fre = fr \ fri
-
-show co,fr
+if "cos-opt"
+  include "cos-opt.cat"
+else
+  include "cos-no-opt.cat"
+end

herd/machModelChecker.ml

@@ -32,7 +32,11 @@ module Make
     let mixed = O.variant Variant.Mixed || morello
     let memtag = O.variant Variant.MemTag
     let kvm = O.variant Variant.Kvm
-
+    let optacetrue =
+      let open OptAce in
+      match O.optace with
+      | True -> true
+      | False|Iico -> false
     let bell_fname =  Misc.app_opt (fun (x,_) -> x) O.bell_model_info
     let bell_info = Misc.app_opt (fun (_,x) -> x) O.bell_model_info
 
@@ -60,7 +64,12 @@ module Make
       let doshow = S.O.PC.doshow
       let showraw = S.O.PC.showraw
       let symetric = S.O.PC.symetric
-      let variant = Misc.delay_parse O.variant Variant.parse
+      let variant =
+        let variant =
+          if optacetrue then
+            Misc.(|||) (Variant.equal Variant.CosOpt) O.variant
+          else O.variant in
+        Misc.delay_parse variant Variant.parse
     end
     module U = MemUtils.Make(S)
     module MU = ModelUtils.Make(O)(S)
@@ -303,7 +312,9 @@ module Make
                 E.EventRel.of_pred all_evts all_evts E.same_static_event
               end;
               "same-instance", lazy begin E.EventRel.of_pred all_evts all_evts E.same_instance end;
-              "equiv-spec", lazy begin Equiv.build (Lazy.force rf_reg) all_evts end;
+              "equiv-spec",
+                lazy begin Equiv.build (Lazy.force rf_reg) all_evts end;
+              "pco", lazy conc.S.pco;
             ]))) in
       let m =
         let spec = conc.S.str.E.speculated in

herd/mem.ml

@@ -112,7 +112,7 @@ module type S = sig
   val check_sizes : S.test -> S.event_structure -> unit
 
   val check_rfmap :
-    S.E.event_structure -> S.read_from S.RFMap.t -> bool
+      S.E.event_structure -> S.read_from S.RFMap.t -> bool
 
   val when_unsolved :
       S.test -> S.E.event_structure -> S.read_from S.RFMap.t -> S.M.VC.cnstrnt list -> 'a -> 'a
@@ -906,8 +906,12 @@ let match_reg_events es =
       let ok = match C.optace with
         | OptAce.False -> fun _ _ -> true
         | OptAce.True ->
-            let pred = U.is_before_strict es in
-            fun er ew -> not (pred er ew)
+           let pred = U.is_before_strict es
+           and iico = U.iico es in
+           fun er ew ->
+           not
+             (E.is_explicit er && E.is_explicit ew && pred er ew
+              || E.EventRel.mem (er,ew) iico)
         | OptAce.Iico ->
            let iico = U.iico es in
            fun load store -> not (E.EventRel.mem (load,store) iico) in
@@ -1563,9 +1567,11 @@ let match_reg_events es =
              (fun _loc ws k ->
                List.filter
                  (fun w ->
+                   not (E.is_explicit w) ||
                    not
                      (List.exists
-                        (fun w' -> U.is_before_strict es w w') ws))
+                        (fun w' ->
+                          E.is_explicit w' && U.is_before_strict es w w') ws))
                  ws::k)
              loc_stores []
         | OptAce.False|OptAce.Iico ->
@@ -1719,11 +1725,14 @@ let match_reg_events es =
           | OptAce.True ->
             (*jade: looks compatible with speculation, but there might be some
               unforeseen subtlety here so flagging it to be sure*)
-            match U.compute_pco rfm ppoloc with
-            | None -> raise Exit
-            | Some pco -> E.EventRel.union pco0 pco in
+             let ppoloc =
+               E.EventRel.restrict_rel
+                 (fun e1 e2 -> E.is_explicit e1 && E.is_explicit e2)
+                 ppoloc in
+               match U.compute_pco rfm ppoloc with
+               | None -> raise Exit
+               | Some pco -> E.EventRel.union pco0 pco in
 (* Cross product *)
-
         Misc.fold_cross
           possible_finals
           (fun ws res ->
@@ -1800,29 +1809,32 @@ let match_reg_events es =
    Limited to memory, since  generated rfmaps are correct for registers *)
 (* NOTE: this is more like an optimization,
    models should rule out those anyway *)
+
     let check_rfmap es rfm =
       let po_iico = U.is_before_strict es in
-
       S.for_all_in_rfmap
         (fun wt rf -> match wt with
-        | S.Load er when E.is_mem_load er ->
+        | S.Load er when E.is_mem_load er && E.is_explicit er ->
             begin match rf with
             | S.Store ew ->
-                assert (not (po_iico er ew)) ;
+                not (E.is_explicit ew) ||
+                begin
+                  assert (not (po_iico er ew)) ;
                 (* ok by construction, in theory *)
-                not
-                  (E.EventSet.exists
-                     (fun e ->
-                       E.is_store e &&  E.same_location e ew &&
-                       po_iico ew e &&
-                       po_iico e er)
-                     es.E.events)
+                  not
+                    (E.EventSet.exists
+                       (fun e ->
+                         E.is_store e && E.same_location e ew &&
+                         E.is_explicit e && po_iico ew e &&
+                         po_iico e er)
+                       es.E.events)
+                end
             | S.Init ->
                 not
                   (E.EventSet.exists
                      (fun e ->
                        E.is_store e && E.same_location e er &&
-                       po_iico e er)
+                       E.is_explicit e && po_iico e er)
                      es.E.events)
             end
         | _ -> true)

herd/variant.ml

@@ -60,6 +60,8 @@ type t =
   | Exp
 (* Instruction-fetch support (AKA "self-modifying code" mode) *)
   | Self
+(* Have cat interpreter to optimise generation of co's *)
+  | CosOpt
 (* Test something *)
   | Test
 (* One hundred tests *)
@@ -73,7 +75,7 @@ let tags =
     Precision.tags @
    ["toofar"; "deps"; "morello"; "instances"; "noptebranch"; "pte2";
    "pte-squared"; "PhantomOnLoad"; "OptRfRMW"; "ConstrainedUnpredictable";
-   "exp"; "self"; "test"; "T[0-9][0-9]"]
+   "exp"; "self"; "cos-opt"; "test"; "T[0-9][0-9]"]
 
 let parse s = match Misc.lowercase s with
 | "success" -> Some Success
@@ -106,6 +108,7 @@ let parse s = match Misc.lowercase s with
 | "constrainedunpredictable"|"cu" -> Some ConstrainedUnpredictable
 | "exp" -> Some Exp
 | "self" -> Some Self
+| "cos-opt" -> Some CosOpt
 | "test" -> Some Test
 | s ->
    begin
@@ -155,10 +158,12 @@ let pp = function
   | ConstrainedUnpredictable -> "ConstrainedUnpredictable"
   | Exp -> "exp"
   | Self -> "self"
+  | CosOpt -> "cos-opt"
   | Test -> "test"
   | T n -> Printf.sprintf "T%02i" n
 
 let compare = compare
+let equal v1 v2 = compare v1 v2 = 0
 
 let get_default a v =
   try match v with

herd/variant.mli

@@ -58,12 +58,15 @@ type t =
   | Exp
 (* Instruction-fetch support (AKA "self-modifying code" mode) *)
   | Self
+(* Have cat interpreter to optimise generation of co's *)
+  | CosOpt
 (* Test something *)
   | Test
 (* One hundred tests *)
   | T of int
 
 val compare : t -> t -> int
+val equal : t -> t -> bool
 val tags : string list
 val parse : string -> t option
 val pp : t -> string