When data is held in several copies, what does it take for them to act as one? And who could ever tell the difference?
We find out by exploring how three ancient Greek trading houses filled one another's requests in the sequence they really came, though none of them could read the hour.
After Maurice P. Herlihy and Jeannette M. Wing, Linearizability: A Correctness Condition for Concurrent Objects, 1990
Each link is an idea one paper took from another. Point at one, or tap it, to read how.
a paper this book retells a paper retold in another book a paper outside the series
A shared object, such as a queue, may be held in several copies on several machines. Programmers want it to behave as if there were one copy.
The difficulty is that calls on the object overlap in time, and each takes time to answer. Agreeing on some one-at-a-time order of the calls is not enough, because a call that finished before another began must come first. The condition that Herlihy and Wing gave in 1990, linearizability, asks for exactly that: every call appears to take effect at one instant between its start and its answer, and the answers are those of a single copy. Three results make the condition usable.
We tell it with three trading houses and the board where House 3 holds its waiting requests.
Client 1 enqueues x at copy A, and the update is sent on to copy B. Client 2 then enqueues y at copy B, and client 3 dequeues at copy B. When does the update reach B?
House 1, House 2 and House 3 stand round the coast of Arche with a mountain between them. Word passes between them only on slips carried along the one road, and in the trading season nobody on the island can read the hour.
House 3 has grain in its storehouse, and both other houses need it. The houses have agreed that the request placed first is filled first, so House 3 has to know which request that was.
With no hour to go by, House 3 reads the tallies: a number written on every slip and raised on every arrival, with the houses' numbers to break ties. The tallies never put a request ahead of one that led to it, and no house can win by having a quicker messenger.*
The tallies are built from slips and nothing else, though, and news also crosses the mountain. One morning shows what that allows. Scroll to follow it.
House 1 sends a request and has its confirmation back before the sun is high. A goatherd carries the news over the mountain to House 2, and at noon House 2 sends a request of its own.
House 1 has made two entries this morning. Houses 2 and 3 have made none, and every house has heard nothing. Each house's tally is shown beside its name.
House 1 writes the request as its third entry, so the request's tally is . A messenger takes the slip to House 3.
The slip reaches House 3, which puts the request on its board and raises its own tally past the slip's. It sends back word that the request is entered, marked with its new tally, .
The confirmation reaches House 1 before the sun is high, and House 1's tally is raised past it.
A goatherd crossing Mount Phyle by the smugglers' tracks mentions the request at House 2. The goatherd carries no slip, and House 2 has had none all morning, so its tally has not moved.
House 2 writes a request of its own. Its tally is , low, since no slip has reached it for hours, and lower than House 1's request's.
House 3 enters the second request and serves the lower tally first, which is House 2's. That is fair by the tallies. Yet House 1's request had been entered and confirmed before House 2 even asked.
By the tallies nothing went wrong. No slip joined the two requests, so either could come first. But House 2 knows, and so does anyone who talked to the goatherd, that House 1's request had been entered and confirmed before House 2 even asked. By what the sun saw, House 1 was first.
The tallies have always had this gap. They respect every slip, and the goatherd carries none. One answer is to make better clocks, kept so close together by the slips that nobody crossing the mountain can arrive before setting out.* That is a way of catching the goatherd. The houses want something else: a promise about how requests are filled that no goatherd can ever catch them breaking, whatever clocks they keep or do without.
Such a promise would be to fill first the request placed first as the sun saw it. Nobody on Arche can read the sun, so it is not yet clear what the promise would even say.
A promise about requests has to be said in terms of what the houses themselves see. A house sees two moments of its request: when it sends the request, and when the confirmation comes back. Somewhere in between, the request was put on the board where House 3 holds its waiting requests.
Serving has two ends as well. A loader at House 3 goes to the board, takes a request and loads the grain for it, and that too begins and ends. Each house, and each loader, does one thing at a time.
So every piece of business has a span, from its beginning to its end. One piece of business comes before another when it was over before the other began. Otherwise the two overlap, and neither came first. This is judged by the sun, whether or not anyone could see it. Three requests are drawn below. Choose any two, and see whether one came before the other.
Each line is one house. A thick stretch is the span of one request, from its sending to its confirmation. Later moments are further out. Choose the first dot of any two requests.
A is House 1's request, B is House 2's first request and C is House 2's second.
Now the promise. Picture a single steward with a single board, doing one thing at a time: they enter a request, or they serve the oldest waiting one. No request goes onto their board and none comes off it except through their own hands. The houses cannot see the steward and do not need to. They need only that everything they got could have come from such a steward, with each thing the steward did falling somewhere inside the span of the business it belonged to. Said exactly, all the requests and all the servings can be set in one sequence such that three demands hold.
Every serving takes the request that a single steward, with a single board, taking everything in that sequence, would have served.
Each piece of business takes its place in the sequence at some moment between its beginning and its end.
Anything finished before another began comes before it.
The second demand is what ties the promise to the sun. Without it the steward could act whenever it suited them, and the promise would say nothing about when anything happened. With it, the third follows: if House 1's request was over before House 2's began, the steward's moment for House 1 came first, and a single steward serves the older request first. So the goatherd's morning breaks the rule.
A rule can fail in two ways. It can be too strict and forbid mornings that are plainly fine, or too loose and allow mornings that are plainly wrong. Four mornings test this one both ways.
Write <H for the real-time order of a history H: a <H b when a responds before b is invoked. The board is a FIFO queue: a request is Enq, a serving is Deq.
All the requests and all the servings can be set in a single sequence such that:
Linearizability, §2.2: a history is linearizable if, after adding responses to some pending invocations and dropping the rest, it is equivalent to a legal sequential history that respects the real-time order <H.
Each of the four mornings is put to the rule in the same way: could a single steward have produced it, with every piece of business falling inside its span?
Two of the mornings the rule has to allow if it is not too strict, and two it has to forbid if it is not too loose. Choose a morning and read the verdict.
Requests are thick stretches on House 1's and House 2's lines, from sending to confirmation. A serving is a grey stretch on House 3's line, ending in a dot for the request it took. Later moments are further out.
Choose a morning.
The four verdicts show where the rule draws its line. Overlapping requests may be served either way round, and requests one after the other may not. A request may be served while word of its entry is still on the road, because its moment came at its entry. No fall of the times excuses serving one request twice.
Business still unfinished when a morning is judged needs one allowance. A request sent but not yet confirmed may be counted as on the board or not, whichever fits what happens next.
The rule and the tallies now both claim to say which request came first. They might be the same answer, or one a stricter form of the other.
The rule and the tallies do not give the same answer about which request came first, and neither answer includes the other.
For the tallies, one request is first if a chain of slips leads from it to the other. Requests no chain joins are put in sequence by tally and house number, fairly but arbitrarily.* For the sun, one request is first if it was over before the other began, whether or not any slip joined them. Each of the two mornings below sets one answer against the other.
The number in a dot is the tally the request was written under. A thick stretch is a request's span. An arc is a slip. Later moments are further out.
Choose a morning.
On the goatherd's morning no slip joined the two requests, so the tallies could put House 2 first, and the sun put House 1 first. Turn it round: House 1 sends a request, and before it is confirmed sends House 2 a slip about it, and House 2 then makes a request. A chain of slips joins them, so the tallies put House 1 first. But House 1's request was not over when House 2's began, so for the sun they overlap, and the rule would let House 2 go first.
The rule can be kept, and easily, by the arrangement the tallies were invented to avoid. Let House 3 have the only board and enter each request when its slip reaches the gate. The entry falls after the slip was written and before the confirmation leaves, so it lies inside the request's span. Serve in order of entry, and House 3 itself keeps the rule.
Serving requests in the sequence they reach House 3's gate keeps the rule of the board. Serving them in the sequence of their tallies need not. And the tallies' sequence can put one request before another where the rule of the board would allow either.
Serving by arrival had one fault: the house with the shorter road wins every pair of requests that overlap. The rule does not mind, because it says nothing about requests that overlap. The tallies do mind, and pay for it by sometimes serving a later request first. The two answers protect different things.
So one board at House 3's gate keeps the rule. Each house might rather hold a copy of the board close at hand, and the rule has to say whether that is allowed.
Write <H for the real-time order of a history H: a <H b when a responds before b is invoked. H is linearizable if it can be extended to a history equivalent to a legal sequential history S with <H ⊆ <S. For the board, a FIFO queue, legal means each Deq returns the oldest item Enq-ed and not yet returned. The implementation is one copy at House 3's gate, and an operation takes effect at the step where its request is applied. Claim. The operations in the order of those steps form such an S.
Whether there may be more than one board is settled by what the rule mentions. It speaks only of sendings, confirmations and servings, all things that happen at the houses' gates.
The rule never mentions the board itself. So it cannot tell one board from three copies held in step by slips, or from any other arrangement behind the gates. Whatever stands behind them is judged by what comes out of them.
A house sends a request, gets its confirmation, and sees loaders serve. The rule speaks of these and of nothing else.
One board, three copies held in step by slips, or any other arrangement. The rule is silent on all of them.
No house, comparing notes with every other and with anyone who watched the sun, could tell that there is more than one board. That is what it means for many copies to act as one.
How copies might be held so is another matter, and this book does not take it up. What it takes up is what the promise gives to a house that relies on it.
The first thing to settle is how far one check reaches. Grain is not the only thing asked for, and if the houses have several boards, the rule might have to be checked across all of them at once.
House 2 presses oil, and all three houses ask for it the same way, on a board of its own at House 2. If the rule had to hold over both boards together, every change to how one board is run would have to be weighed against the other.
It does not have to. It is enough that each board keeps the rule by itself.
All the business keeps the rule if and only if, for every board, the business on that board, taken by itself, keeps it.
Two boards fit together without anyone arranging it because the sun ties them, and the sun never contradicts itself. Two boards could fail to fit only through a loop: one request before another on the grain board, that one before a third by the sun, and so round to the start. The proof shows that such a loop would need the sun to put something before itself.
Other sensible rules lack this property, and taking the sun out shows it. Ask only that everything could have come from a single steward, with each house's own business in the order the house did it, and nothing said about moments. Under that looser rule the goatherd's morning is fine. Now let House 1 ask for grain and then oil, and House 2 ask for oil and then grain. Choose a rule, and see whether each board passes it alone and whether the two pass it together.
House 1 asks for grain, then oil. House 2 asks for oil, then grain. House 1's oil reaches the oil board before House 2 places its own, so the oil board serves House 1's first. The grain board serves House 2's grain first, though House 1's grain was finished long before.
Choose a rule.
Each board passes the looser rule alone, and together they fail it. Houses that kept only the looser rule would need one plan spanning every board. Under the rule of the board the fault shows on the grain board by itself, where it lies. The sun's demand is what lets each board be kept, and judged, on its own.
Each board can be judged alone, then. A house may still fear that keeping the rule could force it to stand at the gate and wait on someone else's business.
For a history H and an object x, write H|x for the subhistory of operations on x, and <H for the real-time order: a <H b when a responds before b is invoked. Claim (locality, Theorem 1, the "if" direction): if every H|x is linearizable, then H is.
Standing at the gate is something the rule never asks of a house with a request. Whatever is on the board, a single steward can always put a new request at the end, so the rule never makes a request wait on anyone else's business.
If the business so far keeps the rule, a waiting request can be entered now and the rule still kept.
So when a house does wait for its confirmation, the cause is the arrangement behind the board, a slip still on the road, and never the rule. Serving is different. A loader who comes to an empty board has nothing to take, and a single steward would make the loader wait until a request comes. That wait is asked for, not forced: serve the oldest request has no answer while there are no requests.
A stronger promise does not always keep this. Suppose a house wanted several things done as one, with nothing else between them. The three cases below take a waiting request, a loader at an empty board, and two such groups in turn.
Choose a case.
In the last case each group must have gone before the other's request, so one of the two has to be called off. Promises about such groups can force a house to undo its business. The rule of the board, whose business is always single, never does.
All of this has supposed one steward, doing one thing at a time. House 3's real board has many hands on it at once.
A total operation, such as Enq, has a response in every state. Claim (the nonblocking property, Theorem 2): if H is linearizable and p is a pending invocation of a total operation, then there is a response r such that H extended by p and r is linearizable.
House 3's real board is busy, with many clerks and loaders at work at once. The master of the board has arranged it so that nobody ever stands aside for anybody.
The board has numbered slots, each holding one request tablet or nothing, and a peg at the first slot nobody has been given yet. A clerk takes the number at the peg and moves the peg on, then puts a tablet in that slot. A loader reads the peg, goes along the slots from the first, and takes the first tablet there is. No clerk or loader waits for another, and a clerk who stops halfway stops no one else.
Everything happens at one board at one house, and no slip crosses the road. With a single steward, each request had its moment at its entry. Here an entry is two movements by one of many hands, and it is no longer plain that a request has a moment at all. Watch a race: the clerk entering House 1's request and the clerk entering House 2's begin at the same time, and a loader comes by.
Four slots are shown, all empty, and the peg stands at the first. Two clerks are about to enter requests, one for House 1 and one for House 2.
The clerk entering House 1's request takes the number at the peg and moves the peg on, in a single movement. The tablet is not yet in its slot.
The clerk entering House 2's request takes the next number, and the peg moves on again.
The second clerk puts House 2's tablet in slot 2 and is done. The first clerk has not yet reached slot 1.
Say yes, ahead of House 2's. Then a loader who comes now finds slot 1 empty and serves House 2. Say no, and let the first clerk put the tablet in first. Then a loader finds it in slot 1 and serves House 1. Both runs follow.
The loader reads the peg, looks at slot 1, finds it empty, and takes House 2's tablet from slot 2.
The first clerk puts House 1's tablet in slot 1 before the loader looks. The loader reads the peg, finds the tablet in slot 1, and serves House 1.
Nothing has gone wrong in either run. The two requests overlapped, so either sequence keeps the rule. The trouble is only that when the second clerk is done, which sequence it will be is not yet settled. A race still to be run will settle it, so no step anyone has taken so far can be called the moment House 1's request joined the board.
At House 3's gate the rule was shown to be kept by pointing to each request's moment. On the busy board there is no moment to point to, and showing that it keeps the rule needs another way.
The queue of §4.2. The board is an array items and an index back; slots are never reused.
Enq is INC(back) then STORE.Deq is READ(back) then SWAP along the array.The other way is to ask what the board could mean at each moment, and to stop asking what it does mean. Once the first clerk's tablet is in, the board could stand for House 2, then House 1, or for House 1, then House 2.
The slots record one thing for certain, and it limits the sequences. A tablet put in before another clerk even took a number must come first. Any two not so placed may go either way. Choose a run to see what the board could stand for once every tablet is in, then send a loader up and see which tablet is taken.
Choose a run.
The thing to show is this: at every moment, every sequence the board could stand for is one the business so far could honestly have produced. Two facts carry it. A tablet just put in never has to stand ahead of anything already waiting, because a tablet that had to stand behind it would belong to a clerk who took a number after it went in, and it is only now going in. And a loader going up from slot 1 always takes a tablet that could be first, because a tablet that had to come before it would lie in a lower slot, and the loader would have taken that one.
At every moment, every sequence of waiting requests the board could stand for is one the business so far could have produced, so the busy board keeps the rule.
A house that relies on a board known to keep the rule gets everything a single steward would guarantee: requests are served in the sequence they came by the sun, none vanishes, and none is served that nobody made. The obvious one-line promise, no later request is served before an earlier one, would not have done as well, since a board that lost tablets would keep that promise.
The rule can be kept, then, even by a board that no one can pause. What it leaves unpromised should be set down as plainly as what it gives.
Let A: REP → 2ABS map each state of the array and index to the set of queue values it could stand for, and let Lin(H|ABS) be the queue values the business so far could have produced. Write x <r y when the STORE of x precedes the INC of y. Claim (§4.3.2, Theorem 17): for every linearized representation value r, A(r) ⊆ Lin(H|ABS).
This is an outline, and so is the paper's. Herlihy and Wing give the two facts of steps 4 and 5 and the shape of the argument; the lemmas that make it airtight are in their technical report.
The rule leaves four things unpromised, and a house that relies on it should know each of them.
The rule is judged by the sun, which nobody on Arche can read in the trading season. A house knows the rule is kept only because the arrangement behind the board has been shown to keep it, as House 3's gate and the busy board were. The rule gives the island no hour and needs none.
Every demand says what must not happen, so a board that never served anyone would break none of them. A loader may even be overtaken on every round, finding each tablet taken just before reaching it, and go round for ever while the rule holds. That every request is served in the end is a separate promise.
The rule says what copies must look like from the gates, and nothing about the slips that would keep them in step.
The tallies keep a different promise, fairness between requests that overlap, and give up the sun to keep it. Which first the houses want is theirs to choose.
What the rule does promise is enough for a house to rely on. Whatever stands behind the gate, the requests are filled as one steward with one board would have filled them, in the sequence they came by the sun.
Read the island again with machines in the counting rooms. Each house, loader and clerk is a process, each board is a shared object, and the rule of the board is linearizability. Hover over a row, or tap it, to see who is who.
A shared object is correct if every call appears to take effect at one instant between its start and its answer, in an order that respects real time.
Then one copy or many are judged alike, each object can be checked alone, and no caller is made to wait where the call is always defined.
Setting The Ring Road
| the houses; the loaders; the clerks | Sequential processes, each waiting for one operation's response before issuing the next. Processes, §2.1. |
| the board; placed first, filled first | A FIFO queue. The paper's running example, Fig. 1 and Fig. 3. |
| a request; a serving | Enq; Deq, which returns the oldest item. Axioms E and D, Fig. 3. Enq is total; Deq is partial. |
| sending a request; its confirmation | An invocation and its matching response. §2.1. |
| before; overlap; judged by the sun | One operation's response precedes the other's invocation; otherwise concurrent. The real-time partial order <H, §2.2, which no process observes. |
| a single steward with a single board | The object's sequential specification. A legal sequential history. |
| the rule of the board | Extend the history with responses to some pending invocations, drop the rest; the result is equivalent to a legal sequential history that respects <H. Linearizability, L1 and L2, §2.2. |
| each thing's moment inside its span | The instant between invocation and response at which the operation appears to take effect. §1, §6.2. |
| the goatherd's morning | An enqueue completes before another begins, and the later item is dequeued first. Sequentially consistent but not linearizable: H₇; with overlap, H₂ (Fig. 1b). |
| the four mornings | H₁ (acceptable), H₂ (not), H₃ (an operation takes effect before its response), H₄ (one item dequeued twice, not acceptable), Fig. 1. |
| the tallies' first | Lamport's happened-before, extended to a total order by process identifiers. Not in this paper; neither it nor <H contains the other. |
| serving by entry at House 3's gate | A single-copy implementation whose linearization point is the step at which the request is applied. The single-valued abstraction function of §4.2, in the easy case. |
| copies acting as one | Linearizability is stated on invocations and responses alone and does not see the implementation. §2.2; the implementor is free to realise any level of concurrency, §6.2. |
| One Board at a Time; grain and oil | A history is linearizable if and only if each object's subhistory is. Locality, Theorem 1, §3.1. |
| the looser rule; each board served the other house first | Sequential consistency; each queue's subhistory is sequentially consistent and the whole is not. Lamport 1979; H₈, §3.3. |
| No Request Waits on Another | A pending invocation of a total operation can always be completed without breaking linearizability. Nonblocking, Theorem 2, §3.2. |
| a loader at an empty board | Blocking on a partial operation, which the nonblocking property allows. Deq on the empty queue, §3.2. |
| several things done as one; one of two called off | A transaction; serializability is neither local nor nonblocking. §3.3. The paper's blocking example, H₉, uses two registers; H₈ read as transactions is strictly serializable per object and not overall. Footnote 1: there is no counterpart to aborting for linearizability. |
| the busy board; slots; the peg | The lock-free queue: the array items and the index back. §4.2. |
| taking a number; putting a tablet in; looking at the peg; emptying a slot | INC (returning the old value); STORE; READ; SWAP with null. §4.2. |
| the race of the two clerks and the loader | Two concurrent enqueues and a dequeue whose request depends on a later race, so no single-valued abstraction function exists. §4.2. The paper's trace shows READ(q.back) returning 2 after two INCs from 1; with INC returning the old value it would be 3, giving the two slots the trace walks. |
| what the board could mean | An abstraction function to sets of queue values, with the representation invariant kept between every step. A: REP → 2ABS, §4.2–4.3.3. |
| put in before another's number was taken | x's STORE precedes y's INC. The partial order <r. |
| sequences the business could have produced | Linearized values. Lin(H), §4.3.1. |
| The Board Keeps the Rule | A(r) ⊆ Lin(H|ABS) for every linearized representation value. §4.3.2; Theorem 17, Appendix II, using Lemmas 15 and 16. Supporting lemmas are proved in the technical report [45]. |
| in order, none vanishes, none invented | Theorems 6–8, §5.2. Theorem 6 alone was Gottlieb, Lubachevsky and Rudolph's condition. |
| a loader overtaken for ever; a board that never serves | Linearizability is a safety property only. §4.2; §6.2. |
The paper behind this book. Maurice P. Herlihy and Jeannette M. Wing, Linearizability: A Correctness Condition for Concurrent Objects. ACM Transactions on Programming Languages and Systems 12, 3 (July 1990), 463–492. The definition, locality (Theorem 1), the nonblocking property (Theorem 2), the comparison with sequential consistency and serializability, the proof method with set-valued abstraction functions, and the concurrent queue.
The ideas. A shared object is correct, Herlihy and Wing propose, if every operation appears to take effect at a single instant somewhere between its call and its return. Then the results are those of some one-at-a-time execution, and that execution respects real time: an operation that finished before another started comes first. This is linearizability. It lets a concurrent queue be specified as an ordinary queue, and it says nothing about how the object is built, so one copy or many are judged alike.
Real-time order is not Lamport's causal order. An operation can finish before another starts with no message between them, and operations joined by messages can still overlap. Neither order contains the other, and linearizability is the one an outside observer comparing notes would expect.
Linearizability is local: a system is linearizable exactly when each object is. And it is nonblocking: a pending call of an operation that is always defined can always be completed. Sequential consistency drops real time and loses locality; serializability, over multi-operation transactions, loses both and needs a way to abort.
When no single step of an implementation can be named as an operation's instant, Herlihy and Wing map each state to the set of abstract values it could stand for, and show that set is always among the values the history could have produced. Their example is a lock-free queue built from fetch-and-increment and swap.
Herlihy, M. P., and Wing, J. M. Linearizability: a correctness condition for concurrent objects. ACM Trans. Program. Lang. Syst. 12, 3 (1990), 463–492.