Turning an Incident Report into a Design Issue with TLA+
summary
A precise TLA+ specification of Cosmos DB behavior reproduces the 28-day outage as a counterexample and shows the root cause is missing session tokens between dispatcher enqueue and worker read. The team builds a small simulator and runs the TLC checker on two text files — a single-file checker on a laptop — which exhaustively explores schedules, finds scenarios with writes visible but reads returning 404, and verifies the fix: attach the session token and the assertion holds for all explored cases.
AI-written summary · about
chapters (13)
- 0:00Start
- 0:49Highlights
- 2:19A Workflow Beyond Incident Reports
- 3:24Story Time: an Incident
- 5:04What's the Big Deal?
- 6:08What is Azure CosmosDB?
- 6:53Key Detail: Communication with Azure Cos
- 8:02CosmosDB: Consensus Machine
- 8:41CosmosDB: Consistency Levels
- 10:27CosmosDB: What to Model for Our Purpose?
- 24:49Thinking in States: Branching Possibilities
- 26:54The Corrected Design
- 29:56Summary
related talks
01h 13mDesigning distributed systems with TLA+
43mWeeks of Debugging Can Save You Hours of TLA+
34mTLA+ at Microsoft to build planetary-scale systems
01h 12mWorkshop: TLA+ in action (Part 4)
01h 13mWorkshop: TLA+ in action (Part 3)
01h 14mWorkshop: TLA+ in action (Part 1)
01h 11mWorkshop: TLA+ in action (Part 2)
01h 12mDistributed systems showdown — TLA + vs real code