The Linux Kernel Memory Model and Its Tooling

The Linux kernel has to run on x86, ARMv8, Power, RISC-V, and a long tail of others, and its concurrency primitives have to mean the same thing on all of them. That is a harder problem than specifying a language, because the kernel cannot assume a compiler that understands its primitives and cannot assume the hardware provides more than the weakest supported architecture. The answer the kernel community arrived at is a formal model, maintained in the source tree, that defines what READ_ONCE, smp_mb, and rcu_dereference mean and that can be executed against test programs.

The model is called LKMM, for Linux Kernel Memory Model, and it lives in tools/memory-model alongside a translation layer that feeds litmus tests to the herd7 checker.

Why the kernel needed its own model

A language-level model is written for programs the compiler can see through. The kernel’s code is different in three ways that matter.

First, the primitives are macros and inline functions, not language keywords. READ_ONCE expands to something involving a volatile cast and a dependency-preserving access; the compiler has no built-in knowledge that it means “read this exactly once, with no tearing and no invented reloads”. The semantics have to be defined by the kernel and implemented by the macro.

Second, the kernel needs orderings the language does not provide. The C11 model has no equivalent of smp_mb__after_atomic, no equivalent of rcu_dereference, and no notion of a barrier that orders only against other threads in the same shareability domain. The kernel’s primitives encode assumptions about the architecture that the language model abstracts away.

Third, the kernel’s correctness arguments are made by people who need to reason about specific instruction sequences on specific machines. A model that says “the implementation may do anything not forbidden” is not usable for that. LKMM is written to be checkable against the actual code generation, and the translation layer exists so that a litmus test written in kernel primitives can be run against the architecture model of the machine the kernel is compiled for.

The primitive set

LKMM defines a small vocabulary, and the whole model is expressed in terms of it.

READ_ONCE and WRITE_ONCE are the base case: a single access that the compiler must not split, duplicate, or eliminate. They provide no ordering. Their purpose is to stop the compiler from doing something the programmer did not ask for, and they are the primitive on which the rest is built.

smp_mb is a full barrier for inter-processor ordering. smp_rmb and smp_wmb are the one-directional variants, ordering reads against reads and writes against writes respectively. Their weaker form is the point: on many architectures a read-read barrier compiles to nothing. Using the full barrier where a one-directional variant already suffices is then a performance cost rather than a correctness one — the reverse substitution, a narrow barrier where the full one is needed, is a bug.

smp_store_release and smp_load_acquire are the release and acquire pair, mapping to STLR and LDAR on ARMv8 and to a plain store or load on x86. The release-acquire semantics are the same as in the language model, but the kernel’s versions are defined in terms of the kernel’s own relation set.

smp_mb__before_atomic and smp_mb__after_atomic exist because atomic read-modify-write operations have ordering properties of their own, and a barrier adjacent to one may be redundant or may need to be a different barrier depending on the architecture. On x86 a LOCK-prefixed instruction is a full barrier, so smp_mb__after_atomic is a no-op there; on a machine with a weaker atomic implementation it may not be.

rcu_dereference is the dependency-ordered load. Its guarantee is that the value it returns is loaded once, and that subsequent accesses through the returned pointer are ordered after the load by the dependency, without a barrier. It is the primitive the ARMv8 dependency rules make free, and it is the one most dependent on the compiler preserving the dependency.

The relation set, and what it adds

LKMM is an axiomatic model in the same style as the architecture models: it defines relations over events and a set of constraints, and an execution is allowed if a candidate satisfies all of them. The relations include the expected ones — program order, reads-from, modification order — and several the architecture models do not have.

The from-read relation (also called reads-before) connects a read to every write that follows the write it read in the modification order. It is the standard way to express “this read happened before that write became visible” without needing a global order, and it is what makes the coherence axioms expressible as constraints on a graph rather than as temporal statements.

The barrier relations are defined per barrier type. smp_mb contributes edges from every event before it to every event after it, in both directions; smp_rmb contributes only read-to-read edges; smp_wmb only write-to-write. The asymmetry is the model’s whole content: the constraints differ only in which events the barrier relates.

The RCU relations are separate. A grace period is not a barrier and is not ordered like one; the model defines a relation between the end of a grace period and the accesses of readers that started before it, and the constraint is that a reader’s critical section must not overlap a grace period in a way that lets a freed object be observed. This is the hardest part of the model to state, and the one where the kernel’s semantics diverge most from any language model.

Reading a kernel litmus test

A test written in kernel primitives looks like the architecture tests but uses the macros, and the tooling translates it into the herd7 input format.

C MP+release-acquire

{
    int x = 0;
    int y = 0;
}

P0(int *x, int *y)
{
    WRITE_ONCE(*x, 1);
    smp_store_release(y, 1);
}

P1(int *y, int *x)
{
    int r0;
    int r1;

    r0 = smp_load_acquire(y);
    r1 = READ_ONCE(*x);
}

exists (1:r0=1 /\ 1:r1=0)

The exists clause names the outcome the test asks about: thread 1 read the flag as set and the data as stale. The release store orders the WRITE_ONCE before the flag, and the acquire load orders the later READ_ONCE after the flag, so the model reports this outcome as unreachable. Replacing smp_store_release with a plain WRITE_ONCE removes the first edge, and the outcome becomes reachable — which is what makes the test useful, since the pair of runs localises the ordering to the one primitive that changed.

The translation layer handles the C dialect, the macro expansion, and the mapping onto the target architecture’s instruction set. The output is a litmus file in the same format used for the architecture models, and from there the checking is identical: enumerate candidates, test the axioms, report whether the assertion is reachable.

Deliberate divergences from C11

LKMM is not a subset of the C11 model, and the differences are instructive.

C11’s memory_order_relaxed gives an atomic access with no ordering, and the model constrains what value a relaxed read may return through the coherence rules on the object’s modification order. LKMM’s READ_ONCE and WRITE_ONCE are a different construction: single-copy accesses whose main purpose is to constrain the compiler, not to participate in an atomic ordering. The model treats them as plain reads and writes with the compiler-level constraints attached. The distinction matters because kernel code mixes READ_ONCE with explicit barriers, in ways that have no C11 counterpart.

C11’s fences are defined by the ordering they establish, not by the direction of the accesses they pass. LKMM instead exposes the directional barriers that hardware actually provides — smp_rmb for read-read order, smp_wmb for write-write — because a kernel that needs only one direction should not pay for both. On an architecture where a read-read barrier costs nothing, smp_rmb compiles to nothing, and that economy is visible in the model’s relation set rather than buried in an implementation detail.

C11’s out-of-thin-air rules and LKMM’s causality treatment differ in form. LKMM inherits the architecture models’ approach — the coherence and atomicity axioms plus the per-architecture ordering — rather than the language model’s commitment-sequence construction. The result is a model that is more directly checkable against hardware, and the trade is that its treatment of exotic relaxed-atomic cases is not identical to the language’s.

Where the model is enforced

The model is a specification, and the kernel’s actual behaviour is whatever the compilers emit. The enforcement mechanisms are the barrier documentation, which states the rules in prose with the model as the reference, and the test suite, which is run against the model when primitives change. A patch that adds a primitive or changes a macro is expected to come with litmus tests demonstrating its semantics, and the tests are checked into the tree.

The remaining gap is the compiler. READ_ONCE and WRITE_ONCE are defined to constrain the optimiser, and rcu_dereference relies on the optimiser preserving a dependency it cannot see the purpose of. The kernel’s answer is a set of macros written to be optimisation-resistant, plus a body of experience about which constructs compilers break. That is an engineering answer rather than a formal one, and it is the reason the dependency annotations exist: the hardware guarantee is only as strong as the compiler’s willingness to leave the dependency in place.