diff --git a/herd/AArch64Arch_herd.ml b/herd/AArch64Arch_herd.ml index 2cfda801c3..1bad43763b 100644 --- a/herd/AArch64Arch_herd.ml +++ b/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 diff --git a/herd/ARMArch_herd.ml b/herd/ARMArch_herd.ml index b956bb1a07..6a21f2bbcf 100644 --- a/herd/ARMArch_herd.ml +++ b/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 diff --git a/herd/ASLAction.ml b/herd/ASLAction.ml index 93c9d8fa4e..ca33334038 100644 --- a/herd/ASLAction.ml +++ b/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 diff --git a/herd/ASLExtra.ml b/herd/ASLExtra.ml index be40439196..2494489c6b 100644 --- a/herd/ASLExtra.ml +++ b/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 diff --git a/herd/BPFArch_herd.ml b/herd/BPFArch_herd.ml index 4c35aea8c6..087e3b2541 100644 --- a/herd/BPFArch_herd.ml +++ b/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 diff --git a/herd/BellAction.ml b/herd/BellAction.ml index 64a3524ac0..e454e72fde 100644 --- a/herd/BellAction.ml +++ b/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 diff --git a/herd/BellArch_herd.ml b/herd/BellArch_herd.ml index c33102cdf8..012eb9992a 100644 --- a/herd/BellArch_herd.ml +++ b/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 diff --git a/herd/BellSem.ml b/herd/BellSem.ml index d2f0b32b5b..cb62e85597 100644 --- a/herd/BellSem.ml +++ b/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 diff --git a/herd/CAction.ml b/herd/CAction.ml index d0722ac69f..f0a95e1b94 100644 --- a/herd/CAction.ml +++ b/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 diff --git a/herd/CArch_herd.ml b/herd/CArch_herd.ml index 1a975cf056..24f89bc5fa 100644 --- a/herd/CArch_herd.ml +++ b/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 diff --git a/herd/JavaAction.ml b/herd/JavaAction.ml index 9455dfe9db..0296a70b64 100644 --- a/herd/JavaAction.ml +++ b/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 diff --git a/herd/JavaArch_herd.ml b/herd/JavaArch_herd.ml index d9c69f4719..702532b0fa 100644 --- a/herd/JavaArch_herd.ml +++ b/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 diff --git a/herd/MIPSArch_herd.ml b/herd/MIPSArch_herd.ml index f3e79ba554..a116b49bfb 100644 --- a/herd/MIPSArch_herd.ml +++ b/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 diff --git a/herd/PPCArch_herd.ml b/herd/PPCArch_herd.ml index 3ffdae6779..2bb99b6a57 100644 --- a/herd/PPCArch_herd.ml +++ b/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 diff --git a/herd/RISCVArch_herd.ml b/herd/RISCVArch_herd.ml index a685e44168..ee8707fc65 100644 --- a/herd/RISCVArch_herd.ml +++ b/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" diff --git a/herd/X86Arch_herd.ml b/herd/X86Arch_herd.ml index 01e585b56e..52cf2810e9 100644 --- a/herd/X86Arch_herd.ml +++ b/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 = [] diff --git a/herd/X86_64Arch_herd.ml b/herd/X86_64Arch_herd.ml index 3f879073c4..e6174b3eb9 100644 --- a/herd/X86_64Arch_herd.ml +++ b/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 diff --git a/herd/action.mli b/herd/action.mli index 9b68763d5d..f3f2ce66b6 100644 --- a/herd/action.mli +++ b/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 diff --git a/herd/arch_herd.mli b/herd/arch_herd.mli index 771a461bfd..aacdc996c2 100644 --- a/herd/arch_herd.mli +++ b/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 diff --git a/herd/event.ml b/herd/event.ml index f0a04c9bd3..436c2f1880 100644 --- a/herd/event.ml +++ b/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 diff --git a/herd/libdir/riscv-defs.cat b/herd/libdir/riscv-defs.cat index 7d5b3c4334..e3f96ab94c 100644 --- a/herd/libdir/riscv-defs.cat +++ b/herd/libdir/riscv-defs.cat @@ -26,14 +26,15 @@ 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 *) (*************) @@ -41,7 +42,7 @@ let RCsc = (Acq|Rel|AcqRel) & (AMO|X) (* 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] diff --git a/herd/libdir/riscv-tso-defs.cat b/herd/libdir/riscv-tso-defs.cat index 3cd3077663..950360347c 100644 --- a/herd/libdir/riscv-tso-defs.cat +++ b/herd/libdir/riscv-tso-defs.cat @@ -26,15 +26,14 @@ 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 *) (*************) @@ -42,7 +41,7 @@ let RCsc = (Acq|Rel|AcqRel|AMO) & (AMO|X) (* 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] diff --git a/herd/machAction.ml b/herd/machAction.ml index 66465e2b42..cba2703f1a 100644 --- a/herd/machAction.ml +++ b/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 _ diff --git a/herd/machModelChecker.ml b/herd/machModelChecker.ml index aa8de85ba0..79cbd02a50 100644 --- a/herd/machModelChecker.ml +++ b/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", diff --git a/herd/mem.ml b/herd/mem.ml index 6fe0dd5407..c7ab6dcca7 100644 --- a/herd/mem.ml +++ b/herd/mem.ml @@ -140,7 +140,7 @@ module type S = sig S.E.event -> S.E.A.location val make_atomic_load_store : - S.E.event_structure -> S.E.EventRel.t + S.test -> S.E.event_structure -> S.E.EventRel.t end @@ -1914,73 +1914,105 @@ let add_eq v1 v2 eqs = rfm E.EventRel.empty (* - * Reconstruct load/store atomic pairs, - * By definition such a pair exists 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. + * Reconstruct load/store atomic pairs. + * Computation for explicit accesses proceeds as follows: + * First, all "atomic" effects are grouped first by thread + * and then by location. Those "atomic" effects are + * then partitioned according to their generating instruction, + * AMO's (atomic proper below) or load-reserve and store-conditional + * (exclusives below). + * For exclusives, to each read we associate the + * closest generalised po successor exclusive store, + * by using a set of stores ordered by po. + * We additionally check that no exclusive read exists + * between the read and the write. + * For atomics proper, we proceed as above to associate an atomic write + * to each atomic load, we then check that the read and its associated write + * are generated by the same instruction. + * Finally, the computation is simpler for non-explicit such atomic + * pairs. In that case, pairs are given simply by the intra causality + * data relation. Namely, those pairs all stem from the atomic modification + * of page table entries. *) - let make_atomic_load_store es = - 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 + let make_atomic_load_store _test es = + + let atms,excls,nexps = U.collect_atomics_and_exclusives es in + + let module EvtSet = EvtSetByPo(struct let es = es end) in + + + (* + * Compute `[NExp & PTE & R]; iico_data & loc; [NExp & PTE & W])`, + * by simply restricting iico_data domain and range to + * implicit reads and writes. + * This assumes that all non-explicit atomic access modify operations + * are PTE updates. + *) + + let make_atomic_pairs_nexps evts = + let rs,ws = List.partition E.is_load evts in + let rs = E.EventSet.of_list rs + and ws = E.EventSet.of_list ws in + E.EventRel.restrict_domains_to_sets + rs ws es.E.intra_causality_data + + (* + * Compute `[Exp & R & X]; (same-instance \ id) & loc; [Exp & W & X]`, + * by matching each explicit atomic read with its (generalised) + * po-successor explicit atomic write to the same address. + * It is a fatal error for this write not to be emited + * by the same instruction instance as the read. + *) + + and make_atomic_pairs_exps atms = 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 + (fun k (_,atms) -> + U.LocEnv.fold + (fun _ evts k -> + let evts = + (* Get rid of RMW effects that are both read and write *) + List.filter (fun e -> E.is_load e <> E.is_store e) evts in + let rs,ws = List.partition E.is_load evts in + let ws = EvtSet.of_list ws in + List.fold_left + (fun k er -> + match EvtSet.find_first_after er ws with + | Some ew -> + assert (E.same_instance er ew) ; + (er,ew)::k + | None -> (* Cann occur for failing CAS *) + k) + k rs) + atms k) + [] atms |> E.EventRel.of_list + + (* Computes `[R & EX]; po \ (po; [M & EX]; po); [W & EX]`, + using OCaml code. *) + and make_atomic_pairs_exclusives excls = + List.fold_left + (fun k (_,evts) -> + let po = + Misc.doubleton_fold + (fun k e1 e2 -> + if E.po_strict e1 e2 then (e1,e2)::k + else if E.po_strict e2 e1 then (e2,e1)::k + else k) + [] evts |> E.EventRel.of_list in + (* Notice: po is from exclusive to exclusive *) + let open E.EventRel in + diff + (restrict_domains E.is_load E.is_store po) + (sequence po po) (* local po is already from EX to EX *) + ::k) + [] excls |> E.EventRel.unions in + + let amo = + E.EventRel.union + (make_atomic_pairs_nexps nexps) + (make_atomic_pairs_exps atms) + and lxsx = make_atomic_pairs_exclusives excls in + E.EventRel.union amo lxsx (* Retrieve last store from rfmap *) let get_max_store _test _es rfm loc = @@ -2554,7 +2586,7 @@ let add_eq v1 v2 eqs = | OptAce.True -> check_rfmap es rfm then (* Atomic load/store pairs *) - let atomic_load_store = make_atomic_load_store es in + let atomic_load_store = make_atomic_load_store test es in if C.variant Variant.OptRfRMW && some_same_rf_rmw rfm atomic_load_store diff --git a/herd/memUtils.ml b/herd/memUtils.ml index 7229413dd7..64d6917ee5 100644 --- a/herd/memUtils.ml +++ b/herd/memUtils.ml @@ -395,17 +395,38 @@ let lift_proc_info i evts = | None -> Some (LocEnv.singleton loc [e]) | Some m -> Some (LocEnv.accumulate loc e m) - let collect_atomics es = - let m,sp = + let accumulate_proc proc e = + IntMap.update proc @@ + function + | None -> Some [e] + | Some es -> Some (e::es) + + let collect_atomics_and_exclusives es = + let atms,excls,nexps = E.EventSet.fold - (fun e (m,sp as k) -> + (fun e (atms,excls,nexps 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 + | None -> + if E.is_spurious e then + atms,excls,(e::nexps) + else k + | Some proc -> + if E.is_explicit e then + accumulate_loc_proc proc (get_loc e) e atms,excls,nexps + else + atms,excls,(e::nexps) + else if E.is_exclusive e then + match E.proc_of e with + | None -> + Warn.fatal + "Exclusive effect %s must be issued by a thread" + (E.debug_event_str e) + | Some proc -> + atms,accumulate_proc proc e excls,nexps else k) - es.E.events (IntMap.empty,[]) in - IntMap.bindings m,sp + es.E.events (IntMap.empty,IntMap.empty,[]) in + IntMap.bindings atms,IntMap.bindings excls,nexps let partition_events es = let env = diff --git a/herd/memUtils.mli b/herd/memUtils.mli index d635e6136d..ce6829af13 100644 --- a/herd/memUtils.mli +++ b/herd/memUtils.mli @@ -87,17 +87,21 @@ module Make : functor (S: SemExtra.S) -> sig val collect_loads_non_spec : S.event_structure -> S.event list LocEnv.t (* - * Collect atomic effects indexed by threads and by locations. + * Collect atomic and exclusive 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. + * returns a tuple [(atms,excls,nexps)], where: + * + [atms] is a list of location maps, one per thread. + * The values of this map are the explicit atomic effects + * of the given thread. + * + [excls] is a list of exlusive effects, one per thread. + * + [nexps] is the list of non-explicit (atomic) effects. *) - val collect_atomics : - S.event_structure -> (Proc.t * S.event list LocEnv.t) list * S.event list + val collect_atomics_and_exclusives : + S.event_structure -> + (Proc.t * S.event list LocEnv.t) list + * (Proc.t * S.event list) list + * S.event list (* Partition by location *) val partition_events : S.event_set -> S.event_set list diff --git a/herd/slrc11.ml b/herd/slrc11.ml index db7109aff4..bcbe210907 100644 --- a/herd/slrc11.ml +++ b/herd/slrc11.ml @@ -876,7 +876,7 @@ module Make (M:Cfg) let check_rfms test rfms _kfail _kont model_kont res = let (_, cs0, es0) = rfms in let (es, rfm, cs) = solve test es0 cs0 in - let rmws = M.make_atomic_load_store es in + let rmws = M.make_atomic_load_store test es in let evts = E.EventSet.filter real es.E.events in let inits = E.EventSet.filter E.is_mem_store_init evts in let po = U.po_iico es in diff --git a/herd/tests/instructions/RISCV/A021.litmus b/herd/tests/instructions/RISCV/A021.litmus new file mode 100644 index 0000000000..9064a2c2d0 --- /dev/null +++ b/herd/tests/instructions/RISCV/A021.litmus @@ -0,0 +1,17 @@ +RISCV A021 +(* Tests rule 3 of ppo: Rfi from write exclusive is in ppo, forbidden. *) +{ + 0:x6=x; 0:x8=y; + 1:x6=x; 1:x8=y; 1:x9=z; +} + P0 | P1 ; + ori x5,x0,1 | lw x5,0(x8) ; + sw x5,0(x6) | fence r,w ; + fence iorw,iorw | ori x7,x0,1 ; + ori x7,x0,1 | lr.w x10,(x9) ; + sw x7,0(x8) | sc.w x11,x7,(x9) ; + | lw x13,0(x9) ; + | xor x14,x13,x13 ; + | add x16,x6,x14 ; + | lw x15,0(x16) ; +~exists (1:x5=1 /\ 1:x13=1 /\ 1:x15=0) diff --git a/herd/tests/instructions/RISCV/A021.litmus.expected b/herd/tests/instructions/RISCV/A021.litmus.expected new file mode 100644 index 0000000000..76a3aa36fd --- /dev/null +++ b/herd/tests/instructions/RISCV/A021.litmus.expected @@ -0,0 +1,16 @@ +Test A021 Forbidden +States 7 +1:x5=0; 1:x13=0; 1:x15=0; +1:x5=0; 1:x13=0; 1:x15=1; +1:x5=0; 1:x13=1; 1:x15=0; +1:x5=0; 1:x13=1; 1:x15=1; +1:x5=1; 1:x13=0; 1:x15=0; +1:x5=1; 1:x13=0; 1:x15=1; +1:x5=1; 1:x13=1; 1:x15=1; +Ok +Witnesses +Positive: 7 Negative: 0 +Condition ~exists (1:x5=1 /\ 1:x13=1 /\ 1:x15=0) +Observation A021 Never 0 7 +Hash=ca29792908216df96447f220d919053d + diff --git a/herd/tests/instructions/RISCV/A022.litmus b/herd/tests/instructions/RISCV/A022.litmus new file mode 100644 index 0000000000..acadb770e2 --- /dev/null +++ b/herd/tests/instructions/RISCV/A022.litmus @@ -0,0 +1,16 @@ +RISCV A022 +(* Tests rule 3 of ppo: Rfi from write atomic is in ppo, forbidden. *) +{ + 0:x6=x; 0:x8=y; + 1:x6=x; 1:x8=y; 1:x9=z; +} + P0 | P1 ; + ori x5,x0,1 | lw x5,0(x8) ; + sw x5,0(x6) | fence r,w ; + fence iorw,iorw | ori x7,x0,1 ; + ori x7,x0,1 | amoswap.w x11,x7,(x9) ; + sw x7,0(x8) | lw x13,0(x9) ; + | xor x14,x13,x13 ; + | add x16,x6,x14 ; + | lw x15,0(x16) ; +~exists (1:x5=1 /\ 1:x13=1 /\ 1:x15=0) diff --git a/herd/tests/instructions/RISCV/A022.litmus.expected b/herd/tests/instructions/RISCV/A022.litmus.expected new file mode 100644 index 0000000000..01bcbd3685 --- /dev/null +++ b/herd/tests/instructions/RISCV/A022.litmus.expected @@ -0,0 +1,12 @@ +Test A022 Forbidden +States 3 +1:x5=0; 1:x13=1; 1:x15=0; +1:x5=0; 1:x13=1; 1:x15=1; +1:x5=1; 1:x13=1; 1:x15=1; +Ok +Witnesses +Positive: 3 Negative: 0 +Condition ~exists (1:x5=1 /\ 1:x13=1 /\ 1:x15=0) +Observation A022 Never 0 3 +Hash=59012c83b13704a1ae4f80decce7e06f + diff --git a/herd/tests/instructions/RISCV/A023.litmus b/herd/tests/instructions/RISCV/A023.litmus new file mode 100644 index 0000000000..31b3da2af8 --- /dev/null +++ b/herd/tests/instructions/RISCV/A023.litmus @@ -0,0 +1,17 @@ +RISCV A023 +(* Reference for A021 and A022, allowed. *) +{ + 0:x6=x; 0:x8=y; + 1:x6=x; 1:x8=y; 1:x9=z; +} + P0 | P1 ; + ori x5,x0,1 | lw x5,0(x8) ; + sw x5,0(x6) | fence r,w ; + fence iorw,iorw | ori x7,x0,1 ; + ori x7,x0,1 | sw x7,0(x9) ; + sw x7,0(x8) | lw x10,0(x9) ; + | xor x11,x10,x10 ; + | add x13,x6,x11 ; + | lw x12,0(x13) ; + +exists (1:x5=1 /\ 1:x10=1 /\ 1:x12=0) diff --git a/herd/tests/instructions/RISCV/A023.litmus.expected b/herd/tests/instructions/RISCV/A023.litmus.expected new file mode 100644 index 0000000000..60824fbccf --- /dev/null +++ b/herd/tests/instructions/RISCV/A023.litmus.expected @@ -0,0 +1,13 @@ +Test A023 Allowed +States 4 +1:x5=0; 1:x10=1; 1:x12=0; +1:x5=0; 1:x10=1; 1:x12=1; +1:x5=1; 1:x10=1; 1:x12=0; +1:x5=1; 1:x10=1; 1:x12=1; +Ok +Witnesses +Positive: 1 Negative: 3 +Condition exists (1:x5=1 /\ 1:x10=1 /\ 1:x12=0) +Observation A023 Sometimes 1 3 +Hash=1cef5e303435fcd77fc6fab84399ba4f + diff --git a/lib/misc.ml b/lib/misc.ml index a4772bbe61..91bfaff96c 100644 --- a/lib/misc.ml +++ b/lib/misc.ml @@ -344,6 +344,14 @@ let check_same eq f xs = None xs with Exit -> None +let doubleton_fold f = + let rec fold_rec k = function + | [] -> k + | x::xs -> + let k = List.fold_left (fun k y -> f k x y) k xs in + fold_rec k xs in + fold_rec + (* Bool's *) let (|||) p1 p2 = fun e -> p1 e || p2 e diff --git a/lib/misc.mli b/lib/misc.mli index 8b326670d8..e72196325b 100644 --- a/lib/misc.mli +++ b/lib/misc.mli @@ -165,6 +165,11 @@ val group_iteri : ('a -> 'a -> int) -> (int -> 'a -> 'a list -> unit) -> 'a list (* Check that f yields the same result on all list elements *) val check_same : ('a -> 'a -> bool) -> ('b -> 'a) -> 'b list -> 'a option +(* [doubleton_fold f k_) [x_1;..;x_n] k_0] + computes [(f (f (... (f (f k_0 x_1 x_2) x_1 x_3)) ...) x_{n-1} x_n))] + for all i,j where i in [1..n], j in [1..n], i < j *) +val doubleton_fold : ('b -> 'a -> 'a -> 'b) -> 'b -> 'a list -> 'b + (* Lift boolean connectors to predicates *) val (|||) : ('a -> bool) -> ('a -> bool) -> 'a -> bool val (&&&) : ('a -> bool) -> ('a -> bool) -> 'a -> bool