Memory Model
summary
RISC-V defines an RVWMO memory model with axiomatic and operational models side-by-side, a concrete litmus example (message passing) and a practical justification: store buffers explain TSO behavior and loads may forward from buffers. The spec lists 13 preserved-program-order rules (address/data/control deps, fences, release/ acquire RCsc behavior), atomicity and progress axioms, and separates extensions ZAM and ZTSO. The spec is published, tools are ported to RISC-V, and the document is currently up for ratification.
AI-written summary · about
chapters (16)
- 0:00Intro
- 1:03OUTLINE
- 1:47WHAT IS A MEMORY CONSISTENCY MODEL?
- 3:40A WIDE RANGE OF MEMORY MODELS
- 8:10ARCHITECTURE VS. MICROARCHITECTURE
- 10:38OPERATIONAL VS. AXIOMATIC In modern practice, at ISA level, two common modeling approaches: Axiomatic: define a set of criteria ("axloms") to be satisfied
- 12:08SEQUENTIAL CONSISTENCY CLAMPORT 701 Axiomatic
- 16:53ADDING A STORE BUFFER
- 19:04TOTAL STORE ORDERING (SPARC, X86, RVTSO)
- 20:42RISC-V WEAK MEMORY ORDERING (RVWMO)
- 24:37PPO RULES 5-7
- 25:33PPO RULES 9-11
- 27:45PPO RULE 2
- 30:22PROGRESS AXIOM
- 30:44MEMORY MODEL ISA EXTENSIONS
- 31:04ONGOING/FUTURE WORK
related talks
23mMemory Consistency Model Status Update
01h 02mThe Two Memory Models
21mWeak Memory Demands Model-based Compiler Testing
16mModel Checking for a Multi-Execution Memory Model
01h 11mProgramming language memory models: Problems, solutions, and directions
59mA Relaxed Guide to memory_order_relaxed
14mMaking Weak Memory Models Fair
16mCompound Memory Models