Weeks of Debugging Can Save You Hours of TLA+
summary
A TLA+ model of a simple webshop reproduces a real-world bug: after about 1800 reads the backend sometimes sees no order because replication lag plus the wrong consistency level causes a missing read. The model checks all executions, produces the shortest counterexample in ~10 steps, and a 200-line database abstraction helps experiment with fixes: switching to strong vs eventual consistency or using session consistency with the correct session token eliminates the anomaly.
AI-written summary · about
chapters (17)
- 0:00TLA+ methodology intro
- 1:07Distributed system approaches
- 4:15Pierogi webshop prototype
- 8:11End-to-end prototype tests
- 10:00Modeling system with TLA+
- 16:26Consistency bug in testing
- 19:39Debugging with TLA+
- 24:18Fixing with stronger consistency
- 27:36Session consistency solution
- 31:06Database abstraction in TLA+
- 33:13TLA+ and non-determinism
- 35:02Who uses TLA+
- 37:11TLA+ benefits beyond verification
- 38:38Q&A: Spec and code sync
- 41:03Q&A: When to use TLA+
- 42:07Q&A: Automating TLA+ specs
- 43:08Closing remarks
related talks
01h 13mDesigning distributed systems with TLA+
01h 13mWorkshop: TLA+ in action (Part 3)
01h 12mDistributed systems showdown — TLA + vs real code
01h 12mWorkshop: TLA+ in action (Part 4)
01h 11mWorkshop: TLA+ in action (Part 2)
31mTurning an Incident Report into a Design Issue with TLA+
01h 14mWorkshop: TLA+ in action (Part 1)
41mDesigning software with complex configurations