[AARCH-24800,herd] Ordering semantics for Load instructions whose destination register is WZR/XZR

catalogue/aarch64-oban/aarch-24800/libdir/aarch64.cat

@@ -0,0 +1,191 @@
+(*
+ * The Armv8 Application Level Memory Model.
+ *
+ * This is a machine-readable, executable and formal artefact, which aims to be
+ * the latest stable version of the Armv8 memory model.
+ * If you have comments on the content of this file, please send an email to
+ * memory-model@arm.com
+ * For a textual version of the model, see section B2.3 of the Armv8 ARM:
+ * https://developer.arm.com/documentation/ddi0487/
+ *
+ * Authors:
+ * Will Deacon <will.deacon@arm.com>
+ * Jade Alglave <jade.alglave@arm.com>
+ * Nikos Nikoleris <nikos.nikoleris@arm.com>
+ * Artem Khyzha <artem.khyzha@arm.com>
+ *
+ * Copyright (C) 2016-present, Arm Ltd.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in
+ *       the documentation and/or other materials provided with the
+ *       distribution.
+ *     * Neither the name of ARM nor the names of its contributors may be
+ *       used to endorse or promote products derived from this software
+ *       without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+ * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+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)
+with DC-after from (all-DC-Exp_W-enums local-hw-reqs)
+with IC-after from (all-IC-Imp_Instr_R-enums local-hw-reqs)
+
+(*** Hazard-ordered-before ***)
+
+(** Explicitly-hazard-ordered-before **)
+let Exp-haz-ob =
+  [Exp & R]; (po & same-loc); [Exp & R]; sca-class?; [Exp & R]; (ca & ext); [Exp & W]; sca-class?; [Exp & W]
+
+(** TLBI-ordered-before **)
+
+(* TTD-read-ordered-before *)
+let TTD-read-ordered-before =
+  TLBI-after; [TLBI]; po; [dsb.full]; po; [~(Imp & M)]
+  | TLBI-after; [TLBI]; po; [dsb.full]; po; [IFB]; po; [Imp & M]
+  | (if "ETS2" || "ETS3" then TLBI-after; [TLBI]; po; [dsb.full]; po; [Imp & TTD & M] else 0)
+
+(* TLBI-ordered-before *)
+let TLBI-ob =
+     TTD-read-ordered-before
+   | tr-ib^-1; TTD-read-ordered-before & ext
+   | po-va-loc; TTD-read-ordered-before & ext
+
+(** IC-ordered-before **)
+
+(* Instr-read-ordered-before *)
+let Instr-read-ordered-before =
+  IC-after; [IC]; po; [dsb.full]; po; [~(Imp & M)]
+  | (if "DIC" then ca else 0)
+
+(* IC-ordered-before *)
+let IC-ob = [Imp & Instr & R]; po; [Imp & Instr & R]; Instr-read-ordered-before
+
+(* Hazard-ordered-before *)
+let haz-ob =
+  Exp-haz-ob | TLBI-ob | IC-ob
+
+(*** Hardware-required-ordered-before ***)
+let hw-reqs = local-hw-reqs | haz-ob
+
+(*** Observed-by ***)
+
+(** Explicitly-observed-by **)
+let Exp-obs = 
+  [Exp & M]; rf & ext; [Exp & M]
+  | [Exp & M]; ca & ext; [Exp & M]
+
+(** Tag-observed-by **)
+let Tag-obs =
+   [Exp & W]; rf & ext; [Imp & Tag & R]
+   | [Imp & Tag & R]; ca & ext; [Exp & W]
+
+(** TTD-observed-by **)
+
+(* TLBUncacheable-coherence-after *)
+let TLBuncacheable-ca =
+  [range([TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R])]; ca; [Exp & W | HU]
+
+(* Hardware-update-coherence-after *)
+let HU-ca =
+  [Exp & R]; ca; [HU]
+
+(* TLBI-coherence-after *)
+let TLBI-ca =
+   [TLBI]; TLBI-after; [Imp & TTD & R]; ca; [W]
+
+(* TTD-observed-by *)
+let TTD-obs =
+    [Imp & TTD]; rf | rf; [Imp & TTD]
+    | TLBuncacheable-ca
+    | HU-ca
+    | [HU]; ca; [W] | [W]; ca; [HU]
+    | TLBI-ca
+
+(** Instr-observed-by **)
+
+(* IC-coherence-after *)
+let IC-ca =
+    (if not "DIC" && not "IDC" then [IC]; IC-after; [Imp & Instr & R]; ca; [W]; DC-after; [DC.CVAU] else 0)
+    | (if not "DIC" && "IDC" then [IC]; IC-after; [Imp & Instr & R]; ca; [W] else 0)
+    | (if "DIC" && "IDC" then [Imp & Instr & R]; ca; [W] else 0)
+
+(* Instr-observed-by *)
+let Instr-obs =
+    rf; [Imp & Instr & R]
+    | IC-after
+    | [DC.CVAU]; DC-after; [W] | [W]; DC-after; [DC.CVAU]
+    | IC-ca
+
+(** Observed-by **)
+let obs =
+    Exp-obs; sca-class?
+    | Tag-obs; sca-class?
+    | TTD-obs
+    | Instr-obs
+
+(*** Ordered-before ***)
+let rec ob =
+    hw-reqs
+    | obs
+    | ob; ob
+
+(*** External visibility requirement ***)
+irreflexive ob as external
+
+(*** Internal visibility requirements ***)
+irreflexive [Exp & R]; ((po & same-loc) | rmw); [Exp & W]; rfi; [Exp & R] as coRW1-Exp
+irreflexive [Imp & Tag & R]; (po & same-loc); [Exp & Tag & W]; rfi; [Imp & Tag & R] as coRW1-MTE
+irreflexive [Exp & W]; (po & same-loc); [Exp & W]; (ca & int); [Exp & W] as coWW-Exp
+irreflexive [Exp & W]; (po & same-loc); [Exp & R]; (ca & int); [Exp & W] as coWR-Exp
+irreflexive [Exp & Tag & W]; (po & same-loc); [Imp & Tag & R]; (ca & int) as coWR-MTE
+
+(*** Atomic: LDXR/STXR, AMO and HU constraint to forbid intervening writes. ***)
+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
+
+(*** Additional synchronisation requirements for CMODX ***)
+let CMODX-conflicts = same-loc & (
+  (Imp & Instr & R & Within-CMODX-List) * W
+  | (Imp & Instr & R) * (Within-CMODX-List & W)
+  | W * (Within-CMODX-List & Imp & Instr & R)
+  | (Within-CMODX-List & W) * (Imp & Instr & R)
+  )
+
+let CMODX-ordering =
+  [Imp & Instr & R]; ob; [W]
+  | [W]; ob; [Imp & Instr & R]
+
+let CMODX-unordered-conflicts =
+  CMODX-conflicts \ (CMODX-ordering | CMODX-ordering^-1)
+
+flag ~empty CMODX-unordered-conflicts as violates-CMODX-requirements

catalogue/aarch64-oban/aarch-24800/libdir/aarch64bbm.cat

@@ -0,0 +1,88 @@
+(*
+ * The Armv8 Application Level Memory Model.
+ *
+ * This is a machine-readable, executable and formal artefact, which aims to be
+ * the latest stable version of the Armv8 memory model.
+ * If you have comments on the content of this file, please send an email to
+ * jade.alglave@arm.com
+ * For a textual version of the model, see section B2.3 of the Armv8 ARM:
+ * https://developer.arm.com/documentation/ddi0487/
+ *
+ * Authors:
+ * Nikos Nikoleris <nikos.nikoleris@arm.com>
+ *
+ * Copyright (C) 2016-present, Arm Ltd.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in
+ *       the documentation and/or other materials provided with the
+ *       distribution.
+ *     * Neither the name of ARM nor the names of its contributors may be
+ *       used to endorse or promote products derived from this software
+ *       without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+ * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *)
+
+(*
+ * Include aarch64memattrs.cat to define relations on Memory Attributes.
+ *)
+include "aarch64memattrs.cat"
+
+(* Can we move this to stdlib? *)
+(* Coherence-after *)
+let ca = fr | co
+
+let PTE-MT-update =
+  [Normal]; ca; [Device]
+  | [Device]; ca; [Normal]
+
+let PTE-SH-update =
+  [NSH]; ca; [ISH | OSH]
+  | [ISH]; ca; [OSH | NSH]
+  | [OSH]; ca; [NSH | ISH]
+
+let PTE-ICH-update =
+  [iNC]; ca; [iWT | iWB]
+  | [iWT]; ca; [iWB | iNC]
+  | [iWB]; ca; [iNC | iWT]
+
+let PTE-OCH-update =
+  [oNC]; ca; [oWT | oWB]
+  | [oWT]; ca; [oWB | oNC]
+  | [oWB]; ca; [oNC | oWT]
+
+let PTE-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 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 TTDV = PTEV
+let TTDINV = PTEINV
+let TTD-update-needsBBM = PTE-update-needsBBM

catalogue/aarch64-oban/aarch-24800/libdir/aarch64deps.cat

@@ -0,0 +1,101 @@
+(*
+ * The Armv8 Application Level Memory Model.
+ *
+ * This is a machine-readable, executable and formal artefact, which aims to be
+ * the latest stable version of the Armv8 memory model.
+ * If you have comments on the content of this file, please send an email to
+ * memory-model@arm.com
+ * For a textual version of the model, see section B2.3 of the Armv8 ARM:
+ *   https://developer.arm.com/docs/ddi0487/
+ *
+ * Authors:
+ * Jade Alglave <jade.alglave@arm.com>
+ * Artem Khyzha <artem.khyzha@arm.com>
+ *
+ * Copyright (C) 2016-present, Arm Ltd.
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *     * Redistributions in binary form must reproduce the above copyright
+ *       notice, this list of conditions and the following disclaimer in
+ *       the documentation and/or other materials provided with the
+ *       distribution.
+ *     * Neither the name of ARM nor the names of its contributors may be
+ *       used to endorse or promote products derived from this software
+ *       without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
+ * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
+ * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
+ * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED
+ * TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+ * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+ * LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+ * NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+ * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ *)
+catdep (* This option tells that the cat file computes dependencies *)
+
+include "aarch64util.cat"
+
+(* Local register read successor *)
+let lrrs =
+  [Wreg]; (po & same-gpr & ~(intervening(Wreg,(po & same-gpr)))); [Rreg]
+
+(* Local memory write successor *)
+let lmws =
+ [Exp & M | Imp & Tag & R]; (po & same-loc); [Exp & W]
+ | [Imp & TTD & R]; (po & same-loc); [Exp & W | HU]
+
+(* Local MMU Fault successor *)
+let lfs =
+ [Exp & M]; (po & same-loc); [MMU & FAULT]
+
+(* Local memory read successor *)
+let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
+
+(* Dependency through registers and memory *)
+let rec dtrm =
+  [~range(lxsx)]; lrrs
+  | lmrs
+  | iico_data
+  | dtrm; dtrm
+
+(** Data, Address and Control dependencies *)
+
+let data = [Exp & R]; dtrm & po; [Rreg]; iico_data & ii_data; [Exp & W]
+let addr = [Exp & R]; dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]
+let ctrl = [Exp & R]; dtrm & po; [Rreg]; iico_data; [BCC]; po
+
+(** Pick dependencies *)
+let rec pick-dtrm =
+  dtrm
+  | iico_ctrl
+  | pick-dtrm; pick-dtrm
+
+let pick-basic-dep =
+   [Exp & R | Rreg];  pick-dtrm?
+
+let pick-addr-dep =
+   [Exp & R]; pick-dtrm & po; [Rreg]; iico_data & ii_addr; [Exp & M | Imp & Tag & R | Imp & TTD & R | HU | TLBI | DC.CVAU | IC.IVAU]
+let pick-data-dep =
+   [Exp & R]; pick-dtrm & po; [Rreg]; (iico_data | (iico_data; iico_ctrl)) & ii_data; [Exp & W]
+let pick-ctrl-dep =
+   [Exp & R]; pick-dtrm & po; [Rreg]; iico_data; [BCC]; po
+
+let pick-dep =
+   ( pick-basic-dep
+   | pick-addr-dep
+   | pick-data-dep
+   | pick-ctrl-dep
+   ) & ~same-instance
+
+include "aarch64show.cat"
+