Everything about distributed systems is terrible
summary
Models an upload → queue → worker pipeline with a perfect exactly-once queue, then relaxes assumptions and adds a second worker, using a TLA+ model checker to enumerate state space and produce counterexample traces. The model finds a 16-step failure and later a 20-step failure that require adding both a retry-on-stale-edit and a nightly cleaner to prevent orphan content. Each new scenario checks in minutes (about two minutes for the 16-step trace), not months.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:32Leslie Lamport
- 2:27Thought Experiment
- 4:39State Space
- 7:08Non Determinism
- 14:33Model Checker
- 16:36Important Caveats
- 18:33Non-Determinism
- 22:13The Model Checker
- 25:52How Many Steps Does It Take To Break
- 28:42Adding Permissions
- 30:45Resources To Start Learning
- 35:43Where To Get Started
related talks
01h 13mDesigning distributed systems with TLA+
29mHorrors of Distributed Systems
52mDistributed Computing Dealing with Time and Failure in the Wild
34mDistributed Systems - What Can Go Wrong and How to Get It Right
13mExplaining Distributed Systems Like I'm 5
01h 12mDistributed systems showdown — TLA + vs real code
42mFive Common Mistakes With Distributed Systems
43mWhat We Talk About When We Talk About Distributed Systems