search

riscv / sail-riscv

Sail RISC-V model
https://lists.riscv.org/g/tech-golden-model
Other
467 stars 169 forks source link

Use physical addresses for LR/SC reservations #501

Closed Timmmm closed 4 months ago

Timmmm commented 5 months ago

This is how reservation is architecturally defined, how real CPUs are likely to be implemented, and doesn't require spurious cancellations on xRET and traps.

Fixes #360.

github-actions[bot] commented 5 months ago

Test Results

712 tests  ±0   712 :white_check_mark: ±0   0s :stopwatch: ±0s   6 suites ±0     0 :zzz: ±0    1 files   ±0     0 :x: ±0 

Results for commit 585e6ff5. ± Comparison against base commit d96f89b5.

:recycle: This comment has been updated with latest results.

defermelowie commented 4 months ago

This changes the behaviour of sc when address translation fails of an address that has no valid reservation set. In the current model the address translation is omitted and therefore no exception occurs. However after this change, the failing address translation causes an exception. Not sure which behaviour is considered "correct".

At first glance the new behaviour seems to match spike: https://github.com/riscv-software-src/riscv-isa-sim/blob/98d2c29e431f3b14feefbda48c5f70c2f451acf2/riscv/mmu.h#L266

Alasdair commented 4 months ago

I suspect the answer is it's implementation defined what happens. Right now the RISC-V axiomatic memory model in the ISA manual does not specify anything regarding virtual memory.

If we do end up with an axiomatic model with virtual memory, we might need something like load_reservation(vAddr, pAddr) to capture all the allowed behaviors, assuming implementations have a choice in how they implement LR and SC.

Timmmm commented 4 months ago

@billmcspadden-riscv ok this is ready now.