This repository contains a TLA+ model for checking if an object history is linearizable.
See also: Reading the Herlihy & Wing Linearizability paper with TLA+, part 2: prophecy variables
The Herlihy & Wing 1990 paper entitled Linearizability: a correctness condition for concurrent objects introduced linearizability as a correctness condition for reasoning about the behavior of concurrent data structures.
Peter Bailis's blog entry Linearizability versus Serializability has a good definition:
Linearizability is a guarantee about single operations on single objects. It provides a real-time (i.e., wall-clock) guarantee on the behavior of a set of single operations (often reads and writes) on a single object (e.g., distributed register or data item).
In plain English, under linearizability, writes should appear to be instantaneous. Imprecisely, once a write completes, all later reads (where “later” is defined by wall-clock start time) should return the value of that write or the value of a later write. Once a read returns a particular value, all later reads should return that value or the value of a later write.
There are several linearizable data stores whose behaviors have been specified with TLA+:
- Lamport's book Specifying Systems uses an example of a linearizable memory in Section 5.3.
- The Raft Consensus algorithm supports linearizable semantics and has a TLA+ specification written by Diego Ongaro.
- Azure Cosmos DB supports a consistency model with linearizable reads and has high-level TLA+ specifications written by Murat Demirbas.
However, none of these models use the definition of linearizability outlined in the original paper by Herlihy & Wing.
Indeed, the definition in the original paper is awkward to use with TLC (the TLA+ model checker), because it involves reordering of event histories, which leads to state space explosion.
However, I found it useful to work directly with the definition of linearizability as an exercise for practicing with TLA+, as well as to gain a better understanding of how linearizability is defined.
- Linearizability.tla contains a definition of
linearizability. In particular, the
IsLinearizableHistoryoperator returns true if an event history is linearizable. - LinQueue.tla instantiates the Linearizability module for
a queue (FIFO) object. It contains an
IsLinearizableHistoryoperator that returns true if an event history for a queue is linearizable. - LinQueuePlusCal.tla is a PlusCal version. If a history is linearizable, using TLC with this module makes it easy to see a valid linearization.
- Utilities.tla conatins some general-purpose operators.
On p469, the paper defines a linearizable object as an object whose concurrent histories are linearizable with respect to some sequential specification.
To understand linearizability, we need to understand what a concurrent history is.
As a motivating example, figure one from the paper shows several possible histories for a concurrently accessed queue. Figures 1(a) and 1(c) are linearizable, and Figures 1(b) and 1(d) are not.
Each interval represents an operation. There are two types of operations: {E, D} for enqueue and dequeue. There are three processes: {A, B, C}. There are three items that can be added to the queue: {x, y, z}.
Here's how I modeled these four histories in TLA+:
H1 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"Ok", proc|->"B"],
[op|->"Ok", proc|->"A"],
[op|->"D", proc|->"B"],
[op|->"Ok", val|->"x", proc|->"B"],
[op|->"D", proc|->"A"],
[op|->"Ok", val|->"y", proc|->"A"],
[op|->"E", val|->"z", proc|->"A"]>>
H2 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"Ok", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"D", proc|->"A"],
[op|->"Ok", proc|->"B"],
[op|->"Ok", val|->"y", proc|->"A"]
>>
H3 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"D", proc|-> "B"],
[op|->"Ok", val|->"x", proc|->"B"]>>
H4 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"Ok", proc|->"A"],
[op|->"Ok", proc|->"B"],
[op|->"D", proc|-> "A"],
[op|->"D", proc|-> "C"],
[op|->"Ok", val|->"y", proc|->"A"],
[op|->"Ok", val|->"y", proc|->"C"]
>>
We can use the IsLinearizableHistory operator from LinQueue.tla to verify that
H2 is not linearizable.
For H3, we can use the FindLinearization algorithm from LinQueuePlusCal.tla to
find a linearization. Specify linearizable = FALSE as the invariant and
run the model checker. The variable S contains the linearization:
Here's the value for S:
<<
[op|->"E", val|->"x", proc|->"A"],
[op|->"Ok", proc|->"A"],
[op|->"D", proc|-> "B"],
[op|->"Ok", val|->"x", proc|->"B"]
>>
I endeavored to make the TLA+ representation as close as possible to how the definitions were written in the paper, rather than trying to optimize for reducing the state space of the TLC model checker.
p469:
A history H is linearizable if it can be extended (by appending zero or more response events) to some history H’ such that:
- L1: complete(H’) is equivalent to some legal sequential history S, and
- L2: <H ⊆ <S
Here's how I modeled this in TLA+:
IsLinearizableHistory(H) ==
\E Hp \in ExtendedHistories(H) :
LET completeHp == Complete(Hp)
IN \E f \in Orderings(Len(completeHp)) :
LET S == completeHp ** f
IN /\ IsSequential(S) \* L1
/\ IsLegal(S) \* L1
/\ AreEquivalent(S, completeHp) \* L1
/\ RespectsPrecedenceOrdering(H, S) \* L2
From p467:
If H is a history, complete(H) is the maximal subsequence of H consisting only of invocations and matching responses.
A subsequence is a sequence that can be derived from another sequence by deleting some or no elements without changing the order of the remaining elements (source: Wikipedia)
Complete(H) ==
LET subseqs == Subsequences(H)
IN CHOOSE CH \in subseqs :
/\ OnlyInvAndMatchingResponses(CH)
/\ \A s \in subseqs : OnlyInvAndMatchingResponses(s) => Len(s) <= Len(CH) \* maximal
p467
A history H is sequential if:
- The first event of H is an invocation.
- Each invocation, except possibly the last, is immediately followed by a matching response. Each response is immediately followed by a matching invocation.
IsSequential(H) ==
LET IsLastInvocation(h,i) == \A j \in 1..Len(h) : IsInvocation(h[j]) => j<=i
IN /\ Len(H)>0 => IsInvocation(H[1])
/\ \A i \in 1..Len(H) : IsInvocation(H[i]) => (IsLastInvocation(H,i) \/ Matches(H, i, i+1))
/\ \A i \in 1..Len(H) : IsResponse(H[i]) => Matches(H,i-1,i)
The specificiation for a legal sequential history varies based on the kind of object whose behavior you are trying to model. The paper uses a queue (FIFO) as the example object being modeled.
Most of the work is done by the recursive LegalQueue function.
RECURSIVE LegalQueue(_, _)
\* Check if a history h is legal given an initial queue state q
LegalQueue(h, q) == \/ h = << >>
\/ LET first == Head(h)
rest == Tail(h)
IN \/ /\ first.op = "E"
/\ LegalQueue(rest, Append(q, first.val))
\/ /\ first.op = "D"
/\ Len(q)>0
/\ first.val = Head(q)
/\ LegalQueue(rest, Tail(q))
IsLegalQueueHistory(h) == LegalQueue(h, << >>)
\* Given a sequential history H, true if it represents a legal queue history
IsLegal(H) ==
LET RECURSIVE Helper(_, _)
Helper(h, s) == IF h = << >> THEN IsLegalQueueHistory(s)
ELSE LET hr == Tail(Tail(h))
inv == h[1]
res == h[2]
e == [op|->inv.op, val|-> IF inv.op = "E" THEN inv.val ELSE res.val]
IN Helper(hr, Append(s, e))
IN Helper(H, <<>>)