From 5ecc9d51e42ea61987e32a21d7b63e5e44e03c1f Mon Sep 17 00:00:00 2001 From: KotorinMinami Date: Fri, 10 Jan 2025 02:17:03 +0800 Subject: [PATCH] Change *_reservation to take physaddr --- c_emulator/riscv_platform.c | 9 +++++---- c_emulator/riscv_platform.h | 6 ++++-- c_emulator/riscv_sail.h | 11 ++++++++++- model/riscv_insts_aext.sail | 4 ++-- model/riscv_sys_control.sail | 4 ++-- 5 files changed, 23 insertions(+), 11 deletions(-) diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index e19008c51..29a911c87 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -163,9 +163,9 @@ mach_bits plat_clint_size(unit u) return rv_clint_size; } -unit load_reservation(mach_bits addr) +unit load_reservation(struct zphysaddr addr) { - reservation = addr; + reservation = addr.zphysaddr; reservation_valid = true; RESERVATION_DBG("reservation <- %0" PRIx64 "\n", reservation); return UNIT; @@ -181,10 +181,11 @@ static mach_bits check_mask(void) return (zxlen_val == 32) ? 0x00000000FFFFFFFF : -1; } -bool match_reservation(mach_bits addr) +bool match_reservation(struct zphysaddr addr) { mach_bits mask = check_mask(); - bool ret = reservation_valid && (reservation & mask) == (addr & mask); + bool ret + = reservation_valid && (reservation & mask) == (addr.zphysaddr & mask); RESERVATION_DBG("reservation(%c): %0" PRIx64 ", key=%0" PRIx64 ": %s\n", reservation_valid ? 'v' : 'i', reservation, addr, ret ? "ok" : "fail"); diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index 8d8d8aaef..ec5a4c8e4 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -1,6 +1,8 @@ #pragma once #include "sail.h" +struct zphysaddr; + bool sys_enable_rvc(unit); bool sys_enable_fdext(unit); bool sys_enable_svinval(unit); @@ -42,8 +44,8 @@ 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 load_reservation(struct zphysaddr); +bool match_reservation(struct zphysaddr); unit cancel_reservation(unit); void plat_insns_per_tick(sail_int *rop, unit); diff --git a/c_emulator/riscv_sail.h b/c_emulator/riscv_sail.h index abaad4e6d..5bf299557 100644 --- a/c_emulator/riscv_sail.h +++ b/c_emulator/riscv_sail.h @@ -1,7 +1,6 @@ /* Top-level interfaces to the Sail model. Ideally, this would be autogenerated. */ - typedef int unit; #define UNIT 0 typedef uint64_t mach_bits; @@ -68,3 +67,13 @@ struct zMcause { extern struct zMcause zmcause, zscause; extern mach_bits zminstret; + +enum kind_zphysaddr { Kind_zphysaddr }; +struct zphysaddr { + enum kind_zphysaddr kind; + union { + struct { + uint64_t zphysaddr; + }; + }; +}; diff --git a/model/riscv_insts_aext.sail b/model/riscv_insts_aext.sail index f9cc25fb5..f355ea65a 100644 --- a/model/riscv_insts_aext.sail +++ b/model/riscv_insts_aext.sail @@ -91,7 +91,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(physaddr_bits(addr)); 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 } }, } @@ -138,7 +138,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = { TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }, TR_Address(addr, _) => { // Check reservation with physical address. - if not(match_reservation(physaddr_bits(addr))) then { + if not(match_reservation(addr)) then { /* cannot happen in rmem */ X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS } else { diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index a8c755724..6f7060f6b 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -90,8 +90,8 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool = val speculate_conditional = impure {interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool -val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : physaddrbits -> unit -val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : physaddrbits -> bool +val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : physaddr -> unit +val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : physaddr -> bool val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit /* Exception delegation: given an exception and the privilege at which