(* * 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 "aarch64util.cat" (* Tag-Check-intrinsically-before *) let tc-ib = [Imp & Tag & R]; iico_data; [B]; iico_ctrl; [(Exp & W) \ Tag | TagCheck & FAULT] (* Translation-intrinsically-before *) let tr-ib = [Imp & TTD & R]; iico_data; [B]; iico_ctrl; [Exp & M | MMU & FAULT] (* Fetch-intrinsically-before *) let f-ib = [Imp & Instr & R]; iico_data; [B]; iico_ctrl; [_] (* Notions of Same Location - PA, VA, and including Fault Effects *) let TTD-same-oa = same-oa(TTD*TTD) let same-loc = loc | tr-ib^-1; TTD-same-oa; tr-ib let po-loc = po & same-loc let va-loc = (tr-ib; same-low-order-bits; tr-ib^-1) & loc let po-va-loc = po & va-loc (* Local read successor *) let lrs = [W]; (po-loc \ intervening-write(po-loc)) ; [R] (* Local write successor *) let lws = [M]; po-loc; [W | MMU & FAULT] (* 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; [CSE]; po; [R] | addr; [Exp]; po; [W] | (addr | 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 | iico_order) | (po | iico_order); [L] (* Locally-ordered-before *) let rec lob = 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 | pick-lob); [Exp & M | Imp & Tag & R | (TagCheck | 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-loc; [W] | [Imp & TTD & R]; rmw; [HU] | [Exp & M]; po-loc; [TLBUncacheable & FAULT] | [Exp & R]; addr; [TLBI | DC.CVAU | IC] | [Exp & R]; ctrl; [HU] | [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