Linux Kernel Memory Model LKMM
An axiomatic (cat/herd7) model for the Linux kernel's own concurrency primitives — READ_ONCE/WRITE_ONCE, smp_mb()/smp_rmb()/smp_wmb()/smp_store_release()/smp_load_acquire(), RCU, and locking. Deliberately defined as a weak 'virtual architecture' so that code verified against it is sound on every CPU the kernel supports (x86, ARM, POWER, RISC-V, …). Notably formalises RCU grace-period ordering, which language standards such as C11 do not express.
Properties
Property vector survey-sourced — from Tables 1–2 of the Moiseenko et al. survey, except cells that cite a specific source.
- Compilation optimal mapping to
- yes x86
- yes POWER
- yes Armv7
- yes Armv8
- Reordering sound
- yes Store→Load
- yes Store→Store
- yes Load→Load
- yes Load→Store
- Other local transformations
- no Trace preserving
- no Common subexpr. elim.
- Reasoning guarantees
- yes Coherence
- yes No undefined behaviour
- no In-order execution
- yes No out-of-thin-air
- Atomicity guarantees
- no Multicopy atomic
Ordering relationships
- Strictly weaker than
- Sequential Consistency (SC) — LKMM permits reorderings of plain and *_ONCE accesses (e.g. store-buffering, SB) that SC forbids; DRF-style synchronisation must be requested explicitly with smp_mb() and friends. See litmus/strictly-weaker/SC-vs-LKMM.
- Compiles correctly to
- x86-TSO — Linux kernel primitives compile correctly to x86; LKMM is designed to be no stronger than the hardware it runs on.
- ARMv8 / AArch64 Memory Model — Linux kernel primitives compile correctly to ARMv8/AArch64.
- IBM POWER Memory Model — Linux kernel primitives compile correctly to IBM POWER.
- RISC-V Weak Memory Ordering (RVWMO) — Linux kernel primitives compile correctly to RISC-V (RVWMO).
- Incomparable with
- C11/C++11 Memory Model — Neither contains the other: LKMM provides RCU grace-period ordering and the smp_* barrier family with no C11 counterpart, while C11 offers per-object seq_cst atomics LKMM does not model. The incomparability is at the level of primitives, not reorderings of shared operations. See litmus/incomparable/C11-vs-LKMM.
- Operational Happens-Before Model (OHMM) — Both are syntactic-dependency-preserving models that forbid thin-air by respecting syntactic dependencies, but over different primitives (Linux-kernel barriers vs a JMM-style happens-before machine); neither subsumes the other.
References
- Jade Alglave, Luc Maranget, Paul E. McKenney, Andrea Parri, Alan Stern. Frightening Small Children and Disconcerting Grown-ups: Concurrency in the Linux Kernel. ASPLOS 2018, 2018. doi:10.1145/3173162.3177156