(* * 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/docs/ddi0487/ * * Authors: * Jade Alglave * 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. *) catdep (* This option tells that the cat file computes dependencies *) include "aarch64util.cat" (* Local write successor *) let lws = [M]; (po & same-loc); [W | MMU & FAULT] (* Local read successor *) let lrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R] (* Dependency through registers and memory *) let rec dtrm = [~range(lxsx)]; rf-reg | lrs | iico_data | dtrm; dtrm (** Data, Address and Control dependencies *) let ADDR = Rreg \ DATA let basic-dep = [Exp & R | Rreg]; dtrm? let data = (basic-dep; [DATA]; iico_data+; [W]) \ same-instance let addr = [Exp & M]; (basic-dep; [ADDR]; iico_data+; [M | TLBI | IC.IVAU | DC.CVAU]) \ same-instance let ctrl = (basic-dep; [BCC]; po) \ same-instance (** Pick dependencies *) let pick-dtrm = (dtrm|iico_ctrl)+ let pick-basic-dep = [Exp & R | Rreg]; pick-dtrm? let pick-addr-dep = pick-basic-dep; [ADDR]; iico_data+; [M] let pick-data-dep = pick-basic-dep; [DATA]; iico_data+; [W] let pick-addr-dep = pick-basic-dep; [ADDR]; iico_data+; [M] let pick-ctrl-dep = pick-basic-dep; [BCC]; po let pick-dep = ( pick-basic-dep | pick-addr-dep | pick-data-dep | pick-ctrl-dep ) \ same-instance include "aarch64show.cat"