(*========================================================================*) (* Sail *) (* *) (* Copyright (c) 2013-2017 *) (* Kathyrn Gray *) (* Shaked Flur *) (* Stephen Kell *) (* Gabriel Kerneis *) (* Robert Norton-Wright *) (* Christopher Pulte *) (* Peter Sewell *) (* Alasdair Armstrong *) (* Brian Campbell *) (* Thomas Bauereiss *) (* Anthony Fox *) (* Jon French *) (* Dominic Mulligan *) (* Stephen Kell *) (* Mark Wassell *) (* *) (* All rights reserved. *) (* *) (* This software was developed by the University of Cambridge Computer *) (* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) (* (REMS) project, funded by EPSRC grant EP/K008528/1. *) (* *) (* Redistribution and use in source and binary forms, with or without *) (* modification, are permitted provided that the following conditions *) (* are met: *) (* 1. Redistributions of source code must retain the above copyright *) (* notice, this list of conditions and the following disclaimer. *) (* 2. 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. *) (* *) (* THIS SOFTWARE IS PROVIDED BY THE AUTHOR 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 AUTHOR 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. *) (*========================================================================*) open import Pervasives_extra (* Data structures for building up instructions *) (* careful: changes in the read/write/barrier kinds have to be reflected in deep_shallow_convert *) type read_kind = (* common reads *) | Read_plain (* Power reads *) | Read_reserve (* AArch64 reads *) | Read_acquire | Read_exclusive | Read_exclusive_acquire | Read_stream (* RISC-V reads *) | Read_RISCV_acquire | Read_RISCV_strong_acquire | Read_RISCV_reserved | Read_RISCV_reserved_acquire | Read_RISCV_reserved_strong_acquire (* x86 reads *) | Read_X86_locked (* the read part of a lock'd instruction (rmw) *) instance (Show read_kind) let show = function | Read_plain -> "Read_plain" | Read_reserve -> "Read_reserve" | Read_acquire -> "Read_acquire" | Read_exclusive -> "Read_exclusive" | Read_exclusive_acquire -> "Read_exclusive_acquire" | Read_stream -> "Read_stream" | Read_RISCV_acquire -> "Read_RISCV_acquire" | Read_RISCV_strong_acquire -> "Read_RISCV_strong_acquire" | Read_RISCV_reserved -> "Read_RISCV_reserved" | Read_RISCV_reserved_acquire -> "Read_RISCV_reserved_acquire" | Read_RISCV_reserved_strong_acquire -> "Read_RISCV_reserved_strong_acquire" | Read_X86_locked -> "Read_X86_locked" end end type write_kind = (* common writes *) | Write_plain (* Power writes *) | Write_conditional (* AArch64 writes *) | Write_release | Write_exclusive | Write_exclusive_release (* RISC-V *) | Write_RISCV_release | Write_RISCV_strong_release | Write_RISCV_conditional | Write_RISCV_conditional_release | Write_RISCV_conditional_strong_release (* x86 writes *) | Write_X86_locked (* the write part of a lock'd instruction (rmw) *) instance (Show write_kind) let show = function | Write_plain -> "Write_plain" | Write_conditional -> "Write_conditional" | Write_release -> "Write_release" | Write_exclusive -> "Write_exclusive" | Write_exclusive_release -> "Write_exclusive_release" | Write_RISCV_release -> "Write_RISCV_release" | Write_RISCV_strong_release -> "Write_RISCV_strong_release" | Write_RISCV_conditional -> "Write_RISCV_conditional" | Write_RISCV_conditional_release -> "Write_RISCV_conditional_release" | Write_RISCV_conditional_strong_release -> "Write_RISCV_conditional_strong_release" | Write_X86_locked -> "Write_X86_locked" end end type barrier_kind = (* Power barriers *) Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync (* AArch64 barriers *) | Barrier_DMB | Barrier_DMB_ST | Barrier_DMB_LD | Barrier_DSB | Barrier_DSB_ST | Barrier_DSB_LD | Barrier_ISB | Barrier_TM_COMMIT (* MIPS barriers *) | Barrier_MIPS_SYNC (* RISC-V barriers *) | Barrier_RISCV_rw_rw | Barrier_RISCV_r_rw | Barrier_RISCV_r_r | Barrier_RISCV_rw_w | Barrier_RISCV_w_w | Barrier_RISCV_i (* X86 *) | Barrier_x86_MFENCE instance (Show barrier_kind) let show = function | Barrier_Sync -> "Barrier_Sync" | Barrier_LwSync -> "Barrier_LwSync" | Barrier_Eieio -> "Barrier_Eieio" | Barrier_Isync -> "Barrier_Isync" | Barrier_DMB -> "Barrier_DMB" | Barrier_DMB_ST -> "Barrier_DMB_ST" | Barrier_DMB_LD -> "Barrier_DMB_LD" | Barrier_DSB -> "Barrier_DSB" | Barrier_DSB_ST -> "Barrier_DSB_ST" | Barrier_DSB_LD -> "Barrier_DSB_LD" | Barrier_ISB -> "Barrier_ISB" | Barrier_TM_COMMIT -> "Barrier_TM_COMMIT" | Barrier_MIPS_SYNC -> "Barrier_MIPS_SYNC" | Barrier_RISCV_rw_rw -> "Barrier_RISCV_rw_rw" | Barrier_RISCV_r_rw -> "Barrier_RISCV_r_rw" | Barrier_RISCV_r_r -> "Barrier_RISCV_r_r" | Barrier_RISCV_rw_w -> "Barrier_RISCV_rw_w" | Barrier_RISCV_w_w -> "Barrier_RISCV_w_w" | Barrier_RISCV_i -> "Barrier_RISCV_i" | Barrier_x86_MFENCE -> "Barrier_x86_MFENCE" end end type trans_kind = (* AArch64 *) | Transaction_start | Transaction_commit | Transaction_abort instance (Show trans_kind) let show = function | Transaction_start -> "Transaction_start" | Transaction_commit -> "Transaction_commit" | Transaction_abort -> "Transaction_abort" end end type instruction_kind = | IK_barrier of barrier_kind | IK_mem_read of read_kind | IK_mem_write of write_kind | IK_mem_rmw of (read_kind * write_kind) | IK_cond_branch (* unconditional branches are not distinguished in the instruction_kind; they just have particular nias (and will be IK_simple *) (* | IK_uncond_branch *) | IK_trans of trans_kind | IK_simple instance (Show instruction_kind) let show = function | IK_barrier barrier_kind -> "IK_barrier " ^ (show barrier_kind) | IK_mem_read read_kind -> "IK_mem_read " ^ (show read_kind) | IK_mem_write write_kind -> "IK_mem_write " ^ (show write_kind) | IK_cond_branch -> "IK_cond_branch" | IK_trans trans_kind -> "IK_trans " ^ (show trans_kind) | IK_simple -> "IK_simple" end end let ~{ocaml} read_kindCompare rk1 rk2 = match (rk1, rk2) with | (Read_plain, Read_plain) -> EQ | (Read_plain, Read_reserve) -> LT | (Read_plain, Read_acquire) -> LT | (Read_plain, Read_exclusive) -> LT | (Read_plain, Read_exclusive_acquire) -> LT | (Read_plain, Read_stream) -> LT | (Read_reserve, Read_plain) -> GT | (Read_reserve, Read_reserve) -> EQ | (Read_reserve, Read_acquire) -> LT | (Read_reserve, Read_exclusive) -> LT | (Read_reserve, Read_exclusive_acquire) -> LT | (Read_reserve, Read_stream) -> LT | (Read_acquire, Read_plain) -> GT | (Read_acquire, Read_reserve) -> GT | (Read_acquire, Read_acquire) -> EQ | (Read_acquire, Read_exclusive) -> LT | (Read_acquire, Read_exclusive_acquire) -> LT | (Read_acquire, Read_stream) -> LT | (Read_exclusive, Read_plain) -> GT | (Read_exclusive, Read_reserve) -> GT | (Read_exclusive, Read_acquire) -> GT | (Read_exclusive, Read_exclusive) -> EQ | (Read_exclusive, Read_exclusive_acquire) -> LT | (Read_exclusive, Read_stream) -> LT | (Read_exclusive_acquire, Read_plain) -> GT | (Read_exclusive_acquire, Read_reserve) -> GT | (Read_exclusive_acquire, Read_acquire) -> GT | (Read_exclusive_acquire, Read_exclusive) -> GT | (Read_exclusive_acquire, Read_exclusive_acquire) -> EQ | (Read_exclusive_acquire, Read_stream) -> GT | (Read_stream, Read_plain) -> GT | (Read_stream, Read_reserve) -> GT | (Read_stream, Read_acquire) -> GT | (Read_stream, Read_exclusive) -> GT | (Read_stream, Read_exclusive_acquire) -> GT | (Read_stream, Read_stream) -> EQ end let inline {ocaml} read_kindCompare = defaultCompare let ~{ocaml} read_kindLess b1 b2 = read_kindCompare b1 b2 = LT let ~{ocaml} read_kindLessEq b1 b2 = read_kindCompare b1 b2 <> GT let ~{ocaml} read_kindGreater b1 b2 = read_kindCompare b1 b2 = GT let ~{ocaml} read_kindGreaterEq b1 b2 = read_kindCompare b1 b2 <> LT let inline {ocaml} read_kindLess = defaultLess let inline {ocaml} read_kindLessEq = defaultLessEq let inline {ocaml} read_kindGreater = defaultGreater let inline {ocaml} read_kindGreaterEq = defaultGreaterEq instance (Ord read_kind) let compare = read_kindCompare let (<) = read_kindLess let (<=) = read_kindLessEq let (>) = read_kindGreater let (>=) = read_kindGreaterEq end let read_is_exclusive = function | Read_plain -> false | Read_reserve -> true | Read_acquire -> false | Read_exclusive -> true | Read_exclusive_acquire -> true | Read_stream -> false | Read_RISCV_acquire -> false | Read_RISCV_strong_acquire -> false | Read_RISCV_reserved -> true | Read_RISCV_reserved_acquire -> true | Read_RISCV_reserved_strong_acquire -> true | Read_X86_locked -> true end let ~{ocaml} write_kindCompare wk1 wk2 = match (wk1, wk2) with | (Write_plain, Write_plain) -> EQ | (Write_plain, Write_conditional) -> LT | (Write_plain, Write_release) -> LT | (Write_plain, Write_exclusive) -> LT | (Write_plain, Write_exclusive_release) -> LT | (Write_conditional, Write_plain) -> GT | (Write_conditional, Write_conditional) -> EQ | (Write_conditional, Write_release) -> LT | (Write_conditional, Write_exclusive) -> LT | (Write_conditional, Write_exclusive_release) -> LT | (Write_release, Write_plain) -> GT | (Write_release, Write_conditional) -> GT | (Write_release, Write_release) -> EQ | (Write_release, Write_exclusive) -> LT | (Write_release, Write_exclusive_release) -> LT | (Write_exclusive, Write_plain) -> GT | (Write_exclusive, Write_conditional) -> GT | (Write_exclusive, Write_release) -> GT | (Write_exclusive, Write_exclusive) -> EQ | (Write_exclusive, Write_exclusive_release) -> LT | (Write_exclusive_release, Write_plain) -> GT | (Write_exclusive_release, Write_conditional) -> GT | (Write_exclusive_release, Write_release) -> GT | (Write_exclusive_release, Write_exclusive) -> GT | (Write_exclusive_release, Write_exclusive_release) -> EQ end let inline {ocaml} write_kindCompare = defaultCompare let ~{ocaml} write_kindLess b1 b2 = write_kindCompare b1 b2 = LT let ~{ocaml} write_kindLessEq b1 b2 = write_kindCompare b1 b2 <> GT let ~{ocaml} write_kindGreater b1 b2 = write_kindCompare b1 b2 = GT let ~{ocaml} write_kindGreaterEq b1 b2 = write_kindCompare b1 b2 <> LT let inline {ocaml} write_kindLess = defaultLess let inline {ocaml} write_kindLessEq = defaultLessEq let inline {ocaml} write_kindGreater = defaultGreater let inline {ocaml} write_kindGreaterEq = defaultGreaterEq instance (Ord write_kind) let compare = write_kindCompare let (<) = write_kindLess let (<=) = write_kindLessEq let (>) = write_kindGreater let (>=) = write_kindGreaterEq end (* Barrier comparison that uses less memory in Isabelle/HOL *) let ~{ocaml} barrier_number = function | Barrier_Sync -> (0 : natural) | Barrier_LwSync -> 1 | Barrier_Eieio -> 2 | Barrier_Isync -> 3 | Barrier_DMB -> 4 | Barrier_DMB_ST -> 5 | Barrier_DMB_LD -> 6 | Barrier_DSB -> 7 | Barrier_DSB_ST -> 8 | Barrier_DSB_LD -> 9 | Barrier_ISB -> 10 | Barrier_TM_COMMIT -> 11 | Barrier_MIPS_SYNC -> 12 | Barrier_RISCV_rw_rw -> 13 | Barrier_RISCV_r_rw -> 14 | Barrier_RISCV_r_r -> 15 | Barrier_RISCV_rw_w -> 16 | Barrier_RISCV_w_w -> 17 | Barrier_RISCV_i -> 18 | Barrier_x86_MFENCE -> 19 end let ~{ocaml} barrier_kindCompare bk1 bk2 = let n1 = barrier_number bk1 in let n2 = barrier_number bk2 in if n1 < n2 then LT else if n1 = n2 then EQ else GT let inline {ocaml} barrier_kindCompare = defaultCompare (*let ~{ocaml} barrier_kindCompare bk1 bk2 = match (bk1, bk2) with | (Barrier_Sync, Barrier_Sync) -> EQ | (Barrier_Sync, _) -> LT | (_, Barrier_Sync) -> GT | (Barrier_LwSync, Barrier_LwSync) -> EQ | (Barrier_LwSync, _) -> LT | (_, Barrier_LwSync) -> GT | (Barrier_Eieio, Barrier_Eieio) -> EQ | (Barrier_Eieio, _) -> LT | (_, Barrier_Eieio) -> GT | (Barrier_Isync, Barrier_Isync) -> EQ | (Barrier_Isync, _) -> LT | (_, Barrier_Isync) -> GT | (Barrier_DMB, Barrier_DMB) -> EQ | (Barrier_DMB, _) -> LT | (_, Barrier_DMB) -> GT | (Barrier_DMB_ST, Barrier_DMB_ST) -> EQ | (Barrier_DMB_ST, _) -> LT | (_, Barrier_DMB_ST) -> GT | (Barrier_DMB_LD, Barrier_DMB_LD) -> EQ | (Barrier_DMB_LD, _) -> LT | (_, Barrier_DMB_LD) -> GT | (Barrier_DSB, Barrier_DSB) -> EQ | (Barrier_DSB, _) -> LT | (_, Barrier_DSB) -> GT | (Barrier_DSB_ST, Barrier_DSB_ST) -> EQ | (Barrier_DSB_ST, _) -> LT | (_, Barrier_DSB_ST) -> GT | (Barrier_DSB_LD, Barrier_DSB_LD) -> EQ | (Barrier_DSB_LD, _) -> LT | (_, Barrier_DSB_LD) -> GT | (Barrier_ISB, Barrier_ISB) -> EQ | (Barrier_ISB, _) -> LT | (_, Barrier_ISB) -> GT | (Barrier_TM_COMMIT, Barrier_TM_COMMIT) -> EQ | (Barrier_TM_COMMIT, _) -> LT | (_, Barrier_TM_COMMIT) -> GT | (Barrier_MIPS_SYNC, Barrier_MIPS_SYNC) -> EQ (* | (Barrier_MIPS_SYNC, _) -> LT | (_, Barrier_MIPS_SYNC) -> GT *) end*) let ~{ocaml} barrier_kindLess b1 b2 = barrier_kindCompare b1 b2 = LT let ~{ocaml} barrier_kindLessEq b1 b2 = barrier_kindCompare b1 b2 <> GT let ~{ocaml} barrier_kindGreater b1 b2 = barrier_kindCompare b1 b2 = GT let ~{ocaml} barrier_kindGreaterEq b1 b2 = barrier_kindCompare b1 b2 <> LT let inline {ocaml} barrier_kindLess = defaultLess let inline {ocaml} barrier_kindLessEq = defaultLessEq let inline {ocaml} barrier_kindGreater = defaultGreater let inline {ocaml} barrier_kindGreaterEq = defaultGreaterEq instance (Ord barrier_kind) let compare = barrier_kindCompare let (<) = barrier_kindLess let (<=) = barrier_kindLessEq let (>) = barrier_kindGreater let (>=) = barrier_kindGreaterEq end