An initial fix to riscv lr/sc, needs a review.

This uses a stronger model than the version in Sail-1 in order to
perform address alignment checks.  The reservation is kept on virtual
addresses, and maintained in the platform model, but now the lr/sc
definitions need calls to externs to update this state.  An
alternative was to reserve physical addresses, but that appeared to be
more complicated without a lot more changes.  Ideally, the model
should be parameterizable over both options.

6 files changed, 133 insertions, 42 deletions

diff --git a/riscv/platform.ml b/riscv/platform.ml
index 0366e601..ddae4840 100644
--- a/riscv/platform.ml
+++ b/riscv/platform.ml
@@ -97,7 +97,24 @@ let clint_size () = bits_of_int64 P.clint_size
 
 let insns_per_tick () = Big_int.of_int P.insns_per_tick
 
+(* load reservation *)
+
+let reservation = ref "none"  (* shouldn't match any valid address *)
+
+let load_reservation addr =
+  Printf.eprintf "reservation <- %s\n" (!reservation);
+  reservation := string_of_bits addr
+
+let match_reservation addr =
+  Printf.eprintf "reservation: %s, key=%s\n" (!reservation) (string_of_bits addr);
+  string_of_bits addr = !reservation
+
+let cancel_reservation () =
+  Printf.eprintf "reservation <- none\n";
+  reservation := "none"
+
 (* terminal I/O *)
+
 let term_write char_bits =
   let big_char = Big_int.bitwise_and (uint char_bits) (Big_int.of_int 255) in
   P.term_write (char_of_int (Big_int.to_int big_char))
diff --git a/riscv/riscv.sail b/riscv/riscv.sail
index 35f3c625..687531c1 100644
--- a/riscv/riscv.sail
+++ b/riscv/riscv.sail
@@ -328,7 +328,7 @@ function extend_value(is_unsigned, value) = match (value) {
 
 val process_load : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
 function process_load(rd, addr, value, is_unsigned) =
-  match (extend_value(is_unsigned, value)) {
+  match extend_value(is_unsigned, value) {
     MemValue(result) => { X(rd) = result; true },
     MemException(e)  => { handle_mem_exception(addr, e); false }
   }
@@ -913,20 +913,43 @@ union clause ast = LOADRES : (bool, bool, regbits, word_width, regbits)
 
 mapping clause encdec = LOADRES(aq, rl, rs1, size, rd) <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_bits(size) @ rd @ 0b0101111
 
-val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> unit
+/* We could set load-reservations on physical or virtual addresses.
+ * For now we set them on virtual addresses, since it makes the
+ * sequential model of SC a bit simpler, at the cost of an explicit
+ * call to load_reservation in LR and cancel_reservation in SC.
+ */
 
-function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
-  let vaddr : xlenbits = X(rs1) in
-  match translateAddr(vaddr, Read, Data) {
-    TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
-    TR_Address(addr) =>
-      match width {
-        WORD   => process_load(rd, addr, mem_read(addr, 4, aq, rl, true), false),
-        DOUBLE => process_load(rd, addr, mem_read(addr, 8, aq, rl, true), false),
-        _      => internal_error("LOADRES expected WORD or DOUBLE")
-      }
+val process_loadres : forall 'n, 0 < 'n <= 8. (regbits, xlenbits, MemoryOpResult(bits(8 * 'n)), bool) -> bool effect {escape, rreg, wreg}
+function process_loadres(rd, addr, value, is_unsigned) =
+  match extend_value(is_unsigned, value) {
+    MemValue(result) => { X(rd) = result; load_reservation(addr); true },
+    MemException(e)  => { handle_mem_exception(addr, e); false }
   }
 
+function clause execute(LOADRES(aq, rl, rs1, width, rd)) =
+  let vaddr : xlenbits = X(rs1) in
+  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, Read, Data) {
+         TR_Failure(e) => { handle_mem_exception(vaddr, e); false },
+         TR_Address(addr) =>
+           match width {
+             WORD   => process_loadres(rd, vaddr, mem_read(addr, 4, aq, rl, true), false),
+             DOUBLE => process_loadres(rd, vaddr, mem_read(addr, 8, aq, rl, true), false),
+             _      => internal_error("LOADRES expected WORD or DOUBLE")
+           }
+       }
 
 function clause print_insn (LOADRES(aq, rl, rs1, width, rd)) =
   "lr" ^ lrsc_width_str(width) ^ aqrl_str(aq, rl) ^ " " ^ rd ^ ", " ^ rs1
@@ -941,31 +964,51 @@ mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd) <-> 0b00011 @ bool_
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
-  status : bits(1) = if speculate_conditional_success() then 0b0 else 0b1;
-  X(rd) = EXTZ(status);
-
-  if status == 0b1 then true else {
-    vaddr : xlenbits = X(rs1);
-    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(unit) = 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")
-            } in
-            match (res) {
-              MemValue(_)     => true,
-              MemException(e) => { handle_mem_exception(addr, e); false }
+  /* 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 }
+    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(unit) = 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(_)     => { X(rd) = EXTZ(0b0); cancel_reservation(); true },
+                MemException(e) => { handle_mem_exception(addr, e); false }
+              }
             }
           }
         }
diff --git a/riscv/riscv_extras.lem b/riscv/riscv_extras.lem
index b3d84df6..88ac3e6f 100644
--- a/riscv/riscv_extras.lem
+++ b/riscv/riscv_extras.lem
@@ -45,7 +45,12 @@ val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
 let read_ram addrsize size hexRAM address =
   read_mem Read_plain address size
 
-let speculate_conditional_success () = excl_result ()
+val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
+let load_reservation addr = ()
+
+let speculate_conditional_success _ = excl_result ()
+
+let cancel_reservation () = ()
 
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
diff --git a/riscv/riscv_extras_sequential.lem b/riscv/riscv_extras_sequential.lem
index b3d84df6..88ac3e6f 100644
--- a/riscv/riscv_extras_sequential.lem
+++ b/riscv/riscv_extras_sequential.lem
@@ -45,7 +45,12 @@ val read_ram : forall 'rv 'a 'b 'e. Size 'a, Size 'b =>
 let read_ram addrsize size hexRAM address =
   read_mem Read_plain address size
 
-let speculate_conditional_success () = excl_result ()
+val load_reservation : forall 'a. Size 'a => bitvector 'a -> unit
+let load_reservation addr = ()
+
+let speculate_conditional_success _ = excl_result ()
+
+let cancel_reservation () = ()
 
 val plat_ram_base : forall 'a. Size 'a => unit -> bitvector 'a
 let plat_ram_base () = wordFromInteger 0
diff --git a/riscv/riscv_mem.sail b/riscv/riscv_mem.sail
index 9ead3aeb..008c1642 100644
--- a/riscv/riscv_mem.sail
+++ b/riscv/riscv_mem.sail
@@ -92,6 +92,7 @@ function phys_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -
   else MemException(E_SAMO_Access_Fault)
 }
 
+// dispatches to MMIO regions or physical memory regions depending on physical memory map
 function checked_mem_write(addr : xlenbits, width : atom('n), data: bits(8 * 'n)) -> forall 'n, 'n > 0. MemoryOpResult(unit) =
   if   within_mmio_writable(addr, width)
   then mmio_write(addr, width, data)
@@ -133,8 +134,6 @@ function mem_write_value (addr, width, value, aq, rl, con) = {
   }
 }
 
-val "speculate_conditional_success" : unit -> bool effect {exmem}
-
 val MEM_fence_rw_rw = {ocaml: "skip", lem: "MEM_fence_rw_rw"} : unit -> unit effect {barr}
 val MEM_fence_r_rw  = {ocaml: "skip", lem: "MEM_fence_r_rw"}  : unit -> unit effect {barr}
 val MEM_fence_r_r   = {ocaml: "skip", lem: "MEM_fence_r_r"}   : unit -> unit effect {barr}
diff --git a/riscv/riscv_sys.sail b/riscv/riscv_sys.sail
index bb3d13db..e8128edf 100644
--- a/riscv/riscv_sys.sail
+++ b/riscv/riscv_sys.sail
@@ -363,7 +363,6 @@ function legalize_sedeleg(s : Sedeleg, v : xlenbits) -> Sedeleg = {
   Mk_Sedeleg(EXTZ(v[8..0]))
 }
 
-/* TODO: handle views for interrupt delegation */
 bitfield Sinterrupts : bits(64) = {
   SEI : 9,  /* external interrupts */
   UEI : 8,
@@ -670,6 +669,24 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
   & check_TVM_SATP(csr, p)
   & check_Counteren(csr, p)
 
+/* Reservation handling for LR/SC.
+ *
+ * The reservation state is maintained external to the model since the
+ * reservation behavior is platform-specific anyway and maintaining
+ * this state outside the model simplifies the concurrency analysis.
+ *
+ * These are externs are defined here in the system module since
+ * we currently perform reservation cancellation on privilege level
+ * transition.  Ideally, the platform should get more visibility into
+ * where cancellation can be performed.
+ */
+
+val load_reservation = {ocaml: "Platform.load_reservation", lem: "load_reservation"} : xlenbits -> unit
+
+val match_reservation = {ocaml: "Platform.match_reservation", lem: "speculate_conditional_success"} : xlenbits -> bool effect {exmem}
+
+val cancel_reservation = {ocaml: "Platform.cancel_reservation", lem: "cancel_reservation"} : unit -> unit
+
 /* Exception delegation: given an exception and the privilege at which
  * it occured, returns the privilege at which it should be handled.
  */
@@ -776,6 +793,7 @@ union ctl_result = {
 function handle_trap(del_priv : Privilege, intr : bool, c : exc_code, pc : xlenbits, info : option(xlenbits))
                     -> xlenbits = {
   print("handling " ^ (if intr then "int#" else "exc#") ^ BitStr(c) ^ " at priv " ^ del_priv ^ " with tval " ^ BitStr(tval(info)));
+  cancel_reservation();
   match (del_priv) {
     Machine => {
        mcause->IsInterrupt() = intr;
@@ -840,6 +858,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = privLevel_of_bits(mstatus.MPP());
       mstatus->MPP()  = privLevel_to_bits(User);
 
+      cancel_reservation();
+
       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
       print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
       mepc
@@ -851,6 +871,8 @@ function handle_exception(cur_priv : Privilege, ctl : ctl_result,
       cur_privilege   = if mstatus.SPP() == true then Supervisor else User;
       mstatus->SPP()  = false;
 
+      cancel_reservation();
+
       print("CSR mstatus <- " ^ BitStr(mstatus.bits()) ^ " (input: " ^ BitStr(mstatus.bits()) ^ ")"); // Spike compatible log
       print("ret-ing from " ^ prev_priv ^ " to " ^ cur_privilege);
       sepc