18.1-2RVWMO: The Memory Consistency Model

A memory consistency model is the ISA’s answer to one question: which values may a load return? RVWMO (RISC-V Weak Memory Ordering) answers it weakly — single-hart code appears in-order to itself, but other harts may observe your memory operations in a different order unless one of a short list of rules says otherwise. This is the contract your load/ store unit, store buffer, and cache hierarchy sign. (Scope note: this chapter formalizes regular main memory only — I/O ordering, instruction fetch, FENCE.I, and page-table walks are defined elsewhere and not yet folded into the formalism.)

18.1.1 The vocabulary

An execution has a global memory order global memory order A total order over the memory operations of ALL harts in one execution. RVWMO legality = there exists a global memory order respecting preserved program order and the load-value/atomicity/progress axioms. defined in ch. I·18 — open in glossary : one total order over every hart’s memory operations. Memory instructions give rise to operations — load, store, or (for AMOs) both at once — and every operation is single-copy atomic single-copy atomic Property of every RVWMO memory operation: it can never be observed partially complete by anyone. defined in ch. I·18 — open in glossary : nobody ever sees half of one.

Bookkeeping rules that matter to hardware:

• An aligned instruction of ≤ XLEN bits → exactly one operation. Exceptions: a failed SC generates none; RV32 FLD/FSD may generate several.
• Misaligned accesses (and >XLEN FP accesses) may decompose into byte-granularity components, unordered among themselves — the license that makes trap-and-emulate byte loops legal. Inside a misaligned atomicity granule (PMA), no decomposition happens.
• LR and SC are paired when no other LR/SC sits between them.
• Operations may carry annotations: aq on LR/AMO ⇒ acquire-RCsc, rl on SC/AMO ⇒ release-RCsc; RCpc rcpc/rcsc annotation Acquire/release annotation strengths: RCsc (sequentially-consistent sync ops) is what aq/rl on LR/SC/AMO produce; RCpc (processor-consistent) currently arises only from Ztso's implicit annotations. PPO rules 5-7 define their exact force. defined in ch. I·18 — open in glossary annotations currently arise only from Ztso, but the model is forward-compatible with native load-acquire/store-release instructions.

18.1.2 Syntactic dependencies

RVWMO orders through register dataflow — syntactically, not semantically. j has a syntactic dependency syntactic dependency j depends on i when a source register of j traces (possibly through carrying instructions) to a destination register of i. Address/data/control flavors order memory ops via PPO 9-11. Loads, JALR, LR/SC/AMOs carry NO src->dst dependency; successful SC's rd IS a destination. defined in ch. I·18 — open in glossary on i if a source register of j traces back through the register graph (via instructions that “carry” dependencies) to a destination of i. Three flavors matter: address (feeds an address source register), data (feeds a store’s data register), control (a branch/indirect jump in between depends on i). x0 never participates; the per-instruction fine print (loads/JALR/AMOs carry nothing; a successful SC’s rd is a destination; CSR instructions mirror Table 7) is cataloged in §18.3.

18.1.3 Preserved program order — the 13 rules

The global memory order must respect this subset of each hart’s program order (both operations to regular main memory):

18.1.4 The three axioms

An execution is legal iff a global memory order exists that respects PPO and satisfies:

• Load Value load value axiom Each byte of a load returns the store latest in {stores earlier in global memory order, stores earlier in PROGRAM order} - the second clause architecturally legalizes store-buffer forwarding of the hart's own not-yet-global stores. defined in ch. I·18 — open in glossary : each byte of a load returns the latest store to that byte among (1) stores earlier in the global memory order and (2) stores earlier in program order. Clause (2) is store-to-load forwarding, architecturally blessed: your store buffer may serve a younger load before the store is globally visible.
• Atomicity atomicity axiom For aligned paired LR/SC: if the LR read byte x from store s, no OTHER hart's store to x may sit between s and the SC's write in the global memory order. defined in ch. I·18 — open in glossary : for an aligned paired LR/SC, no other hart’s store to a read byte may intrude between the store the LR read from and the SC’s own store, in the global order.
• Progress progress axiom No memory operation may be preceded by an infinite sequence of operations in the global memory order - stores eventually become visible; spinloops eventually see updates. defined in ch. I·18 — open in glossary : no operation is preceded by an infinite sequence — stores eventually become visible; spin loops eventually observe updates.

Seeing it: message passing

The canonical two-hart test, in both verdicts — step through the executions:

18.2 Dependency granularity through CSRs

Syntactic dependencies thread through CSRs at defined granularities (Table 12): fflags per-bit (bits 4..0 independent), frm whole, fcsr per-field — with the aliasing between them tracked. Read-only CSRs don’t participate. The FP flags are accumulating CSRs accumulating csr A CSR that is both source and destination of an instruction but carries a dependency only from itself to itself - the FP exception flag bits (NV/DZ/OF/UF/NX), so FP ops never serialize on fflags. defined in ch. I·18 — open in glossary : they carry a dependency only from themselves to themselves, so a chain of FP ops does not serialize on the flags register.