(* * 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: * 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. *) (*** Device Memory ***) (* Device Memory Types *) let PTEDevice-GRE = try PTEDevice-GRE with emptyset let PTEDevice-nGRE = try PTEDevice-nGRE with emptyset let PTEDevice-nGnRE = try PTEDevice-nGnRE with emptyset let PTEDevice-nGnRnE = try PTEDevice-nGnRnE with emptyset (* A PTE can only have one of the above Device memory types *) let DeviceMemoryType-conflict = (PTEDevice-GRE & PTEDevice-nGRE) | (PTEDevice-GRE & PTEDevice-nGnRE) | (PTEDevice-GRE & PTEDevice-nGnRnE) | (PTEDevice-nGRE & PTEDevice-nGnRE) | (PTEDevice-nGRE & PTEDevice-nGnRnE) | (PTEDevice-nGnRE & PTEDevice-nGnRnE) assert empty DeviceMemoryType-conflict as Invalid-Device-Memory-Type let PTEDevice = try PTEDevice with emptyset let PTEDevice = PTEDevice | PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE (*** Normal Memory ***) let PTENon-shareable = try PTENon-shareable with emptyset let PTEInner-shareable = try PTEInner-shareable with emptyset let PTEOuter-shareable = try PTEOuter-shareable with emptyset (* Memory cannot have more than one Shareability Attribute *) let Shareability-conflict = (PTENon-shareable & PTEInner-shareable) | (PTEInner-shareable & PTEOuter-shareable) | (PTENon-shareable & PTEOuter-shareable) assert empty Shareability-conflict as Invalid-Shareability let PTEInner-write-back = try PTEInner-write-back with emptyset let PTEInner-write-through = try PTEInner-write-through with emptyset let PTEInner-non-cacheable = try PTEInner-non-cacheable with emptyset (* Memory cannot have more than one Inner Cacheability Attribute *) let InnerCacheability-conflict = (PTEInner-write-back & PTEInner-write-through) | (PTEInner-write-through & PTEInner-non-cacheable) | (PTEInner-non-cacheable & PTEInner-write-back) assert empty InnerCacheability-conflict as Invalid-Inner-Cacheability let PTEOuter-write-back = try PTEOuter-write-back with emptyset let PTEOuter-write-through = try PTEOuter-write-through with emptyset let PTEOuter-non-cacheable = try PTEOuter-non-cacheable with emptyset (* Memory cannot have more than one Outer Cacheability Attribute *) let OuterCacheability-conflict = (PTEOuter-write-back & PTEOuter-write-through) | (PTEOuter-write-through & PTEOuter-non-cacheable) | (PTEOuter-non-cacheable & PTEOuter-write-back) assert empty OuterCacheability-conflict as Invalid-Outer-Cacheability let PTENormal = try PTENormal with emptyset let PTETaggedNormal = try PTETaggedNormal with emptyset (*** Common attributes ***) let PTEXS = try PTEXS with emptyset (*** Sanity checks ***) (* Memory cannot be of type Normal and Device at the same time *) let MemoryType-conflict = PTENormal & PTEDevice assert empty MemoryType-conflict as Invalid-Memory-Type (* No other memory attribute is allowed *) let PTEMemAttr = try PTEMemAttr with emptyset let PTEAll-Valid-Mem-Attr = PTENormal | PTETaggedNormal | PTENon-shareable | PTEInner-shareable | PTEOuter-shareable | PTEInner-write-back | PTEInner-write-through | PTEInner-non-cacheable | PTEOuter-write-back | PTEOuter-write-through | PTEOuter-non-cacheable | PTEDevice | PTEDevice-GRE | PTEDevice-nGRE | PTEDevice-nGnRE | PTEDevice-nGnRnE | PTEXS let Invalid-Memory-Attr = PTEMemAttr \ (PTEAll-Valid-Mem-Attr) assert empty Invalid-Memory-Attr as Invalid-Memory-Attribute (* Default Shareability *) let PTEInner-shareable = PTEInner-shareable | (PTE \ (PTEDevice | PTENon-shareable | PTEOuter-shareable)) (* Default Inner Cacheability *) let PTEInner-write-back = PTEInner-write-back | (PTE \ (PTEDevice | PTEInner-write-through | PTEInner-non-cacheable)) (* Default Outer Cacheability *) let PTEOuter-write-back = PTEOuter-write-back | (PTE \ (PTEDevice | PTEOuter-write-through | PTEOuter-non-cacheable)) let ISH-WB = PTEInner-shareable & PTEInner-write-back & PTEOuter-write-back (* Default Memory Type *) let PTETaggedNormal = PTETaggedNormal | (if "memtag" then ISH-WB else 0) let PTENormal = PTENormal | PTENon-shareable | PTEInner-shareable | PTEOuter-shareable | PTEInner-write-back | PTEInner-write-through | PTEInner-non-cacheable | PTEOuter-write-back | PTEOuter-write-through | PTEOuter-non-cacheable let PTENormal = if "memtag" then PTENormal \ ISH-WB else PTENormal