Invariants, safety, liveness and distributed correctness

Why it matters

Distributed systems fail in interleavings that tests rarely hit: a leader that does not know it was replaced, a retried request applied twice, a read served by a stale replica. The defence is a disciplined argument: what can fail, what must never happen, what must eventually happen, and which invariant connects them. Systems papers state their guarantees in exactly these terms, and interviews for distributed-systems and systems-research roles ask you to argue correctness out loud or to find the bug in a protocol sketch.

Core ideas

Fault and timing models. A guarantee means nothing without its model. Nodes may crash and stop, crash and recover with stable storage, omit messages or behave arbitrarily (Byzantine). Networks may lose, delay, duplicate or reorder messages. Timing may be synchronous (known bounds), asynchronous (no bounds) or partially synchronous (bounds that hold eventually). The FLP result shows that in a fully asynchronous system no deterministic protocol can guarantee consensus if even one process may crash; protocols such as Paxos and Raft therefore keep safety unconditionally and rely on partial synchrony only for liveness.

Safety and liveness. Safety says nothing bad ever happens ("at most one leader per term", "committed entries are never lost"); any violation is visible in a finite prefix of an execution. Liveness says something good eventually happens ("every client request eventually completes"); no finite prefix can violate it, so it needs assumptions such as fairness or eventual timing bounds. Every property can be written as the intersection of a safety property and a liveness property.

Invariants. An invariant holds in every reachable state. To prove one, show it holds initially and that every transition preserves it. If the second step fails, the invariant may still be true but not inductive, and you strengthen it with auxiliary facts, such as "no log entry has a term larger than its server's current term". Raft's safety argument has this shape: Election Safety, Log Matching and Leader Completeness together imply State Machine Safety. Quorum intersection (any two majorities of the same configuration share a member) and monotonically increasing terms or epochs are the recurring building blocks.

Consistency models. Linearizability: every operation appears to take effect atomically at one point between its invocation and its response, respecting real time. Sequential consistency drops the real-time requirement. Serializability concerns multi-object transactions without real-time constraints; strict serializability adds them. Weaker models such as causal or eventual consistency trade guarantees for availability. To check a history for linearizability, find an order of operations that respects real-time precedence and the object's sequential specification. Knossos and Porcupine automate this for registers and key/value maps; Elle checks transactional isolation anomalies.

Model checking. TLA+ describes a system as an initial-state predicate and a next-state relation. The TLC model checker explores every reachable state of a small instance (three servers, two values, bounded terms) and prints a counterexample trace when an invariant fails. It finds design bugs that random testing would need enormous luck to hit, but it is bounded: passing small instances is evidence, not proof. Machine-checked proofs or careful hand proofs cover the general case.

Traces. In practice you debug by reconstructing a timeline: per-node logs with terms, indices and message identifiers, merged in happens-before order. Find the first state that violates an invariant, then ask which message or timeout produced it. The 6.5840 Raft tests write visual timelines of partitions, crashes and checks when a test fails, which makes this skill concrete.

Common misconceptions

• "If tests pass under failures, the protocol is correct." Tests sample a few interleavings; invariants and model checking reason about all of them within a model.
• "Raft makes progress whenever a majority is up." Safety holds always; progress also needs a stable leader and message delays well below the election timeout.
• "Linearizable and serializable mean the same thing." Linearizability is a real-time guarantee on single operations; serializability is about transactions and allows real-time reordering.
• "A true invariant is enough for a proof." It must be inductive; otherwise a step from an unreachable state that satisfies it can break it, and the proof fails.
• "Model checking a small configuration proves the system correct." It shows no violation within the bounds explored; larger configurations or longer histories can still fail.

How to approach it

Restate Raft's Figure 3 properties in your own words and prove one by hand, then work through the 6.5840 linearizability lecture with the Herlihy and Wing paper. Write a small TLA+ specification, plant a bug and read TLC's counterexample. In interviews, open every correctness answer with the fault model, name the invariant, and only then walk through the protocol.