Consistency Models: Linearizability, Sequential, Causal and Eventual Consistency

Version note: The code in this post was built and run with C# 14 and .NET 10.

Guess First

A book costs 400. Alice updates the price to 450; her request starts at millisecond 0 and is acknowledged at millisecond 30. Meanwhile Carol reads the price between milliseconds 5 and 10 and sees 450. Bob reads after Carol's read has finished, between milliseconds 12 and 15, and sees 400.

Alice's write had not yet been acknowledged while Bob was reading, so at first glance it seems reasonable that Bob saw the old value. But Carol had seen the new value before Bob. Is this history "correct"? The answer depends on which consistency model your system promises. By the end of this post a program will tell you in which model this history is valid and in which it is not.

What Is a Consistency Model?

In the previous post we saw that replicas can show different values at the same time. To discuss "correct behavior" we first need to define what counts as correct. A consistency model is that definition: a contract that says which histories of reads and writes clients may observe. In Jepsen's terms, a model is a set of histories. A system provides a model if every history it produces is in that set.

This definition has a practical benefit: you can test a guarantee without looking inside the system, just by recording what clients see. That is how Jepsen tests databases: record operations and their results with timestamps, then use a checker to decide whether the history fits the promised model. In this post we do the same on a small scale.

Linearizability: As If There Were a Single Copy

Linearizability, defined by Herlihy and Wing in 1990, is the strongest model for a single object (in our example a register, a single value). Every operation must appear to take effect atomically at some point between its start and its end. Those points arrange all operations into a single order, and that order respects both the meaning of the register (every read returns the value of the last write before it) and real time: if A finished before B started, A comes before B in the order.

The intuition: however many replicas the system is split into, clients see it as a single copy. Every read that starts after a write has been acknowledged sees that write (or a newer one). Once a read has returned the new value, no read that starts later can return the old one. Kleppmann calls this a "recency guarantee". Locks, leader election, unique constraints and rules like "stock must not go below zero" need this guarantee.

Checking a History

Let us model a history as records: each operation's client, kind, value, and start and end times. The checker tries every possible ordering, looking for one that follows the rules. The only difference is the rule for "which operation must come before which": real time for linearizability, only the same client's own operations for sequential consistency:

namespace Bookstore.Consistency;

public enum Kind { Write, Read }

// One operation on the "price" register: who, what, when it started and finished
public record Op(string Client, Kind Kind, int Value, int Invoked, int Completed)
{
    public override string ToString() => $"{Client}:{(Kind == Kind.Write ? "W" : "R")}({Value})[{Invoked}-{Completed}]";
}

public static class HistoryChecker
{
    public const int Initial = 400;

    // Linearizable: a legal register order that respects real time
    public static bool IsLinearizable(IReadOnlyList<Op> history) =>
        Search(history, (a, b) => a.Completed < b.Invoked);

    // Sequential: a legal register order that respects each client's own order only
    public static bool IsSequential(IReadOnlyList<Op> history) =>
        Search(history, (a, b) => a.Client == b.Client && a.Completed < b.Invoked);

    private static bool Search(IReadOnlyList<Op> history, Func<Op, Op, bool> mustPrecede)
    {
        bool Extend(List<Op> placed, int current)
        {
            if (placed.Count == history.Count) return true;
            foreach (Op next in history.Except(placed))
            {
                // every op that must come before "next" is already placed
                bool ready = history.Except(placed).All(other => other == next || !mustPrecede(other, next));
                bool legal = next.Kind == Kind.Write || next.Value == current;
                if (ready && legal)
                {
                    placed.Add(next);
                    if (Extend(placed, next.Kind == Kind.Write ? next.Value : current)) return true;
                    placed.RemoveAt(placed.Count - 1);
                }
            }
            return false;
        }
        return Extend([], Initial);
    }
}

This brute-force approach is enough for histories of five or six operations; Jepsen's Knossos and Elle checkers solve the same problem for thousands of operations with much smarter algorithms (checking linearizability is, in general, a problem with no known efficient solution (NP-complete)). Five histories:

using Bookstore.Consistency;

Dictionary<string, Op[]> histories = new()
{
    ["1 read overlaps the write"] =
        [new("Alice", Kind.Write, 450, 0, 20), new("Bob", Kind.Read, 400, 5, 8)],
    ["2 stale read after the write finished"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Bob", Kind.Read, 400, 12, 15)],
    ["3 two readers disagree"] =
        [new("Alice", Kind.Write, 450, 0, 30), new("Carol", Kind.Read, 450, 5, 10), new("Bob", Kind.Read, 400, 12, 15)],
    ["4 Alice does not see her own write"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Alice", Kind.Read, 400, 12, 14)],
    ["5 Bob sees new, then old"] =
        [new("Alice", Kind.Write, 450, 0, 10), new("Bob", Kind.Read, 450, 12, 15), new("Bob", Kind.Read, 400, 16, 18)],
};

Console.WriteLine($"{"history",-40} {"linearizable",-13} sequential");
foreach ((string name, Op[] ops) in histories)
{
    Console.WriteLine($"{name,-40} {HistoryChecker.IsLinearizable(ops),-13} {HistoryChecker.IsSequential(ops)}");
}

history                                  linearizable  sequential
1 read overlaps the write                True          True
2 stale read after the write finished    False         True
3 two readers disagree                   False         True
4 Alice does not see her own write       False         False
5 Bob sees new, then old                 False         False

In the first history Bob's read overlaps Alice's write; an order in which the read takes effect before the write is possible, so seeing the old value is linearizable. In the second, Alice's write finished at millisecond 10, Bob started at 12 and still sees 400: the typical result of replication lag, not linearizable. The third is the opening question: even though Bob's read overlaps the write, Carol had seen the new value before Bob started. Once the new value has been seen there is no going back; not linearizable.

Sequential Consistency: Forget Real Time, Keep the Order

Sequential consistency, defined by Lamport in 1979 for multiprocessor computers, drops the real-time condition: all operations must fit into a single order in which each client's own operations appear in the order that client issued them. The real-time relationship between different clients' operations does not matter.

The checker's second column shows this. The second and third histories are sequential: there is an order that places Bob's reads before Alice's write without breaking Bob's own order. The fourth and fifth are not even sequential. In the fourth, Alice cannot see her own write: in Alice's order the write comes before the read, so the read must return 450. In the fifth, Bob sees the new value and then the old one: in Bob's order the moment he reads 450 is after the write, his next read must come after that, and nobody writes 400 afterwards.

Dropping the real-time condition looks like a small difference in theory; in practice it means "a change one user made may not yet be visible to another user they just phoned about it". If there is a communication channel outside the system (a phone, an e-mail, another service), sequential consistency is not enough.

Causal Consistency and Session Guarantees

Causal consistency requires the happens-before relation from the fourth post to be respected: if one operation causally influenced another, everyone sees them in that order. Concurrent operations may appear in different orders to different clients. A question and the answer to it appear in the same order everywhere; two comments written without knowledge of each other may appear in different orders.

Below causal consistency are weaker guarantees concerning a single client's session. These are the session guarantees from the previous post: read-your-writes (you see what you wrote; the fourth history breaks it), monotonic reads (you never go back from a value you have seen; the fifth history breaks it), monotonic writes (your writes are applied in the order you made them) and writes-follow-reads (a write you make based on something you read becomes visible after what you read). Causal consistency includes all of them.

Why these guarantees matter shows up on the availability side. Jepsen's map classifies models by how available they can remain during a network partition:

The red models (including linearizable, sequential, serializable and snapshot isolation) require some nodes to refuse to answer during a partition in an asynchronous network. The yellow ones (causal and the session guarantees) can work everywhere as long as a client stays attached to the same replica (sticky). The green ones (such as read committed) allow every non-failing node to answer. The CAP (Consistency, Availability, Partition tolerance) theorem in the next post is the proven limit for one point on this map: linearizability.

Eventual Consistency: Only "Eventually"

Eventual consistency is the most used term that promises the least: if no new writes arrive, all replicas eventually converge to the same value. When they converge, what reads return in the meantime, and which value they converge to are not part of the definition. In the language of the second post, it is a liveness guarantee with no safety guarantee at all. The LWW (last-write-wins) example in the third post provided eventual consistency: both replicas converged to the same value. That value just happened to be wrong.

A more useful variant is strong eventual consistency: two replicas that have received the same writes (in any order) are in the same state. That is the guarantee CRDTs (Conflict-free Replicated Data Types) give, and the subject of the eleventh post. The Microservices series post "No Transactions Across Microservices: Embracing Eventual Consistency by Design" treats eventual consistency at the workflow level: intermediate states, sagas and the waiting shown to the user. The "eventual" there is the business-rule-level counterpart of the replication definition here.

The Transaction Side: Serializable, Linearizable and Strict Serializability

In the database world the word consistency means something else too, and that is where confusion starts. Transaction isolation levels (read committed, repeatable read, snapshot isolation, serializable) define how transactions that touch several objects see each other. Serializable requires the outcome of transactions to equal running them one at a time in some order; it does not require that order to respect real time. Linearizable is for a single object and does respect real time.

The model that combines them is strict serializability: transactions can be arranged in an order, and the order respects real time. That is the model at the top of the map, and it is the guarantee Google Spanner calls "external consistency". Snapshot isolation sits below serializable: each transaction reads a consistent snapshot, but write skew is allowed. SNAPSHOT in SQL (Structured Query Language) Server and REPEATABLE READ in PostgreSQL are this model. The EF (Entity Framework) Core series showed choosing an isolation level from code in "Transactions in EF Core: SaveChanges, BeginTransaction and Savepoints"; the detailed implementation is for the upcoming Database › SQL Server in Depth series.

Common Pitfalls

Using "consistent" without a definition. The C in ACID (Atomicity, Consistency, Isolation, Durability), which means the application's invariants, the C in CAP (linearizability) and the "consistent" in "eventually consistent" are three different things. When someone in a design discussion says "it has to be consistent", ask which model they mean.

Mistaking serializable for linearizable. A read from a replica of a serializable database may not see a transaction that was just committed; serializability does not forbid that.

Assuming session guarantees are free. Read-your-writes breaks the moment the load balancer sends the user to another replica. It takes an explicit mechanism: sticky routing, a version token, or reading the user's own data from the leader.

Assuming eventual consistency means "a few milliseconds". The definition gives no bound. If a replica stays partitioned for an hour, "eventually" is an hour later; design the workflow accordingly.

Blindly trusting the documented guarantee. Many databases Jepsen has tested over the years did not provide their promised model under certain failures. We will come back to this lesson in the eleventh post.

A Small Experiment

★☆☆ In the first history, move Bob's read to between milliseconds 21 and 25. What does the checker say? Why?

★★☆ Add IsReadYourWrites to HistoryChecker: it should check that reads by a client that start after one of its own writes return that value or a newer one. Run the five histories through it. Which history is not sequential but still satisfies read-your-writes?

★★★ Extend the checker to two registers (price and stock) and build this history: Alice writes price, then stock; Bob reads the new stock, then the old price. Is each register's own sub-history sequential? Are both registers together? Ask the same question for linearizability. The answers show why linearizability is a "local" property (it can be checked object by object) and sequential consistency is not.

In this post we defined the models and saw on the map the tension between linearizability and availability. In the next post we look at the most famous and most misunderstood statement of that tension: what exactly the CAP theorem says, why the "pick 2 of 3" summary is wrong, and PACELC (if Partition: Availability or Consistency, Else: Latency or Consistency), which describes the choice between latency and consistency that exists even when there is no partition.