Skip to content

Commit 5ecc9d5

Browse files
committed
Change *_reservation to take physaddr
1 parent d9c94ff commit 5ecc9d5

File tree

5 files changed

+23
-11
lines changed

5 files changed

+23
-11
lines changed

c_emulator/riscv_platform.c

+5-4
Original file line numberDiff line numberDiff line change
@@ -163,9 +163,9 @@ mach_bits plat_clint_size(unit u)
163163
return rv_clint_size;
164164
}
165165

166-
unit load_reservation(mach_bits addr)
166+
unit load_reservation(struct zphysaddr addr)
167167
{
168-
reservation = addr;
168+
reservation = addr.zphysaddr;
169169
reservation_valid = true;
170170
RESERVATION_DBG("reservation <- %0" PRIx64 "\n", reservation);
171171
return UNIT;
@@ -181,10 +181,11 @@ static mach_bits check_mask(void)
181181
return (zxlen_val == 32) ? 0x00000000FFFFFFFF : -1;
182182
}
183183

184-
bool match_reservation(mach_bits addr)
184+
bool match_reservation(struct zphysaddr addr)
185185
{
186186
mach_bits mask = check_mask();
187-
bool ret = reservation_valid && (reservation & mask) == (addr & mask);
187+
bool ret
188+
= reservation_valid && (reservation & mask) == (addr.zphysaddr & mask);
188189
RESERVATION_DBG("reservation(%c): %0" PRIx64 ", key=%0" PRIx64 ": %s\n",
189190
reservation_valid ? 'v' : 'i', reservation, addr,
190191
ret ? "ok" : "fail");

c_emulator/riscv_platform.h

+4-2
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
#pragma once
22
#include "sail.h"
33

4+
struct zphysaddr;
5+
46
bool sys_enable_rvc(unit);
57
bool sys_enable_fdext(unit);
68
bool sys_enable_svinval(unit);
@@ -42,8 +44,8 @@ mach_bits plat_clint_base(unit);
4244
mach_bits plat_clint_size(unit);
4345

4446
bool speculate_conditional(unit);
45-
unit load_reservation(mach_bits);
46-
bool match_reservation(mach_bits);
47+
unit load_reservation(struct zphysaddr);
48+
bool match_reservation(struct zphysaddr);
4749
unit cancel_reservation(unit);
4850

4951
void plat_insns_per_tick(sail_int *rop, unit);

c_emulator/riscv_sail.h

+10-1
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
/* Top-level interfaces to the Sail model.
22
Ideally, this would be autogenerated.
33
*/
4-
54
typedef int unit;
65
#define UNIT 0
76
typedef uint64_t mach_bits;
@@ -68,3 +67,13 @@ struct zMcause {
6867
extern struct zMcause zmcause, zscause;
6968

7069
extern mach_bits zminstret;
70+
71+
enum kind_zphysaddr { Kind_zphysaddr };
72+
struct zphysaddr {
73+
enum kind_zphysaddr kind;
74+
union {
75+
struct {
76+
uint64_t zphysaddr;
77+
};
78+
};
79+
};

model/riscv_insts_aext.sail

+2-2
Original file line numberDiff line numberDiff line change
@@ -91,7 +91,7 @@ function clause execute(LOADRES(aq, rl, rs1, width, rd)) = {
9191
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
9292
TR_Address(addr, _) =>
9393
match mem_read(Read(Data), addr, width_bytes, aq, aq & rl, true) {
94-
MemValue(result) => { load_reservation(physaddr_bits(addr)); X(rd) = sign_extend(result); RETIRE_SUCCESS },
94+
MemValue(result) => { load_reservation(addr); X(rd) = sign_extend(result); RETIRE_SUCCESS },
9595
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
9696
},
9797
}
@@ -138,7 +138,7 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
138138
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
139139
TR_Address(addr, _) => {
140140
// Check reservation with physical address.
141-
if not(match_reservation(physaddr_bits(addr))) then {
141+
if not(match_reservation(addr)) then {
142142
/* cannot happen in rmem */
143143
X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS
144144
} else {

model/riscv_sys_control.sail

+2-2
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,8 @@ function check_CSR(csr : csreg, p : Privilege, isWrite : bool) -> bool =
9090

9191
val speculate_conditional = impure {interpreter: "excl_res", c: "speculate_conditional", lem: "speculate_conditional_success"} : unit -> bool
9292

93-
val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : physaddrbits -> unit
94-
val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : physaddrbits -> bool
93+
val load_reservation = impure {interpreter: "Platform.load_reservation", c: "load_reservation", lem: "load_reservation"} : physaddr -> unit
94+
val match_reservation = pure {interpreter: "Platform.match_reservation", lem: "match_reservation", c: "match_reservation"} : physaddr -> bool
9595
val cancel_reservation = impure {interpreter: "Platform.cancel_reservation", c: "cancel_reservation", lem: "cancel_reservation"} : unit -> unit
9696

9797
/* Exception delegation: given an exception and the privilege at which

0 commit comments

Comments
 (0)