Memory Ordering
Two threads. Each writes its own variable, then reads the other's. Whichever ran first, its write was already in memory when the other read, so at least one of them must see a one. On x86 both can read zero, and the hardware is working correctly. This page enumerates every schedule of the four operations under three models and shows you where the impossible outcome comes from.
Both of them wrote first
1 The program: four operations, two threads, each keeping its own order
Both variables start at zero: x = 0, y = 0. Four operations. Each thread runs its own two in order; the models below differ only in what happens between a store and memory.
2 Every interleaving of those four under one shared memory, and the three outcomes they produce
Pick a model. Everything below is enumerated from it when you press: the schedules, the counts, and the outcomes.
3 The same four with a store buffer per thread, re-enumerated, and the fourth outcome that appears
Every outcome allows
| What the two threads read | Schedules that end this way |
|---|
Why one shared memory cannot produce it
The enumeration above shows that it does not happen. Here is why it cannot.
Under one shared memory the four operations happen in some order, one at a time. Consider whichever of the two stores comes first in that order, and say it is store x = 1. Thread 1's load of x has to come after thread 1's own store of y, and that store comes after store x = 1 by assumption. So thread 1 reads x after x was set to one, and r2 = 1.
The argument is the same with the threads exchanged. Whichever store goes first, the other thread's load comes after it and sees a one. So at least one register is one, and r1 = r2 = 0 is impossible rather than merely unobserved.
A store buffer breaks the argument at its first step: with buffers there is no single order the two stores are in, because neither has reached memory when the loads happen.
4 A fence between each store and load, and the outcome set shrinking back
One schedule at a time,
Every step, and the state after it. A load reads its own thread's buffer first and memory otherwise, which is where both zeros come from.
| Step | Op | Memory | Registers | Buffers 0 / 1 |
|---|
The address bar follows the schedule, so one can be pointed at rather than described.
These ran in this browser when the page loaded. Each claim, whether it held, and the number behind it.
| claim | held | measured |
|---|---|---|
| sequential consistency has 6 interleavings | yes | 6 enumerated, 6 from choosing 2 of 4 positions |
| and three outcomes, none of them both-zero | yes | 0,1 1,0 1,1 |
| both processors reading zero is impossible under Lamport's condition | yes | absent from the enumeration |
| give each thread a store buffer and it happens | yes | 80 schedules, outcomes 0,0 0,1 1,0 1,1 |
| a fence between the store and the load takes it away again | yes | 20 schedules, outcomes 0,1 1,0 1,1 |
| a store buffer only adds outcomes, never removes one | yes | all 3 survive |
| a thread reads back its own store before the buffer drains | yes | all 2 schedules forward |
| every schedule runs to the end, with both buffers emptied | yes | all 80 reach memory |
| no schedule is counted twice | yes | every path distinct |
What is real here, and what is not
This page measures nothing about the computer you are reading it on
It enumerates a model. Every number here is the output of a search over schedules of four operations, run in your browser, and none of it is a measurement of your processor. That distinction matters enough to put first: a page that showed you a real reordering on your own hardware would be a different and harder thing, and this is not it.
The store buffer is modelled as x86-TSO, which is a published model rather than a guess
A store enters the thread's own FIFO buffer; a load reads the newest matching entry in that buffer if there is one, and memory otherwise; the buffer drains at a point the schedule chooses. That is the model in Owens, Sarkar and Sewell's x86-TSO paper, cited below. It is not our invention and not an approximation of one.
Real processors do more than this, and none of it changes this program's answer
Buffers have a capacity, stores to the same line coalesce, loads are issued speculatively and replayed. None of that is modelled. For these four operations the set of outcomes is the same with or without it, which is why a model this small is worth trusting here and would not be worth trusting for a longer program.
ARM and POWER are weaker still, and are out of scope
Those architectures allow outcomes TSO forbids, including ones this program cannot produce here. Everything on this page is about x86-TSO, and saying so is more useful than a fourth model nobody asked for.
The fence is modelled by its effect, not by its cost
A fence here stops its thread until that thread's buffer has drained. That is what it does. What it costs in cycles is a real number on a real machine and this page does not know it, so it does not print one.
Sound: no
The measurement here is a set of outcomes, not a duration. A sound would be decoration, and the studio's rule is that a sound has to carry the measurement or not be built.
Sources
- Russ Cox, Hardware Memory Models, 2021, which states the store-buffer litmus test and its outcome on x86 directly.
- Scott Owens, Susmit Sarkar and Peter Sewell, A better x86 memory model: x86-TSO, TPHOLs 2009 — the model this page implements.
- Leslie Lamport, How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs, IEEE Transactions on Computers C-28(9), September 1979, pages 690 to 691, which defines sequential consistency.
- Logical Art, the studio this belongs to.