Sequential Consistency: The Model You Already Have

Sequential consistency (SC) is a specific, formal claim, not a vague feeling that "memory works normally". Lamport's definition has two parts: the result of any execution is the same as if all operations of all processors were executed in some single sequential order, and the operations of each individual processor appear in that order in the order specified by its program.

Picture a single switch in front of memory. Every core hands its loads and stores to the switch; the switch services them one at a time, in some interleaving; each core's own operations go through the switch in program order. Any interleaving is allowed, which is why concurrent programs are still hard under SC — but every core observes the *same* interleaving, which is what makes reasoning tractable.

It is worth being clear about what SC does *not* give you. It does not prevent races, it does not make counter++ atomic, and it does not stop two threads from interleaving in a catastrophic order. It gives exactly one thing: a single global order that everybody agrees on. That single guarantee is the foundation almost every informal correctness argument silently rests on, which is why losing it is so disorienting.

The canonical demonstration is four lines long. Two variables start at zero. One core writes x then reads y; the other writes y then reads x. The question is whether both reads can return zero.

Under sequential consistency the answer is provably no. Whichever store the global order puts first, the core that performs its read later must see it. Enumerate all six interleavings and r1 == 0 && r2 == 0 appears in none of them. This is not a subtle argument — it is the kind of reasoning a competent engineer does at a whiteboard in ten seconds and is completely confident in.

On real x86-64 hardware, both reads return zero regularly. Not rarely, not under exotic conditions — run this in a loop on two cores and you will collect thousands of instances a second. The store sits in the writing core's store buffer, invisible to the other core, while the read proceeds against cache. Nothing is broken; the machine is behaving exactly as specified. It is the whiteboard argument that was wrong, because it assumed a model the hardware never promised.

The useful reframing is that SC is not the default that hardware sometimes violates — it is a guarantee with a price that you request where you need it. Every mainstream ISA gives you weaker ordering for free and lets you pay for stronger ordering with fences and with atomic operations that carry ordering semantics.

Languages sell you the same guarantee at a higher level, and on better terms. The C++ and Java memory models both offer a bargain usually called DRF-SC: if your program contains no data races — every conflicting access pair is ordered by synchronisation — then the implementation guarantees your program behaves sequentially consistently. You get the intuitive model back, provided you never race. The compiler inserts whatever fences the target ISA requires to make that true, which is why the same source is correct on both x86-64 and AArch64 even though the two hardware models differ substantially.

That bargain is the practical takeaway of this entire module. Use the language's synchronisation, and you may reason with the switch model. Reach past it — with plain loads and stores on shared data, or with relaxed atomics chosen for speed — and you have opted into the hardware model of whatever machine you happen to be on, which is a much less pleasant place to be. See Hardware Memory Models Are Not Language Memory Models for what those models actually permit and Memory Barriers: Ordering, Not Flushing for the instructions that buy ordering back.