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

Improve store-conditional speculative failures and exception priority #681

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

Improve store-conditional speculative failures and exception priority #681

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
82 changes: 44 additions & 38 deletions model/riscv_insts_aext.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,52 +115,58 @@ function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
// This is checked during decoding.
assert(width_bytes <= xlen_bytes);

if speculate_conditional () == false then {
/* should only happen in rmem
* rmem: allow SC to fail very early
*/
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
/* normal non-rmem case
* rmem: SC is allowed to succeed (but might fail later)
*/
/* Get the address, X(rs1) (no offset).
* Extensions might perform additional checks on address validity.
*/
match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(virtaddr_bits(vaddr), width))
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
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, _) => {
// Check reservation with physical address.
if not(match_reservation(physaddr_bits(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 },
MemValue(_) => {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
MemValue(true) => { X(rd) = zero_extend(0b0); cancel_reservation(); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = zero_extend(0b1); cancel_reservation(); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL }
// Get the address, X(rs1) (no offset).
// Extensions might perform additional checks on address validity.
let res : Retired = match ext_data_get_addr(rs1, zeros(), Write(Data), width_bytes) {
Ext_DataAddr_Error(e) => { ext_handle_data_check_error(e); RETIRE_FAIL },
Ext_DataAddr_OK(vaddr) => {
if not(is_aligned(virtaddr_bits(vaddr), width))
then { handle_mem_exception(vaddr, E_SAMO_Addr_Align()); RETIRE_FAIL }
else {
// Write and ReadWrite are equivalent here:
// both result in a SAMO exception.
match translateAddr(vaddr, Write(Data)) {
TR_Failure(e, _) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
TR_Address(addr, _) => {
// Explicitly do access checks first in case the memory does
// not exist or doesn't support LR/SC. Without this check we
// may get a spurious failure (see below) for LR/SC to memory
// that should cause an access fault.
let typ = Write(default_write_acc);
let priv = effectivePrivilege(typ, mstatus, cur_privilege);
match phys_access_check(typ, priv, addr, width_bytes) {
Some(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
None() => {
if not(speculate_conditional()) | not(match_reservation(physaddr_bits(addr))) then {
// Spurious failure (this is allowed), or the reservation
// address does not match.
X(rd) = zero_extend(0b1); RETIRE_SUCCESS
} else {
match mem_write_ea(addr, width_bytes, aq & rl, rl, true) {
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
MemValue(_) => {
let rs2_val = X(rs2);
match mem_write_value(addr, width_bytes, rs2_val[width_bytes * 8 - 1 .. 0], aq & rl, rl, true) {
MemValue(true) => { X(rd) = zero_extend(0b0); RETIRE_SUCCESS },
MemValue(false) => { X(rd) = zero_extend(0b1); RETIRE_SUCCESS },
MemException(e) => { handle_mem_exception(vaddr, e); RETIRE_FAIL },
}
}
}
}
}
},
}
}
}
}
}
}
};
// The spec says "Regardless of success or failure, executing an SC
// instruction invalidates any reservation held by this hart", however
// "failure" here does not include failure due to exceptions.
// See https://github.com/riscv/riscv-isa-manual/issues/1010
if res == RETIRE_SUCCESS then cancel_reservation();
res
}

mapping clause assembly = STORECON(aq, rl, rs2, rs1, size, rd)
Expand Down
Loading