Memory Systems · Cluster
Memory Modeling
Formal models of reads, writes, and ordering.
- 01 Sequential Consistency as the Reference Memory Model Lamport's two conditions, the executions they exclude, and why every weaker model is described by which of those exclusions it gives up.
- 02 Store Buffers and the x86-TSO Model How a per-core write buffer leaves store-load as the only program-order pair that may invert, why forbidding it would defeat the buffer, and what a locked instruction orders.
- 03 Happens-Before and the Definition of a Data Race How sequenced-before and synchronizes-with compose into a partial order, why a race is a pair of unordered conflicting accesses, and what the standard does once one exists.
- 04 Coherence and the Modification Order of a Single Location The four coherence axioms, why per-location agreement is much weaker than a global order, and how IRIW separates the two.
- 05 Release, Acquire, and the Synchronizes-With Edge What an acquire load is forbidden to move above, what a release store is forbidden to move below, and why the edge is directional rather than a barrier.
- 06 The DRF-SC Guarantee and What It Buys a Programmer Why race-free programs are sequentially consistent on hardware that is not, and the composition rules that let this promise survive layers of abstraction.
- 07 Litmus Tests as Executable Specifications How a five-line concurrency test becomes a machine-checkable claim, what the litmus file format encodes, and how a model checker decides which outcomes are forbidden.
- 08 Dependencies, RCsc, and RCpc Acquire on ARMv8 How address and data dependencies order accesses without a barrier, and why ARMv8.3 added a second, cheaper form of acquire load alongside the original one.
- 09 Causality and Out-of-Thin-Air Values in the Java Model Why the Java Memory Model needed a causality order rather than happens-before alone, and how the happens-before consistency rules leave room for a value with no writer.
- 10 The Linux Kernel Memory Model and Its Tooling How LKMM formalises READ_ONCE, smp_mb, and RCU into an executable model, what its relation set adds to the architecture models, and where it deliberately diverges from C11.