Distributed systems architects face a fundamental tension. Stronger consistency models like linearizability provide intuitive semantics but impose coordination costs that limit availability and latency. Weaker models offer better performance characteristics but introduce subtle correctness challenges that can manifest as application bugs.

The term eventual consistency has become a catch-all for anything weaker than strong consistency. This obscures crucial distinctions. The space between eventual consistency and linearizability contains a rich taxonomy of precisely defined models, each offering different guarantees with different costs. Understanding this landscape is essential for making principled design decisions.

This analysis maps the formal hierarchy of weak consistency models, from the minimal guarantees of eventual consistency through the causal ordering constraints that enable many practical applications. We examine session guarantees that provide stronger semantics for individual clients, and confront the verification challenges that make reasoning about weak consistency fundamentally harder than reasoning about strong consistency. The goal is not to advocate for any particular model, but to provide the theoretical framework necessary for navigating the consistency zoo with precision.

Consistency models form a partial order based on the sets of executions they permit. Model A is stronger than model B if every execution allowed by A is also allowed by B. This ordering is partial because some models are incomparable—neither strictly stronger nor weaker than each other.

At the weakest end sits eventual consistency, which guarantees only that if no new updates are made, all replicas will eventually converge to the same value. This minimal guarantee permits executions that return arbitrarily stale data or exhibit anomalies like reading values that appear to go backward in time. The formal definition requires convergence but says nothing about the path to get there.

Causal consistency strengthens eventual consistency by requiring that causally related operations appear in the same order at all replicas. The definition relies on the happens-before relation: if operation A could have influenced operation B, then any replica observing B must also observe A. Concurrent operations—those with no causal relationship—may appear in different orders at different replicas.

Sequential consistency requires that all operations appear to execute in some total order consistent with each process's program order. Unlike linearizability, this order need not respect real-time constraints. An operation that completes before another begins might appear after it in the sequential order. This seemingly small relaxation has profound implications for both implementation and verification.

Between these models lie numerous intermediate points. PRAM consistency requires only that each process's operations appear in program order, without constraining how different processes' operations interleave. Processor consistency adds coherence requirements for individual objects. The CAP theorem's availability requirement can be satisfied by any model weaker than linearizability, but different models offer different tradeoffs between semantic strength and implementation complexity.

Takeaway

Consistency models form a precise mathematical hierarchy, not a vague spectrum. Understanding exactly what anomalies each model permits—and which it rules out—is prerequisite to choosing appropriately for a given application.

Pure eventual consistency offers minimal guarantees, but practical systems often provide session guarantees that strengthen semantics for individual client sessions while preserving the scalability benefits of weak consistency across the system as a whole.

Read-your-writes guarantees that a client will observe its own writes. This prevents the jarring anomaly where you submit a form, refresh the page, and see the old data. Formally, if session S performs write W and then read R, R must return a state that includes W. This guarantee is purely local—other sessions may not immediately observe W.

Monotonic reads ensures that successive reads by a session return increasingly recent values. If a client reads version 5, subsequent reads will not return versions 1 through 4. This prevents the unsettling experience of data appearing to go backward. The guarantee constrains only reads within a session; different sessions may observe different histories.

Monotonic writes guarantees that writes by a session are serialized in program order. If a client writes A then B, all replicas will apply A before B. Without this guarantee, a client might update a record and then delete it, only to have some replicas apply the delete first, leaving the record in an unexpected state.

Writes-follow-reads ensures that if a session reads a value and then writes, the write is serialized after the read value. This captures the common pattern of read-modify-write operations. The combination of all four session guarantees provides semantics sometimes called session causality, which is strictly weaker than full causal consistency but sufficient for many applications. Implementing these guarantees typically requires tracking session state and enforcing ordering constraints at the client or session-affine routing layer.

Takeaway

Session guarantees let you strengthen consistency selectively, providing intuitive semantics for individual users without paying the global coordination costs of stronger models.

A fundamental asymmetry separates strong and weak consistency verification. For linearizable systems, a single anomalous execution proves the system incorrect—we can detect violations by observing behavior that no linearizable system could produce. For weak consistency models, testing faces a harder problem: distinguishing a correctly eventually-consistent system from an incorrect one requires reasoning about executions that might occur, not just those observed.

Consider eventual consistency's convergence requirement. Demonstrating convergence requires showing that all executions eventually reach agreement. No finite test can verify this property because a system might converge in all tested scenarios while having pathological cases where convergence fails or takes arbitrarily long. The property is fundamentally about all possible executions, not any particular execution.

Linearizability checking is NP-complete in the number of operations, making exhaustive testing of even short histories computationally expensive. Weaker models often have similar or greater verification complexity. Causal consistency checking requires determining whether a valid causal ordering exists for an observed execution—a constraint satisfaction problem that scales poorly with execution size.

Formal verification offers a path forward. Specification languages like TLA+ allow defining consistency models precisely and proving that implementations satisfy them. The challenge is that proofs require formal models of the implementation, not just the interface. Verification of distributed protocols has succeeded in catching subtle bugs in Paxos variants, Raft implementations, and database replication protocols.

Runtime verification provides a middle ground. Systems can be instrumented to track metadata sufficient to detect consistency violations online. For causal consistency, vector clocks enable detecting causality violations. For session guarantees, session-scoped version tracking is sufficient. These approaches detect violations when they occur but cannot prove their absence. The gap between testing and proof remains fundamental—weak consistency models require formal methods for strong assurance.

Takeaway

Testing can find consistency bugs but cannot prove their absence. Formal verification is not academic overhead—for weak consistency models, it may be the only path to justified confidence in correctness.

The space between eventual consistency and linearizability is not a void but a structured landscape of precisely defined models. Each model represents a specific point in the tradeoff between coordination cost and semantic strength. Choosing appropriately requires understanding exactly what anomalies each model permits.

Session guarantees offer a particularly practical middle ground, strengthening semantics for individual clients while preserving system-wide scalability. The formal hierarchy of models provides the vocabulary necessary for precise requirements and principled implementation choices.

Verification remains the hardest challenge. Weak consistency models resist testing because correctness is a property of all possible executions, not observed ones. This makes formal methods not merely useful but often necessary for justified confidence. The rigor demanded by weak consistency verification reflects the inherent complexity of reasoning about systems that permit more behaviors than our intuitions expect.