diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/sail_impl_base.lem | 373 | ||||
| -rw-r--r-- | src/lem_interp/sail_instr_kinds.lem | 436 |
2 files changed, 441 insertions, 368 deletions
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem index 219677ac..f029b952 100644 --- a/src/lem_interp/sail_impl_base.lem +++ b/src/lem_interp/sail_impl_base.lem @@ -49,7 +49,7 @@ (*========================================================================*) open import Pervasives_extra - +open import Sail_instr_kinds class ( EnumerationType 'a ) @@ -478,373 +478,10 @@ end (* 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 ~{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 +(* read_kind, write_kind, barrier_kind, trans_kind and instruction_kind have + been moved to sail_instr_kinds.lem. This removes the dependency of the + shallow embedding on the rest of sail_impl_base.lem, and helps avoid name + clashes between the different monad types. *) type event = | E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name) diff --git a/src/lem_interp/sail_instr_kinds.lem b/src/lem_interp/sail_instr_kinds.lem new file mode 100644 index 00000000..89ff67b2 --- /dev/null +++ b/src/lem_interp/sail_instr_kinds.lem @@ -0,0 +1,436 @@ +(*========================================================================*) +(* 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 |