5.4Sequential Consistency for Data-Race-Free Programs

Having the cake and eating it

Children and computer architects would like to have their cake and eat it too: reason with the (relatively) intuitive model of SC while getting the performance of a relaxed model like XC. For the important class of data-race-free (DRF) data-race-free (drf) An execution in which no data operations race; a program is DRF if all its SC executions are DRF. defined in Chapter 5 — open in glossary programs, both are simultaneously possible.

Informally, a data race data race Two conflicting data operations that appear in the global memory order without an intervening pair of transitively conflicting synchronization operations by the same threads. defined in Chapter 5 — open in glossary occurs when two threads access the same location, at least one access is a write, and no synchronization intervenes. Races are often (not always) programming errors, and many programmers aim to write DRF programs anyway. SC for DRF sc for drf The contract that all executions of data-race-free programs are SC executions; programmers label synchronization, implementations map it to FENCEs/RMWs. defined in Chapter 5 — open in glossary is a contract with two sides:

• Programmers ensure their programs are DRF under SC — correctly synchronized, with every synchronization operation synchronization operation A memory operation tagged as synchronization (e.g., lock acquire or release); untagged operations are data operations by default. defined in Chapter 5 — open in glossary labeled as such;
• Implementors map the labeled synchronization to the FENCEs and RMWs the relaxed model supplies, guaranteeing that all executions of DRF programs are SC executions.

XC and most commercial relaxed models have the FENCEs and RMWs needed to “recover SC” this way — and the approach is the foundation of the Java and C++ memory models (§5.9).

Two examples

In both tables below, C1 stores data1 and data2 inside a FENCEd, locked critical section, while C2 loads the two locations in the opposite order. The difference: whether C2 synchronizes.

Table 5.7 — C2 does not synchronize. Its loads run concurrently with C1’s stores. XC may reorder S1/S2 (no FENCE between them) and L1/L2, so four outcomes are possible — including one no SC execution allows:

The (r1, r2) = (0, NEW) outcome — see it via the witness, e.g. S2, L1, L2, S1 — is XC’s reordering exposed by the race (S1 races with L2, S2 with L1).

Table 5.8 — C2 acquires the same lock. Now C1’s critical section runs entirely before C2’s, or vice versa:

Only (0, 0) and (NEW, NEW) remain — the SC outcomes — and this holds whether or not C1 reorders its stores or C2 its loads:

“A tree falls in the woods (reordered stores), but no one hears it (no concurrent loads).”

Generalizing from the two examples, SC for DRF claims: either an execution has data races that expose XC’s reordering, or the execution is data-race-free and indistinguishable from an SC execution.

The definitions, precisely

For XC: require that every synchronization operation is preceded and succeeded by a FENCE, as in Table 5.8. With that, XC supports SC for DRF — the proof is beyond the book’s scope, but the intuition is exactly the two tables above.

The catches

And isn’t there always a catch? Guaranteeing DRF at high performance — without labeling too many operations as synchronization — is hard, for two reasons.

1. Optimal labeling is undecidable. Figure 5.4’s gadget makes FENCE necessity depend on the halting problem:

The practical escape is conservatism: add a FENCE whenever unsure — always correct, possibly slower. In the limit, surround every memory operation with FENCEs and any program behaves SC.

2. Bugs happen. A program with an accidental data race loses the guarantee — after a race, execution may stop obeying SC, and the programmer must reason with the relaxed model itself. The good news: executions obey SC at least until the first data race, so debugging can start with SC reasoning alone.

Two ways to reason

A programmer on a relaxed memory system can:

1. reason directly with the model’s rules (Table 5.5 and friends), or
2. insert enough synchronization to eliminate data races (synchronization races — competing lock acquires — are still allowed) and reason entirely in SC.

The book recommends option 2 almost always, leaving option 1 to experts writing synchronization libraries and device drivers.