From 33bf236e682648c1afa271cf7ac4c89d4ce68432 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Tue, 16 Jun 2026 12:25:10 +0100 Subject: [PATCH 01/10] [herd] Fix typo in libdir/aarch64fences.cat Signed-off-by: Nikos Nikoleris --- herd/libdir/aarch64fences.cat | 2 +- herd/tests/instructions/AArch64.kvm/A018.litmus.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/herd/libdir/aarch64fences.cat b/herd/libdir/aarch64fences.cat index 3ef45cca5d..8296f3cde5 100644 --- a/herd/libdir/aarch64fences.cat +++ b/herd/libdir/aarch64fences.cat @@ -45,5 +45,5 @@ let dsb.full = DSB.NSH | DSB.ISH | DSB.OSH | DSB.SY let dsb.ld = DSB.NSHLD | DSB.ISHLD | DSB.OSHLD | DSB.LD flag ~empty (DSB.NSHLD | DSB.ISHLD | DSB.OSHLD) as Maintenance-scope-for-DSB-LD-is-deprecated let dsb.st = DSB.NSHST | DSB.ISHST | DSB.OSHST | DSB.ST -flag ~empty (DSB.NSHST | DSB.ISHST | DSB.OSHST) as Maintnenace-scope-for-DSB-ST-is-deprecated +flag ~empty (DSB.NSHST | DSB.ISHST | DSB.OSHST) as Maintenance-scope-for-DSB-ST-is-deprecated diff --git a/herd/tests/instructions/AArch64.kvm/A018.litmus.expected b/herd/tests/instructions/AArch64.kvm/A018.litmus.expected index 4fabaefcb2..590feb72aa 100644 --- a/herd/tests/instructions/AArch64.kvm/A018.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A018.litmus.expected @@ -4,7 +4,7 @@ States 1 Loop Ok Witnesses Positive: 1 Negative: 0 -Flag Maintnenace-scope-for-DSB-ST-is-deprecated +Flag Maintenance-scope-for-DSB-ST-is-deprecated Condition forall (0:X0=1) Observation A018 Always 1 0 Hash=218f088f0c448c84eeeb7c12fcb86c43 From 3cb2806e15936a79d842d0f263b15a4122a0f3a8 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 16:45:26 +0100 Subject: [PATCH 02/10] [tools] Add miaou support for the domain procedure Signed-off-by: Nikos Nikoleris --- tools/miaou.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/tools/miaou.ml b/tools/miaou.ml index 4ae9e4c821..04bf235284 100644 --- a/tools/miaou.ml +++ b/tools/miaou.ml @@ -564,7 +564,14 @@ and cons_seqs (fs:exp list) (es:exp list) = List { l with items = List.rev items; } | _ as i -> i end - | e -> + | App (_,Var (_,"domain"), rel) -> + let e3 = Next.next () in + begin match tr_rel e1 e3 rel with + | List ({ items; _ } as l) -> + List { l with items = List.rev items; } + | _ as i -> i + end + | e -> Item (fail (ASTUtils.exp2loc e) "ignoring expression") and tr_evts_not e1 e = notItem (tr_evts e1 e) From 474743e11e4b15ad606d4f3df5adddfa628b7ec8 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 15:20:27 +0100 Subject: [PATCH 03/10] [herd] Fix writable2 function in machModelChecker writable2 e1 e2 was intended to return true if either e1 or e2 or both are writable PteVals. A PteVal is consider to give writeable access to the OA, if it is valid and the af the db are set. If hardware updates are enabled for the CPU that uses the PteVal, the af and the db can be set automatically on access. In this case the PteVal can be writable even when the af and db are not set. This patches fixes the function writable to consider whether hardware update for the right CPU or for no CPU is the event is due to an initialisation. Signed-off-by: Nikos Nikoleris --- herd/machModelChecker.ml | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/herd/machModelChecker.ml b/herd/machModelChecker.ml index 73a74ac4c9..aad63454f2 100644 --- a/herd/machModelChecker.ml +++ b/herd/machModelChecker.ml @@ -156,24 +156,18 @@ module Make S.A.V.Cst.PteVal.same_oa p1 p2 | _ -> false - let writable2 = - let writable ha hd e = match S.E.value_of e with + let writable2 e1 e2 = + let writable e = + let ha,hd = + let open DirtyBit in + match S.E.proc_of e, O.dirty with + | Some proc, Some d -> d.ha proc,d.hd proc + | _, _ -> false,false in + match S.E.value_of e with | Some (S.A.V.Val (Constant.PteVal p)) -> - S.A.V.Cst.PteVal.writable ha hd p + S.A.V.Cst.PteVal.writable ha hd p | _ -> false in - fun e1 e2 -> - let p = S.E.proc_of e1 in - match p with - | None -> - Warn.user_error - "Init or spurious write as first argument of writable2" - | Some p -> - let ha,hd = - let open DirtyBit in - match O.dirty with - | Some d -> d.ha p,d.hd p - | None -> false,false in - writable ha hd e1 || writable ha hd e2 + writable e1 || writable e2 end From db2be17949fd0bd62e2d5ae9cdc053b29752190a Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 15:43:14 +0100 Subject: [PATCH 04/10] [herd] Move the definition of ca from aarch64.cat to cos.cat This allows other cat files to use ca. Signed-off-by: Nikos Nikoleris --- herd/libdir/aarch64.cat | 3 --- herd/libdir/cos.cat | 3 +++ 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat index bfeb957ad6..6001dcd436 100644 --- a/herd/libdir/aarch64.cat +++ b/herd/libdir/aarch64.cat @@ -48,9 +48,6 @@ catdep (* This option says that the cat file computes dependencies *) include "aarch64hwreqs.cat" -(*** Coherence-after ***) -let ca = fr | co - (*** TLBI-after, DC-after, IC-after ***) include "enumerations.cat" with TLBI-after from (all-TLBI-Imp_TTD_R-enums local-hw-reqs) diff --git a/herd/libdir/cos.cat b/herd/libdir/cos.cat index d50481a7e9..c045bb0ab3 100644 --- a/herd/libdir/cos.cat +++ b/herd/libdir/cos.cat @@ -5,3 +5,6 @@ if "cos-opt" else include "cos-no-opt.cat" end + +(*** Coherence-after ***) +let ca = fr | co From d74e825d27dad7b22aa66f37ad552ecb7b76c40d Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 15:44:33 +0100 Subject: [PATCH 05/10] [herd] Fix the definitions that flag tests that need BBM Signed-off-by: Nikos Nikoleris --- herd/libdir/aarch64.cat | 4 +- herd/libdir/aarch64bbm.cat | 30 ++++------ herd/libdir/aarch64memattrs.cat | 2 - herd/libdir/aarch64util.cat | 12 ++-- .../AArch64.kvm/A031.litmus.expected | 2 +- .../AArch64.kvm/A036.litmus.expected | 1 + lib/interpreter.ml | 56 +++++-------------- 7 files changed, 37 insertions(+), 70 deletions(-) diff --git a/herd/libdir/aarch64.cat b/herd/libdir/aarch64.cat index 6001dcd436..32b1ae8747 100644 --- a/herd/libdir/aarch64.cat +++ b/herd/libdir/aarch64.cat @@ -167,8 +167,8 @@ irreflexive [Exp & Tag & W]; (po & same-loc); [Imp & Tag & R]; (ca & int) as coW empty (rmw & (fr; co)) \ (([Exp]; rmw; [Exp]) & (fri ; [Exp & W]; coi)) as atomic (*** Break Before Make ***) -let BBM = ([TTDV]; ca; [TTDINV]; co; [TTDV]) -flag ~empty (TTD-update-needsBBM & ~BBM) as requires-BBM +let BBM = [TLBCacheableTTD]; ca; [TLBUncacheableTTD]; ob; [TLBI]; ob & inv-scope; [TLBCacheableTTD] +flag ~empty (TTD-update-needsBBM \ BBM) as Warning-BBM-expected (*** Additional synchronisation requirements for CMODX ***) let CMODX-conflicts = same-loc & ( diff --git a/herd/libdir/aarch64bbm.cat b/herd/libdir/aarch64bbm.cat index 79c96e9ad3..513cf3a0ba 100644 --- a/herd/libdir/aarch64bbm.cat +++ b/herd/libdir/aarch64bbm.cat @@ -46,43 +46,37 @@ *) include "aarch64memattrs.cat" -(* Can we move this to stdlib? *) -(* Coherence-after *) -let ca = fr | co - -let PTE-MT-update = +let TTD-MT-update = [Normal]; ca; [Device] | [Device]; ca; [Normal] -let PTE-SH-update = +let TTD-SH-update = [NSH]; ca; [ISH | OSH] | [ISH]; ca; [OSH | NSH] | [OSH]; ca; [NSH | ISH] -let PTE-ICH-update = +let TTD-ICH-update = [iNC]; ca; [iWT | iWB] | [iWT]; ca; [iWB | iNC] | [iWB]; ca; [iNC | iWT] -let PTE-OCH-update = +let TTD-OCH-update = [oNC]; ca; [oWT | oWB] | [oWT]; ca; [oWB | oNC] | [oWB]; ca; [oNC | oWT] -let PTE-DT-update = +let TTD-DT-update = [Device-GRE]; ca; [Device-nGRE | Device-nGnRE | Device-nGnRnE] | [Device-nGRE]; ca; [Device-GRE | Device-nGnRE | Device-nGnRnE] | [Device-nGnRE]; ca; [Device-GRE | Device-nGRE | Device-nGnRnE] | [Device-nGnRnE]; ca; [Device-GRE | Device-nGRE | Device-nGnRE] -let PTE-OA-update = ([PTE]; ca; [PTE & oa-changes(PTE, ca^-1)]) -let PTE-OA-update-writable = PTE-OA-update & - ([PTE]; ca; [PTE & at-least-one-writable(PTE, ca^-1)]) +let TTD-OA-update = oa-changes(TTD*TTD) & ca +let TTD-at-least-one-writable = at-least-one-writable(TTD*TTD) -let PTE-update-needsBBM = ([PTEV]; ca \ (ca; [PTEV]; ca); [PTEV]) & - (PTE-MT-update | PTE-SH-update | PTE-ICH-update | PTE-OCH-update | PTE-DT-update - | PTE-OA-update) +let TLBUncacheableTTD = TTDINV | TTDAF0 +let TLBCacheableTTD = TTD \ TLBUncacheableTTD -let TTDV = PTEV -let TTDINV = PTEINV -let TTD-update-needsBBM = PTE-update-needsBBM +let TTD-update-needsBBM = + [TLBCacheableTTD]; (TTD-MT-update | TTD-SH-update | TTD-ICH-update | TTD-OCH-update | TTD-DT-update + | TTD-OA-update & TTD-at-least-one-writable); [domain([TLBCacheableTTD]; rf; [Imp & TTD & R])] diff --git a/herd/libdir/aarch64memattrs.cat b/herd/libdir/aarch64memattrs.cat index 27e49fafac..1c689f1aaf 100644 --- a/herd/libdir/aarch64memattrs.cat +++ b/herd/libdir/aarch64memattrs.cat @@ -41,8 +41,6 @@ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -let TTD = PTE - (*** Device Memory ***) (* Device Memory Types *) diff --git a/herd/libdir/aarch64util.cat b/herd/libdir/aarch64util.cat index 9b8a779bdf..411ded9260 100644 --- a/herd/libdir/aarch64util.cat +++ b/herd/libdir/aarch64util.cat @@ -55,12 +55,13 @@ let ii_data = [DATA]; (iico_data|iico_ctrl)+ * -variant vmsa *) -let PTE = if "vmsa" then PTE else emptyset -let PTEV = if "vmsa" then PTEV else emptyset -let PTEINV = if "vmsa" then PTEINV else emptyset +let TTD = if "vmsa" then PTE else emptyset +let TTDV = if "vmsa" then PTEV else emptyset +let TTDINV = if "vmsa" then PTEINV else emptyset +let TTDAF0 = if "vmsa" then PTEAF0 else emptyset let inv-domain = if "vmsa" then inv-domain else 0 -let D-PTE = if "vmsa" then D-PTE else emptyset -let I-PTE = if "vmsa" && "ifetch" then PTE \ D-PTE else emptyset +let D-TTD = if "vmsa" then D-PTE else emptyset +let I-TTD = if "vmsa" && "ifetch" then PTE \ D-PTE else emptyset let AF = if "vmsa" then AF else emptyset let DB = if "vmsa" then DB else emptyset let MMU = if "vmsa" then MMU else emptyset @@ -97,7 +98,6 @@ let IC = IC.IALLUIS | IC.IALLU | IC.IVAU let Imp = NExp let SPONTANEOUS = SPURIOUS let inv-scope = inv-domain -let TTD = PTE let D-TTD = if "vmsa" then D-PTE else emptyset let I-TTD = if "vmsa" then I-PTE else emptyset let Tag = T diff --git a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected index fef58ad5a4..9b3222b3fd 100644 --- a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected @@ -6,7 +6,7 @@ States 3 Ok Witnesses Positive: 8 Negative: 0 -Flag requires-BBM +Flag Warning-BBM-expected Condition ~exists ([PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2) Observation A031 Never 0 8 Hash=b49f887241d4043b0d917f97925e00ab diff --git a/herd/tests/instructions/AArch64.kvm/A036.litmus.expected b/herd/tests/instructions/AArch64.kvm/A036.litmus.expected index fd0c770d44..a8ffc6e63a 100644 --- a/herd/tests/instructions/AArch64.kvm/A036.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A036.litmus.expected @@ -6,6 +6,7 @@ Ok Witnesses Positive: 8 Negative: 0 Flag Shareability-argument-for-DMB-is-deprecated +Flag Warning-BBM-expected Condition exists (0:X0=2 /\ 0:X1=1) Observation A036 Always 8 0 Hash=cfe50b9b0465b36af5f17bad83823a0b diff --git a/lib/interpreter.ml b/lib/interpreter.ml index 7ba97995e2..920e498330 100644 --- a/lib/interpreter.ml +++ b/lib/interpreter.ml @@ -916,6 +916,17 @@ module Make *) let arg_mismatch () = raise (PrimError "argument mismatch") + let filter_rel f = + function + | V.Rel r -> + V.Rel (E.EventRel.restrict_rel f r) + | V.TransRel tr -> + V.Rel + E.EventRel. + (restrict_rel f @@ transitive_closure tr) + | _ -> arg_mismatch () + + let partition arg = match arg with | Set evts -> let r = U.partition_events evts in @@ -1136,50 +1147,13 @@ module Make and different_values arg = let different_val e1 e2 = not (U.same_value e1 e2) in - match arg with - | V.Rel r -> - let r = E.EventRel.restrict_rel different_val r in - V.Rel r - | V.TransRel tr -> - let r = E.EventRel.transitive_closure tr in - let r = E.EventRel.restrict_rel different_val r in - V.Rel r - | _ -> arg_mismatch () + filter_rel different_val arg - and same_oaRel arg = - match arg with - | V.Rel r -> - V.Rel (E.EventRel.restrict_rel U.same_oa r) - | V.TransRel tr -> - V.Rel - E.EventRel. - (restrict_rel U.same_oa @@ transitive_closure tr) - | _ -> arg_mismatch () + and same_oaRel arg = filter_rel U.same_oa arg - and check_two pred arg = match arg with - | V.Tuple [V.Set ws; (V.Rel _ | V.TransRel _) as prec; ] -> - let m = - match prec with - | V.Rel m -> m - | V.TransRel m -> E.EventRel.transitive_closure m - | _ -> assert false - in - let ws = - E.EventSet.filter - (fun w -> - E.is_store w && E.is_pt w && - begin - match E.EventSet.as_singleton (E.EventRel.succs m w) with - | Some p -> pred w p - (* w does not qualify when zero of two or more prec-related events *) - | None -> false - end) - ws in - V.Set ws - | _ -> arg_mismatch () + and oa_changes arg = filter_rel (fun w p -> not (U.same_oa w p)) arg - let oa_changes = check_two (fun w p -> not (U.same_oa w p)) - and at_least_one_writable = check_two U.writable2 + and at_least_one_writable arg = filter_rel U.writable2 arg let as_transitive = function From 9ed3ed79e853203a7260cf0210e9b23fee5145b0 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 16:48:55 +0100 Subject: [PATCH 06/10] [herd] Add tex macros for the aarch64.cat for the BBM relations --- herd/libdir/catdefinitions.tex | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/herd/libdir/catdefinitions.tex b/herd/libdir/catdefinitions.tex index 61a45de749..9532e6012d 100644 --- a/herd/libdir/catdefinitions.tex +++ b/herd/libdir/catdefinitions.tex @@ -98,6 +98,21 @@ % % +\newcommand{\TTDupdateneedsBBMemph}[2]{The TTD update from #1 to #2 needs BBM} +\newcommand{\TTDupdateneedsBBM}[2]{The TTD update from #1 to #2 needs BBM} +\newcommand{\TLBCacheableTTD}[1]{The value of #1 is TLB Cacheable} +\newcommand{\TLBUncacheableTTD}[1]{The value of #1 is TLB Uncacheable} +\newcommand{\TTDV}[1]{The value of #1 is a valid TTD} +\newcommand{\TTDMTupdate}[2]{#1 and #2 specify different memory type} +\newcommand{\TTDDTupdate}[2]{#1 and #2 specify different Device memory type} +\newcommand{\TTDSHupdate}[2]{#1 and #2 specify different Shareability} +\newcommand{\TTDICHupdate}[2]{#1 and #2 specify different inner Cacheability} +\newcommand{\TTDOCHupdate}[2]{#1 and #2 specify different outer Cacheability} +\newcommand{\TTDOAupdate}[2]{#1 and #2 specify different OA} +\newcommand{\TTDatleastonewritable}[2]{Either #1 or #2 grant write permission} +\newcommand{\BBMemph}[2]{There is a \emph{Break-before-make sequence} between #1 and #2} +\newcommand{\BBM}[2]{There is a Break-before-make sequence between #1 and #2} + \newcommand{\Exp}[1]{#1 is an Explicit Effect} \newcommand{\ExpMREof}[1]{the Explicit \MRE{} of #1} \newcommand{\ImpMREof}[1]{the Implicit \MRE{} of #1} From 4d4e6f99403c7f269a89e1f88126634a586017dd Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Thu, 11 Jun 2026 16:18:48 +0100 Subject: [PATCH 07/10] [catalogue] Add a new catalogue for aarch64 illustrative of BBM Signed-off-by: Nikos Nikoleris --- Makefile | 13 ++++++++++++ .../aarch64-BBM/tests/CoRW2+PteOA.litmus | 12 +++++++++++ .../tests/CoRW2+PteOA.litmus.expected | 11 ++++++++++ catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus | 12 +++++++++++ .../tests/CoWR+PteOA.litmus.expected | 12 +++++++++++ .../MP+dsb.ishs-[isb]+posptev0pteoa.litmus | 17 ++++++++++++++++ ...b.ishs-[isb]+posptev0pteoa.litmus.expected | 15 ++++++++++++++ ...sync.ishWptev0pteoa-popteoal+dmb.ld.litmus | 20 +++++++++++++++++++ ...ptev0pteoa-popteoal+dmb.ld.litmus.expected | 14 +++++++++++++ .../MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus | 18 +++++++++++++++++ ...i-sync.ishpteoadb0p+dmb.ld.litmus.expected | 12 +++++++++++ .../MP+tlbi-sync.ishpteoap+dmb.ld.litmus | 18 +++++++++++++++++ ...tlbi-sync.ishpteoap+dmb.ld.litmus.expected | 13 ++++++++++++ ...sRpteaf0pte-amo.casptepteoa.af1+pos.litmus | 18 +++++++++++++++++ ...te-amo.casptepteoa.af1+pos.litmus.expected | 12 +++++++++++ ...P+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus | 17 ++++++++++++++++ ...nc.ishspteaf0pteoa.af1+pos.litmus.expected | 15 ++++++++++++++ .../tests/RW+RR+rel+acq+PteOA.litmus | 14 +++++++++++++ .../tests/RW+RR+rel+acq+PteOA.litmus.expected | 14 +++++++++++++ catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus | 13 ++++++++++++ .../tests/W+WW+PteOA.litmus.expected | 14 +++++++++++++ catalogue/aarch64-BBM/tests/coRR+BBM.litmus | 18 +++++++++++++++++ .../tests/coRR+BBM.litmus.expected | 14 +++++++++++++ .../tests/coRR+dsb.ishs-[isb]+PteOA.litmus | 14 +++++++++++++ .../coRR+dsb.ishs-[isb]+PteOA.litmus.expected | 14 +++++++++++++ .../aarch64-BBM/tests/coRW+Wpteoa-copy.litmus | 15 ++++++++++++++ .../tests/coRW+Wpteoa-copy.litmus.expected | 12 +++++++++++ 27 files changed, 391 insertions(+) create mode 100644 catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus create mode 100644 catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus create mode 100644 catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus create mode 100644 catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus create mode 100644 catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus create mode 100644 catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/coRR+BBM.litmus create mode 100644 catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus create mode 100644 catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected create mode 100644 catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus create mode 100644 catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected diff --git a/Makefile b/Makefile index 0cb9096b92..c1f00f905a 100644 --- a/Makefile +++ b/Makefile @@ -283,6 +283,19 @@ cata-test:: test.herd.cata.aarch64-ETS3 cata-test:: test.herd.cata.bpf cata-test:: test.herd.cata.x86_64 +test.herd.cata-ext.%: + @ echo + $(HERD_REGRESSION_TEST) \ + -j $(J) \ + $(NOHASH) \ + -herd-path $(HERD) \ + -libdir-path ./herd/libdir \ + -litmus-dir catalogue/$*/tests \ + $(REGRESSION_TEST_MODE) + @ echo "herd7 catalogue $* instructions tests: OK" + +cata-test-all:: test.herd.cata-ext.aarch64-bbm + test.herd-mixed.cata.%: @ echo $(HERD_CATALOGUE_REGRESSION_TEST) \ diff --git a/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus new file mode 100644 index 0000000000..4442d41283 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus @@ -0,0 +1,12 @@ +AArch64 CoRW2+PteOA +Variant=vmsa +{ + [PTE(x)]=(oa:PA(x)); + 0:X1=x; + 1:X4=(oa:PA(y)); 1:X5=PTE(x); +} + P0 | P1 ; + LDR W0,[X1] | STR X4,[X5] ; + MOV W2,#1 | ; + STR W2,[X1] | ; +exists(0:X0=1) diff --git a/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected new file mode 100644 index 0000000000..a38d7d2d10 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/CoRW2+PteOA.litmus.expected @@ -0,0 +1,11 @@ +Test CoRW2+PteOA Allowed +States 1 +0:X0=0; +No +Witnesses +Positive: 0 Negative: 2 +Flag Warning-BBM-expected +Condition exists (0:X0=1) +Observation CoRW2+PteOA Never 0 2 +Hash=9de3aed52a968ab42947a7ce50719893 + diff --git a/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus new file mode 100644 index 0000000000..28c687d1ce --- /dev/null +++ b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus @@ -0,0 +1,12 @@ +AArch64 CoWR+PteOA +Variant=vmsa +{ + [PTE(x)]=(oa:PA(x)); + 0:X1=x; + 1:X4=(oa:PA(y)); 1:X5=PTE(x); +} + P0 | P1 ; + MOV W0,#1 | STR X4,[X5] ; + STR W0,[X1] | ; + LDR W2,[X1] | ; +exists(0:X2=0) diff --git a/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected new file mode 100644 index 0000000000..5dd9c9c771 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/CoWR+PteOA.litmus.expected @@ -0,0 +1,12 @@ +Test CoWR+PteOA Allowed +States 2 +0:X2=0; +0:X2=1; +Ok +Witnesses +Positive: 1 Negative: 2 +Flag Warning-BBM-expected +Condition exists (0:X2=0) +Observation CoWR+PteOA Sometimes 1 2 +Hash=07e4543b71a8507c54a06609bbe02023 + diff --git a/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus new file mode 100644 index 0000000000..bafb26f76f --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus @@ -0,0 +1,17 @@ +AArch64 MP+dsb.ishs-[isb]+posptev0pteoa +Variant=vmsa +{ + [y]=1; + [PTE(x)]=(oa:PA(x)); + 0:X1=x; 1:X1=x; + 1:X4=(valid:0); 1:X5=PTE(x); + 1:X6=(oa:PA(y)); +} + P0 | P1 ; + L1: | STR X4,[X5] ; + LDR W0,[X1] | STR X6,[X5] ; + DSB ISH | ; + ISB | ; + L2: | ; + LDR W2,[X1] | ; +exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x))) diff --git a/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected new file mode 100644 index 0000000000..638b6df112 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+dsb.ishs-[isb]+posptev0pteoa.litmus.expected @@ -0,0 +1,15 @@ +Test MP+dsb.ishs-[isb]+posptev0pteoa Allowed +States 5 +0:X0=0; 0:X2=0; ~Fault(P0:L2,x); +0:X0=0; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation); +0:X0=0; 0:X2=1; ~Fault(P0:L2,x); +0:X0=1; 0:X2=0; ~Fault(P0:L2,x); +0:X0=1; 0:X2=1; ~Fault(P0:L2,x); +Ok +Witnesses +Positive: 1 Negative: 5 +Flag Warning-BBM-expected +Condition exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x))) +Observation MP+dsb.ishs-[isb]+posptev0pteoa Sometimes 1 5 +Hash=b59acf4b892251b7a42f01048c3b71de + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus new file mode 100644 index 0000000000..32d186d274 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus @@ -0,0 +1,20 @@ +AArch64 MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld +Variant=vmsa +{ + [x]=1; [y]=2; + [PTE(x)]=(oa:PA(x)); + 0:X1=(valid:0); 0:X0=PTE(x); + 0:X5=(oa:PA(y),valid:1); + 0:X3=z; 0:X4=x; + 1:X3=z; 1:X4=x; +} + P0 | P1 ; + STR X1,[X0] | LDR W2,[X3] ; + DSB ISH | DMB LD ; + LSR X9,X4,#12 | LDR W5,[X4] ; + TLBI VAAE1IS,X9 | ; + DSB ISH | ; + STR X5,[X0] | ; + MOV W2,#1 | ; + STLR W2,[X3] | ; +exists (1:X2=1 /\ 1:X5=1) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected new file mode 100644 index 0000000000..c7e10c7fd1 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishWptev0pteoa-popteoal+dmb.ld.litmus.expected @@ -0,0 +1,14 @@ +Test MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld Allowed +States 5 +1:X2=0; 1:X5=0; +1:X2=0; 1:X5=1; +1:X2=0; 1:X5=2; +1:X2=1; 1:X5=0; +1:X2=1; 1:X5=2; +No +Witnesses +Positive: 0 Negative: 6 +Condition exists (1:X2=1 /\ 1:X5=1) +Observation MP+tlbi-sync.ishWptev0pteoa-pteoal+dmb.ld Never 0 6 +Hash=7d38f0901d8d6b17719acf4e80afbd92 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus new file mode 100644 index 0000000000..8b6ccea373 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus @@ -0,0 +1,18 @@ +AArch64 MP+tlbi-sync.ishpteoadb0p+dmb.ld +Variant=vmsa +{ + [x]=1; [y]=2; + [PTE(x)]=(oa:PA(x),db:0); + 0:X1=(oa:PA(y),db:0); 0:X0=PTE(x); + 0:X3=z; 0:X4=x; + 1:X3=z; 1:X4=x; +} + P0 | P1 ; + STR X1,[X0] | LDR W2,[X3] ; + DSB ISH | DMB LD ; + LSR X9,X4,#12 | LDR W5,[X4] ; + TLBI VAAE1IS,X9 | ; + DSB ISH | ; + MOV W2,#1 | ; + STR W2,[X3] | ; +exists (1:X2=1 /\ 1:X5=1) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected new file mode 100644 index 0000000000..b90c646963 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoadb0p+dmb.ld.litmus.expected @@ -0,0 +1,12 @@ +Test MP+tlbi-sync.ishpteoadb0p+dmb.ld Allowed +States 3 +1:X2=0; 1:X5=1; +1:X2=0; 1:X5=2; +1:X2=1; 1:X5=2; +No +Witnesses +Positive: 0 Negative: 4 +Condition exists (1:X2=1 /\ 1:X5=1) +Observation MP+tlbi-sync.ishpteoadb0p+dmb.ld Never 0 4 +Hash=6f66d48a711d25dc7a97d5151c6a07d1 + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus new file mode 100644 index 0000000000..96b760a3d7 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus @@ -0,0 +1,18 @@ +AArch64 MP+tlbi-sync.ishpteoap+dmb.ld +Variant=vmsa +{ + [x]=1; [y]=2; + [PTE(x)]=(oa:PA(x)); + 0:X1=(oa:PA(y),valid:1); 0:X0=PTE(x); + 0:X3=z; 0:X4=x; + 1:X3=z; 1:X4=x; +} + P0 | P1 ; + STR X1,[X0] | LDR W2,[X3] ; + DSB ISH | DMB LD ; + LSR X9,X4,#12 | LDR W5,[X4] ; + TLBI VAAE1IS,X9 | ; + DSB ISH | ; + MOV W2,#1 | ; + STR W2,[X3] | ; +exists (1:X2=1 /\ 1:X5=1) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected new file mode 100644 index 0000000000..f9d4f7caad --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishpteoap+dmb.ld.litmus.expected @@ -0,0 +1,13 @@ +Test MP+tlbi-sync.ishpteoap+dmb.ld Allowed +States 3 +1:X2=0; 1:X5=1; +1:X2=0; 1:X5=2; +1:X2=1; 1:X5=2; +No +Witnesses +Positive: 0 Negative: 4 +Flag Warning-BBM-expected +Condition exists (1:X2=1 /\ 1:X5=1) +Observation MP+tlbi-sync.ishpteoap+dmb.ld Never 0 4 +Hash=68710d542d637562dda4d817ef00baef + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus new file mode 100644 index 0000000000..c8f00110d8 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus @@ -0,0 +1,18 @@ +AArch64 MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos +Variant=vmsa +TTHM=P1:HA +{ + [x]=1; + [y]=2; + 0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); pteval_t 0:X2=0; 0:X3=(oa:PA(y)); 0:X4=x; + 1:X4=x; +} + P0 | P1 ; + STR X1,[X0] | L01: LDR W2,[X4] ; + DSB ISH | L00: LDR W5,[X4] ; + LSR X5,X4,#12 | ; + TLBI VAAE1IS,X5 | ; + DSB ISH | ; + CAS X1,X3,[X0] | ; + +exists (1:X2=2 /\ 1:X5=1) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected new file mode 100644 index 0000000000..8da2206f2c --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishsRpteaf0pte-amo.casptepteoa.af1+pos.litmus.expected @@ -0,0 +1,12 @@ +Test MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos Allowed +States 3 +1:X2=1; 1:X5=1; +1:X2=1; 1:X5=2; +1:X2=2; 1:X5=2; +No +Witnesses +Positive: 0 Negative: 70 +Condition exists (1:X2=2 /\ 1:X5=1) +Observation MP+tlbi-sync.ishsRpteaf0pte-posptepteoa.af1+pos Never 0 70 +Hash=2d93e28584c394c2b67face920ecd28c + diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus new file mode 100644 index 0000000000..d1acce7f11 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus @@ -0,0 +1,17 @@ +AArch64 MP+tlbi-sync.ishspteaf0pteoa.af1+pos +Variant=vmsa +{ + [x]=1; + [y]=2; + 0:X0=PTE(x); 0:X1=(oa:PA(x), af:0); 0:X2=(oa:PA(y)); 0:X3=x; + 1:X3=x; +} + P0 | P1 ; + STR X1,[X0] | L01: LDR W4,[X3] ; + DSB ISH | L00: LDR W5,[X3] ; + LSR X4,X3,#12 | ; + TLBI VAAE1IS,X4 | ; + DSB ISH | ; + STR X2,[X0] | ; + +exists (1:X4=2 /\ 1:X5=1) diff --git a/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected new file mode 100644 index 0000000000..4190f20ca8 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/MP+tlbi-sync.ishspteaf0pteoa.af1+pos.litmus.expected @@ -0,0 +1,15 @@ +Test MP+tlbi-sync.ishspteaf0pteoa.af1+pos Allowed +States 6 +1:X4=0; 1:X5=0; +1:X4=1; 1:X5=0; +1:X4=1; 1:X5=1; +1:X4=1; 1:X5=2; +1:X4=2; 1:X5=0; +1:X4=2; 1:X5=2; +No +Witnesses +Positive: 0 Negative: 9 +Condition exists (1:X4=2 /\ 1:X5=1) +Observation MP+tlbi-sync.ishspteaf0pteoa.af1+pos Never 0 9 +Hash=e6ef300b6f55d2300ac976c99b0e5c3e + diff --git a/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus new file mode 100644 index 0000000000..02f4180681 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus @@ -0,0 +1,14 @@ +AArch64 RW+RR+rel+acq+PteOA +Variant=vmsa +{ + [x]=1; [y]=2; + [PTE(x)]=(oa:PA(x)); + 0:X0=x; 1:X0=x; + 0:X3=z; 1:X3=z; + 2:X4=(oa:PA(y)); 2:X5=PTE(x); +} + P0 | P1 | P2 ; + LDR W1,[X0] | LDAR W2,[X3] | STR X4,[X5] ; + MOV W2,#1 | LDR W1,[X0] | ; + STLR W2,[X3] | | ; +exists(0:X1=2 /\ 1:X1=1) diff --git a/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected new file mode 100644 index 0000000000..3a8b35f8b1 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/RW+RR+rel+acq+PteOA.litmus.expected @@ -0,0 +1,14 @@ +Test RW+RR+rel+acq+PteOA Allowed +States 4 +0:X1=1; 1:X1=1; +0:X1=1; 1:X1=2; +0:X1=2; 1:X1=1; +0:X1=2; 1:X1=2; +Ok +Witnesses +Positive: 2 Negative: 6 +Flag Warning-BBM-expected +Condition exists (0:X1=2 /\ 1:X1=1) +Observation RW+RR+rel+acq+PteOA Sometimes 2 6 +Hash=2679c3daefc5c2fefdfa8b6eb6c93e54 + diff --git a/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus new file mode 100644 index 0000000000..4d03a56550 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus @@ -0,0 +1,13 @@ +AArch64 W+WW+PteOA +Variant=vmsa +{ + [PTE(x)]=(oa:PA(x)); + 0:X1=x; + 1:X4=(oa:PA(y)); 1:X5=PTE(x); +} + P0 | P1 ; + MOV W0,#1 | STR X4,[X5] ; + STR W0,[X1] | ; + MOV W2,#2 | ; + STR W2,[X1] | ; +exists([x]=0 /\ [y]=1) diff --git a/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected new file mode 100644 index 0000000000..189e8ef0f6 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/W+WW+PteOA.litmus.expected @@ -0,0 +1,14 @@ +Test W+WW+PteOA Allowed +States 4 +[x]=0; [y]=2; +[x]=1; [y]=2; +[x]=2; [y]=0; +[x]=2; [y]=1; +No +Witnesses +Positive: 0 Negative: 4 +Flag Warning-BBM-expected +Condition exists ([x]=0 /\ [y]=1) +Observation W+WW+PteOA Never 0 4 +Hash=91f83a50665f5fef5bb692282cd910f1 + diff --git a/catalogue/aarch64-BBM/tests/coRR+BBM.litmus b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus new file mode 100644 index 0000000000..b1ae195093 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus @@ -0,0 +1,18 @@ +AArch64 coRR+BBM +(* coRR-pte9 *) +Variant=vmsa +{ + [y]=1; + [PTE(x)]=(oa:PA(x)); + 0:X1=x; 1:X1=x; + 1:X4=(valid:0); 1:X5=PTE(x); + 1:X6=(oa:PA(y)); +} + P0 | P1 ; + L1: | STR X4,[X5] ; + LDR W0,[X1] | DSB ISH ; + L2: | LSR X9,X1,#12 ; + LDR W2,[X1] | TLBI VAAE1IS,X9 ; + | DSB ISH ; + | STR X6,[X5] ; +exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x))) diff --git a/catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected new file mode 100644 index 0000000000..ab0fa0a163 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRR+BBM.litmus.expected @@ -0,0 +1,14 @@ +Test coRR+BBM Allowed +States 5 +0:X0=0; 0:X2=0; ~Fault(P0:L2,x); +0:X0=0; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation); +0:X0=0; 0:X2=1; ~Fault(P0:L2,x); +0:X0=1; 0:X2=0; Fault(P0:L2,x,D-MMU:Translation); +0:X0=1; 0:X2=1; ~Fault(P0:L2,x); +No +Witnesses +Positive: 0 Negative: 9 +Condition exists (0:X0=1 /\ 0:X2=0 /\ not (fault(P0:L2,x))) +Observation coRR+BBM Never 0 9 +Hash=f6ece5ca033543aee1f3f75d5cea8844 + diff --git a/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus new file mode 100644 index 0000000000..0b21eb1fd6 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus @@ -0,0 +1,14 @@ +AArch64 coRR+dsb.ishs-[isb]+PteOA +Variant=vmsa +{ + [x]=1; [y]=2; + [PTE(x)]=(oa:PA(x)); + 0:X0=x; + 1:X2=(oa:PA(y)); 1:X1=PTE(x); +} + P0 | P1 ; + LDR W1,[X0] | STR X2,[X1] ; + DSB ISH | ; + ISB | ; + LDR W2,[X0] | ; +exists(0:X1=2 /\ 0:X2=1) diff --git a/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected new file mode 100644 index 0000000000..6f55907cb0 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRR+dsb.ishs-[isb]+PteOA.litmus.expected @@ -0,0 +1,14 @@ +Test coRR+dsb.ishs-[isb]+PteOA Allowed +States 4 +0:X1=1; 0:X2=1; +0:X1=1; 0:X2=2; +0:X1=2; 0:X2=1; +0:X1=2; 0:X2=2; +Ok +Witnesses +Positive: 1 Negative: 3 +Flag Warning-BBM-expected +Condition exists (0:X1=2 /\ 0:X2=1) +Observation coRR+dsb.ishs-[isb]+PteOA Sometimes 1 3 +Hash=be7e96ca19af00f9ecaab86436e5bdd9 + diff --git a/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus new file mode 100644 index 0000000000..01a81ccbf0 --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus @@ -0,0 +1,15 @@ +AArch64 coRW+Wpteoa-copy +Variant=vmsa +{ + [PTE(z)]=(oa:PA(x)); + 0:X1=z; + 1:X4=(oa:PA(y)); 1:X5=PTE(z); + 1:X7=x; + 1:X8=y; +} + P0 | P1 ; + LDR W0,[X1] | STR X4,[X5] ; + MOV W2,#1 | DSB SY ; + STR W2,[X1] | LDR W6,[X7] ; + | STR W6,[X8] ; +exists(0:X0=1) diff --git a/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected new file mode 100644 index 0000000000..10f19656af --- /dev/null +++ b/catalogue/aarch64-BBM/tests/coRW+Wpteoa-copy.litmus.expected @@ -0,0 +1,12 @@ +Test coRW+Wpteoa-copy Allowed +States 2 +0:X0=0; +0:X0=1; +Ok +Witnesses +Positive: 1 Negative: 10 +Flag Warning-BBM-expected +Condition exists (0:X0=1) +Observation coRW+Wpteoa-copy Sometimes 1 10 +Hash=9a8a5039bac4a5d305e3600d23eea57f + From 0534725007d5dcdeb5e7e1ab41c717bbea3652f3 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Tue, 23 Jun 2026 15:40:55 +0100 Subject: [PATCH 08/10] fixup! [herd] Fix writable2 function in machModelChecker --- herd/machModelChecker.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/herd/machModelChecker.ml b/herd/machModelChecker.ml index aad63454f2..df388dab8a 100644 --- a/herd/machModelChecker.ml +++ b/herd/machModelChecker.ml @@ -158,11 +158,10 @@ module Make let writable2 e1 e2 = let writable e = - let ha,hd = - let open DirtyBit in - match S.E.proc_of e, O.dirty with - | Some proc, Some d -> d.ha proc,d.hd proc - | _, _ -> false,false in + let open DirtyBit in + let ha, hd = match O.dirty with + | Some d -> d.some_ha, d.some_hd + | _ -> false, false in match S.E.value_of e with | Some (S.A.V.Val (Constant.PteVal p)) -> S.A.V.Cst.PteVal.writable ha hd p From a8b68d01afa84b5f7907fe91671d070773cf2466 Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Tue, 23 Jun 2026 15:42:02 +0100 Subject: [PATCH 09/10] fixup! [catalogue] Add a new catalogue for aarch64 illustrative of BBM --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index c1f00f905a..5366ba9c11 100644 --- a/Makefile +++ b/Makefile @@ -294,7 +294,7 @@ test.herd.cata-ext.%: $(REGRESSION_TEST_MODE) @ echo "herd7 catalogue $* instructions tests: OK" -cata-test-all:: test.herd.cata-ext.aarch64-bbm +cata-test-all:: test.herd.cata-ext.aarch64-BBM test.herd-mixed.cata.%: @ echo From 731921de230337e883765f8e5afea9c34166cd5f Mon Sep 17 00:00:00 2001 From: Nikos Nikoleris Date: Tue, 23 Jun 2026 16:16:12 +0100 Subject: [PATCH 10/10] fixup! [herd] Fix the definitions that flag tests that need BBM --- herd/libdir/aarch64bbm.cat | 2 +- herd/tests/instructions/AArch64.kvm/A032.litmus.expected | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/herd/libdir/aarch64bbm.cat b/herd/libdir/aarch64bbm.cat index 513cf3a0ba..1444ce45a4 100644 --- a/herd/libdir/aarch64bbm.cat +++ b/herd/libdir/aarch64bbm.cat @@ -79,4 +79,4 @@ let TLBCacheableTTD = TTD \ TLBUncacheableTTD let TTD-update-needsBBM = [TLBCacheableTTD]; (TTD-MT-update | TTD-SH-update | TTD-ICH-update | TTD-OCH-update | TTD-DT-update - | TTD-OA-update & TTD-at-least-one-writable); [domain([TLBCacheableTTD]; rf; [Imp & TTD & R])] + | TTD-OA-update & TTD-at-least-one-writable); [TLBCacheableTTD] diff --git a/herd/tests/instructions/AArch64.kvm/A032.litmus.expected b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected index d63c2a24e7..40ae9cf29f 100644 --- a/herd/tests/instructions/AArch64.kvm/A032.litmus.expected +++ b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected @@ -7,6 +7,7 @@ States 4 Ok Witnesses Positive: 1 Negative: 5 +Flag Warning-BBM-expected Condition exists (0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y))) Observation A032 Sometimes 1 5 Hash=4d4ebbbbd741d64b8bb4bcece91ef26d