The DRF-SC Guarantee and What It Buys a Programmer

A program with no data races behaves, on any conforming implementation, exactly as it would on a machine that executes one memory operation at a time in a single global order. This is the single most consequential theorem in the design of shared-memory languages, because it lets the hardware reorder aggressively while the majority of programs never need to know.

The theorem is called DRF-SC: data-race-free programs get sequential consistency. It is not a hardware property and not a compiler property alone; it is a contract with three parties, and the reason it holds is that each party is responsible for a different piece of the argument.

The statement, precisely

A program is data-race-free if, in every execution, every pair of conflicting accesses — same location, at least one a write — is ordered by happens-before. The guarantee says: if a program is data-race-free and all its synchronisation is implemented with operations whose semantics include the required ordering, then the set of outcomes the program can produce is a subset of the outcomes it would produce under sequential consistency.

Two qualifiers matter. “Subset” rather than “equal” leaves room for implementations to be more restrictive than necessary, which they are entitled to be. And the guarantee is about the program, not about individual operations: a race-free program is SC as a whole, and a program with one race has no guarantee anywhere, because undefined behaviour is not localised.

The contrapositive is the useful form in practice. If a program produces an outcome that sequential consistency forbids, the program contains a race. That is a complete diagnostic, and it is why litmus tests work: an impossible outcome is proof of a missing edge.

The three-part argument

The proof is a composition of three claims, each of which is a separate obligation.

The compiler preserves the edges. The compiler may reorder non-atomic accesses freely, but it must not reorder them across a synchronisation operation in a way that removes an edge the source program had. Concretely, a non-atomic store sequenced before a release store must remain before it in the emitted code, or the compiler must emit a barrier that restores the order. This is why release and acquire are compiler-level concepts as much as hardware ones: they constrain the optimiser, not just the memory system.

The hardware preserves the edges. Each ordering the source uses must be mapped onto an instruction sequence that the target memory model accepts as providing that ordering. A release store on a machine with a store buffer becomes a store preceded by a barrier, or a store-release instruction. A relaxed atomic becomes a plain load or store with no barrier.

The hardware’s own model is at least as strong as its synchronisation primitives claim. If a release store and an acquire load that reads it are documented to order prior writes before subsequent reads, then the machine must actually provide that ordering, on pain of a hardware bug. The TSO model and the per-location coherence axioms are the vocabulary in which those claims are made.

Given the three, an execution of the compiled program has all the happens-before edges the source had, so its conflicting accesses are all ordered, so it is indistinguishable from some sequential execution. The chain is only as strong as its weakest link, and the interesting failures in practice are almost always in the first link.

Why the compiler link is the fragile one

Boehm’s 2005 argument that threads cannot be implemented as a library turns on exactly this point. A compiler that does not know about threads will happily treat a call to pthread_create as an opaque function that cannot affect local variables, and will then cache a value in a register across the call. The thread it creates may write that value. The result is a program that is racy by the language’s definition — the library implementation never created the happens-before edge the source intended, because the source had no way to express it.

This is why the concurrency model had to go into the language rather than into a library. Only the compiler can decide that an access must not be cached, hoisted, or eliminated, and only the compiler can know which accesses are atomic. The same reasoning explains the standard’s insistence that a non-atomic access concurrent with an atomic one is undefined: there is no way for the compiler to emit code that is correct for both.

The practical form of the constraint is that every synchronisation primitive must be visible to the optimiser as a synchronisation primitive. A hand-written spinlock using inline assembly may work on one compiler version and break on the next, because the compiler was never told what the assembly meant. atomic_thread_fence exists to give the compiler that information without a hardware instruction when none is needed.

Composition, and where it fails

DRF-SC is a guarantee about whole programs, and it does not compose automatically across abstraction layers. A correct implementation of a queue on top of atomics is a data-race-free program; a program that uses the queue is also data-race-free if the queue’s operations provide the edges its interface promises. The obligation is on the implementer to document and provide those edges, and on the user to rely only on them.

The failure mode is an interface that provides fewer edges than its users assume. A “thread-safe” container that uses relaxed atomics internally for its own bookkeeping is fine, as long as the operations it exposes still create the happens-before edges callers need. A container that exposes a “get” returning a pointer to internal storage without an acquire edge is not, and the resulting races appear in the caller’s code, far from the container.

Layered abstractions fail in a second way: an implementation that is correct but whose correctness argument depends on the hardware being stronger than the language requires. A lock-free algorithm proved correct on x86 may rely on a property x86 provides and a weaker architecture does not — that stores from one core are seen in the same order by every other core, for instance, or that a store followed by a load can only invert in the one way the store buffer permits. The proof is then valid on x86 and invalid elsewhere. The ARMv8 model permits reorderings that make such code fail, and the failure is a genuine bug in the algorithm rather than in the machine.

What the guarantee does not cover

Three exclusions are worth stating plainly.

It does not cover accesses that are ordered by something other than the language’s synchronisation. A program that uses volatile as a flag, or that relies on a signal handler, or that uses a memory-mapped device register, is outside the model. The rules for those cases come from the platform, and they are usually stricter — a device access may need a full fence for reasons that have nothing to do with other threads.

It does not cover programs whose races are benign in the programmer’s judgement. “Benign” races — a statistics counter incremented without atomics, a flag read for a heuristic — are still undefined behaviour, and the compiler’s optimisations are entitled to break them. The fix is to make the access relaxed-atomic, which costs the atomicity but not the ordering, and which is usually enough.

It does not extend to code compiled with different assumptions in different translation units. If one file is compiled with the concurrency model and another is compiled as single-threaded, the guarantee is void for the pair. This is a real source of bugs in code that mixes precompiled libraries with newer builds, and it is a reason the model is specified at the language level rather than left to flags.

Why weaker hardware does not weaken the promise

The guarantee is often misread as a statement that weak hardware is safe. It is not: weak hardware is safe for race-free programs, and the whole point of the model is that the programs which are not race-free have no promise at all. On a machine that reorders everything, a race-free program still behaves sequentially, because its edges are implemented with fences that the machine honours. The fences are what convert the weak machine into an SC machine for that program.

This is Adve and Hill’s weak ordering definition in its modern form: a model is weakly ordered if it appears sequentially consistent to any program without data races. The definition is a specification of what the hardware must do, not a description of what it does internally, and it is the reason a machine can be both aggressively reordered and correct.

The remaining question, taken up in litmus tests as executable specifications, is how to check that a proposed model actually satisfies the definition — which reorderings it permits, and whether any of them can be observed by a race-free program.