A history of operations, each occupying an interval, is linearizable exactly when some total order of them respects real time — an operation that finished before another started must come first — and replays legally against the object. So enumerate the orders and count the survivors. Three operations give 6 orders, of which 3 respect real time and 0 are legal: a violation. Seven operations give 5040, and the lab refuses, because the refusal is the lesson.
Core ideas
An operation is an interval rather than an instant, two filters cut the orders down, and the number that survives is the verdict.
A call starts when the client issues it and ends when the response arrives, and the operation may be considered to take effect at any single moment inside that interval. Two operations whose intervals overlap may therefore be placed in either order; two whose intervals do not overlap may not. This is the only role real time plays.
The first filter is mechanical: for every pair where one operation ended before the other started, keep only the orders putting them that way round. The second is a replay: run the surviving orders against the object — for a register, each read must return the value last written — and keep the ones that never contradict themselves.
If nothing survives both filters, the history is not linearizable, and that is a property of the history as a whole. It does not mean one particular replica returned a value it never held; every read in the violating history here returns a value that genuinely existed. The defect is that no single sequence of instants can explain all of them at once.
The material
What linearizability asks, how the enumeration answers it, and why no real checker works this way.
A history is a set of operations, each with a start time, an end time and a return value. A linearization is a total order of those operations such that a precedes b whenever a ended before b started, and such that replaying them in that order against the object is legal — every read returns the most recently written value. A history is linearizable if at least one linearization exists.
The definition is an existence claim, and that is what makes the enumeration a decision procedure: generate every total order, apply the two filters, and count. A count of zero settles the question in the negative, and any count above zero settles it in the positive.
Nothing about this history looks wrong operation by operation. B read 1, which was written. C read 0, which was the initial value. Both are values the register genuinely held, and a system that checked each response individually would report no problem at all.
The verdict comes from the combination. C reading 0 would be fine if it could be placed before the write, and real time forbids that because A had already returned when C was issued. B reading 1 would be fine anywhere after the write. It is the pair of constraints together that leaves nothing, which is why linearizability is a property of histories and not of responses.
The growth is factorial, so the cap is not a limitation of the page, it is the shape of the problem. Real checkers do not enumerate: they search with pruning, commit operations greedily and backtrack, or check a weaker property that is cheaper to decide. The lab refuses a seventh operation and prints 5040 rather than quietly truncating, because a silent truncation would teach the opposite of the thing worth learning.
Change C to read 1 instead of 0 and nothing else about the history moves — same intervals, same real-time constraint. Now A B C replays as w1, r→1, r→1, which is legal, and A C B does too. Two of the three real-time-respecting orders survive, the count is 2, and the history is linearizable. A single returned value flipped the verdict, which is the sense in which linearizability is a property of the whole history and a very sharp one.
It is worth being precise about what this buys. Linearizability is the guarantee that the system behaves as though there were one copy of the data and every operation took effect at a single instant between its call and its return. “Quorums Overlap” gave a much weaker property — no acknowledged write is missed entirely — and the gap between the two is the whole reason this lesson exists.
Interactive
Count the legal total orders — and see why six is the cap
Method
Two filters in a fixed sequence, and a verdict that is a count rather than an opinion.
Start, end, what it did, what it returned. A history without return values cannot be checked, and a history without intervals has no real-time constraints to apply.
For every pair, if one ended before the other started, that order is forced. If the intervals overlap, both orders remain open. Write the forced pairs down; they are usually far fewer than the pairs.
k! orders, filtered by the forced pairs. For small k this is a short list and worth writing out, because seeing which orders survive is what makes the next step meaningful.
For a register: track the current value, and reject at the first read that disagrees with it. Zero survivors means the history is not linearizable. More than zero means it is, and the count itself has no further meaning.
A register starting at zero. One client writes 1; two others read it, one returning 1 and one returning 0. Every response is a value the register really held, and the system is nonetheless wrong. The question is how to demonstrate that rather than assert it.
The violation is C, and it is worth saying exactly why rather than pointing at it. C was issued after A had already returned, so whatever instant C took effect at, it was after the write took effect; and it returned the value from before the write. No amount of reordering the two overlapping reads changes that, which is what the three surviving orders demonstrate by all failing.
The second run is the faded half of the example and it is a single character's difference. Two legal orders exist, so the history is linearizable, and nothing about the timings changed. The lesson is that linearizability is decided by the combination of intervals and returned values, and that neither alone is enough to look at.
For a faded rehearsal, take the four-operation history with two concurrent writes: A w1[0,3], B w2[1,5], C r1[4,8], D r2[6,10]. The supplied first move is that there are 24 total orders and the forced pairs are A before C and A before D. Work out how many survive real time, predict whether any are legal, then check both in the lab and explain the result in one sentence about where B had to be placed.
You should be able to write a history as intervals with return values, derive the forced pairs, enumerate and filter the total orders, replay the survivors against a register, report the count with zero as a violation, and say why the procedure does not scale.
Something to change about this lesson? Write it down, tick it off when it is handled, and export the list when you want to act on it. Kept in this browser only: nothing is sent anywhere, and nobody is notified.
No recommendations yet for this lesson.