Designing distributed systems with TLA+
summary
A practical design walkthrough models an asynchronous upload→worker pipeline in TLA+ (using PlusCal) and exhaustively checks behaviors with the TLC model checker, revealing concrete bugs: a missing-case that drops a create message, a 15-step race that leaves content one version behind, and an orphaning race fixed only by combined version checks plus a nightly cleanup. Examples of industry wins include a 35-step AWS bug that would have lost data and an Elasticsearch replication bug found and fixed.
AI-written summary · about
chapters (13)
- 0:00Introduction and logistics
- 1:43Defining distributed systems
- 4:25State space and concurrency
- 9:16Behavior space and failures
- 13:07Scale and Murphy's Law
- 14:41Limitations of code testing
- 17:56Introduction to TLA+
- 22:40Modeling an ETL system
- 34:04Debugging with model checkers
- 37:13Scaling and complex races
- 42:02Industry use cases
- 45:50Learning resources
- 47:39Q&A session
related talks
01h 12mDistributed systems showdown — TLA + vs real code
01h 13mWorkshop: TLA+ in action (Part 3)
01h 12mWorkshop: TLA+ in action (Part 4)
41mDesigning software with complex configurations
34mTLA+ at Microsoft to build planetary-scale systems
38mEverything about distributed systems is terrible
43mWeeks of Debugging Can Save You Hours of TLA+
42mWelcome to TLA-La-Land (or An Introduction to Software Verification)