diff options
| author | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-08-13 11:40:39 +0100 |
|---|---|---|
| committer | Brian Campbell <Brian.Campbell@ed.ac.uk> | 2019-08-13 11:40:39 +0100 |
| commit | eafbb796e16ac61ef39d36b32524b40ada195375 (patch) | |
| tree | bde9e5c0a630695203051daf36e6284f24a4ea9f | |
| parent | e6cd25ff7e36e5134d1de2cdf8bb68dce97a567b (diff) | |
| download | sail-riscv-eafbb796e16ac61ef39d36b32524b40ada195375.zip sail-riscv-eafbb796e16ac61ef39d36b32524b40ada195375.tar.gz sail-riscv-eafbb796e16ac61ef39d36b32524b40ada195375.tar.bz2 | |
Update barriers in Coq.
| -rw-r--r-- | handwritten_support/riscv_extras.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/handwritten_support/riscv_extras.v b/handwritten_support/riscv_extras.v index 5828f88..84f6761 100644 --- a/handwritten_support/riscv_extras.v +++ b/handwritten_support/riscv_extras.v @@ -9,17 +9,17 @@ Import List.ListNotations. Axiom real : Type. -Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_rw. -Definition MEM_fence_r_rw {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_rw. -Definition MEM_fence_r_r {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_r. -Definition MEM_fence_rw_w {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_w. -Definition MEM_fence_w_w {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_w. -Definition MEM_fence_w_rw {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_rw. -Definition MEM_fence_rw_r {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_rw_r. -Definition MEM_fence_r_w {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_r_w. -Definition MEM_fence_w_r {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_w_r. -Definition MEM_fence_tso {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_tso. -Definition MEM_fence_i {rv e} (_:unit) : monad rv unit e := barrier Barrier_RISCV_i. +Definition MEM_fence_rw_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_rw tt). +Definition MEM_fence_r_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_rw tt). +Definition MEM_fence_r_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_r tt). +Definition MEM_fence_rw_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_w tt). +Definition MEM_fence_w_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_w tt). +Definition MEM_fence_w_rw {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_rw tt). +Definition MEM_fence_rw_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_rw_r tt). +Definition MEM_fence_r_w {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_r_w tt). +Definition MEM_fence_w_r {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_w_r tt). +Definition MEM_fence_tso {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_tso tt). +Definition MEM_fence_i {rv e} (_:unit) : monad rv unit e := barrier (Barrier_RISCV_i tt). (* val MEMea : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e val MEMea_release : forall 'rv 'a 'e. Size 'a => bitvector 'a -> integer -> monad 'rv unit 'e |