riscv-isa-manual
riscv-isa-manual copied to clipboard
riscv
Add initial value of Figure A.13
Thanks @laokz.
ACK the first change about the missing initial condition.
NACK the second change. That text is attempting to explain an MMIO variant of message passing (MP). It's trying to say this: if the remote I/O device accesses 0(a0) after the MMIO write from the original thread to 0(a1) propagates to the remote device, then that remote device's subsequent load of the address that the original thread has in 0(a0) will see the value written by the original thread's earlier store to 0(a0). Does that make sense? Feel free to suggest another rewording that would make that clearer if you'd like.
NACK the second change. That text is attempting to explain an MMIO variant of message passing (MP). It's trying to say this: if the remote I/O device accesses 0(a0) after the MMIO write from the original thread to 0(a1) propagates to the remote device, then that remote device's subsequent load of the address that the original thread has in 0(a0) will see the value written by the original thread's earlier store to 0(a0). Does that make sense? Feel free to suggest another rewording that would make that clearer if you'd like.
Cleared. Sorry for my poor English and how should I withdraw the 2nd commit?
Figure A.4 last code snippet typos:
(a) lr.w a0, 0(s0)
(b) sw t1, 4(s0)
(c) sc.w t2, 8(s0) # 8 ==> 0, but duplicate with code 3
Is this for another non-overlapping scenario with different LR/SC size, such as: lr.d / sw / sc.w ?
The last example in Figure A.4 is covered by the two paragraphs that follow it: neither address mismatch nor intervening stores from the same thread technically force the SC to fail. Both scenarios should be rare, but some implementations will benefit from not being forced to cause the SC to fail.
Then it can be fixed as:
(a) lr.d a0, 0(s0)
(b) sw t1, 4(s0)
(c) sc.w t0, t2, 0(s0)
With LR/SC different access size, SC's address within reservation set, and SW non-overlapping, SC still might succeed.
Every other instruction (c) should also adds a rd operand, e.g. t0, because SC needs 3 registers(thanks for @sorear's hint).
Figure A.20 (h)'s a2 should be t1?
Should Figure A.21 (f)'s a2 be t1 and Outcome a0=1?
"Multi-copy atomicity" is an important characteristics. It eliminates the weird "causality" "cumulativity" concerns. Can we explicitly declare it in chapter 14 instead of just mentioning in appendix?
https://github.com/riscv/riscv-isa-manual/blob/master/src/memory-model-herd.tex#L43 lost a '|'?
In Figure A.18 'RVWMO Mapping', by rule4(fence): (a) ->ppo (c), rule1(same-address store): (c) ->ppo (d), rule5(acquire) : (d) ->ppo (e). How can (a), (e) be reordered?
If (d) changed to 'LR/SC Mapping', done.
Thanks for the continued typo hunting.
Figure A.4: yes, all of the sc instructions are missing an operand, thanks. However, the last example intentionally shows 8(s0) rather than 0(s0) to show that the sc may (but is not required to) succeed even if the address is different.
Figures A.20: yes, a2 should become t1, thanks. There seem to be other discrepancies in A.21 as well, if I compare these to the versions that were actually tested (even after accounting for some of the purely cosmetic differences, and the use of address vs. data dependencies): https://github.com/litmus-tests/litmus-tests-riscv/tree/master/tests/mixed-size/HAND.
The term "multi-copy atomicity" isn't used in Chapter 14 because it isn't needed. The normative definition in chapter 14 is self-contained and complete even without the term. That's why it's left to the appendix.
https://github.com/riscv/riscv-isa-manual/blob/master/src/memory-model-herd.tex#L43: yes, this lost a "|", thanks.
Figure A.18: right, one of the few cases that doesn't work is when fence rw,w is paired with an LR/SC pair with .aq.
8(s0) is not a legal operand for the sc instruction, though. IMO the examples are fine, they just need to be more clearly marked as pseudo-code.
@sorear's opinion also looks good to me then I leave A.4 untouched and so does "memory-model-herd.tex", others committed.
Couldn't figure out "other discrepancies", but "in-order commit" issue is really hard to understand(https://stackoverflow.com/questions/39670026/out-of-order-instruction-execution-is-commit-order-preserved, https://stackoverflow.com/questions/52215031/how-is-load-store-reordering-possible-with-in-order-commit).
Changes moved to this PR - https://github.com/riscv/riscv-isa-manual/pull/1293
