search

riscv / riscv-isa-manual

RISC-V Instruction Set Manual
https://riscv.org/
Creative Commons Attribution 4.0 International
3.71k stars 644 forks source link

Question and Bug about "Atomicity Axiom Rule" in RVWMO Explanatory Material, Version 0.1 #1731

Closed diantaowang closed 4 days ago

diantaowang commented 6 days ago

In the latest unprivileged version (riscv-isa-release-b796659-2024-11-14), there is a bug in Figure 4 of A.3.3. Atomicity axiom.

The wrong picture is as follows:

fig4_err

The right picture should be:

fig4_right

Before fix it, I have a question about the fourth code snippet in the above figure. The original text (in A.3.3. Atomicity axiom) in the specification is as follows:

For example, the SC instructions in [litmus_lrsdsc] may (but are not guaranteed to) succeed. None of those successes would violate the atomicity axiom, because the intervening non-conditional stores are from the same hart as the paired load-reserved and store-conditional instructions.

Why the SC instruction in code snippet as follow may sucessed? Obviously, the memory accessed by the SC instruction is not included in the reserved set of the LR instruction. I think the SC instruction must be failed, not likely to succeed.

(a) lr.w a0, 0(s0)
(b) sw t1, 4(s0)
(c) addi s0, s0, 8
(d) sc.w t3, t2, 0(s0)

Thanks!

aswaterman commented 5 days ago

Please submit a PR that fixes the table. Thank you in advance!

As to your question, the SC might succeed on some implementations, because the LR is allowed to reserve more memory than a single word. (For example, some implementations might reserve the whole cache line and ignore the cache line offset LSBs, so an SC to any word on the same cache line might succeed.) On other implementations, the SC might always fail. So, the text describing this example is correct.