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.

model/riscv_insts_aext.sail

@@ -48,9 +48,13 @@ 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 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 +78,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 +120,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 },

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.
  */

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()
  }
  }