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 IsLinearizableHistory operator returns true if an event history is linearizable.
• LinQueue.tla instantiates the Linearizability module for a queue (FIFO) object. It contains an IsLinearizableHistory operator 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:

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.

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, <<>>)