Address the fixme for rmem integration of LR as suggested by Shaked.

5 files changed, 53 insertions, 45 deletions

diff --git a/platform.ml b/platform.ml
index bdd5bd0..6ee2d2b 100644
--- a/platform.ml
+++ b/platform.ml
@@ -128,6 +128,8 @@ let insns_per_tick () = Big_int.of_int P.insns_per_tick
 
 (* load reservation *)
 
+let speculate_conditional () = true
+
 let reservation = ref "none"  (* shouldn't match any valid address *)
 
 let load_reservation addr =
diff --git a/riscv.sail b/riscv.sail
index 5b27e0e..72fed8c 100644
--- a/riscv.sail
+++ b/riscv.sail
@@ -852,57 +852,57 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
-  /* RMEM FIXME:  This definition differs from the Sail1 version:
-   * rs1 is read *before* speculate_conditional_success
-   * (called via match_reservation), partly due to the current api of
-   * match_reservation.  Reverting back to the weaker Sail1 version
-   * will require changes to the API for the ghost reservation state.
-   */
-  vaddr : xlenbits = X(rs1);
-  let aligned : bool =
-    /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
-     * to treat them as valid here; otherwise we'd need to throw an internal_error.
-     * May need to revisit for latex output.
-     */
-    match width {
-      BYTE   => true,
-      HALF   => vaddr[0]    == 0b0,
-      WORD   => vaddr[1..0] == 0b00,
-      DOUBLE => vaddr[2..0] == 0b000
-    } in
-  if (~ (aligned))
-  then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
-  else {
-    if   match_reservation(vaddr) == false
-    then { X(rd) = EXTZ(0b1); true }
+  if speculate_conditional () then {
+    /* normal non-rmem case */
+    vaddr : xlenbits = X(rs1);
+    let aligned : bool =
+      /* BYTE and HALF would only occur due to invalid decodes, but it doesn't hurt
+       * to treat them as valid here; otherwise we'd need to throw an internal_error.
+       * May need to revisit for latex output.
+       */
+      match width {
+        BYTE   => true,
+        HALF   => vaddr[0]    == 0b0,
+        WORD   => vaddr[1..0] == 0b00,
+        DOUBLE => vaddr[2..0] == 0b000
+      } in
+    if (~ (aligned))
+    then { handle_mem_exception(vaddr, E_SAMO_Addr_Align); false }
     else {
-      match translateAddr(vaddr, Write, Data) {
-        TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-        TR_Address(addr) => {
-          let eares : MemoryOpResult(unit) = match width {
-            WORD   => mem_write_ea(addr, 4, aq, rl, true),
-            DOUBLE => mem_write_ea(addr, 8, aq, rl, true),
-            _      => internal_error("STORECON expected word or double")
-          };
-          match (eares) {
-            MemException(e)  => { handle_mem_exception(addr, e); false },
-            MemValue(_) => {
-              rs2_val = X(rs2);
-              let res : MemoryOpResult(bool) = match width {
-                WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
-                DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
-                _      => internal_error("STORECON expected word or double")
-              };
-              match (res) {
-                MemValue(true)     => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
-                MemValue(false)    => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
-                MemException(e)    => { handle_mem_exception(addr, e); false }
+      if   match_reservation(vaddr) == false
+      then { X(rd) = EXTZ(0b1); true }
+      else {
+        match translateAddr(vaddr, Write, Data) {
+          TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+          TR_Address(addr) => {
+            let eares : MemoryOpResult(unit) = match width {
+              WORD   => mem_write_ea(addr, 4, aq, rl, true),
+              DOUBLE => mem_write_ea(addr, 8, aq, rl, true),
+              _      => internal_error("STORECON expected word or double")
+            };
+            match (eares) {
+              MemException(e)  => { handle_mem_exception(addr, e); false },
+              MemValue(_) => {
+                rs2_val = X(rs2);
+                let res : MemoryOpResult(bool) = match width {
+                  WORD   => mem_write_value(addr, 4, rs2_val[31..0], aq, rl, true),
+                  DOUBLE => mem_write_value(addr, 8, rs2_val,        aq, rl, true),
+                  _      => internal_error("STORECON expected word or double")
+                };
+                match (res) {
+                  MemValue(true)     => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
+                  MemValue(false)    => { X(rd) = EXTZ(0b1); cancel_reservation(); true },
+                  MemException(e)    => { handle_mem_exception(addr, e); false }
+                }
               }
             }
           }
         }
       }
     }
+  } else {
+    /* should only happen in rmem */
+    false
   }
 }
 
diff --git a/riscv_platform.c b/riscv_platform.c
index f0aff76..3587206 100644
--- a/riscv_platform.c
+++ b/riscv_platform.c
@@ -42,6 +42,9 @@ unit load_reservation(mach_bits addr)
   return UNIT;
 }
 
+bool speculate_conditional(unit u)
+{ return true; }
+
 bool match_reservation(mach_bits addr)
 { return reservation_valid && reservation == addr; }
 
diff --git a/riscv_platform.h b/riscv_platform.h
index 9378266..728555e 100644
--- a/riscv_platform.h
+++ b/riscv_platform.h
@@ -15,6 +15,7 @@ mach_bits plat_rom_size(unit);
 mach_bits plat_clint_base(unit);
 mach_bits plat_clint_size(unit);
 
+bool speculate_conditional(unit);
 unit load_reservation(mach_bits);
 bool match_reservation(mach_bits);
 unit cancel_reservation(unit);
diff --git a/riscv_sys.sail b/riscv_sys.sail
index 5860994..50a9434 100644
--- a/riscv_sys.sail
+++ b/riscv_sys.sail
@@ -772,9 +772,11 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
  * where cancellation can be performed.
  */
 
+val speculate_conditional = {ocaml: "Platform.speculate_conditional", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
+
 val load_reservation = {ocaml: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : xlenbits -> unit
 
-val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success", c: "match_reservation"} : xlenbits -> bool effect {exmem}
+val match_reservation = {ocaml: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : xlenbits -> bool effect {exmem}
 
 val cancel_reservation = {ocaml: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit