Use physical addresses for LR/SC reservations

This is how reservation is architecturally defined, how real CPUs are likely to be implemented, and doesn't require spurious cancellations on xRET and traps. Fixes #360.
riscv · Jun 18, 2024 · 11e63e7 · 11e63e7
1 parent 157d4d1
commit 11e63e7
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 18 deletions.
diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail
@@ -48,9 +48,14 @@ mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)
 
 
 /* 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.
+ * However the reservation is architecturally defined in terms of physical
+ * addresses, and most chips (especially multi-core) will use physical addresses.
+ * Additionally, matching on physical addresses allows as many SC's to
+ * succeed as the spec allows. This simplifies verification against real chips
+ * since you can force spurious failures from a DUT into the Sail model and
+ * then compare the result (a kind of one-way waiver). Using virtual addresses
+ * requires cancelling the reservation in some additional places, e.g. xRET, and
+ * that will break comparison with a DUT that doesn't require cancellation there.
  */
 
 function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
@@ -74,7 +79,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
         TR_Failure(e, _)    => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
         TR_Address(addr, _) =>
           match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
-            MemValue(result) => { load_reservation(vaddr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
+            MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
             MemException(e)  => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
           },
       }
@@ -116,14 +121,15 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
         if not(is_aligned(vaddr, width))
         then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
         else {
-          if match_reservation(vaddr) == false then {
-            /* cannot happen in rmem */
-            X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
-          } else {
-            match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
-                                                        * both result in a SAMO exception */
-              TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
-              TR_Address(addr, _) => {
+          match translateAddr(vaddr, Write(Data)) {  /* Write and ReadWrite are equivalent here:
+                                                      * both result in a SAMO exception */
+            TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
+            TR_Address(addr, _) => {
+              // Check reservation with physical address.
+              if not(match_reservation(addr)) then {
+                /* cannot happen in rmem */
+                X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
+              } else {
                 let eares = mem_write_ea(addr, width_bytes, aq & rl, rl, true);
                 match (eares) {
                   MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },

diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail
@@ -445,7 +445,6 @@ function handle_illegal() -> unit = {
 /* Platform-specific wait-for-interrupt */
 
 function platform_wfi() -> unit = {
-  cancel_reservation();
   /* speed execution by getting the timer to fire at the next instruction,
    * since we currently don't have any other devices raising interrupts.
    */

diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail
@@ -323,8 +323,6 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen
                       ^ BitStr(c) ^ " at priv " ^ to_str(del_priv)
                       ^ " with tval " ^ BitStr(tval(info)));
 
-  cancel_reservation();
-
   match (del_priv) {
     Machine => {
        mcause[IsInterrupt] = bool_to_bits(intr);
@@ -417,7 +415,6 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
-      cancel_reservation();
       prepare_xret_target(Machine) & pc_alignment_mask()
     },
     (_, CTL_SRET())  => {
@@ -435,7 +432,6 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       then print_platform("ret-ing from " ^ to_str(prev_priv)
                           ^ " to " ^ to_str(cur_privilege));
 
-      cancel_reservation();
       prepare_xret_target(Supervisor) & pc_alignment_mask()
     },
     (_, CTL_URET())  => {
@@ -449,7 +445,6 @@ function exception_handler(cur_priv : Privilege, ctl : ctl_result,
       if   get_config_print_platform()
       then print_platform("ret-ing from " ^ to_str(prev_priv) ^ " to " ^ to_str(cur_privilege));
 
-      cancel_reservation();
       prepare_xret_target(User) & pc_alignment_mask()
     }
   }