Improve store-conditional speculative failures and exception priority #681
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
@Alasdair if you could shed any light on what rmem is expecting here that would be great! |
Timmmm
force-pushed
the
user/timh/store_conditional_tweak
branch
from
55e8a23 to
e2f1189
Compare
arichardson
reviewed
Jan 10, 2025
model/riscv_insts_aext.sail
Outdated
| 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. |
There was a problem hiding this comment.
I know this was only moved around, but the indentation looks odd.
There was a problem hiding this comment.
Ah ha that is due to a slight bug in the VSCode "sticky tabs" option I use. It more or less makes stupid space-based indentation act as if glorious tabs had been used instead, but it seems like increasing/decreasing indentation on lines with incomplete "tabs" doesn't quite work correctly (technically my fault because I implemented that feature).
I changed it to line comments which I think are just better anyway.
Timmmm
force-pushed
the
user/timh/store_conditional_tweak
branch
from
e2f1189 to
551485c
Compare
1. Move `speculate_conditional()` to the same place as `match_reservation()`. I am not 100% sure about this change because I'm not sure what rmem is (and it has a comment about allowing it to fail very early), but it doesn't make sense to me that SC could spuriously fail in a place where it shouldn't be allowed in the sequential model. Codasip uses `speculate_conditional()` to force spurious SC failures into the model (so it matches the DUT), and this is the right place for that use. 2. Do an explicit access check before checking the reservation. Without this you never get an access fault for accesses to memory that doesn't exist or doesn't support LR/SC. 3. Move `cancel_reservation()` to the end of the function. This doesn't change any functionality, I think it's just clearer and makes it obvious that the omission of `cancel_reservation()` in the `MemException(e)` branch was not a mistake.
Timmmm
force-pushed
the
user/timh/store_conditional_tweak
branch
from
551485c to
1e52b56
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
speculate_conditional()to the same place asmatch_reservation(). I am not 100% sure about this change because I'm not sure what rmem is (and it has a comment about allowing it to fail very early), but it doesn't make sense to me that SC could spuriously fail in a place where it shouldn't be allowed in the sequential model.Codasip uses
speculate_conditional()to force spurious SC failures into the model (so it matches the DUT), and this is the right place for that use.Do an explicit access check before checking the reservation. Without this you never get an access fault for accesses to memory that doesn't exist or doesn't support LR/SC.
Move
cancel_reservation()to the end of the function. This doesn't change any functionality, I think it's just clearer and makes it obvious that the omission ofcancel_reservation()in theMemException(e)branch was not a mistake.