Appendix A is the spec’s own commentary on ch. 18 — informal, example-driven, explicitly non-normative (ch. 18 wins any disagreement). For a hardware designer it’s the most valuable prose in Volume I: it explains why each rule has the shape it has, usually in terms of the microarchitecture it’s protecting.
A.1 Why weak?
Weak models buy implementation freedom (performance, power, scalability, verification simplicity of the hardware); strong models buy simpler programming. RVWMO — a release-consistency variant — sits deliberately between. The compatibility arithmetic every designer should know: RVWMO code runs correctly on Ztso hardware (its fences become fetch-only no-ops); TSO-assuming code is NOT correct on RVWMO hardware — and most RVWMO implementations should simply refuse RVTSO-only binaries.
A.2 Litmus notation
Conventions: s0,s1,s2 hold disjoint 8-byte-aligned addresses x, y,
z; everything else starts zero. Execution diagrams use the standard
edge vocabulary rf/co/fr edges Litmus-diagram relations: rf = reads-from (store to the loads returning its value), co = coherence (total order of stores per address), fr = from-reads (load to co-successors of its source store). With ppo/fence/addr/ctrl/data they constrain the global memory order.
defined in ch. I·A — open in glossary
:
| Meaning | |
|---|---|
| rf | Reads From — store → loads returning its value (cross-hart rf constrains the global order; intra-hart rf is informative only) |
| co | Coherence — the total order of stores to each address |
| fr | From-Reads — load → stores that are co-successors of its source store |
| ppo / fence / addr / ctrl / data | Preserved program order and its causes |
A suite of 7000+ machine-checked tests lives at github.com/litmus-tests/litmus-tests-riscv — run them against your RTL.
A.3.1–A.3.2 “Performing”, and why forwarding shapes the axiom
A load performs when its return value is determined; a store performs when globally visible — not when it executes in the pipeline. The global memory order is the order of performing. That’s why a younger load can perform before an older same-address load yet return a newer value: forwarding from the store buffer.
The canonical demonstration — both harts see their own store early:
Hart 0
- li t1, 1
- (a) sw t1,0(s0)
- (b) lw a0,0(s0)
- (c) fence r,r
- (d) lw a1,0(s1)
Hart 1
- li t1, 1
- (e) sw t1,0(s1)
- (f) lw a2,0(s1)
- (g) fence r,r
- (h) lw a3,0(s0)
The PPOCA variant goes further: a control-dependent store may forward to a later load speculatively, before the branch resolves — permitted, because the speculation is confirmed before anything becomes architecturally visible.
A.3.3 Atomicity, decoupled from ordering
RISC-V atomics impose no ordering by default — that’s what aq/rl are for. The atomicity axiom is purely about exclusivity: no other hart’s store to a byte the LR read may sit between that byte’s source store and the SC’s write. Explicitly allowed between an LR/SC pair: loads from anywhere, stores from the same hart, stores to non-overlapping bytes. Table 79’s four snippets (same-hart stores next to the reserved word) may all succeed — deliberately, so cache-line-granularity reservation tracking never fails SCs on false sharing. Conceptual split: AMOs perform “in memory”; LR/SC bring the value up under a reservation.
A.3.4 Progress, minimally
Stores become visible in finite time; spinloops eventually observe unlocks. Nothing more — no fairness, no latency, no QoS (that’s platform territory). Any standard coherence protocol satisfies it for free.
Hardware Designer Notes
Read the axioms as the interface of your LSU: performing = global visibility, forwarding = the sanctioned exception, atomicity = exclusivity only, progress = drains and snoops can’t stall forever. The next pages turn each PPO rule into its microarchitectural rationale.
Minimal Linux-boot hart MUST
- Enforce multi-copy atomicity: never forward one hart's buffered store to another hart
- Track LR/SC atomicity per the axiom — but feel free to track reservations at cache-line granularity
- Run the public litmus suite against RTL — it is the executable form of this appendix
MAY simplify / trap-and-emulate
- Forward buffered stores to your own younger loads (the axiom clause exists for you)
- Let control-dependent stores forward speculatively to later loads (PPOCA) if recovery is airtight
- Refuse TSO-only binaries rather than pretend
Check yourself — axioms in practice
1.Can a Ztso (TSO-by-default) core run binaries compiled for RVWMO? And vice versa?
2.Why would adding 'store before later same-address load' to PPO (the appendix's hypothetical Rule X) be catastrophic?
3.An ordinary store from the same hart sits between an LR and its SC, hitting the same cache line but not the reserved word. May the SC succeed?
4.What exactly does the progress axiom promise a spinlock?