(* * 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 * Jade Alglave * Nikos Nikoleris * Artem Khyzha * * 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 aarch64deps.cat to define dependencies. *) include "aarch64deps.cat" (* Tag-Check-intrinsically-before *) let tc-ib = if "MTE" then [Imp & Tag & R]; iico_data; [B]; iico_ctrl; [((Exp & W) \ Tag) | TagCheck & FAULT] else 0 (* Fetch-intrinsically-before *) let f-ib = [Imp & Instr & R]; iico_data; [B]; iico_ctrl; [_] (* HW TTD Updates permitted only for the AF or DB *) let HU = Imp & TTD & W assert empty HU \ (AF | DB) (* DSB-ordered-before *) let DSB-ob = [M | DC.CVAU | IC]; po; [dsb.full]; po; [~(Imp & M)] | (if "ETS2" then [M | DC.CVAU | IC]; po; [dsb.full]; po; [Imp & TTD & M] else 0) | [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [~(Imp & M)] | (if "ETS2" then [(Exp & R) \ NoRet]; po; [dsb.ld]; po; [Imp & TTD & M] else 0) | [Exp & W]; po; [dsb.st]; po; [~(Imp & M)] | (if "ETS2" then [Exp & W]; po; [dsb.st]; po; [Imp & TTD & M] else 0) (* CSE-ordered-before *) let EXC-ENTRY-CSE = EXC-ENTRY let EXC-RET-CSE = if not "ExS" || "EOS" then EXC-RET else {} let CSE = ISB | EXC-ENTRY-CSE | EXC-RET-CSE let CSE-ob = [Exp & R]; ctrl; [CSE]; po | DSB-ob; [CSE]; po | [Imp & TTD & R]; tr-ib; [CSE]; po | [Imp & Instr & R]; f-ib; [CSE]; po (* Dependency-ordered-before *) let dob = addr | data | ctrl; [W] | addr; [Exp]; po; [W] | addr; [Exp]; po; [CSE]; po; [R] | addr; [Exp]; lrs | data; [Exp]; lrs (* Pick-ordered-before *) let pob = [Exp]; pick-dep; [W] | [Exp]; pick-ctrl-dep; [CSE]; po; [M] | [Exp]; pick-addr-dep; [Exp]; po; [CSE]; po; [M] | [Exp]; pick-addr-dep; [Exp & M]; po; [W] (* Atomic-ordered-before *) let aob = rmw | rmw; lrs; [A | Q] (* Barrier-ordered-before *) let bob = po; [dmb.full]; po | [R \ NoRet]; po; [dmb.ld]; po | [W]; po; [dmb.st]; po; [W | MMU & FAULT] | [range([A];amo;[L])]; po | [L]; po; [A] | [A | Q]; po | [A | Q]; iico_order | po; [L] | iico_order; [L] (* Locally-ordered-before *) let rec lob = lws | lws; sca-class | dob | pob | aob | bob | lob; lob let pick-lob = pick-basic-dep; lob; [W] let TLBUncacheable = MMU & (Translation | AccessFlag) (* Locally-hardware-required-ordered-before *) let rec local-hw-reqs = tc-ib | tr-ib | f-ib | [Exp & M | Imp & Tag & R]; lob; [Exp & M | Imp & Tag & R | TagCheck & FAULT | MMU & FAULT] | [Exp & M | Imp & Tag & R]; pick-lob; [Exp & M | Imp & Tag & R | TagCheck & FAULT | MMU & FAULT] | (if "ETS2" then [Exp & M]; po; [TLBUncacheable & FAULT]; tr-ib^-1; [Imp & TTD & R] else 0) | DSB-ob | CSE-ob | [Imp & TTD & R]; (po & same-loc); [W] | [Imp & TTD & R]; rmw; [HU] | [Exp & M]; (po & same-loc); [TLBUncacheable & FAULT] | [Exp & R]; addr; [TLBI | DC.CVAU | IC] | [Exp & R]; ctrl; [HU] | [Exp & R]; addr; [HU] | [Exp & R]; addr; [Exp]; po; [HU] | [Exp & R]; addr; [Exp]; po; [CSE]; po | [Imp & Instr & R]; po; [~(Imp & Instr & R)] | [Exp & M]; po; [dmb.full]; po; [DC.CVAU] | [DC.CVAU]; po; [dmb.full]; po; [Exp & M] | [DC.CVAU]; po; [dmb.full]; po; [DC.CVAU] | [Exp & M]; (po & scl); [DC.CVAU] | [DC.CVAU]; (po & scl); [Exp & M] | [DC.CVAU]; (po & scl); [DC.CVAU] | local-hw-reqs; local-hw-reqs