Adapt checked_mem_read to have acquire/release/reserve arguments so

that this information propagates from the instruction definition to
the memory accesses. Necessary for Promising RISC-V concurrency model.

2 files changed, 11 insertions, 11 deletions

diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 2d59a891..2bcc9797 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -16,12 +16,12 @@ function phys_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : boo
                                MemValue(v) }
   }
 
-function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n)) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
+function checked_mem_read(t : ReadType, addr : xlenbits, width : atom('n), aq : bool, rl : bool, res: bool) -> forall 'n, 'n > 0. MemoryOpResult(bits(8 * 'n)) =
   /* treat MMIO regions as not executable for now. TODO: this should actually come from PMP/PMA. */
   if   t == Data & within_mmio_readable(addr, width)
   then mmio_read(addr, width)
   else if within_phys_mem(addr, width)
-  then phys_mem_read(t, addr, width, false, false, false)
+  then phys_mem_read(t, addr, width, aq, rl, res)
   else MemException(E_Load_Access_Fault)
 
 /* Atomic accesses can be done to MMIO regions, e.g. in kernel access to device registers. */
@@ -33,12 +33,12 @@ val MEMr_reserved                : forall 'n, 'n > 0. (xlenbits, atom('n)) -> Me
 val MEMr_reserved_acquire        : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
 val MEMr_reserved_strong_acquire : forall 'n, 'n > 0. (xlenbits, atom('n)) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg}
 
-function MEMr                         (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_acquire                 (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_strong_acquire          (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved                (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width)
-function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width)
+function MEMr                         (addr, width) = checked_mem_read(Data, addr, width, false, false, false)
+function MEMr_acquire                 (addr, width) = checked_mem_read(Data, addr, width, true, false, false)
+function MEMr_strong_acquire          (addr, width) = checked_mem_read(Data, addr, width, true, true, false)
+function MEMr_reserved                (addr, width) = checked_mem_read(Data, addr, width, false, false, true)
+function MEMr_reserved_acquire        (addr, width) = checked_mem_read(Data, addr, width, true, false, true)
+function MEMr_reserved_strong_acquire (addr, width) = checked_mem_read(Data, addr, width, true, true, true)
 
 /* NOTE: The rreg effect is due to MMIO. */
 val mem_read : forall 'n, 'n > 0. (xlenbits, atom('n), bool, bool, bool) -> MemoryOpResult(bits(8 * 'n)) effect {rmem, rreg, escape}
@@ -47,7 +47,7 @@ function mem_read (addr, width, aq, rl, res) = {
   if (aq | res) & (~ (is_aligned_addr(addr, width)))
   then MemException(E_Load_Addr_Align)
   else match (aq, rl, res) {
-    (false, false, false) => checked_mem_read(Data, addr, width),
+    (false, false, false) => checked_mem_read(Data, addr, width, false, false, false),
     (true,  false, false) => MEMr_acquire(addr, width),
     (false, false, true)  => MEMr_reserved(addr, width),
     (true,  false, true)  => MEMr_reserved_acquire(addr, width),
diff --git a/riscv/riscv_step.sail b/riscv/riscv_step.sail
index 8e5a0090..f9675115 100644
--- a/riscv/riscv_step.sail
+++ b/riscv/riscv_step.sail
@@ -21,7 +21,7 @@ function fetch() -> FetchResult =
        * well as to generate precise fault addresses in any fetch
        * exceptions.
        */
-      match checked_mem_read(Instruction, ppclo, 2) {
+      match checked_mem_read(Instruction, ppclo, 2, false, false, false) {
         MemException(e) => F_Error(E_Fetch_Access_Fault, PC),
         MemValue(ilo) => {
           if isRVC(ilo) then F_RVC(ilo)
@@ -30,7 +30,7 @@ function fetch() -> FetchResult =
             match translateAddr(PChi, Execute, Instruction) {
               TR_Failure(e) => F_Error(e, PChi),
               TR_Address(ppchi) => {
-                match checked_mem_read(Instruction, ppchi, 2) {
+                match checked_mem_read(Instruction, ppchi, 2, false, false, false) {
                   MemException(e) => F_Error(E_Fetch_Access_Fault, PChi),
                   MemValue(ihi) => F_Base(append(ihi, ilo))
                 }