From 585e6ff5972366075281a416884b6ff3b95bcd62 Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 18 Jun 2024 21:17:35 +0100 Subject: [PATCH] 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 | 29 +++++++++++++++++------------ model/riscv_platform.sail | 1 - model/riscv_sys_control.sail | 5 ----- 3 files changed, 17 insertions(+), 18 deletions(-) diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index 3bf44b8f5..d8238b43d 100644 --- a/model/riscv_insts_aext.sail +++ b/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 }, diff --git a/model/riscv_platform.sail b/model/riscv_platform.sail index 19e3d30ae..6c64b5928 100644 --- 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 index 95ed4d6a5..cbe61bcb0 100644 --- 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() } }