Distributed systems
System models and what you assume
A correctness proof depends on the assumptions behind it. Learn the three parts of a system model, network, node and timing, and the model real systems should design for.
Algorithms are proven correct under a system model. A system model is a formal statement of what can go wrong. Pick a model that is too optimistic and an algorithm that is "correct" breaks in production. Pick one that is too pessimistic and the algorithm is too expensive to run.
Concept
Before you start: read partial failure and network faults. A system model is a list of which of those faults you allow.
The big idea
A model has three parts: how the network behaves, how nodes behave, and how timing behaves.
| Part | Option | What it means | Realistic? |
|---|---|---|---|
| Network | Reliable links | Every message arrives exactly once, eventually | No. Approximated with TCP, retries and deduplication |
| Network | Fair-loss links | Messages may be lost, duplicated or reordered, but retries eventually get through | Yes |
| Network | Arbitrary links | An adversary can drop, change or inject messages | Use TLS to turn this into fair-loss |
| Node | Crash-stop | Works until it crashes, then never returns | Simpler than reality |
| Node | Crash-recovery | Crashes, restarts, loses memory, keeps what was written to disk | Yes. Raft and most databases assume this |
| Node | Byzantine | May do anything, including lying to different peers | Rare inside one company's data center |
| Timing | Synchronous | Message delay and process pauses have known upper bounds | No |
| Timing | Asynchronous | No timing assumptions at all | Very robust, but some problems, such as consensus, become impossible to solve deterministically |
| Timing | Partially synchronous | Usually behaves synchronously, but may exceed the bounds for unknown periods | Yes. Raft and Paxos are always safe, and make progress when the network behaves |
Byzantine tolerance is expensive. It needs 3f+1 nodes to survive f faulty ones, plus signatures. Your own servers are not usually trying to deceive you, so most systems skip it.
Walking through a wrong assumption
Suppose an algorithm assumes a process never pauses for more than 5 seconds. It grants a lock with a 10-second lease and assumes the holder will finish or renew well within that window.
t=0s holder A gets the lock, lease 10 s
t=2s A pauses for a 15-second garbage collection
t=10s lease expires; B gets the lock
t=17s A wakes up and still believes it holds the lockThe broken assumption is about timing, but the damage is to correctness. Two holders now act at once. This is why safety must never depend on timing. The process pauses page covers this in depth.
Common mistakes
- Making safety depend on timing. Timing can affect speed and progress. It must not decide whether data is correct.
- Assuming Byzantine faults in your own data center. The cost is high, and it is rarely the threat you face.
- Forgetting that crash-recovery nodes lose memory. Anything that must survive a restart has to be on disk before the node acts on it.
Check yourself
1. Why do consensus protocols like Raft assume partial synchrony? They stay safe under any timing and make progress when the network behaves well. That is the best trade-off for real networks.
2. How does a crash-recovery node differ from a crash-stop node? It comes back. So anything it must not forget has to be on disk, and it must not act on beliefs it held before the crash without checking them again.
Key takeaways
- A system model lists what can go wrong in the network, the nodes and the timing.
- For most real systems, design for crash-recovery nodes, fair-loss links and partial synchrony.
- Safety must never depend on timing. Timing affects only liveness, which is whether progress happens.
Further learning
Kleppmann's lecture on system models walks through network, node and timing assumptions with clear examples. It is the best twenty minutes of grounding for this page.
Next, see what happens to a process that pauses in process pauses and clock jumps.
Related
Consensus and Raft
How a cluster agrees on one value or one log despite crashes and partitions, how Raft works, and where etcd, ZooKeeper and consensus-backed databases fit.
Network faults and gray failures
Packets are lost, delayed, duplicated and reordered, and partitions can be one-way or partial. Learn the faults to design for, including gray failures that pass health checks.
Process pauses and clock jumps
A process can freeze for seconds and keep believing it is still the leader. Learn the causes of pauses and clock jumps, and why they break leases and locks.