Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Change *_reservation to take physaddr #676

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Change *_reservation to take physaddr #676

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 5 additions & 4 deletions c_emulator/riscv_platform.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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");
Expand Down
6 changes: 4 additions & 2 deletions c_emulator/riscv_platform.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
Expand Down Expand Up @@ -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);
Expand Down
11 changes: 10 additions & 1 deletion c_emulator/riscv_sail.h
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand Down Expand Up @@ -68,3 +67,13 @@ struct zMcause {
extern struct zMcause zmcause, zscause;

extern mach_bits zminstret;

enum kind_zphysaddr { Kind_zphysaddr };
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having to duplicate this sail-internal representation does not sound like a good idea to me. IMO the C callback should just use the underlying bits.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If/when we switch to the struct Model { #include "model.c" } trick then we won't have to do this. But I agree, it's too error-prone until it's actually checked by the compiler.

struct zphysaddr {
enum kind_zphysaddr kind;
union {
struct {
uint64_t zphysaddr;
};
};
};
4 changes: 2 additions & 2 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
},
}
Expand Down Expand Up @@ -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 {
Expand Down
4 changes: 2 additions & 2 deletions model/riscv_sys_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading