(* * 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: * 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 "aarch64fences.cat" let Imp = NExp let C_TLBI = TLBI & domain(po; [dsb.full]) let C_IC = IC & domain(po; [dsb.full]) let add_pair p = map (fun r -> (p | r)) let rec add_both_choices (rs,wts) = match wts with || {} -> rs || wt ++ wts -> let wt = wt ++ 0 in (* Change pair into relation *) let tw = wt^-1 in (* Notice, ^-1 could operate on pairs directly *) let r1 = add_pair wt rs and r2 = add_pair tw rs in let rs = r1|r2 in add_both_choices (rs,wts) end (* takes a relation "unordered-pairs" of the form [X]; r; [Y] where "X" and "Y" are disjoint and "r" is meant to be symmetric and a relation "rel", and returns a set of acyclic relations consistent with "rel" and ordering the unordered pairs one way or the other. *) let enumerate-ordered-pairs (unordered-pairs,rel) = let no-choice = rel & (unordered-pairs | unordered-pairs^-1) in let need-choosing = unordered-pairs \ (no-choice | no-choice^-1) in add_both_choices ({no-choice},need-choosing) let TLBI-Imp_TTD_R-pairs = inv-scope & ((C_TLBI * (Imp & TTD & R)) \ (TLBInXS * PTEXS) \ ((~TLBIIS) * (Imp & TTD & R)) & ext) let all-TLBI-Imp_TTD_R-enums rel = enumerate-ordered-pairs ( TLBI-Imp_TTD_R-pairs, rel ) let all-DC-Exp_W-enums rel = enumerate-ordered-pairs ( scl & (DC.CVAU * (Exp & W)), rel | (IW * (_\IW)) ) let all-IC-Imp_Instr_R-enums rel = enumerate-ordered-pairs ( scl & (C_IC * (Imp & Instr & R)), rel )