(* * 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 * * 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 = [PTENormal]; ca; [PTEDevice] | [PTEDevice]; ca; [PTENormal] let PTE-SH-update = [PTENon-shareable]; ca; [PTEInner-shareable | PTEOuter-shareable] | [PTEInner-shareable]; ca; [PTEOuter-shareable | PTENon-shareable] | [PTEOuter-shareable]; ca; [PTENon-shareable | PTEInner-shareable] let PTE-ICH-update = [PTEInner-non-cacheable]; ca; [PTEInner-write-through | PTEInner-write-back] | [PTEInner-write-through]; ca; [PTEInner-write-back | PTEInner-non-cacheable] | [PTEInner-write-back]; ca; [PTEInner-non-cacheable | PTEInner-write-through] let PTE-OCH-update = [PTEOuter-non-cacheable]; ca; [PTEOuter-write-through | PTEOuter-write-back] | [PTEOuter-write-through]; ca; [PTEOuter-write-back | PTEOuter-non-cacheable] | [PTEOuter-write-back]; ca; [PTEOuter-non-cacheable | PTEOuter-write-through] let PTE-DT-update = [PTEDevice-GRE]; ca; [PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE] | [PTEDevice-nGRE]; ca; [PTEDevice-GRE | PTEDevice-nGnRE | PTEDevice-nGnRnE] | [PTEDevice-nGnRE]; ca; [PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRnE] | [PTEDevice-nGnRnE]; ca; [PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-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