(* * 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 = [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