一致性与线性一致性

6.5840 2026 Lecture 8: Consistency, Linearizability

today's topic: consistency models, specifically linearizability

consistency model:
  a spec for the relationship of different clients' views of a service
  I'll focus on key/value storage with network clients
    given a bunch of put/get calls, what outcome(s) are valid?
  assuming individual operations, in isolation, are correct

in ordinary sequential programming, there's nothing to talk about:
  we expect a read to yield the last written value

when might there be any question about what's correct?
  [simple client/server diagrams]
  read simultaneous with write
  replicas
  caches
  failure, recovery
  lost messages + retransmission

why does a storage system need an explicit consistency model?
  for applications, hard to be correct w/o guarantees from storage
    e.g. producer computes, then executes
      put("result", 27)
      put("done", true)
    consumer executes
      while get("done") == false:
        pause
      v = get("result")
    is v guaranteed to be 27?
  for services, hard to design/optimize w/o a specification
    e.g. OK for clients to read from GFS replicas? from Raft followers?

there are lots of consistency models
  today: linearizability
  but we'll also see:
    eventual consistency
    causal consistency
    fork consistency
    serializability
  driving force: tradeoffs among
    performance
    simplicity
    fault tolerance

linearizability
  it's a specification -- a requirement for how a service must behave
    from clients' point of view: from outside the service
  it's usually what people mean by "strong consistency".
    few "anomalies" / surprises
    a gold standard
    but rules out many optimizations.
  important for us:
    Raft is intended for building fault-tolerant linearizable services
    Lab 4 will be a linearizable key/value store on Raft

starting point
  we assume that there's a serial spec for what individual operations do
  serial = a single server executing operations one at a time
  db[]
  put(k, v):
    db[k] = v
    return true
  get(k):
    return db[k]
  no surprises here.

what about concurrent client operations?
  "concurrent" = overlap in time
  a client sends an RPC request;
    takes some time crossing the network;
    server computes, talks to replicas, &c;
    reply moves through network;
    client receives reply
  other clients may send/receive/wait during that time!
  the serial spec doesn't tell us what results are legal
  we need a way to describe concurrent scenarios,
    so we can talk about which results are/aren't allowed

definition: a history
  describes a time-line of possibly-concurrent operations
  each operation tagged w/ client start and finish times
    time client sent RPC request; time received reply
    as well as argument and return values
  example:
    C1: |-Wx1-| |-Wx2-|
    C2:   |---Rx2---|
  the x-axis is real time
    |- indicates the time at which client sent request
    -| indicates the time at which the client received the reply
  "Wx1" means put(x, 1)
  "Rx2" means get(x) -> 2
  records assumed to start with some undefined value
  C1 sent put(x, 1), recv reply, sent put(x, 2), recv reply
    writes have responses, signifying completion
  C2 sent get(x), recv reply=2

a history is a trace of what clients saw (or might see)
  used to check whether the execution was linearizable
  used by designers in "would this be OK" thought experiments

definition: a history is linearizable if
  * you can find a point in time for each operation
    between its start and finish, and
  * the history's result values are the same as serial
    execution in point order.

example history 1:
  |--Wx1--| |--Wx2--|
     |----Rx2----|
       |--Rx1--|

is this history linearizable?
  can we find a linearization point for each operation?
  we may need to try a few different point assignments.
  this order of points satisfies the rules:
    Wx1 Rx1 Wx2 Rx2
  1. each point lies between start and finish.
  2. the sequence satisfies the serial put/get spec.
  so: yes, this history is linearizable
    (and it's an answer to The Question)

note: either read could have returned either 1 or 2.
  so linearizability often allows multiple different outcomes.
  so we often can't predict in advance, but we can check afterwards.

note: the service may not have executed the operations at those points!
  we're not concerned here with how the service operated internally
  we only care that the client-visible results could have
    resulted from execution in some point order

what can we do with the linearizability definition?
  for designer: could this optimization result in non-linearizable results?
  for programmer: what can I assume / expect as a client?
  for testing: generate requests, check observed history.

why is it called "linearizability"?
  the linearization points turn concurrent operations
    into a serial execution -- "linear".
  thus "linearizable" in the sense that the results are the same
    as some linear execution of the operations.

example 2:
  |-Wx1-| |----Wx2----|
                  |-Rx1-|
  linearizable?
    if yes, linearization points?
  so: concurrent read/write can go either way

example 3: like example 2, but...
  |-Wx1-| |----Wx2----|
    |---Rx2---|
                |-Rx1-|
we can try a few assignments of linearization points.
  how about Wx1 Wx2 Rx2 Rx1?
  not valid because "Wx2 Rx1" doesn't conform to serial spec.
how to show something *isn't* linearizable?
  show that no assignment of points works.
  i.e. breaks either time rule or value rule.
no assignment works for example 2!
  Wx2's point must be before Rx2's point
  so Wx2's point is also before Rx1's point
  so the second read got an impossible value
thus, if a system can produce this history, we know the
  system isn't linearizable: has a bug, or never promised linearizability.
the Rx1 *would* have been legal if there had been no Rx2
  reads -- not just writes -- can affect what's subsequently legal
so, if we want linearizability:
  once any read sees a write, all strictly-subsequent reads must also see it.
    rules out split-brain
  can't forget a revealed write
    rules out e.g. forgetting data due to a crash

GFS is not linearizable: it can produce example 3 since
  the Rx1 could come from a replica that hasn't yet been updated.
  if we wanted GFS to be linearizable,
    one approach is to have client reads go through the primary too.
    would be slower!

example 4:
|--Wx0--|  |--Wx1--|
            |--Wx2--|
C1:      |-Rx2-| |-Rx1-|
C2:      |-Rx1-| |-Rx2-|
can there be a serial order?
  C1 needs Wx2 Rx2 Wx1 Rx1
  C2 needs Wx1 Rx1 Wx2 Rx2
  we can't have both Wx2 before Wx1, and Wx2 after Wx1.
  so not linearizable.
so:
  service can choose either order for concurrent writes
  but all clients must see the writes in the same order
  this is important when there are replicas or caches
    they must all appear to execute operations in the same order

example 5:
|-Wx1-|
        |-Wx2-|
                |-Rx1-|
no order is possible -- not linearizable
so:
  linearizability rules out "stale" reads
  even if the reader doesn't know there was a write
    the time rule requires reads to see the latest completed update
  "no stale data" restricts caching and replication designs

linearizability outlaws many design possibilities / anomalies:
  split brain (two active leaders)
  forgetting completed writes after a crash+reboot
  reading from lagging replicas or out-of-date caches

example 6:
[client / network / server diagram]
C1 sends put(x, 1)
C2 sends put(x, 2)
service receives C1's request;
  network drops response;
  C1's RPC library re-sends request
is it legal for service to execute *both* of C1's request messages?
we then might see this if C3 reads three times:
C1: |--------Wx1---------| (due to retransmission)
C2:        |-Wx2-|
C3:   |-Rx1-| |-Rx2-|  |-Rx1-|
this history is not linearizable!
so, if we want linearizability:
  repeated requests from retransmissions should only execute once!
  the Raft paper mentions this issue (and a solution) in Section 8

linearizable systems are not limited to just read and write operations
  increment
  append
  test-and-set (to implement locks)
  any self-contained single-object operation

application programmers like linearizability:
  * reads see latest data -- never stale
  * all clients see the same data (when there aren't writes)
  * all clients see data changes in the same order
    so my put(v,27); put(done,true); example works
  these benefits will be clearer when we look at weaker consistencies.

can we have better semantics than linearizability?
  or, what might you want that linearizability won't support?
  * transactions: atomic *groups* of operations on different objects
    linearizability only thinks about individual operations, not groups of ops
  * operations that themselves invoke other services

how can we implement linearizability?
  depends on how much replication, caching, and fault-tolerance we want.

single serial server that doesn't crash.
  [diagram: clients, server, op queue, state]
  server picks an order for concurrently arriving client requests.
  executes them in that order, one at a time,
    replies to each before starting the next.
  plus duplicate request suppression

this simple implementation directly implements linearizability definition
  executes in serial order, one at a time
  executes an operation after it is received
    and doesn't reply until after operation is finished
  (thus can't eagerly reply to put()s)

good news: server does not have to reason about histories,
  linearization points, or concurrency.

what about fault-tolerant linearizability?
  primary-backup replication
    like GFS but would need modifications e.g. read only via primary
  Raft!
  and we'll see more examples

what about the performance of linearizable systems?

a fundamental performance limit imposed by no-stale-reads rule:
  [W, E]
  a write on the west coast, which completes
  then a read on the east coast
  there *must* be communication of the written value
    *and* either reader or writer must wait for communication
  speed of light is a serious problem:
    dozens of milliseconds cross-country
    can limit serial throughput to a few tens per second

generally:
  bad news: serial aspect makes it hard to get parallel speedup for individ objs
  bad news: if replication, then lots of communication and waiting
  bad news: if replication, replicas must be reachable,
            limiting fault tolerance
  good news: you can shard by key

what about other consistency models?
  can they allow better performance?
  do they have intuitive semantics?

example: eventual consistency -- a weak model
  [diagram: two copies, clients]
  multiple copies of the data (e.g. in different datacenters, for speed)
  a read consults any replica (e.g. closest)
  a write updates any replica (e.g. closest)
    replica sends response when that one update is done
  replicas synchronize updates in the background
    eventually, other replicas will see my update

many systems provide eventual consistency
  faster than linearizability
    especially if replicas are in different cities for fault-tolerance
  and more available -- any one replica will do
    no waiting for primary/backup communication or Raft quorum
  Amazon's Dynamo; Cassandra; GFS (sort of)

but eventual consistency exposes some anomalies to application programmer:
  * reads can see stale data
    a problem for password change, ACL change
  * writes may appear out of order
    breaks my result/done example
  * different clients may see different data
  * concurrent writes to same item need to be resolved somehow!
    C1: put(x, 1)
    C2: put(x, 2)
    may initially be applied at different replicas
    only later will they be pushed to other replicas
    how to merge concurrent new values?
    how to ensure all replicas choose the same final value?
      so that, eventually, they are identical?
  * eventual consistency cannot support e.g. test-and-set

A general pattern: you can usually choose only one of these:
  Strong consistency
  Maximum availability

But not both.
  Strong consistency makes you wait to update replicas,
    and can't proceed if too many replicas are unavailable.
    Thus poor availability.
  Eventual consistency can proceed even if no other replicas are reachable.
    But has poor consistency.

Next week:
  ZooKeeper, an interesting service built on a Raft-like protocol
    combines strong and weak consistency

---

https://jepsen.io/consistency/models

Linearizability: A Correctness Condition for
Concurrent Objects
MAURICE P. HERLIHY and JEANNETTE M. WING
Carnegie Mellon University
A concurrent object is a data object shared by concurrent processes. Linearizability is a correctness
condition for concurrent objects that exploits the semantics of abstract data types. It permits a high
degree of concurrency, yet it permits programmers to specify and reason about concurrent objects
using known techniques from the sequential domain. Linearizability provides the illusion that each
operation applied by concurrent processes takes effect instantaneously at some point between its
invocation and its response, implying that the meaning of a concurrent object’s operations can be
given by pre- and post-conditions. This paper defines linearizability, compares it to other correctness
conditions, presents and demonstrates a method for proving the correctness of implementations, and
shows how to reason about concurrent objects, given they are linearizable.
Categories and Subject Descriptors: D.1.3 [Programming Techniques]: Concurrent Programming;
D.2.1 [Software Engineering]: Requirements/Specifications; D.3.3 [Programming Lan-
guages]: Language Constructs--abstract data types, concurrent programming structures, data types
and structures; F.1.2 [Computation by Abstract Devices]: Modes of Computation-parallelism;
F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about
Programs-pre- and post-conditions, specification techniques
General Terms: Theory, Verification
Additional Key Words and Phrases: Concurrrency, correctness, Larch, linearizability, multi-
processing, serializability, shared memory, specification
1. INTRODUCTION
1 .l Overview
Informally, a concurrent system consists of a collection of sequential processes
that communicate through shared typed objects. This model encompasses both
message-passing architectures in which the shared objects are message queues,
A preliminary version of this paper appeared in the Proceedings of the 14th ACM Symposium on
Principles of Programming Languages, January 1987 [21].
This research was sponsored by IBM and the Defense Advanced Research Projects Agents (DOD),
ARPA order 4976 (Amendment 20), under contract F33615-87-C-1499, monitored by the Avionics
Laboratory, Air Force Wright Aeronautical Laboratories, Wright-Patterson AFB. Additional spport
for J. M. Wing was provided in part by the National Science Foundation under grant CCR-8620027.
The views and conclusions contained in this document are those of the authors and should not be
interpreted as representing the official policies, either expressed or implied, of the Defense Advanced
Research Projects Agency or the US Government.
Authors’ address: Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA
15213-3890.
Permission to copy without fee all or part of this material is granted provided that the copies are not
made or distributed for direct commercial advantage, the ACM copyright notice and the title of the
publication and its date appear, and notice is given that copying is by permission of the Association
for Computing Machinery. To copy otherwise, or to republish, requires a fee and/or specific
permission.
0 1990 ACM 0164-0925/90/0700-0463 $01.50
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990, Pages 463-492.

464 l M. Herlihy and J. Wing
and shared-memory architectures in which the shared objects are data structures
in memory. Each object has a type, which defines a set of possible values and a
set of primitive operations that provide the only means to create and manipulate
that object. In a sequential system, where an object’s operations are invoked one
at a time by a single process, the meaning of the operations can be given by pre-
and postconditions. In a concurrent system, however, an object’s operations can
be invoked by concurrent processes, and it is necessary to give a meaning to
possible interleavings of operation invocations.
A concurrent computation is linearizable if it is “equivalent,” in a sense formally
defined in Section 2, to a legal sequential computation. We interpret a data type’s
(sequential) axiomatic specification as permitting only linearizable interleavings.
Instead of leaving data uninterpreted, linearizability exploits the semantics of
abstract data types; it permits a high degree of concurrency, yet it permits
programmers to specify and reason about concurrent objects using standard
verification techniques. Unlike alternative correctness conditions such as sequen-
tial consistency [31] or serializability [40], linearizability is a local property: a
system is linearizable if each individual object is linearizable. Locality enhances
modularity and concurrency, since objects can be implemented and verified
independently, and run-time scheduling can be completely decentralized. Linear-
izability is also a nonblocking property: processes invoking totally-defined oper-
ations are never forced to wait. Nonblocking enhances concurrency and implies
that linearizability is an appropriate condition for systems for which real-time
response is critical. Linearizability is a simple and intuitively appealing correct-
ness condition that generalizes and unifies a number of correctness conditions
both implicit and explicit in theliterature.
Using axiomatic specifications and our notion of linearizability, we can reason
about two kinds of problems:
(1) We reason about the correctness of linearizable object implementations using
new techniques that generalize the notions of representation invariant and
abstraction function [18, 251 to the concurrent domain.
(2) We reason about computations that use linearizable objects by transforming
assertions about concurrent computations into simpler assertions about their
sequential counterparts.
Section 2 presents our model of a concurrent system and the formal definition
of linearizability. Section 3 discusses linearizability’s locality and nonblocking
properties and compares it to other correctness conditions. Section 4 presents
our proof technique for reasoning about implementations of linearizable objects,
and illustrates this technique on two novel implementations of a highly concur-
rent queue. Section 5 presents examples of reasoning about concurrent registers
and queues, given that they are linearizable. Section 6 surveys some related work
and discusses the significance of linearizability as a correctness condition.
1.2 Motivation
When defining a correctness condition for concurrent objects, two requirements
seem to make intuitive sense: First, each operation should appear to “take effect”
instantaneously, and second, the order of nonconcurrent operations should be
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 465
E(x) A D(Y) A E(z) A
t 4 I 4 I- . . . .
E(Y) B D(x) B
i 4 I I
(a) H1 (acceptable).
E(x) A D(Y) A
t I I I
(b) Hz (not acceptable).
E(x) A
I- . . .
D(x) B
I t
E(x) A
E(Y) B
t- I
(c) I-I3 (acceptable).
D(Y) A
I I
D(Y) C
I 4
(d) H, (not acceptable).
Fig. 1. FIFO queue histories.
preserved. These requirements allow us to describe acceptable concurrent behav-
ior directly in terms of acceptable sequential behavior, an approach that simplifies
both formal and informal reasoning about concurrent programs. We capture
these notions formally in the next section; here we informally review some
examples to illustrate what we do and do not consider intuitively acceptable
concurrent behavior. Our examples employ a first in, first out (FIFO) queue, a
simple data type that provides two operations: Enq inserts an item in the queue,
and Deq returns and removes the oldest item from the queue. Figure 1 shows
four different ways in which a FIFO queue might behave when manipulated by
concurrent processes. Here, a time axis runs from left to right, and each operation
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

466 l M. Herlihy and J. Wing
W(o) A R(l) A W(O) c
t I --
t
W(l) B
(a) H6 (acceptable).
R(O) B
I I t
W(O) A R(l) A W(O) c
t t --
W(l) B R(1) B
t I t t
(b) Ha (not acceptable).
Fig. 2. Register histories.
is associated with an interval. Overlapping intervals indicate concurrent opera-
tions. We use “E(x) A” (“D(X) A”) to stand for the enqueue (dequeue) operation
of item x by process A.
The behavior shown in H1 (Figure la) corresponds to our intuitive notion of
how a concurrent FIFO queue should behave. In this scenario, processes A and
B concurrently enqueue x and y. Later, B dequeues x, and then A dequeues y and
begins enqueuing z. Since the dequeue for x precedes the dequeue for y, the FIFO
property implies that their enqueues must have taken effect in the same order.
In fact, their enqueues were concurrent, thus they could indeed have taken effect
in that order. The uncompleted enqueue of z by A illustrates that we are interested
in behaviors in which processes are continually executing operations, perhaps
forever.
The behavior shown in HP, however, is not intuitively acceptable. Here, it is
clear to an external observer that x was enqueued before y, yet y is dequeued
without x having been dequeued. To be consistent with our informal require-
ments, A should have dequeued x. We consider the behavior shown in H3 to be
acceptable, even though x is dequeued before its enqueuing operation has re-
turned. Intuitively, the enqueue of x took effect before it completed. Finally, Hq
is clearly unacceptable because y is dequeued twice.
To decide whether a concurrent history is acceptable, it is necessary to take
into account the object’s intended semantics. For example, acceptable concurrent
behaviors for FIFO queues would not be acceptable for stacks, sets, directories,
etc. When restricted to register objects providing read and write operations, our
intuitive notion of acceptability corresponds exactly to the notion used in Misra’s
careful axiomatization of concurrent registers [35]. Our approach can be thought
of as generalizing Misra’s approach to objects with richer sets of operations. For
example, H5 in Figure 2a is acceptable, but H6 is not (examples are taken from
[35]). These two behaviors differ at one point: In Hg, B reads a 0, and in Hg,
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 467
B reads a 1. The latter is intuitively unacceptable because A did a previous read
of a 1, implying that B’s write of 1 must have occurred before A’s read. C’s
subsequent write of 0, though concurrent with B’s write of 1, strictly follows A’s
read of 1.
In the next section, we formalize the intuition presented here by defining
the notion of linearizability to encompass those histories we have argued are
intuitively acceptable.
2. SYSTEM MODEL AND DEFINITION OF LINEARIZABILITY
2.1 Histories
Informally, a concurrent system consists of a collection of sequential threads of
control called processes that communicate through shared data structures called
objects. Each object has a unique name and a type. The type defines a set of
possible values, and a set of primitive operations that provide the only means to
manipulate that object. Processes are sequential: each process applies a sequence
of operations to objects, alternately issuing an invocation and then receiving the
associated response. (Dynamic process creation can be modeled simply by treating
each child process as an additional process that executes no operations before
the fork or after the join.)
Formally, an execution of a concurrent system is modeled by a history, which
is a finite sequence of operation invocation and response events. A subhistory of
a history H is a subsequence of the events of H. An operation invocation is
written as (x op(args*) A), where x is an object name, op is an operation name,
args* denotes a sequence of argument values, and A is a process name. The
response to an operation invocation is written as (x term(res*) A), where term
is a termination condition, and res* is a sequence of results. We use “Ok” for
normal termination. A response matches an invocation if their object names
agree and their process names agree. An invocation is pending in a history if
no matching response follows the invocation. If H is a history, complete(H) is
the maximal subsequence of H consisting only of invocations and matching
responses.
A history H is sequential if:
(1) The first event of H is an invocation.
(2) Each invocation, except possibly the last, is immediately followed by a
matching response. Each response is immediately followed by a matching
invocation.
A history that is not sequential is concurrent.
A process subhistory, H 1 P (H at P), of a history H is the subsequence of all
events in H whose process names are P. An object subhistory H 1 x is similarly
defined for an object x. Two histories H and H’ are equivalent if for every process
P, H 1 P = H’ ) P. A history H is well-formed if each process subhistory H ) P of
H is sequential. All histories considered in this paper are assumed to be well-
formed. Notice that whereas process subhistories of a well-formed history are
necessarily sequential, object subhistories are not.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

468 l M. Herlihy and J. Wing
An operation, e, in a history is a pair consisting of an invocation, inv(e), and
the next matching response, res(e). We denote an operation by [q inv/res A],
where q is an object and A a process. An operation e. lies within another operation
e, in H if inu (e,) precedes inu (eo) and res (eo) precedes res (ei) in H. Angle brackets
for events and square brackets for operations are omitted where they would
otherwise be unnecessarily confusing; object and process names are omitted
where they are clear from context.
For example, H, of Figure 1 is the following well-formed history for a FIFO
queue q.
Q Endx) A
4 EwW B
q Ok( 1 B
q W 1 A
q De4 1 B
q Ok(x) B
q Ded 1 A
q Ok(y) A
q Endz) A
The first event in H, is an invocation of Enq with argument x by process
A, and the fourth event is the matching response with termination condition
Ok and no results. The [q Enq(y)/Ok( ) B] operation lies within the
[q Enq(x)/Ok( ) A] operation. The subhistory, complete (H,), is H1 with the last
(pending) invocation of Enq removed. Reordering the first two events yields one
of many histories equivalent to H,.
A set S of histories is prefix-closed if, whenever H is in S, every prefix of H is
also in S. A single-object history is one in which all events are associated with
the same object. A sequential specification for an object is a prefix-closed set of
single-object sequential histories for that object. A sequential history H is legal
if each object subhistory H ] x belongs to the sequential specification for x. Many
conventional techniques exist for defining sequential specifications. In this paper,
we use the axiomatic style of Larch [19], in which an object’s sequential history
is summarized by a value, which (informally speaking) reflects the object’s state
at the end of the history. These values are used in axioms giving the pre- and
postconditions on the objects operations. For example, axioms for the Enq and
Deq operations for FIFO queues are shown in Figure 3. The post-condition for
Enq states that on termination, the new queue value is the old queue value with
e inserted. The specification for Deq states that applying that operation to a
non-empty queue removes the first item from the queue. An operation is total if,
like Enq, it is defined for every object value, otherwise it is partial, like Deq
which is left undefined for the empty queue.
2.2 Definition of Linearizability
A history H induces an irreflexive partial order <u on operations:
e. <u e, if res(e,) precedes inv(el) in H.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects l 469
Axiom E:
WeI
EnqW / Ok0
(4’ = Wq, e))
Fig. 3. Axioms for queue operations.
Axiom D:
(9 f Ill
DeqO /Ok(e) (q’ = rest(q) A e = first(q))
(Where appropriate, subscripts on partial orders are omitted). Informally, <n
captures the “real-time” precedence ordering of operations in H. Operations
unrelated by <n are said to be concurrent. If H is sequential, <n is a total order.
A history H is linearizable if it can be extended (by appending zero or more
response events) to some history H’ such that:
Ll: complete(H’) is equivalent to some legal sequential history S, and
L2: <H 2 CS.
Informally, extending H to H’ captures the notion that some pending invoca-
tions may have taken effect even though their responses have not yet been
returned to the caller (as in the pending Enq in history H, in Figure 1). Restricting
attention to complete(H’) captures the notion that the remaining pending
invocations have not yet had an effect. Ll states that processes act as if they
were interleaved at the granularity of complete operations. L2 states that this
apparent sequential interleaving respects the real-time precedence ordering of
operations.
We call S a linearization of H. Nondeterminism is inherent in the notion of
linearizability: (1) For each H, there may be more than one extension H’
satisfying the two conditions, Ll and L2, and (2) for each extension H’, there
may be more than one linearization S. A linearizable object is one whose concur-
rent histories are linearizable with respect to some sequential specification.
2.3 Queue Examples Revisited
Let “ . ” denote concatenation of events. The history H1 shown in Figure 1 is
linearizable, because H, . (q Ok( ) A) is equivalent to the following sequential
history:
q h(x) A (History Hi)
q ON ) A
q End B
q Ok( 1 B
q Ded ) B
q Ok(x) B
q De4 1 A
q Ok(y) A
q End4 A
q W 1 A
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

470 l M. Herlihy and J. Wing
Hz is not linear&able:
q h(x) A
q W 1 A
q Endy) B
q De4 1 A
q W 1 B
q Ok(y) A
(History HJ
because the complete Enq operation of x precedes the Enq of y, but y is dequeued
before x.
Linearizability does not rule out histories such as H3, in which an operation
“takes effect” before its return event occurs:
q EnqW A
q De4 1 B
q 0%) B
(History HJ
H, can be extended to Hi = H3 . (q Ok( ) A), which is equivalent to the sequential
history in which the enqueue operation occurs before the dequeue.
Finally, H4,
q J%(x) A
q Endy) B
q ON 1 A
q ON 1 B
q Ded ) A
q Ded 1 C
q Ok(y) A
q Ok(y) C
(History HJ
is not linearizable because y is enqueued once but dequeued twice, and hence H,
is not equivalent to any sequential FIFO queue history.
3. PROPERTIES OF LINEARIZABILITY
This section proves that linearizability is a local and nonblocking property, and
discusses the differences between it and other correctness conditions.
3.1 Locality
A property P of a concurrent system is said to be local if the system as a whole
satisfies P whenever each individual object satisfies P. Linearizability is a local
property:
THEOREM 1. H is linearizable if and only if, for each object x, H 1 x is linearizable.
PROOF. The “only if” part is obvious.
For each X, pick a linearization of H 1~. Let R, be the set of responses appended
to H 1 x to construct that linearization, and let cX be the corresponding lineari-
zation order. Let H’ be the history constructed by appending to H each response
in R,. We will construct a partial order < on the operations of complete(H’)
such that: (1) For each X, <X G <, and (2) <n C <. Let S be the sequential history
constructed by ordering the operations of complete(H’) in any total order that
extends <. Condition (1) implies that S is legal, hence that Ll is satisfied, and
Condition (2) implies that L2 is satisfied.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 471
Let < be the transitive closure of the union of all <X with <n. It is immediate
from the construction that < satisfies Conditions (1) and (2), but it remains to
be shown that < is a partial order. We argue by contradiction. If not, then there
exists a set of operations el, . . . , e,, such that e, < e2 < . . . < e,, e, < el, and
each pair is directly related by some <X or by <H. Choose a cycle whose length is
minimal.
Suppose all operations are associated with the same object X. Since <x is a
total order, there must exist two operations ei-1 and ei such that ei-1 < n ei and
ei <x ei-1, contradicting the linearizability of x.
The cycle must therefore include operations of at least two objects. By rein-
dexing if necessary, let el and e2 be operations of distinct objects. Let z be the
object associated with el. We claim that none of e2, . . . , e, can be an operation
of X. The claim holds for e2 by construction. Let ei be the first operation in
e3, . . . . e, associated with x. Since ei-1 and ei are unrelated by <%, they must be
related by <n; hence the response of ei-1 precedes the invocation of ei. The
invocation of e2 precedes the response of ei-1, since otherwise ei-1 <H e2, yielding
the shorter cycle e2, . . . , ei-1. Finally, the response of el precedes the invocation
of e2, since e, <n e2 by construction. It follows that the response to el precedes
the invocation of ei, hence el <n ei, yielding the shorter cycle el, ei, . . . , e,.
Since e, is not an operation of x, but e, < el, it follows that e, <n e,. But
el <u e2 by construction, and because < H is transitive, e, <n e2, yielding the
shorter cycle e2, . . . , e,, the final contradiction. II
Henceforth, we need consider only single-object histories.
Locality is important because it allows concurrent systems to be designed and
constructed in a modular fashion; linearizable objects can be implemented,
verified, and executed independently. A concurrent system based on a nonlocal
correctness property must either rely on a centralized scheduler for all objects,
or else satisfy additional constraints placed on objects to ensure that they follow
compatible scheduling protocols. Locality should not be taken for granted; as
discussed below, the literature includes proposals for alternative correctness
properties that are not local.
3.2 Blocking versus Nonblocking
Linearizability is a nonblocking property: a pending invocation of a totally-
defined operation is never required to wait for another pending invocation to
complete.
THEOREM 2. Let inv be an invocation of a total operation. If (x inv P) is
a pending invocation in a linearizable history H, then there exists a response
(x res P) such that H . (x res P) is linearizable.
PROOF. Let S be any linearization of H. If S includes a response (x res P) to
(x inv P), we are done, since S is also a linearization of H e (x res P). Otherwise,
(x inv P) does not appear in S either, since linearizations, by definition, include
no pending invocations. Because the operation is total, there exists a response
(x res P) such that
S’ = S - (-2 inv P) . (x res P)
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

472 l M. Herlihy and J. Wing
is legal. S’, however, is a linearization of H . (X res P), and hence is also a
linearization of H. 0
This theorem implies that linearizability per se never forces a process with a
pending invocation of a total operation to block. Of course, blocking (or even
deadlock) may occur as artifacts of particular implementations of linearizability,
but is is not inherent to the correctness property itself. (Techniques for con-
structing nonblocking implementations of linearizable objects are discussed
elsewhere [23].) This theorem suggests that linearizability is an appropriate
correctness condition for systems where concurrency and real-time response
are important. We shall see that alternative correctness conditions, such as
serializability, do not share this nonblocking property.
The nonblocking property does not rule out blocking in situations where it is
explicitly intended. For example, it may be sensible for a process attempting to
dequeue from an empty queue to block, waiting until another process enqueues
an item. Our queue specification captures this intention by making Deq’s speci-
fication partial, leaving it undefined for the empty queue. The most natural
concurrent interpretation of a partial sequential specification is simply to wait
until the object reaches a state in which the operation is defined.
3.3 Comparison to Other Correctness Conditions
Lamport’s notion of sequential consistency [31] requires that a history be equiv-
alent to a legal sequential history. Sequential consistency is weaker than linear-
izability, because it does not require the original history’s precedence ordering
to be preserved. For example, history H7 is sequentially consistent, but not
linearizable:
q End4 A
q Ok( 1 A
q Endy) B
q ON 1 B
q De4 1 B
q Ok(y) B
(History H7)
Sequential consistency is not a local property. Consider the following history
H8, in which processes A and B operate on queue objects p and q.
P End4 A (History H8)
P ON 1 A
q Endy) B
q W ) B
q Enqbd A
q ON 1 A
P Enqb) B
POkOB
P De4 1 A
P Ok(y) A
q D-d ) B
q Ok(x) B
It is easily checked that H, ] p and H8 ] q are sequentially consistent, but Hs itself
it not.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 473
Much work on databases and distributed systems uses serializability [40] as
the basic correctness condition for concurrent computations.l In this model, a
transaction is a thread of control that applies a finite sequence of primitive
operations to a set of objects shared with other transactions.’ A history is
serializable if it is equivalent to one in which transactions appear to execute
sequentially, i.e., without interleaving. A (partial) precedence order can be defined
on non-overlapping pairs of transactions in the obvious way. A history is strictly
serializable if the transactions’ order in the sequential history is compatible with
their precedence order. Strict serializability is ensured by some synchronization
mechanisms, such as two-phase locking [12], but not by others, such as multi-
version timestamp schemes [41], or schemes that provide high levels of availa-
bility in the presence of network partitions [22].
Linearizability can be viewed as a special case of strict serializability where
transactions are restricted to consist of a single operation applied to a single
object. Nevertheless, this single-operation restriction has far-reaching practical
and formal consequences, giving linearizable computations a different flavor from
their serializable counterparts. An immediate practical consequence is that con-
currency control mechanisms appropriate for serializability are typically inap-
propriate for linearizability because they introduce unnecessary overhead and
place unnecessary restrictions on concurrency. For example, the queue imple-
mentation given below in Section 4 is much more efficient and much more
concurrent than an analogous implementation using conventional serializability-
oriented techniques such as two-phase locking or multi-version timestamping.
One important formal difference between linearizability and serializability is
that neither serializability nor strict serializability is a local property. For
example, in history Hs shown above, if we interpret A and B as transactions
instead of processes, then it is easily seen that both Hs ] p and Hs ] q are strictly
serializable but He is not. (Because A and B overlap at each object, they are
unrelated by transaction precedence in either subhistory.) Moreover, since A and
B each dequeues an item enqueued by the other, H8 is not even serializable. A
practical consequence of this observation is that implementors of objects in
serializable systems must rely on global conventions to ensure that all objects’
concurrency control mechanisms are compatible with one another. For example,
it is well known that two-phase locking is incompatible with multiversion
timestamping [46].
Another important formal difference is that serializability places more rigorous
restrictions on concurrency. Serializability is inherently a blocking property:
under certain circumstances, a transaction may be unable to complete a pending
operation without violating serializability, even if the operation is total. Such a
transaction must be rolled back and restarted, implying that additional mecha-
nisms must be provided for that purpose. For example, consider the following
i In practice, serializability is almost always provided in conjunction with failure atomicity, ensuring
that a transaction unable to execute to completion will be automatically rolled back. There is no
counterpart to failure atomicity for linearizability.
* Some models permit transactions to be nested, or to encompass concurrent threads of control. Our
remarks about locality and nonblocking hold for these more elaborate models as well.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

474 l M. Herlihy and J. Wing
history involving two register objects: x and y, and two transactions: A and B.
x Read( ) A (History H,)
y Read( ) B
x Ok(O) A
Y Ok(O) B
x Write(l) B
y Write(l) A
Here, A and B respectively read x and y and then attempt to write new values to
y and x. It is easy to see that both pending invocations cannot be completed
without violating serializability. Although different concurrency control mecha-
nisms would resolve this conflict in different ways, such deadlocks are not an
artifact of any particular mechanism; they are inherent to the notion of serializ-
ability itself. By contrast, we have seen that linearizability never forces processes
executing total operations to wait for one another.
Perhaps the major practical distinction between serializability and lineariza-
bility is that the two notions are appropriate for different problem domains.
Serializability is appropriate for systems such as databases in which it must be
easy for application programmers to preserve complex application-specific invar-
iants spanning multiple objects. A general-purpose serialization protocol, such as
two-phase locking, enables programmers to reason about transactions as if they
were sequential programs (setting aside questions of deadlock or performance).
Linearizability, by contrast, is intended for applications such as multiprocessor
operating systems in which concurrency is of primary interest, and where pro-
grammers are willing to apply special-purpose synchronization protocols, and to
reason explicitly about the effects of concurrency.
4. VERIFYING THAT IMPLEMENTATIONS ARE LINEARIZABLE
In this section, we motivate and describe our method for verifying implementa-
tions of linearizable objects. We begin with our definition of when an implemen-
tation is correct. In order to prove correctness, we reexamine the notions of
representation invariant and abstraction function (Section 4.2), and use their
new interpretation in our proof method (Section 4.3).
4.1 Definition of Correctness
An implementation is a set of histories in which events of two objects, a
representation (or rep) object REP of type REP and an abstract object ABS of type
ABS, are interleaved in a constrained way: for each history H in the implemen-
tation, (1) the subhistories H ( REP and H ( ABS satisfy the usual well-formedness
conditions; and (2) for each process P, each rep operation in H ] P lies within an
abstract operation in H ] P. Informally, an abstract operation is implemented by
the sequence of rep operations that occur within it.
An implementation is correct with respect to the specification of ABS if for
every history H in the implementation, H ( ABS is linearizable.
4.2 Representation Invariant and Abstraction Function
We first review how to verify the correctness of sequential objects [18, 251. In
the sequential domain, an implementation consists of an abstract type ABS, the
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990

Linearizability: A Correctness Condition for Concurrent Objects 475
type being implemented, and a representation type REP, the type used to
implement ABS. The subset of REP values that are legal representations
is characterized by a predicate called the rep invariant, I: REP + BOOL.
The meaning of a legal representation is given by an abstraction function,
A: REP + ABS, defined for representation values that satisfy the invariant.
An abstract operation (Y is implemented by a sequence, p, of rep operations
that carries the rep from one legal value to another, perhaps passing through
intermediate values where the abstraction function is undefined. The rep invar-
iant is thus part of both the precondition and postcondition for each operation’s
implementation; it must be satisfied between abstract operations, although it
may be temporarily violated while an operation is in progress. An implementation,
p, of an abstract operation, a, is correct if there exists a rep invariant, I, and
abstraction function, A, such that whenever p carries one legal rep value r to
another r’, CY carries the abstract value from A(r) to A(r’).
This verification technique must be substantially modified before it can be
applied to concurrent objects: we change both the meaning of the rep invariant
and the signature of the abstraction function. To help motivate these changes
and to make our discussion as concrete as possible, consider the following highly
concurrent implementation of a linearizable FIFO queue. The queue’s represen-
tation is a record with two components: items is an array having a low bound of
1 and a (conceptually) infinite high bound, and buck is the (integer) index of the
next unused position in items.
rep = record [back: int, items: array [item]]
Each element of items is initialized to a special null value, and back is initialized
to 1. Enq and Deq are implemented as follows:
Enq = proc (q: queue, x: item)
i: int := INC(q.back) %Allocate a new slot.
STORE (q.items[i], x) % Fill it.
end Enq
Deq = proc (q: queue) returns (item)
while true do
range: int := READ(q.back) - 1
for i: int in 1 . . range do
x: item := SWAP(q.items[i], null)
if x -= null then return(x) end
end
end
end Deq
An Enq execution occurs in two distinct steps, which may be interleaved with
steps of other concurrent operations: an array slot is reserved by atomically
incrementing back, and the new item is stored in items.3 Deq traverses the array
in ascending order, starting at index 1. For each element, it atomically swaps
null with the current contents. If the value returned is not equal to null,
3 Like the FETCH-AND-ADD operation [30], INC returns the value of its argument from before the
invocation, not the newly incremented value.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

476 l M. Herlihy and J. Wing
Deq returns that value, otherwise it tries the next slot. If the index reaches
q.back - 1 without encountering a nonnull element, the operation is restarted.
(Note that there is a small chance that a dequeuing process may starve if it is
continually overtaken by other dequeuing processes. Any queue item, however,
will eventually be dequeued as long as there are active dequeuers.) All atomic
steps can be interleaved with steps of other operations. An interesting aspect of
this implementation is that there is no mutual exclusion: no process can delay
other processes by halting in a critical section. As an aside, we note that this
implementation could be rendered more efficient by reclaiming slots from which
items have been dequeued, reducing both the overall size of the rep of the queue
and the cost of dequeuing an item. Such optimizations, however, would add
nothing to our discussion of verification, so we ignore them in this paper.
The first difficulty arises when trying to define a rep invariant for this
implementation. For sequential objects, the rep invariant must be satisfied at the
start and tinish of each abstract operation, but it may be violated temporarily
while an operation is in progress. For concurrent objects, however, it no longer
makes sense to view the object’s representation as assuming meaningful values
only between abstract operations. For example, our queue implementation per-
mits operations to be in progress at every instant, thus the object may never be
“between operations.” When implementing a queue operation, one must be
prepared to encounter a rep value that reflects the incomplete effects of concur-
rent operations, a problem that has no analog in the sequential domain. To
assign a meaning to such transient values, the abstraction function must be
defined continually, not just between abstract operations. As a consequence, the
rep invariant must be preserved by each rep operation in the sequence imple-
menting each abstract operation.
Another, more subtle difficulty arises when attempting to define an abstraction
function. One natural approach is the following, proposed by Lamport [32]. A
(continually defined) abstraction function A is chosen so that each abstract
operation “takes effect” instantaneously at some step in its execution. In our
queue example, when a process enqueues an item X, exactly one of the opera-
tions implementing the Enq would carry the rep from r to r’, where A(r’) =
ins(A(r), x). Surprisingly, perhaps, this technique fails to work for our queue
implementation. To see why, we assume that such a function A exists, and we
derive a contradiction. Consider the following scenario. Processes A and B invoke
concurrent Enq operations, respectively enqueuing x and y. By incrementing the
back counter, A reserves array position 1 and B reserves array position 2. B stores
y in the array and returns. This computation is represented by the following
history, where rep operations are indented and shown in upper-case.
End4 A
EnqW B
INC(q.back) A
OK(l) A
INC(q.back) B
OK(2) B
STORE(q.items[2], y) B
OK( 1 B
ON 1 B
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 477
Let r be the rep value after this history. Because B’s Enq operation has
returned, A(r) must reflect B’s Enq. Because A’s Enq operation is still in progress,
A(r) may or may not reflect A’s Enq, depending on how A is defined. Thus, since
no other operations have occurred, A(r) must be one of [y], [y, n], or [x, y], where
the leftmost item is at the head of the queue.
We now derive a contradiction by showing that each of these values is
contradicted by some future computation. First, assume A(r) is [x, y]. If we now
suspend A and allow a third process C to execute a Deq, C’s Deq will return y,
contradicting our assumption.
De4 1 C
READ(q.back) C
OK(2) C
SWAP(q.items[l], y) C
OK(nul1) C
SWAP(q.items[B],y) C
OK(Y) C
Ok(y) C
Second, assume A(r) is [y] or [y, x]. Allow A to complete its Enq, leaving a rep
value r’. Now x must be in the queue, since its Enq is complete, and moreover it
must follow y in the queue since, by hypothesis, A’s enqueue appears to take
effect after B’s. It follows that A(r’) must be [y, x]. If C then executes a Deq,
however, it will return x, a contradiction.
STORE(q.items[l], x) A
OK( 1 A
Ok( ) A
Ded 1 C
READ(q.back) C
OK(2) C
SWAP(q.items[l], y) C
OK(x) C
Ok(x) C
The problem here is that the linearization order depends on a race condition:
A’s Enq will appear to occur before B’s if A stores into location 1 before C reads
from it, otherwise the order is reversed. Such nondeterminism is perfectly
acceptable, however, because all resulting histories are linearizable. We circum-
vent this difficulty by redefining the abstraction function to map a rep value to
a set of abstract values. This set represents the possible set of linearizations
permitted by the current value of the rep. For objects that permit low levels of
concurrrency, the value of the abstraction function might be a singleton set.
In conclusion, the rep invariant I must be continually satisfied and the
abstraction function continually defined, not only between abstract operations,
but also between rep operations implementing abstract operations. The abstrac-
tion function maps each rep value to a nonempty set of abstract values:
A: REP + 2ABS
The nondeterminism inherent in a concurrent computation thus gives our notions
of abstraction function and rep invariant a different flavor from their sequential
counterparts.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

478 l M. Herlihy and J. Wing
4.3 Verification Method
In the next three sections we show how we use our new interpretation of
representation invariant and abstraction function for proofs of correctness. We
illustrate these ideas on the queue example presented in the previous section, as
well as for an alternative implementation that uses critical sections.
4.3.1 Linearized Values. So far, linearizability is discussed in terms of histo-
ries. This characterization is useful for motivating the property, and for demon-
strating properties such as locality, but it is awkward for verification. For
linearizable histories, however, assertions about interleaved histories can be
transformed into assertions about sets of sequential histories, and thus, sets of
values. The transformed assertions can be stated and proved with the help of
familiar axiomatic methods developed for sequential programs.
For a given history H, we call the value of an object at the end of a linearization
of H a linearized value. Since a given history may have more than one lineariza-
tion, an object may have more than one linearized value at the end of a history.
We let Lin(H) denote the set of all linearized values of H. Informally, a history’s
linearized values represent the object’s possible values from the point of view of
an external observer. Figure 4 shows a queue history with its set of linearized
values after each event. Initially, only the empty queue is associated with the
empty history. After the invocation of Enq(x), there are two linearized values,
since the enqueue may or may not have taken effect. After the invocation of
Enq(y), there are five linearized values: either Enq may or may not have occurred,
and if both have occurred, either ordering is possible. After the response to
Enq(y), y is known to have been enqueued, and after the response to Enq(x),
both x and y must have been enqueued, although their order remains ambiguous
until x is dequeued.
4.3.2 Proof Method. To show correctness, the verification technique for se-
quential implementations is generalized as follows. Assume that the implemen-
tation of r is correct, hence H 1 REP is linearizable for all H in the implementation.
Our verification technique focuses on showing the following property:
For all r in Lin(H 1 REP), I(r) holds and A(r) G Lin(H 1 ABS)
This condition implies that Lin(H 1 ABS) is nonempty, hence that H 1 ABS is
linearizable. Note that the set inclusion is necessary in one direction only; there
may be linearized abstract values that have no corresponding representation
values. Such a situation arises when the representation “chooses” to linearize
concurrent operations in one of several permissible ways.
4.3.3 The Queue Example. Returning to our queue example, our verification
method is applied as follows. Let H I REP be a complete history for a queue
representation, REP. If r is a linearized value for H I REP, define items(r) to be
the set of non-null items in the array r.items. Let cr be the partial order such
that x cr y if the STORE operation for x precedes the INC operation for y in
H 1 REP. We can encode the partial order cr as auxiliary data. For a queue q, let
c4 denote the total order on its items, and items(q), the set of its items.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 479
History
Et-W) A
W(y) 13
Ok0 6
Ok0 A
DeqO C
Ok(x) C
Fig. 4. Linearized values.
The implementation has the following rep invariant:
I(r) = (r.back L 1)
A (Vi. i 2 r.back + r.items[i] = null)
A (lbound(r.items) = 1)
where Ibound is the lowest array index, and the following abstraction function:
A(r) = 14 ] items(r) = items(q) A cr C <J
In other words, a queue representation value corresponds to the set of queues
whose items are the items in the array, sorted in some order consistent with the
precedence order of their Enq operations. Thus, our implementation allows for
an item with a higher index to be removed from the array before an item with a
lower index, but only if the items were enqueued concurrently.
Figure 5 shows a sequence of abstract operations of Figure 4 along with their
implementing sequence of rep operations. Column two is the set of abstracted
linearized rep values. Column three is the set of linearized abstract values. Our
correctness criterion requires showing that each set in column two is a subset of
the corresponding set in column three.
Appendix II outlines a complete formal proof of correctness (see also [45]). It
relies on two key facts: (1) Enq enqueues an item x that is maximal with respect
to <,., and (2) Deq removes and returns an item x that is minimal with
respect to Cr.
4.3.4 Critical Sections. So far our method for proving the correctness of an
implementation assumes there exists a continually defined abstraction function.
If the object’s implementation includes critical sections, however, it may not
always be possible to define such a function. Within the critical section, the rep
invariant may be temporarily violated, leaving the abstraction function unde-
fined. We show here how to overcome this difficulty relying on the standard trick
of using (auxiliary) hidden data [37], thereby permitting us to reintroduce a
continually defined abstraction function with the extended representation as its
domain.
Both the problem and the solution are best illustrated by a simple example.
Let us replace the atomic SWAP operation with a sequence of rotations executed
within a critical section. Items are represented by 32-bit quantities, and the
queue representation is expanded to associate a lock with each item:
rep = recordtback: int, items: array[item],
locks: array[mutex])
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

480 l M. Herlihy and J. Wing
ROT& y) atomically rotates the 64-bit quantity by one bit. The Deq operation
is implemented as follows:
Deq = proc(q: queue) returns (item)
while true do
range: int := READ(q.back)-1
x: item := null
for i: int in l..range do
LOCK(q.locks[i] ) % start critical section
for k: int in 1..32 do
ROT(q.items[i], x)
end
UNLOCK(q.items[i]) % end critical section
if x -= null then return(x) end
end
end Deq
Although it is clear that this implementation is linearizable, its correctness
cannot be proved directly using the method outlined so far. While the rotation is
in progress, the abstraction function is undefined because necessary state infor-
mation is encoded in the process’s program counter and local variables, not in
the representation itself. Thus, we introduce an auxiliary array of items to hold
the value being shifted out of the queue, shown here as an additional field in the
representation. Auxiliary data and statements are shown in italics. Statements
enclosed in angle brackets are executed atomically.
rep = record(back: int
items: array[item] ,
aux: array[item],
locks: array[mutex]
Enq = proc(q: queue, x: item)
i: int := INC(q.back)
(STORE(q.items[i], x)
STORE(q.aux[i], x)) % Make a redundant copy.
end Enq
Deq = proc(q: queue) returns (item)
while true do
range: int := READ(q.back)-1
x: item := null
for i: int in l..range do
LOCK(q.locks[i]) % start critical section
for k: int in 1..32 do
ROT(q.items[i], x)
end
STURE(q.aux[i], null) % Update auxiliary array.
UNLOCK(q.items[i]) % end critical section
if x -= null then return(x) end
end
end Deq
By embedding the representation object in an extended representation, we can
give a continually defined abstraction function, one that agrees with the original
abstraction function when the object is quiescent. We can use our proof method
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 481
History A(Lin(H 1 REP)) Lin(H I AM)
EnW A INC(q.back) A
OK(l) A
STORE(q.items[l], x) A
OK0 A
EnW B
INC(q.back) B
OK(Z) B
STORE(q.items[P], y) B
OK0 B
Ok0 B
Ok0 A
DeqO C
READ(q.back) C
OK(2) C
SWAP(q.items[l], null) C
OK(x) C
Ok(x) C
Fig. 5. A queue history.
to show the correctness of the extended representation, which then implies the
correctness of the original.
The implementation has the following rep invariant:
I(r) = (r.back > 1)
A (Vi. i 2 r.back + (r.items[i] = null A r.aux[i] = null))
A (Vi. (i < r.back A r.locks[i] = FREE) + r.items[i] = r.aux[i])
A (lbound(r.items) = 1 A lbound(r.aux) = 1)
The third conjunct is the most interesting since it states that the auxiliary array
and the “real” array agree on all unlocked items.
Below, let A’ be the extended abstraction function defined on the object r
of the original rep type, and z, the auxiliary data. As before, we define cr to be
the partial order on items in the r.items array, and similarly define <= to be the
partial order on items in the r.aux array. The abstraction function is:
A’(r, z) = (q ] (3i. (i < r.back A r.locks[i] # FREE))
+ (items(q) = items(z) A <* C c4)
A (Vi. (i < r.back A r.locks[i] = FREE))
4 (items(q) = items(r) A cr C <,)I
If a rotation is in progress the extended abstraction function simply uses the
auxiliary value. When the object is quiescent, each lock is free, and A’ agrees
with the original A.
5. REASONING ABOUT LINEARIZABLE OBJECTS
In the previous section we showed how to reason about the correctness of an
implementation, given that linearizability is our correctness condition. In this
section we show how we reason about properties of concurrent objects given just
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

482 l M. Herlihy and J. Wing
their (sequential) specifications and the assumption that they are implemented
correctly, i.e., that they are linearizable.
5.1 Concurrent Registers
Here are axioms for Read and Write operations for all concurrent register
objects, r:
(true)
Read( )/Ok(u)
(r.val = r’.val = u)
(true]
Write(u)/Ok( )
(r’.val = u)
These sequential axioms can be combined with our linearizability condition to
prove assertions about the interleavings permitted by concurrent registers. Below,
in a linearization H of a register history, let ui denote the value of the register
after the ith (complete) operation of H.
Every value read was written, but not overwritten.
THEOREM 3. If r is a Read( )/Ok(u) operation in H, then there exists a
Write(u)/Ok( ) operation w such that r does not precede w, and there is no other
Write operation w ’ such that w precedes w ’ and w ’ precedes r.
PROOF. Let r be the kth operation in a linearization of H, and let i < k be
the greatest index such that ai = u. By construction, the ith operation in H is the
Write(u) operation. If w ’ exists, then there exists j such that i < j < k and
uj # u, a contradiction. 0
Register values are persistent in the absence of Write operations.
THEOREM 4. An interval in a history is a sequence of contiguous euents. If I is
an interval that does not overlap any Write operations, then all Read operations
that lie within I return the same ualue.
PROOF. Pick two Read operations ei and ej, i < j, that lie within the interval
I. If ui # uj, then a Write operation must be linearized after e; and before ej,
contradicting the assumption that no Writes overlap 1. Cl
5.2 Concurrent Queues
The proofs of the following properties of concurrent queues use the following
fact, which follows from Axioms E and D in Figure 3. For simplicity, we assume
all values of items in a queue are unique.
LEMMA 5. In any sequential queue history where x is enqueued before y, x is
not dequeued after y.
THEOREM 6. If the Enq of x, Enq of y, Deq of x, and Deq of y are complete
operations of H such that x’s Enq precedes y’s Enq, then y’s Deq does not precede
x’s Deq (i.e., either x’s Deq precedes y’s, or they are concurrent).
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 483
PROOF. Suppose not, i.e., y’s Deq precedes x’s Deq. Pick a linearization, and
let qi and qj be queue values following the Deq operations of x and y respectively.
From the assumption that j < i, qj-1 = [y, . . . , X, . . .I, which implies that y is
enqueued before x, a contradiction. 0
Gottlieb, Lubachevsky, and Rudolph [15] adopt the property proved in Theo-
rem 6 as the (informal) correctness property for a linearizable queue implemen-
tation. The difficulty of reasoning informally about concurrent histories is
illustrated by observing that Theorem 6 by itself is incomplete as a concurrent
queue specification, since it does not prohibit implementations in which enqueued
items spontaneously disappear from the queue, or new items spontaneously
appear. Such behavior is easily ruled out by the following two theorems:
Items do not spontaneously vanish from the queue.
THEOREM 7. If the Enq of x precedes the Enq of y, and if y has been dequeued,
then either x has been dequeued or there is a pending Deq concurrent with the
Deq of Y.
PROOF. Pick a linearization. Suppose x has not been dequeued. Let qj be the
value of the queue following the Deq of y, If y has been dequeued, but x has not,
qj-1 = [Yt * * - 9 X9 * * -19 contradicting the assumption that the Enq of x precedes
the Enq of y. 0
Items do not spontaneously appear in the queue.
THEOREM 8. If x has been dequeued, then it was enqueued, and the Deq
operation does not precede the Enq.
PROOF. Suppose not. Pick a linearization, and let qi and qj be the queue values
after the Enq and Deq operations respectively. From our assumption, j < i. Then
qj-1 = [X, e a .] and qi = [. . . , x], implying by the uniqueness of the values of the
items, that i I j - 1 < j, a contradiction. 0
6. DISCUSSION
6.1 Related Work
The axiomatic approach to specifying sequential programs has its origins in
Hoare’s early work on verification [ 241. Owicki and Gries extended Hoare’s work
to handle concurrent programs [37] by including axioms for general concurrent
programming language constructs such as the parallel operator. Apt et al. [3] use
an axiomatic approach for CSP [27]. Many researchers have also developed proof
techniques for concurrent programs using conditional critical regions and moni-
tors [7, 14,28,44]. We appeal to this past work when we perform syntax-directed
reasoning about our implementations. In particular, we rely on standard tech-
niques to deal with noninterference, using auxiliary data to encode both the
program counters of other processes (e.g., the auxiliary array of Section 4.3.4)
and history information (e.g., the cr partial order on items). All of this work,
however, differs from ours by focusing on control structures. Data are either left
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

484 - M. Herlihy and J. Wing
completely uninterpreted or assumed to be of simple primitive types like booleans
and integers. In contrast, our work on specifying and verifying concurrent objects
focuses on data entirely, exploiting the semantics of the data type to increase the
degree of concurrency. Our work builds upon, not replaces, older verification
technology.
Related axiomatic work in abstract data types deals with proofs of correctness
of their implementations [25], where, typically, first-order predicate logic pre-
and post conditions are used for the specification of each operation of the type.
Standish [43] and Nakajima [36] use a similar approach. The algebraic approach,
which defines data types to be heterogeneous algebras [5], uses axioms to specify
properties of programs and abstract data types, but the axioms are restricted to
equations. Much work has been done on algebraic specifications for abstract data
types [2,8, 10,171. Any one of these approaches would be adequate for specifying
the sequential behavior of a data type as required by our definition of when a
sequential history is legal. In practice, we use Larch [19, 201. Our contribution to
the area of specifying abstract data types is that we can work with data in a
concurrent, not just sequential, domain.
In short, whereas verification of concurrent programs focused on control, we
focus on data; whereas past verification of abstract data types is applicable for
sequential programs, ours is applicable for concurrent ones.
One notable exception is Lamport’s work [32] in which he proposed a model
and assertion language for specifying safety and liveness properties of concurrent
objects. His approach is more general than ours, as it addresses liveness as well
as safety properties, and nonlinearizable as well as linearizable behavior. Our
approach, however, focuses exclusively on a subset of concurrent computations
that we believe to be the most interesting and useful. In place of a specification
language powerful enough to specify all conceivable concurrent behaviors, we
re-interpret assertions about “well-behaved” concurrent computations as asser-
tions about their equivalent sequential computations.
Moreover, Lamport’s technique is based on a continually defined abstraction
function (called a state function) that maps the representation to a single
abstract value. This abstraction function defines the instant at which each
operation appears to take effect: each primitive step of each operation either
leaves the function’s value unchanged, or it instantaneously causes the operation
to take effect. This technique is not powerful enough to verify highly concurrent
objects such as the queue implementation given in Section 4. Indeed, our
linearizable queue example has since inspired Abadi and Lamport to extend
Lamport’s original technique to include not only history variables, but prophecy
variables [ 11. Prophecy variables are related to hidden variables called possibilities
which we use in our proofs in the Appendices.
Our notion of linearizability generalizes and unifies similar notions found
in specific examples in the literature. The use of concurrency control
mechanisms such as monitors [26] or Ada tasks [9] is usually illustrated by
simple implementations of linearizable objects such as bounded FIFO queues.
These implementations permit very little concurrency, since operations exe-
cute one at a time. A more interesting example is due to Lamport 1321, who
verifies linearizability and liveness for a queue implementation that permits one
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects l 485
enqueuing process to execute concurrently with one dequeuing process. There
exists extensive literature on concurrent B-trees [4, 33, 421 and related search
structures [6, 11, 13, 16, 291. Although the correctness properties for these data
structures are often stated in ad hoc terms, it is clear that they are meant to be
linearizable. The algorithms cited above provide excellent additional examples of
nontrivial techniques for implementing linearizable objects.
Misra [35] has proposed an axiomatic treatment of concurrent hardware
registers in which the register’s value is expressed as a function of time. Restricted
to registers, our axiomatic treatment is equivalent to his in the sense that both
characterize the full set of linearizable register histories. Theorems 3 and 4
capture two properties of Misra’s registers. Misra’s explicit use of time in axioms
is appropriate for hardware, where reasoning in terms of the register’s hypothet-
ical value is useful as a guide to hardware designers. Our approach, however, is
also appropriate for objects implemented in software, as we have found that
reasoning directly in terms of partial orders generalizes more effectively to data
types having a richer set of operations.
Gottlieb et al. [15] have investigated architectural support for implementing
concurrent objects without critical sections, an approach illustrated by our
linearizable implementation of a FIFO queue. They present a linearizable imple-
mentation of a concurrent queue (different from ours). The correctness condition
asserted for their queue, however, is the property stated in Theorem 6, which by
itself is incomplete as a concurrent queue specification since it does not prohibit
implementations in which enqueued items spontaneously disappear from the
queue, or new items spontaneously appear. As shown by Theorems 7 and 8, such
anomalous behavior is easily ruled out by our queue axioms and the assumption
of linearizability.
6.2 Final Remarks
Without linearizability, the meaning of an operation may depend on how it is
interleaved with concurrent operations. Specifying such behavior would require
a more complex specification language, as well as producing more complex
specifications. Linearizability provides the illusion that each operation takes
effect instantaneously at some point between its invocation and its response,
implying that the meaning of a concurrent object’s operations can still be given
by pre- and post conditions.
The role of linearizability for concurrent objects is analogous to the role of
linearizability for database theory: it facilitates certain kinds of formal (and
informal) reasoning by transforming assertions about complex concurrent behav-
ior into assertions about simpler sequential behavior. Like serializability, linear-
izability is a safety property; it states that certain interleavings cannot occur, but
makes no guarantees about what must occur. Other techniques, such as temporal
logic [32,34,39], must be used to reason about liveness properties such as fairness
or priority.
An implementation of a concurrent object need not realize all interleavings
permitted by linearizability, but all interleavings it does realize must be linear-
izable. The actual set of interleavings permitted by a particular implementation
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

486 l M. Herlihy and J. Wing
may be quite difficult to specify at the abstract level, being the result of
engineering trade-offs at lower levels. As long as the object’s client relies only on
linearizability to reason about safety properties, the object’s implementor is free
to support any level of concurrency that appears to be cost-effective.
In conclusion, linearizability provides benefits for specifying, implementing,
and verifying concurrent objects in multiprocessor systems. Rather than intro-
ducing complex new formalisms to reason directly about concurrent computa-
tions, we feel it is more effective to transform problems in the concurrent domain
into simpler problems in the sequential domain.
I. GENERAL PROOFS OF CORRECTNESS
The proofs of the lemmas in this section are given elsewhere [45].
1.1 Possibilities and Linearized Values
For each linearized value, it is sometimes useful to keep track of which invocations
were completed in the linearization that yielded that value, and what their
responses were. A possibility for a history H is a triple (v, P, R), where v is
a linearized value of H, P is the subset of pending invocations in H not com-
pleted when forming the linearization that yielded u, and R is the set
of responses appended to H to form u. We let Pass(H) denote the set of
possibilities of a history H. The relationship between the set of possibilities
and set of linearized values for a given history H is the following: for each
(u, P, R) u E Pass(H), u E Lin(H). For the example in Figure 4, the possibilities
([ I, 1Ensb4 AJ,Q9 and ([xl, 0, VW ) 4) are in Poss((Enq(x) A)). In the first
case, the linearization is the empty history: the queue is empty, the pending Enq
invocation was not completed, and no responses were appended. In the second
case, the linearization is a single Enq operation: the queue holds x, no pending
invocations were left incomplete, and A’s Enq was completed normally. Similarly,
(ix, ~1, 0, VW 1 A, W 1 Bl) and ([Y, 4, 0, 04 1 A, W 1 W) are two of the
possibilities (among many others) in Poss( (Enq(x) A) . (Enq(y) B)).
1.2 Four Generic Axioms
In order to carry out a formal proof of correctness for our queue example, it helps
to appeal to the following four type-independent axioms. These axioms are used
to derive a history’s set of possibilities, and hence its set of linearized values.
Let x be the object whose operations appear in H. The following closure axiom
states that if u is in Lin(H) and (inv A) is a pending invocation in H that is not
completed to form u, but could be completed with a response (res A) to yield a
legal value u ’ for X, then u ’ is also in Lin(H):
Axiom C:
(u, P, R) E Pass(H) A (inv A) E P A (x = u) inv/res (X = u’l
- (v’, P - (inv A}, R U {res A}) E Pass(H)
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 487
We write “(x = u) inv/res (x = ~‘1” to indicate that the condition must be
derivable from the sequential axioms for X.
The following invocation axiom states that any linearization of H is also a
linearization of H . (inv A):
Axiom I:
(u, P, R) E Pass(H)
4 (u, P U (inv A], R) E Poss(H . (inv A))
The following response axiom states that any linearization of H in which the
pending (inv A) is completed with (res A) is also a linearization of H . (res A):
Axiom R:
(u, P, R) E Pass(H) and (res A) E R
+ (u, P, R - (res A]) E Poss(H a (res A))
The following initialization axiom states that the possibility for the initial value
ug of an object corresponds to the empty history.
Axiom S:
((uo, 0, @>I = Pass(A)
For each operation of a typed object, Axioms C, I, R, and S are instantiated to
yield type-specific axioms.
For a given history H with m events, we use Possi(H) to denote the set of
possibilities for the ith prefix of H, for 0 I i 5 m. A derivation that shows that
(u, P, R) E Pass,(H) is a sequence of implications of the form:
(uo, PO, Ro) E Posse(H)
. . .
f (Uj, Pit Rj) E POSS,(H)
*...
where u, = u, P, = P, R, = R, and each implication is justified by Axiom C, I,
or R.
Intuitively, a derivation is like a history. Each implication in a derivation is
like a step in a proof, and each such step is justified by an axiom.
The axioms C, I, R, and S are sound:
THEOREM 9. If there exists a deriuation showing that (u, P, R) is a possibility
for H, then u is a linearized value for H.
Axioms C, I, R, and S are complete.
THEOREM 10. If u E Lin(H), then there exists a deriuation that (u, P, R) E
Pass(H).
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

488 l M. Herlihy and J. Wing
II. PROOF OF CORRECTNESS FOR THE QUEUE
11.1 Two Lemmas About Concurrent Queues
In a derivation, an Enq inference for x is an instantiation of Axiom C of the
form:
(qj, Pi, Rj) E PoSSk
3 (ins(qj, x), Pj - {Ens(x) A), Rj U (Ok( ) A)) E POSSE
A Deq inference is defined analogously.
Two inferences commute in a derivation if their order can be reversed without
invalidating the derivation. A derivation showing (q, P, R) E Poss, is in canonical
form if each Enq inference for an item in q occurs “as late as possible,” i.e., it
does not commute with the next inference in the derivation.
Lemma 11 implies that if x is in q, the event following the Enq inference for x
is either the return event for x, or the return event for an item that follows x
in q.
LEMMA 11. If 6 is a canonical derivation showing that (q, P, R) E Poss,,,, and
x is an item in q, then the inference following the Enq inference for x is either
the Enq inference for the item following x in q, or an application of Axiom R for
the matching response to Enq(x).
Lemma 12 states that we can consider equivalence classes of queues rather
than individual queues.
LEMMA 12. If (q, P, R) E Pass,, and q* is a queue value constructed by
rearranging the items of q in an order consistent with the partial precedence order
of their Enq operations, then (q *, P, R) E Poss,,, .
11.2 Main Proof
Figure 6 shows the Enq and Deq implementation annotated with assertions that
are true before and after each abstract invocation and response and each rep
operation. To avoid distraction, we assume queue values are unique. It is conven-
ient to keep as implicit auxiliary data the partial order, cr, on items in the array,
defined in Section 4.3.3. The set of possibilities, Poss, referred to in the annota-
tions can also be encoded as auxiliary data in terms of the sets, P (pending
invocations) and R (possible responses), which are components of a possibility.
If I is a set of items partially ordered by <, define:
and
(I, <) = (q 1 I = items(q) and < 5 c,J
((1, <), P, RI = ((4, P, R) I 4 E (I, 41.
The partially ordered set of queue items (I, <), captures the nonquiescent
abstract state of the queue, i.e., the possible values of the queue while there are
concurrent Enq and Deq operations or pending invocations. Notice that we can
rewrite the abstraction function as A(r) = (items(r), <,). The set [(I, <), P, R]
identifies each of the possible sets of queue values with a set of pending
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 489
lS(q, P, R) E Possl
Enq = proc (q: queue, x: item)
(3(q’, P’, R’) E Poss’ . q’ = q A P’ U (Enq(x) A) A R’ = R)
{3(q, P, R) E Poss . (En&) A) E PI
: int := INC(q.back)
;Posd = Poss)
(3(q, P, R) E Poss. (Enq(x) A) E Pj
STORE(q.items[i], x)
{3(q’, P’, R’) E Poss’ .P’ = P - (Enq(r) A} A R’ = R U (Ok() A}
A index(q.items’, x) = i A z E max(items(q’)) A q.back 5 q.back’)
(3(q, P, R) E Poss . (Ok() A) E RJ
end Enq
(3(q’, P’, R’) E Poss’.q’ = q A P’ = P A R’ = R - {Ok( ) A))
13(q, P, R) E Possl
Deq = Proc (q: queue) returns (item)
(3(q’, P’, R’) E Poss’ . q’ = q A P’ = P U {Deq( ) A) A R’ = R)
(3(q, P, R) E Poss . (Deq() A) E PJ
while true do
range : int := READ(q.back) - 1
(Poss’ = POSSJ
for i: int in 1 . . range do
(3(q, P, R) E Poss . (Deq() A) E P)
x: item := SWAP(q.items[i], null)
[3(q’, P’, R’) E Poss’ .P’ = P - (Deq( ) A) A R’ = R U {Ok(r) A) A
(z = null V z E min(items(q’)))l
if x -= null then return(x) end
end
end
end
(3(q, P, R) E Pass. (Ok(r) A) E R]
end Deq
(3(q’, P’, R’) E Poss’ . q’ = q A P’ = P A R’ = R - (Ok(x) A)]
Fig. 6. Annotated queue implementation.
invocations and a set of possible responses, thereby forming a set of (queue)
possibilities. The following two lemmas make use of Lemma 12, stated in the
previous section.
LEMMA 13. If x is a maximal element with respect to <, x 4 I, (Enq(x) A) B P,
(Ok() A) E R, and [(I, <), P U iEnq(x) A], R - (Ok() Al] C_ Pass, then
[(I U (xl, c), P, R] G Poss.
LEMMA 14. If (Deq( ) A) 4 P, (Ok(x) A) E R, and [(I, <), P U {Deq( ) Al,
R - (Ok(x) A]] C Poss, then for all x such that x is a minimal element of I,
[(I - (x), 4, P, R] C Pass.
Lemma 13 will allow us to show that the set of linearized queue values does not
change over a STORE operation and similarly, Lemma 14, for a SWAP operation,
by using cr for < and by recalling that for each (u, P, R) E Poss, u is a linearized
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

490 l M. Herlihy and J. Wing
value. We use the next two lemmas to satisfy the conditions of the previous two
lemmas.
LEMMA 15. Enq enqueues an item x that is maximal with respect to c,..
LEMMA 16. Deq removes and returns an item x that is minimal with respect
to -cr.
Here is a proof of correctness.
THEOREM 17. The queue implementation is correct.
PROOF. Assuming every rep history is linearizable, we need to show that every
queue history, H 1 q, is linearizable. It suffices to show that the “subset” property,
UrELin(H ( r) A(r) C Lin(H 1 q), remains invariant over abstract invocation and
responses and over complete rep operations. Thus, it can be conjoined to the pre-
and post conditions of Figure 6 as justified by the Owicki-Gries proof method
[38]. Axioms I and R give us the result for abstract invocation and response
events. INC and READ leave the abstraction function the same. Thus, we are
left with two cases, STORE and SWAP. By Lemma 15 we know that STORE
adds a maximal item and thus, we can apply Lemma 13 to show that the subset
property is preserved. Similarly, by Lemma 16 we know that SWAP removes a
minimal item and thus, we can apply Lemma 14 to show that the subset property
is preserved. 0
ACKNOWLEDGMENTS
The authors thank Jim Horning, Leslie Lamport, Larry Rudolph, and William
Weihl for lively verbal and electronic discussions about our notions of lineariza-
bility and correctness. We also thank James Aspnes, Stewart Clamen, David
Detlefs, Richard Lerner, and Mark Maimone for their comments on earlier
versions of this paper. Finally, we would like to thank Jim Gray and the
anonymous referees for their comments and suggestions.
REFERENCES
1. ABADI, M., AND LAMPORT, L. The existence of refinement mappings. Tech. Rep. 29, DEC
Systems Research Center, Aug. 1988.
2. GOGUEN, J. A., THATCHER, J. W., WAGNER, E. G., AND WRIGHT, J. B. Abstract data types as
initial algebras and correctness of data representations. In Proceedings of the Conference on
Computer Graphics, Pattern Recognition and Data Structures (May 1975). ACM, New York, 1975,
89-93.
3. APT, K. R., FRANCEZ, N., AND DEROEVER, W. P. A proof system for communicating sequential
processes. ACM Trans. Program. Lang. Syst. 2, 3 (July 1980), 359-385.
4. BAYER, R., AND SCHKOLNICK, M. Concurrency of operations on B-trees. Acta Znf. I, 1 (1977),
1-21.
5. BIRKHOFF, G., AND LIPSON, J. D. Heterogeneous algebras. J. Comb. Z’heor. 8 (1970), 115-133.
6. BISWAS, J., AND BROWNE, J. C. Simultaneous update of priority structures. In Proceedings of
the 1987 International Conference on Parallel Processing (St. Charles, Ill., 1987). 124-131.
7. BROOKES, S. D. An axiomatic treatment of a parallel language. In Proceedings of Conference on
Logics of Programs. Lecture Notes in Computer Science. Vol. 193. Springer-Verlag, Berlin, 1985.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Linearizability: A Correctness Condition for Concurrent Objects 491
8. BURSTALL, R. M., AND GOGUEN, J. A. Putting theories together to make specifications. In
Fifth International Joint Conference on Artificial Intelligence (Cambridge, Mass., Aug. 1977).
1045-1058. Invited paper.
9. DEPARTMENT OF DEFENSE. Reference Manual for the ADA Programming Language. ANSI/
MIL-STD-1815A-1983,1983.
10. EHRIG, H., AND MAHR, B. Fundamentals of Algebraic Specification 1. Springer-Verlag, Berlin,
1985.
11. ELLIS, C. S. Concurrent search and insertion in 2-3 trees. Acta Znf. 14 (1980), 63-86.
12. ESWARAN, K. P., GRAY, J. N., LORIE, R. A., AND TRAIGER, I. L. The notion of consistency and
predicate locks in a database system. Commun. ACM 19, 11 (Nov. 1976), 624-633.
13. FORD, R., AND CALHOUN, J. Concurrency control mechanisms and the serializability of concur-
rent tree algorithms. In 3rd ACM Symposium on Principles of Database Systems (1984). ACM,
New York, 1984,51-60.
14. GERTH, R., AND DEROEVER, W. P. Proving monitors revisited: A first step towards verifying
object oriented systems. Fundamental Znf. 9 (1986), 371-400.
15. GOTTLIEB, A., LUBACHEVSKY, B. D., AND RUDOLPH, L. Basic techniques for the efficient
coordination of very large numbers of cooperating sequential processors. ACM Trans. Program.
Lang. Syst. 5, 2 (April 1983), 164-189.
16. GUIBAS, L., AND SEDGEWICK, R. A dichromatic framework for balanced trees. In 19th ACM
Symposium on Foundations of Computer Science (Providence, R.I., 1978). ACM, New York, 1978,
8-21.
17. GUTTAG, J. V. The specification and application to programming of abstract data types. Ph.D.
thesis, Univ. of Toronto, Toronto, Sept. 1975.
18. GUTTAG, 3. V., HOROWITZ, E., AND MUSSER, D. R. Abstract data types and software validation.
Commun. ACM 21,12 (Dec. 1978), 1048-1064.
19. GUTTAG, J. V., HORNING, J. J., AND WING, J. M. Larch in five easy pieces. Tech. Rep. 5, DEC
Systems Research Center, July 1985.
20. GU~AG, J. V., HORNING, J. J., AND WING, J. M. The Larch family of specification languages.
IEEE Softw. 2,5 (Sept. 1985), 24-36.
21. HERLIHY, M., AND WING, J. Axioms for concurrent objects. In 14th ACM Symposium on
Principles of Programming Languages (Jan. 1987). ACM, New York, 1987, 13-26.
22. HERLIHY, M. P. Dynamic quorum adjustment for partitioned data. ACM Trans. Database Syst.
12,2 (June 1987), 170-194.
23. HERLIHY, M. P. Impossibility and universality results for wait-free synchronization. In Seuenth
ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing (PODC) (Toronto,
Ont., Aug. 1988). ACM, New York, 1988, 276-290.
24. HOARE, C. A. R. An axiomatic basis for computer programming. Commun. ACM 12, 10 (Oct.
1969), 576-583.
25. HOARE, C. A. R. Proof of correctness of data representations. Acta Inf. 1, 1 (1972), 271-281.
26. HOARE, C. A. R. Monitors: An operating system structuring concept. Commun. ACM 17, 10
(Oct. 1974), 549-557.
27. HOARE, C. A. R. Communicating sequential processes. Commun. ACM 21, 8 (Aug. 1978),
666-677.
28. HOWARD, J. H. Proving monitors. Commun. ACM 19,5 (May 1976), 273-279.
29. JONES, C. B. Software Development: A Rigorous Approach. Prentice-Hall, Englewood Cliffs,
N.J., 1980.
30. KRUSKAL, C. P., RUDOLPH, L., AND SNIR, M. Efficient synchronization on multiprocessors
with shared memory. In Fifth ACM SZGACT-SZGOPS Symposium on Principles of Distributed
Computing (Aug. 1986). ACM, New York, 1986.
31. LAMPORT, L. How to make a multiprocessor computer that correctly executes multiprocess
programs. IEEE Trans. Comput. C-28,9 (Sept. 1979), 690-691.
32. LAMPORT, L. Specifying concurrent program modules. ACM Trans. Program. Lang. Syst. 5, 2
(April 1983), 190-222.
33. LEHMAN, P. L., AND YAO, S. B. Efficient locking for concurrent operations on B-trees. ACM
Trans. Database Syst. 6, 4 (Dec. 1981), 650-670.
34. MANNA, Z., AND PNUELI, A. Verification of concurrent programs, Part I: The temporal frame-
work. Tech. Rep. STAN-CS-81-836, Dept. of Computer Science, Stanford Univ., June 1981.
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

492 l M. Herlihy and J. Wing
35. MISRA, J. Axioms for memory access in asynchronous hardware systems. ACM Trans. Program.
Lang. Syst. 8, 1 (Jan. 1986), 142-153.
36. NAKAJIMA, R., HONDA, M., AND NAKAHARA, H. Hierarchical program specification and verifi-
cation-A many-sorted logical approach. Acta Znf. 14 (1980), 135-155.
37. OWICKI, S., AND GRIES, D. Verifying properties of parallel programs: An axiomatic approach.
Commun. ACM 19,5 (May 1976), 279-285.
38. OWICKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs. Acta Znf. 6, 4
(1976), 319-340.
39. OWICKI, S., AND LAMPORT, L. Proving liveness properties of concurrent programs. ACM Trans.
Program. Lang. Syst. 4, 3 (July 1982), 455-495.
40. PAPADIMITRIOU, C. H. The serializability of concurrent database updates. J. ACM 26, 4 (Oct.
1979), 631-653.
41. REED, D. P. Implementing atomic actions on decentralized data. ACM Trans. Comput. Syst. 1,
1 (Feb. 1983), 3-23.
42. SAGIV, Y. Concurrent operations on B-trees with overtaking. In Symposium on Principles of
Database Sy&ems (Waterloo, Ont., Jan. 1985). ACM, New York, 1985, 28-37.
43. STANDISH, T. A. Data structures: An axiomatic approach. Rep. 2639, Bolt, Beranek, and
Newman, Cambridge, Mass., Aug. 1973.
44. STIRLING, C. A generalization of Owicki-Gries-Hoare logic for a concurrent while language.
Tech. Rep., Edinburgh Univ., March 1987.
45. HERLIHY, M. P., AND WING, J. M. Axioms for concurrent objects. Tech. Rep. CMU-CS-86-154,
Computer Science Dept., Carnegie Mellon Univ., 1986.
46. WEIHL, W. E. Local atomicity properties: Modular concurrent control for abstract data types.
ACM Trans. Program. Lang. Syst. 11, 2 (April 1989), 249-283.
Received January 1988, revised November 1988 and July 1989, accepted October 1989
ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, July 1990.

Q: What problem does linearizability solve?

A: The problem being solved is fulfilling the need for a consistency
model: a definition of correct client-visible behavior of a network
service in the face of concurrent requests from multiple clients, lost
and re-transmitted requests, communication delays, server replication,
server failure and recovery, and server sharding. A consistency model
helps programmers design applications (clients) so that they provide
the behavior the programmers intend. And it helps service designers
decide whether specific design decisions are OK or not.

Here's an example of the kind of question linearizability can help
answer. Suppose we have a replicated storage service (like GFS).
Client C1 sends a write RPC for a certain key and receives a "success"
reply; after that, client C2 sends a read RPC for the same key and
receives a value back; no other clients modify that key; is C2
guaranteed to see C1's write? The answer to this question is important
for the design of the storage service, since it affects whether
replicas can serve reads, whether updates must be preserved if servers
crash, whether caches must be kept strictly up to date, &c.

Linearizability's answer is yes, C2 must see C1's write. And as a
result, a linearizable storage system often involves complex and
expensive management of replication, crash recovery, caching, &c.

Q: What's the definition of linearizability?

A: Linearizability is defined on "histories": traces of client
operations, annotated by the time at which each client operation
starts (is launched by a client), and the time at which the client
sees that the operation has finished. Linearizability tells you if an
individual history is legal. We say that a service is linearizable if
every history it can generate is linearizable.

There is one event in the history for a client starting an operation,
and another for the client deciding the operation has finished. Thus
the history makes concurrency among clients, and network delays,
explicit. Typically the start and finish events correspond to a
request and a response message exchanged with the server.

A history is linearizable if you can assign a "linearization point" (a
time) to each operation, where each operation's point lies between the
times of its start and finish events, and the history's response
values are the same as you'd get if you executed the operations one at
a time in point order. If no assignment of linearization points
satisfies these two requirements, the history is not linearizable.

Q: Why is linearizability a desirable consistency model?

A: Because it is relatively strong, in the sense of forbidding many
"anomalous" behaviours that might cause problems for application
programmers. Services with stronger consistency guarantees tend to be
easier for programmers to design for than weaker ones.

For example, suppose one part of an application computes a value,
writes it to the storage system, and then sets a flag in the storage
system indicating that the computed value is ready:

  v = compute...
  put("value", v)
  put("done", true)

On a different computer a program checks "done" to see if the value is
available, and uses it if it is:

  if get("done") == true:
    v = get("value")
    print v

If the storage system that implements put() and get() is linearizable,
the above programs will work as expected.

With many weaker consistency models, the above programs will not work
as one might hope. For example, a storage system providing "eventual
consistency" might re-order the two puts (so that "done" is true even
though "value" is not available), or might yield a stale (old) value
for either of the get()s.

Q: When trying to demonstrate that a history is linearizable, how does
one decide where to place the linearization point for each operation?

A: The idea is that, in order to show that an execution is
linearizable, you (the human) need to find places to put the little
orange lines (linearization points). That is, in order to show that a
history is linearizable, you need to find an assignment of
linearization points (and thus an order of operations) that conforms
to these requirements:

  * All function calls have a linearization point at some instant
    between their invocation and their response.

  * All functions appear to occur instantly at their linearization
    point, behaving as specified by the sequential definition.

So, some placements of linearization points are invalid because they lie
outside of the time span of a request; others are invalid because they
violate the sequential definition (for a key/value store, a violation means
that a read does not observe the most recently written value, where
"recent" refers to linearization points).

For a complex history you may need to try many assignments of
linearization points in order to find one that demonstrates that the
history is linearizable. If you try them all, and none works, then the
history is not linearizable.

Q: Why not use the time at which the client sent the command as the
linearization point? I.e. have the system execute operations in the
order that clients sent them?

A: It's hard to build a system that guarantees that behavior -- the
start time is the time at which the client code issued the request,
but the service might not receive the request until much later due to
network delays. That is, requests may arrive at the service in an
order that's quite different from the order of start times. The
service could in principle delay execution of every arriving request
in case a request with an earlier issue time arrives later, but it's
hard to know how long to wait since networks can impose unbounded
delays. And it would increase delays for every request, perhaps by a
lot. That said, Spanner, which we'll look at later, uses a related
technique.

A correctness specification like linearizability needs to walk a fine
line between being lax enough to implement efficiently, but strict
enough to provide useful guarantees to application programs. "Appears to
execute operations in invocation order" is too strict to implement
efficiently, whereas linearizability's "appears to execute somewhere
between invocation and response" is implementable though not as
straightforward for application programmers.

Q: How do services implement linearizability?

A: If the service is implemented as a single server, with no
replication or caching or internal parallelism, it's nearly enough for
the service to execute client requests one a time as they arrive. One
complication comes from clients that re-send requests because they
think the network has lost messages: for requests with side-effects,
the service must take care to execute any given client request only
once. Replication, fault tolerance, and caching involve further design
complexity.

An nice consequence of linearizability is that the service has freedom
in the order in which it executes concurrent (overlapping-in-time)
operations. In particular, if operations from client C1 and C2 are
concurrent, the server could execute C2's operation first even if C1
started before C2. On the other hand, if C1 finished before C2
started, linearizability requires the service to act as if it executed
C1's operation before C2's (i.e. C2's operation is required to observe
the effects of C1's operation, if any).

Q: What are other consistency models?

A: Look for

    eventual consistency
    causal consistency
    fork consistency
    serializability
    sequential consistency
    timeline consistency

And there are others from the worlds of databases, CPU memory/cache
systems, and file systems.

In general, different models differ in how intuitive they are for
application programmers, and how much performance you can get with
them. For example, eventual consistency allows many anomalous results
(e.g. even if a write has completed, subsequent reads might not see
it), but in a distributed/replicated setting can be implemented with
higher performance than linearizability.

Q: Why is linearizability used as a consistency model versus other ones,
such as eventual consistency?

A: People do often build storage systems that provide consistency weaker
than linearizability, such as eventual and causal consistency.

Linearizability has some nice properties for application writers:

  * reads always observe fresh data.
  * if there are no concurrent writes, all readers see the
    same data.
  * on most linearizable systems you can add mini-transactions
    like test-and-set (because most linearizable designs end up
    executing operations on each data item one-at-a-time).

Weaker schemes like eventual and causal consistency can allow higher
performance, since they don't require all copies of data to be updated
right away. This higher performance is often the deciding factor. For
some applications weak consistency causes no problems, for example if
one is storing data items that are never updated, such as images or
video.

However, weak consistency introduces some complexity for application
writers:

  * reads can observe out-of-date (stale) data.
  * reads can observe writes out of order.
  * if you write, and then read, you may not see your write,
    but instead see stale data.
  * concurrent updates to the same items aren't executed
    one-at-a-time, so it's hard to to implement mini-transactions
    like test-and-set or atomic increment.

Q: Linearizability doesn't seem particularly "strong", since you can
be reading different data even when you execute two commands at the
same time; are there stronger notions?

A: True, linearizability is reminiscent of using threads in a program
without using locks. It's possible to program correctly this way but
it requires care.

An example of a stronger notion of consistency is transactions, as
found in many databases, which effectively lock any data used. For
programs that read and write multiple data items, transactions make
programming easier than linearizability. "Serializability" is the name
of one consistency model that provides transactions.

However, transaction systems are significantly more complex, slower, and
harder to make fault-tolerant than linearizable systems.

Q: Is it a problem that concurrent get()s might see different values if
there's also a concurrent put()?

A: It's often not a problem in the context of storage systems. For
example, if the value we're talking about is my profile photograph,
and two different people ask to see it at the same time that I'm
updating the photo, then it's reasonable for them to see different
photos (either the old or new one).

Another way of looking at this is that it's the same behavior that
programmers already are familiar with on multi-core computers:
concurrent loads from different cores of a memory location that's
simultaneously being written are not guaranteed to all see the same
value.

Q: What are some examples of real-world linearizable storage systems?
And of storage systems with weaker consistency guarantees?

A: Google's Spanner and Amazon's S3 are storage systems that provide
linearizability.

Google's GFS, Amazon's Dynamo, and Cassandra provide weaker
consistency; they are probably best classified as eventually
consistent.

Q: What do people do to ensure their distributed systems are correct?

A: Thorough testing is a common plan, perhaps using a linearizability
checker such as Porcupine.

Use of formal methods is also common; have a look here for some
examples:

https://arxiv.org/pdf/2210.13661.pdf

https://assets.amazon.science/67/f9/92733d574c11ba1a11bd08bfb8ae/how-amazon-web-services-uses-formal-methods.pdf

https://dl.acm.org/doi/abs/10.1145/3477132.3483540

https://www.ccs.neu.edu/~stavros/papers/2022-cpp-published.pdf

https://www.cs.purdue.edu/homes/pfonseca/papers/eurosys2017-dsbugs.pdf

https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf

Q: How hard is it to formally prove a service to be correct?

A: It turns out that proving significant theorems about complex
programs is difficult -- much more difficult than ordinary
programming.

You can get a feel for this by trying the labs for this course:

  https://6826.csail.mit.edu/2020/

Q: How does a team decide that they have tested a product thoroughly
enough to ship to customers?

A: It's a good idea to start shipping product, and getting revenue,
before your company runs out of money and goes bankrupt. People test
as much as they can before that point, and usually try to persuade a
few early customers to use the product (and help reveal bugs) with the
understanding that it might not work correctly. Maybe you are ready to
ship when the product is functional enough to satisfy many customers
and has no known major bugs.

Independent of this, a wise customer will also test software that they
depend on. No serious organization expects any software to be bug-free.

Q: How do linearizability checkers work?

A: A simple linearizability checker would try every possible order (or
choice of linearization points) to see if one is valid according to
the rules in the definition of linearizability. Because that would be
too slow on big histories, clever checkers avoid looking at clearly
impossible orders (e.g. if a proposed linearization point is before
the operation's start time), decompose the history into sub-histories
that can be checked separately when that's possible, and use
heuristics to try more likely orders first.

These papers describe the techniques; I believe Knossos is based on the
first paper, and Porcupine adds ideas from the second paper:

    http://www.cs.ox.ac.uk/people/gavin.lowe/LinearizabiltyTesting/paper.pdf
    https://arxiv.org/pdf/1504.00204.pdf

Q: Are there examples of real-world systems tested with Porcupine or
similar testing frameworks?

A: Such testing is common -- for example, have a look at
https://jepsen.io/analyses; Jepsen is an organization that has tested
the correctness (and linearizability, where appropriate) of many storage
systems.

For Porcupine specifically, here's an example:

  https://www.vldb.org/pvldb/vol15/p2201-zare.pdf