diff options
| author | Brian Campbell | 2019-07-31 17:30:11 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-07-31 17:30:11 +0100 |
| commit | c8036903b9e23d8eba6f2b929ddf5eaaea157d71 (patch) | |
| tree | ab9609e9b9daa46b6e8a7eab31b5d5c8ff28dedb /lib/coq/Sail2_instr_kinds.v | |
| parent | 66b2f1c1757a4cdf6bef1040b152d43ce09021f3 (diff) | |
Coq: Update barrier definitions
Diffstat (limited to 'lib/coq/Sail2_instr_kinds.v')
| -rw-r--r-- | lib/coq/Sail2_instr_kinds.v | 37 |
1 files changed, 20 insertions, 17 deletions
diff --git a/lib/coq/Sail2_instr_kinds.v b/lib/coq/Sail2_instr_kinds.v index 85d78226..d03d5e63 100644 --- a/lib/coq/Sail2_instr_kinds.v +++ b/lib/coq/Sail2_instr_kinds.v @@ -153,28 +153,31 @@ Inductive a64_barrier_type := Inductive barrier_kind := (* Power barriers *) - Barrier_Sync | Barrier_LwSync | Barrier_Eieio | Barrier_Isync + | Barrier_Sync : unit -> barrier_kind + | Barrier_LwSync : unit -> barrier_kind + | Barrier_Eieio : unit -> barrier_kind + | Barrier_Isync : unit -> barrier_kind (* AArch64 barriers *) - | Barrier_DMB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*) - | Barrier_DSB (*: a64_barrier_domain -> a64_barrier_type -> barrier_kind*) - | Barrier_ISB + | Barrier_DMB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_DSB : a64_barrier_domain -> a64_barrier_type -> barrier_kind + | Barrier_ISB : unit -> barrier_kind (* | Barrier_TM_COMMIT*) (* MIPS barriers *) - | Barrier_MIPS_SYNC + | Barrier_MIPS_SYNC : unit -> barrier_kind (* 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_w_rw - | Barrier_RISCV_rw_r - | Barrier_RISCV_r_w - | Barrier_RISCV_w_r - | Barrier_RISCV_tso - | Barrier_RISCV_i + | Barrier_RISCV_rw_rw : unit -> barrier_kind + | Barrier_RISCV_r_rw : unit -> barrier_kind + | Barrier_RISCV_r_r : unit -> barrier_kind + | Barrier_RISCV_rw_w : unit -> barrier_kind + | Barrier_RISCV_w_w : unit -> barrier_kind + | Barrier_RISCV_w_rw : unit -> barrier_kind + | Barrier_RISCV_rw_r : unit -> barrier_kind + | Barrier_RISCV_r_w : unit -> barrier_kind + | Barrier_RISCV_w_r : unit -> barrier_kind + | Barrier_RISCV_tso : unit -> barrier_kind + | Barrier_RISCV_i : unit -> barrier_kind (* X86 *) - | Barrier_x86_MFENCE. + | Barrier_x86_MFENCE : unit -> barrier_kind. Scheme Equality for barrier_kind. (* |