Safety and liveness
Why is eventual consistency a different kind of claim, and why is a bound the real product?
The cut that must come first: safety or liveness
Two kinds of property can be asked of a system.
- A safety property says "a bad thing never happens". It is violated by a finite prefix of a history. You can show the counterexample and stop. Example: "no two clients ever see two different values for the same lock."
- A liveness property says "a good thing eventually happens". It is violated only by an infinite history. No finite observation can refute it, because the answer to any counterexample is "wait longer". Example: "every request eventually gets an answer."
Linearizability, sequential consistency, causal consistency, the session guarantees and consistent prefix (all explained below and in Sessions, convergence and quorums) are safety properties. They are falsifiable. So they are testable, and so they can be enforced.
Eventual consistency is a liveness property. No finite observation violates it. It cannot be tested, cannot be monitored, cannot appear in a service-level objective (SLO, a measurable target such as "99.9% of requests under 200 ms"), and cannot be violated. Putting it at the bottom of a ladder whose other rungs are safety properties is a category error. It is also the reason the term has come to mean almost nothing.
Two consequences to carry through the rest of this mechanism.
Eventual consistency is vacuous under the conditions you care about. Its standard statement is conditional: if no new updates are made, all replicas converge. A system under continuous write load never satisfies the "if", so the guarantee says literally nothing about it. Pebble's ledger is never quiet.
Liveness becomes operable only when it is bounded, and the bound is the real product. This is the bound rule. Bounded staleness ("a read is never more than 5 seconds behind") is what every serious "eventually consistent" system actually sells. The bound turns a liveness claim into a safety claim that you can alarm on. The same move appears again and again in systems:
| Liveness claim | Bounded form | The bound |
|---|---|---|
| Replicas eventually converge | Bounded staleness | seconds of lag |
| The job eventually finishes | Timeout | a deadline |
| Late events eventually arrive | Watermark (a stream-processing marker meaning "I will wait at most this long for late data") | allowed lateness |
| The message is eventually delivered | Retry budget / deadline | number of tries |
| Compaction eventually catches up | Write-stall threshold | allowed backlog |
Strong eventual consistency splits the difference honestly. It has two parts: eventual delivery (liveness) plus convergence. Convergence means: any two replicas that have delivered the same set of updates are in the same state. That second part is a safety property, and it can be checked in finite time. The name "strong eventual" is therefore earned.