vault

Data-Race-Free Programs and the DRF-SC Theorem

15 min read

Data-Race-Free Programs and the DRF-SC Theorem

The DRF-SC theorem — read “data-race-free implies sequential consistency,” and also written SC-for-DRF — is the central bargain of every modern shared-memory programming language. It states: if a program contains no data race when its executions are analyzed under sequential consistency, then every actual execution of that program on real relaxed hardware is guaranteed to behave as if it were sequentially consistent — that is, as some simple interleaving of the threads’ operations with no reordering visible. In exchange, the moment a program does contain a data race, the language withdraws all guarantees to a greater or lesser degree: C++ declares the behavior undefined (anything may happen), while Java merely declares it weird-but-bounded. The idea was crystallized by Sarita Adve and Mark Hill in “Weak Ordering — A New Definition” (International Symposium on Computer Architecture, ISCA 1990) and, in its programmer-facing “data-race-free-0” form, by Adve and Kourosh Gharachorloo’s tutorial (Adve & Gharachorloo 1996). It is the reason a working programmer can reason about locks and mutexes as if memory were simple, even though the CPU and compiler beneath are aggressively reordering everything (Cox, “Programming Language Memory Models”).

Mental Model — a contract with two clauses

The best way to hold DRF-SC in your head is as a contract between you and the language implementation, with obligations flowing both ways. You promise one thing: you will fully synchronize every conflicting access to shared data — every pair of accesses where at least one is a write is separated by some synchronization (a lock, an acquire/release atomic, a channel send/receive). In return, the implementation promises something enormous: it will hide the entire terrifying machinery of store buffers, out-of-order execution, speculative loads, and compiler code motion, and present you a world that looks like sequential consistency — one global order, program order preserved per thread. Break your half of the contract — leave one conflicting access unsynchronized — and the implementation is released from its half.

flowchart TD
    START["Your program"] --> Q{"Any data race<br/>under SC analysis?"}
    Q -- "No (fully synchronized)" --> SC["Guaranteed SC behavior:<br/>reason as simple interleaving.<br/>Hardware/compiler reorderings<br/>are invisible to you"]
    Q -- "Yes (a conflicting<br/>access is unsynchronized)" --> RACE{"Which language?"}
    RACE -- "C, C++, Rust, Swift" --> UB["Undefined behavior:<br/>'DRF-SC or catch fire'.<br/>Compiler may assume<br/>the race never happens"]
    RACE -- "Java, JavaScript, Go" --> BOUND["Bounded but weird:<br/>no SC, but memory safety<br/>and type safety preserved;<br/>values from thin air excluded"]

What the diagram shows and the insight to take: the single branch point — is there a data race? — determines your entire universe. On the “no” branch you get to think in the intuitive model and never learn what a store buffer is. On the “yes” branch the languages fork sharply: the C-family “catch fire” languages (Cox) treat a race as a licence to miscompile arbitrarily, because forbidding that would forbid optimizations that assume single-threaded semantics; the memory-safe languages instead cap the damage so that a race can corrupt your logic but never your type system or the runtime’s integrity. The one thing to remember: DRF-SC is not a property of the hardware — it is a property of your program’s synchronization discipline, adjudicated against an SC model.

Precise definitions — the words that carry the weight

Everything hinges on defining a data race exactly, so define it carefully. Two memory accesses conflict when they touch the same memory location and at least one of them is a write (two concurrent reads never conflict — reading is harmless). A data race exists when two conflicting accesses from different threads are not ordered by the happens-before relation — informally, when they can execute “at the same time” with no synchronization forcing one to precede the other (Cox). The JSR-133 (Java Memory Model) FAQ states this as three conditions holding together: a write of a variable by one thread, a read (or write) of the same variable by another thread, and the two not ordered by synchronization (Manson & Goetz 2004).

The subtlety that trips everyone: “not ordered by happens-before” is evaluated under sequential consistency. The theorem is not “if no race happens at runtime” — it is “if, considering all sequentially-consistent executions, none contains a race.” This is what makes the theorem usable: you reason about races in the simple model (SC), and if you find none there, you are handed SC behavior in the complex model (relaxed hardware). You never have to reason about the relaxed model directly.

Do not confuse a data race with a race condition. A race condition is a logic bug: the program’s correctness depends on the relative timing of events (e.g., a check-then-act that another thread invalidates between the check and the act). A data race is a memory-model bug: unsynchronized conflicting access. They are orthogonal. A program can have a race condition with no data race (e.g., two threads correctly locking a shared counter, but the higher-level protocol still has a time-of-check/time-of-use flaw), and — in a language where it were not UB — a data race with no race-condition consequence. In C++ the two collapse in one direction: a data race is always a bug because it is always undefined behavior, regardless of whether it would have been “benign” on your hardware.

Where the theorem came from

The result has a lineage worth knowing because the names recur throughout memory-model literature. Lamport defined sequential consistency in 1979 as the target behavior. Adve and Hill (1990) gave the theorem its modern shape with a programmer-centric reframing: rather than describing hardware by the reorderings it performs, describe it by the software contract it honors. Their definition — a design is “weakly ordered with respect to a synchronization model if and only if it appears sequentially consistent to all software that obeys the synchronization model” (as quoted by Cox, “Hardware Memory Models”) — inverts the whole question. Instead of asking “what does this CPU do?”, ask “which programs does this CPU keep the SC promise for?”

Adve and Gharachorloo’s 1996 IEEE Computer tutorial then packaged this for practitioners as the data-race-free-0 (DRF0) model: a class of programs in which all competing (conflicting) accesses are distinguished as synchronization and properly ordered, for which “the behavior of DRF0 programs is contained in SC” (per the tutorial’s summary). The same paper connects DRF0 to release consistency and the properly-labeled (PL) framework, where the programmer labels synchronizing accesses as acquire or release — the vocabulary that later became C++‘s memory_order_acquire/memory_order_release (see Acquire Release and Fence Semantics). When the C++ and Java committees standardized their memory models in the 2000s (JSR-133 in 2004 for Java 5; the C++11 model, whose rationale is Boehm & Adve’s 2008 “Foundations of the C++ Concurrency Memory Model”), both adopted DRF-SC as the load-bearing guarantee for race-free code (Cox).

Uncertain

Verify: the exact title/venue “Weak Ordering — A New Definition,” Adve & Hill, ISCA 1990, and the DRF0 attribution to Adve & Hill’s companion work. Reason: the primary ISCA paper and the Adve–Gharachorloo tutorial PDF could not be fetched as parseable text during this write (the CMU PDF returned binary; the ACM DOI is paywalled) — the definitions above are quoted via Russ Cox’s memory-model series and the tutorial’s search-indexed abstract, both reliable secondaries, not the primary PDFs. To resolve: fetch the ISCA 1990 paper and the IEEE Computer Dec 1996 tutorial and confirm the precise wording of the DRF0 theorem and the “appears sequentially consistent” definition. #uncertain

Why the bargain is worth making — for both sides

The theorem exists because both sides get something they desperately need. Consider the alternative of demanding sequential consistency unconditionally, for every program racy or not. The classic obstacle is the store buffer (see Cache Coherence and the Store Buffer). Modern CPUs post a store into a local buffer and let the executing thread race ahead before the write reaches coherent memory; the same thread reads its own buffered value early. This single optimization breaks SC, as the store-buffering litmus test (equivalently, Dekker’s algorithm) shows: two threads each write their own flag then read the other’s, and under SC at least one must see the other’s write — yet on x86-TSO, ARM, and POWER both can read the stale zero because both stores are still buffered (Cox, “Hardware Memory Models”). To guarantee SC unconditionally the hardware would have to drain the store buffer (a full fence) around essentially every access, forfeiting the buffer’s entire performance benefit. No mainstream architecture pays that.

DRF-SC threads the needle. Between synchronization points, the hardware and compiler may reorder freely — that is where the speed lives. At synchronization points, the required fences are inserted (by the lock implementation, the atomic’s ordering, the channel operation). Because a race-free program’s threads only communicate through those synchronization points, the reorderings that happened in between are never observable to another thread — the fence at the handoff makes all the prior writes visible together. The programmer, meanwhile, gets to reason in SC and never insert a fence by hand. This is the deal: the programmer pays with synchronization discipline; the implementation pays with fences only at synchronization points; and the reordering freedom in between is the profit both share.

What happens when you break the contract

The languages diverge precisely here, and the divergence is a genuine design decision, not an accident.

C, C++, Rust, and Swift take “DRF-SC or catch fire.” A data race is undefined behavior — the compiler is entitled to assume it never occurs and to optimize on that assumption, so a racy program may do literally anything, including corrupting unrelated data or crashing (Cox). The rationale, from Boehm and Adve, is that any weaker promise would forbid ordinary single-threaded optimizations. A compiler routinely introduces speculative writes, reloads, and register promotion that are perfectly legal for sequential code; if a racy concurrent read could observe those transient states with defined semantics, the compiler could no longer perform them. So the C-family chose to keep the optimizer maximally free and push the entire burden onto the programmer: never race, or forfeit everything. Cox summarizes the stance as: a racy access must be allowed to cause unbounded damage to the rest of the execution (Cox).

Java, JavaScript, and Go take “DRF-SC or weird-but-bounded.” These languages cannot accept undefined behavior for a racy program, because they are memory-safe: a security sandbox in which a data race could forge a pointer or violate the type system would be no sandbox at all. So the Java Memory Model (JSR-133) defines the behavior of racy programs — not to make it nice, but to make it bounded. Even a racy read must return a value written by some actual write to that variable, never a value fabricated “out of thin air” (Cox; JSR-133 FAQ). The cost of this promise is the notorious complexity of the JMM’s “causality” rules, which exist entirely to forbid out-of-thin-air outcomes while still permitting standard compiler optimizations — a boundary that turned out to be extraordinarily hard to formalize (see The Java Memory Model and the Springer analysis of Java’s DRF guarantee). Go takes a similar memory-safe stance: races are not UB, but their outcome is not guaranteed to be SC and may corrupt data structures, so the Go memory model simply advises against them and ships a race detector.

Worked example — the same race, two verdicts

Consider a lazily-initialized singleton, the archetypal DRF-SC teaching case:

// Shared:
Config* g_cfg = nullptr;   // plain pointer, NOT atomic
 
// Thread A (initializer)
Config* p = new Config();  // (1) construct object, fill fields
g_cfg = p;                 // (2) publish pointer  -- plain store
 
// Thread B (reader)
if (g_cfg) {               // (3) plain load
    use(g_cfg->field);     // (4) read a field
}
  • Lines (2) and (3) are conflicting accesses (same location g_cfg, one is a write) from different threads with no synchronization between them — a textbook data race.
  • In C++, this is undefined behavior even if it “works” on your x86 laptop. The compiler or the weakly-ordered CPU may make the store at (2) visible before the constructor writes inside (1) have propagated, so Thread B dereferences a pointer to a half-built object and reads garbage from field. Worse, because it is UB, the compiler is permitted to assume g_cfg never changes concurrently and hoist or fold the load in ways that break the code in still stranger ways.
  • The fix is to make the publication a synchronizing operation, converting the race into a happens-before edge:
std::atomic<Config*> g_cfg{nullptr};
 
// Thread A
Config* p = new Config();
g_cfg.store(p, std::memory_order_release);   // release: all prior writes publish
 
// Thread B
Config* p = g_cfg.load(std::memory_order_acquire);  // acquire: sees them
if (p) use(p->field);

Now the release store at publication synchronizes-with the acquire load, establishing happens-before from the constructor writes to the field read. The program is data-race-free, DRF-SC applies, and you may reason about it as plain sequential code — the acquire/release pairing is exactly the release mechanism DRF0’s “properly-labeled” framework anticipated. The C++ memory model’s finer memory_order levels are the subject of The C Plus Plus Memory Model and Atomic Ordering.

Failure Modes and Common Misunderstandings

“My race is benign — it’s just a stats counter.” In C++ there is no such thing as a benign data race; it is UB regardless of intent, and compilers have miscompiled “obviously harmless” racy counters. Use std::atomic with memory_order_relaxed if you truly don’t need ordering — that is race-free and nearly free, and it keeps you inside the contract.

“DRF means my program is sequentially consistent, so I don’t need SC atomics.” Subtle trap. DRF-SC gives SC behavior for the DRF program as a whole, but only if your synchronization is correct. Acquire/release atomics are enough for pairwise message-passing, but multi-variable protocols like IRIW (independent reads of independent writes) can still observe non-SC orderings unless you use seq_cst atomics (Cox, “Hardware Memory Models”). “Race-free” is necessary; using the right strength of synchronization is also necessary.

“DRF-SC means my program is correct.” No — it only means memory behaves sequentially consistently. Your higher-level logic can still have deadlocks, race conditions, and lost updates. DRF-SC removes the memory-model uncertainty; it does nothing for algorithmic correctness.

Confusing the analysis model with the execution model. The theorem quantifies over SC executions to decide race-freedom, then delivers SC over relaxed executions. Beginners try to reason about races on the relaxed hardware directly and tie themselves in knots. Reason about races in SC; that is the entire point.

Alternatives and When to Choose Them

The design space around DRF-SC has exactly three occupied points. Unconditional sequential consistency (Lamport’s ideal, Sequential Consistency) is the simplest to reason about but forfeits the store buffer and is too slow for a general-purpose language default. No memory model at all — the pre-2004 status quo for C and C++, where thread behavior was defined only by the threading library and the platform — is what DRF-SC replaced, and it made portable concurrent code effectively impossible to reason about (JSR-133 FAQ). DRF-SC is the pragmatic middle: SC for the well-behaved, freedom for the implementation, with the only real design choice being the penalty for racing — UB (fast, unforgiving) versus bounded (safe, complex). Systems languages chose UB; managed languages chose bounded; both chose DRF-SC as the core.

Production Notes

The practical corollary of DRF-SC is: the only sound way to ship concurrent code is to be data-race-free, and the only scalable way to know you are is a race detector. Dynamic detectors like ThreadSanitizer (used by C, C++, and Go’s -race) and Java’s tooling are built directly on the happens-before relation the theorem is defined over — they track happens-before edges at runtime and flag any pair of conflicting accesses not so ordered (see Happens-Before Relation). Because a data race may surface one run in a billion, and because in C++ its consequences are unbounded, “it passed the tests” proves nothing; the guarantee comes from establishing race-freedom (via the detector plus discipline), not from observing correct output. The near-universal adoption of DRF-SC — C11, C++11 and later, Java 5+, Go, Rust, Swift, and JavaScript’s SharedArrayBuffer model all guarantee it (Cox) — means this one theorem is the shared foundation a working engineer stands on every time they take a lock and don’t think about the store buffer underneath.

See Also

Graph View

Backlinks