(* * 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, referring to version number: * 814a6fc1610ec1a24f2cbd178e171966375626ac * For a textual version of the model, see section B2.3 of the Armv8 ARM: * https://developer.arm.com/documentation/ddi0487/ha/ * Author: Will Deacon * Author: Jade Alglave * * Copyright (C) 2016-2022, 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. *) AArch64 "ARMv8 AArch64" catdep (* This option tells that the cat file computes dependencies *) (* * Include the cos.cat file shipped with herd. * This builds the co relation as a total order over writes to the same * location and then consequently defines the fr relation using co and * rf. *) include "cos.cat" (* * Include aarch64fences.cat to define barriers. *) include "aarch64fences.cat" (* * Include aarch64deps.cat to define dependencies. *) include "aarch64deps.cat" (* Show relations in generated diagrams *) include "aarch64show.cat" (* * As a restriction of the model, all observers are limited to the same * inner-shareable domain. Consequently, the ISH, OSH and SY barrier * options are all equivalent to each other. *) let dsb.full = DSB.ISH | DSB.OSH | DSB.SY let dsb.ld = DSB.ISHLD | DSB.OSHLD | DSB.LD let dsb.st = DSB.ISHST | DSB.OSHST | DSB.ST (* * A further restriction is that standard litmus tests are unable to * distinguish between DMB and DSB instructions, so the model treats * them as equivalent to each other. *) let dmb.full = DMB.ISH | DMB.OSH | DMB.SY | dsb.full let dmb.ld = DMB.ISHLD | DMB.OSHLD | DMB.LD | dsb.ld let dmb.st = DMB.ISHST | DMB.OSHST | DMB.ST | dsb.st (* Flag any use of shareability options, due to the restrictions above. *) flag ~empty (dmb.full | dmb.ld | dmb.st) \ (DMB.SY | DMB.LD | DMB.ST | DSB.SY | DSB.LD | DSB.ST) as Assuming-common-inner-shareable-domain (* Coherence-after *) let ca = fr | co (* Local read successor *) let lrs = [W]; (po-loc \ (po-loc;[W];po-loc)) ; [R] (* Local write successor *) let lws = po-loc; [W] (* Observed-by *) let obs = rfe | fre | coe (* Read-modify-write *) let rmw = lxsx | amo (* Dependency-ordered-before *) let dob = addr | data | ctrl; [W] | (ctrl | (addr; po)); [ISB]; po; [M] | addr; po; [W] | (addr | data); lrs show ctrl;[M] as ctrl (* Pick-ordered-before *) let pob = pick-dep; [W] | (pick-ctrl-dep | pick-addr-dep; po); [ISB]; po; [M] | pick-addr-dep; [M]; po; [W] (* Atomic-ordered-before *) let aob = rmw | rmw; lrs; [A | Q] (* Barrier-ordered-before *) let bob = po; [dmb.full]; po | [range([A];amo;[L])]; po | [L]; po; [A] | [R\NoRet]; po; [dmb.ld]; po | [A | Q]; po | [W]; po; [dmb.st]; po; [W] | po; [L] (* Tag-ordered-before *) let tob = [R & T]; iico_data; [PRED]; iico_ctrl; [W \ T] (* Locally-ordered-before *) let rec lob = lws; si | dob | pob | aob | bob | tob | lob; lob let pick-lob = pick-basic-dep; lob; [W] (* Ordered-before *) let rec ob = obs; si | lob | pick-lob | ob; ob (* Tag-location-ordered *) let tlo = [R & T]; tob; loc; tob^-1; [R & T] (* Internal visibility requirement *) let po-loc = let Exp = M\domain(tob) in (po-loc & Exp*Exp) | (po & tlo) acyclic po-loc | rmw & same-instance | ca | rf as internal (* External visibility requirement *) irreflexive ob as external (* Atomic: Basic LDXR/STXR constraint to forbid intervening writes. *) empty rmw & (fre; coe) as atomic