[herd] Consequences of splitting exclusive effects from the X events set (PR #1889)

herd/AArch64Arch_herd.ml

@@ -32,7 +32,6 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
 
     let is_kvm = C.variant Variant.VMSA
 
-    let is_amo _ = false
     let pp_barrier_short = pp_barrier
     let reject_mixed = true
 
@@ -45,6 +44,7 @@ module Make (C:Arch_herd.Config)(V:Value.AArch64) =
     let nexp_ifetch = AArch64Explicit.NExp AArch64Explicit.IFetch
 
     let is_atomic = AArch64Annot.is_atomic
+    and is_exclusive = AArch64Annot.is_exclusive
 
     let is_ifetch_annot = function
       | NExp IFetch -> true

herd/ARMArch_herd.ml

@@ -25,7 +25,7 @@ end
 module Make (C:Arch_herd.Config) (V:Value.S) =
   struct
     include ARMBase
-    let is_amo _ = false
+
     let pp_barrier_short = pp_barrier
     let reject_mixed = false
 

herd/ASLAction.ml

@@ -177,6 +177,9 @@ module Make (C: Config) (A : S) = struct
   let is_atomic = function
     | Access _|Fault _|Branching _|Barrier _|CutOff _|NoAction
       -> false
+  let is_exclusive = function
+    | Access _|Fault _|Branching _|Barrier _|CutOff _|NoAction
+      -> false
   let is_fault = function
     | Fault _ -> true
     | Access _| Branching _|Barrier _|CutOff _|NoAction

herd/ASLExtra.ml

@@ -31,7 +31,6 @@ module Make (B : ArchBaseHerd) (C : Arch_herd.Config) (V : Value.S) = struct
   include NoSemEnv
   include NoLevelNorTLBI
 
-  let is_amo _ = false
   let pp_barrier_short = pp_barrier
   let reject_mixed = false
   let mem_access_size _ = None

herd/BPFArch_herd.ml

@@ -21,11 +21,6 @@ struct
 
   module CS = ConstraintSolver.No(V)
 
-  let is_amo = function
-    | AMO _ -> true
-    | _ -> false
-  ;;
-
   let pp_barrier_short = pp_barrier
   let reject_mixed = false
   let get_machsize _ = V.Cst.Scalar.machsize
@@ -39,6 +34,7 @@ struct
   let is_atomic = function
     | X | SC -> true
     | _ -> false
+  and is_exclusive _ = false
   ;;
 
   let is_acquire = function

herd/BellAction.ml

@@ -129,6 +129,7 @@ end = struct
   | Access (_,_,_,true,_,_) ->
       assert (is_mem a); true
   | _ -> false
+  and is_exclusive _ = false
 
   let is_fault _ = false
 

herd/BellArch_herd.ml

@@ -20,9 +20,6 @@ module Make
          (C:Arch_herd.Config)
          (V:Value.S with type Cst.Instr.exec  = BellBase.instruction) = struct
   include BellBase
-  let is_amo = function
-    | Prmw _ -> true
-    | Pnop|Pld _|Pst _|Pfence _|Pcall _|Pbranch _|Pmov _ -> false
 
   let pp_barrier_short = pp_barrier
   let reject_mixed = false

herd/BellSem.ml

@@ -61,17 +61,13 @@ module
       let read_reg_ord = read_reg Port.No
       and read_reg_data = read_reg Port.Data
       and read_reg_addr = read_reg Port.Addr
-      
+
       let read_mem sz a s ii =
         M.read_loc Port.No (mk_read sz false s) (A.Location_global a) ii
 
       let read_mem_atom sz a s ii =
         M.read_loc Port.No (mk_read sz true s) (A.Location_global a) ii
 
-
-(*    let read_mem_atom cop a ii =
-      M.read_loc (mk_read true cop) (A.Location_global a) ii *)
-
       let write_reg r v ii =
         M.mk_singleton_es (Act.Access (Dir.W, (A.Location_reg (ii.A.proc,r)), v, false, [], reg_sz)) ii
 

herd/CAction.ml

@@ -197,6 +197,7 @@ end = struct
   let is_atomic = function
     | Access (_,A.Location_global _,_,_,at,_) -> at
     | _ -> false
+  and is_exclusive _ = false
 
   let is_fault _ = false
 

herd/CArch_herd.ml

@@ -16,7 +16,6 @@
 module Make (C:Arch_herd.Config) (V:Value.S) = struct
   include CBase
   (* Not so simple, should consider expressions... *)
-  let is_amo _ = assert false
 
   let pp_barrier_short = pp_barrier
   let reject_mixed = false

herd/JavaAction.ml

@@ -96,6 +96,7 @@ end = struct
   | Access (_,A.Location_global _,_,_,_) -> true
   | RMW _ -> true
   | _ -> false
+  and is_exclusive _ = false
 
   let to_fault _ = None
 

herd/JavaArch_herd.ml

@@ -20,7 +20,6 @@ module Make (C:Arch_herd.Config) (V:Value.S) = struct
 
   include JavaBase
 
-  let is_amo _            = false
   let pp_barrier_short    = pp_barrier
   let reject_mixed        = false
   let mem_access_size _   = None

herd/MIPSArch_herd.ml

@@ -21,7 +21,7 @@ module Make
          (V:Value.S with type Cst.Instr.exec  = MIPSBase.instruction ) =
   struct
     include MIPSBase
-    let is_amo _ = false
+
     let pp_barrier_short = pp_barrier
     let reject_mixed = false
 

herd/PPCArch_herd.ml

@@ -21,7 +21,6 @@ module Make (C:Arch_herd.Config) (V:Value.S)
   struct
     include PPCBase
 
-    let is_amo _ = false
     let pp_barrier_short = pp_barrier
     let reject_mixed = false
 

herd/RISCVArch_herd.ml

@@ -22,14 +22,6 @@ module Make (C:Arch_herd.Config) (V:Value.S) =
   struct
     include RISCVBase
 
-    let is_amo = function
-      | Amo _ -> true
-      | INop|Ret|Li _|J _|Bcc _|Load _|Store _|LoadReserve _
-      | OpI _|OpI2 _|OpIW _|Op _|OpW _|OpA _
-      |StoreConditional _|FenceIns _
-      |AUIPC _| Ext _
-           -> false
-
     let pp_barrier_short = function
       | FenceI -> "fence.i"
       | FenceTSO -> "fence.tso"

herd/X86Arch_herd.ml

@@ -19,13 +19,6 @@
 module Make (C:Arch_herd.Config)(V:Value.S) =
   struct
     include X86Base
-    let is_amo = function
-      |I_LOCK _ | I_XCHG _ -> true
-      |I_NOP|I_LFENCE|I_SFENCE|I_MFENCE|I_MOVSD|I_JMP _|I_JCC _|I_READ _
-      |I_ADD _|I_XOR _|I_OR _|I_MOV _|I_DEC _|I_CMP _|I_CMOVC _
-      |I_INC _|I_XCHG_UNLOCKED _|I_CMPXCHG _|I_SETNB _
-      |I_MOVB _|I_MOVW _|I_MOVL _|I_MOVQ _|I_MOVT _
-          -> false
 
     let pp_barrier_short = pp_barrier
     let reject_mixed = false
@@ -34,6 +27,7 @@ module Make (C:Arch_herd.Config)(V:Value.S) =
     let get_machsize _ = V.Cst.Scalar.machsize
     let empty_annot = false
     let is_atomic annot = annot
+    let is_exclusive _ = false
     let is_barrier b1 b2 = barrier_compare b1 b2 = 0
 
     let ifetch_value_sets = []

herd/X86_64Arch_herd.ml

@@ -19,12 +19,6 @@
 module Make (C:Arch_herd.Config)(V:Value.S) =
   struct
     include X86_64Base
-    let is_amo = function
-      | I_LOCK _ | I_EFF_EFF (I_XCHG,_,_,_) -> true
-      | I_NOP | I_RET | I_EFF_OP _ | I_EFF _ | I_EFF_EFF _
-      | I_CMPXCHG _ | I_JMP _ | I_JCC _ | I_CMOVC _ | I_MOVNTI _
-      | I_FENCE _ | I_MOVD _ | I_MOVNTDQA _ | I_CLFLUSH _
-        -> false
 
     let pp_barrier_short = pp_barrier
     let reject_mixed = false
@@ -35,6 +29,7 @@ module Make (C:Arch_herd.Config)(V:Value.S) =
     let is_atomic = function
       | Atomic -> true
       | Plain|NonTemporal -> false
+    and is_exclusive _ = false
     and is_nt = function
       | NonTemporal -> true
       | Plain|Atomic -> false

herd/action.mli

@@ -59,6 +59,7 @@ module type S = sig
   val is_tag : action -> bool
   val is_additional_mem : action -> bool (* abstract memory actions, eg locks *)
   val is_atomic : action -> bool
+  val is_exclusive : action -> bool
   val is_fault : action -> bool
   val to_fault : action -> A.fault option
   val get_mem_dir : action -> Dir.dirn

herd/arch_herd.mli

@@ -27,7 +27,6 @@ module type S =
     module V : Value.S with type Cst.Instr.exec = instruction
     module CS : ConstraintSolver.S with module V = V
 
-    val is_amo : instruction -> bool
     val pp_barrier_short : barrier -> string
     val reject_mixed : bool (* perform a check that rejects mixed-size tests *)
     val mem_access_size : instruction -> MachSize.sz option

herd/event.ml

@@ -99,9 +99,10 @@ val same_instance : event -> event -> bool
   val is_additional_mem : event -> bool
 (* Specific memory property examination *)
   val is_atomic : event -> bool
+  val is_exclusive : event -> bool
   val is_fault : event -> bool
   val to_fault : event -> A.fault option
-  val is_amo : event -> bool
+
   val get_mem_dir : event -> Dir.dirn
   val get_mem_size : event -> MachSize.sz
 
@@ -697,11 +698,10 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
       | _ -> false
     let is_additional_mem e = Act.is_additional_mem e.action
     let is_atomic e = Act.is_atomic e.action
+    let is_exclusive e = Act.is_exclusive e.action
     let is_fault e = Act.is_fault e.action
     let to_fault e = Act.to_fault e.action
-    let is_amo e = match e.iiid with
-    | IdSome {A.inst=i; _} when A.is_amo i -> Act.is_mem_store e.action
-    | _ -> false
+
     let get_mem_dir e = Act.get_mem_dir e.action
     let get_mem_size e = Act.get_mem_size e.action
 

herd/libdir/riscv-defs.cat

@@ -26,22 +26,23 @@ let fence =
   fence.rw.r | fence.rw.w | fence.rw.rw |
   fence.tso
 
-
 let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
 let rsw = rf^-1;rf
 let AcqRel = AcqRel|Sc (* Compat *)
 let AQ = (Acq|AcqRel)
 and RL = (Rel|AcqRel)
-let AMO = try AMO with (R & W) (* Compat *)
-let RCsc = (Acq|Rel|AcqRel) & (AMO|X)
+let RCsc = (Acq|Rel|AcqRel) & (EX|X)
+let AMO=X (* Generated by AMO instruction *)
+let SC=EX&W (* Generated by Store Conditional instruction *)
+
 (*************)
 (* ppo rules *)
 (*************)
 
 (* Overlapping-Address Orderings *)
 let r1 = [M];po-loc;[W]
 and r2 = ([R];po-loc-no-w;[R]) \ rsw
-and r3 = [AMO|X];rfi;[R]
+and r3 = [AMO|SC];rfi;[R]
 (* Explicit Synchronization *)
 and r4 = fence
 and r5 = [AQ];po;[M]

herd/libdir/riscv-tso-defs.cat

@@ -26,23 +26,22 @@ let fence =
   fence.rw.r | fence.rw.w | fence.rw.rw |
   fence.tso
 
-
 let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc)
 let rsw = rf^-1;rf
 let AcqRel = AcqRel|Sc (* Compat *)
 let AQ = (Acq|AcqRel)
 and RL = (Rel|AcqRel)
-let AMO = try AMO with (R & W) (* Compat *)
 (* All AMO ops have RCsc annotations *)
-let RCsc = (Acq|Rel|AcqRel|AMO) & (AMO|X)
+let AMO=X and SC=EX&W
+let RCsc = (Acq|Rel|AcqRel|AMO) & (X|EX)
 (*************)
 (* ppo rules *)
 (*************)
 
 (* Overlapping-Address Orderings *)
 let r1 = [M];po-loc;[W]
 and r2 = ([R];po-loc-no-w;[R]) \ rsw
-and r3 = [AMO|X];rfi;[R]
+and r3 = [AMO|SC];rfi;[R]
 (* Explicit Synchronization *)
 and r4 = fence
 and r5 = [AQ];po;[M]

herd/machAction.ml

@@ -31,6 +31,7 @@ module type A = sig
   val dirty_sets : (string * (DirtyBit.my_t -> V.Cst.PteVal.t -> bool)) list
 
   val is_atomic : lannot -> bool
+  val is_exclusive : lannot -> bool
   val is_isync : barrier -> bool
   val pp_isync : string
 
@@ -286,13 +287,16 @@ end = struct
 
   let is_additional_mem _ = false
 
-  let is_atomic a = match a with
-  | Access (_,_,_,an,_,_,_) ->
-      is_mem a && A.is_atomic an
+  let do_is_annot pred a = match a with
+  | Access (_,_,_,an,_,_,_)|Amo (_,_,_,an,_,_,_) ->
+      is_mem a && pred an
   | Arch a ->
-     is_mem_arch_action a && A.is_atomic (A.ArchAction.get_lannot a)
+     is_mem_arch_action a && pred (A.ArchAction.get_lannot a)
   | _ -> false
 
+  let is_atomic = do_is_annot A.is_atomic
+  and is_exclusive = do_is_annot A.is_exclusive
+
   let is_tag = function
     | Access (_,_,_,_,_,_,Access.TAG) -> true
     | Access _|Barrier _|Commit _

herd/machModelChecker.ml

@@ -480,7 +480,6 @@ module Make
                  "NExp", E.is_not_explicit;
                  "SPEC", is_spec;
                  "EXEC", (fun e -> not (is_spec e));
-                 "AMO",E.is_amo;
                  "SPURIOUS", E.is_spurious;
                  "IW", E.is_mem_store_init;
                  "FW",