Workshop: TLA+ in action (Part 3)
summary
A runnable TLA+ model of Dijkstra/Safra EWD998 appears, modeling node color and per-node counters, a token record with position Q and color, and message actions; TLC model checking finds about 17,000 states for 3 nodes and a diameter 37, reveals negative counter and liveness issues, and exposes a bug where a choose expression never selects one recipient. Refinement mapping to the high‑level spec is shown, fairness is adjusted to the system, and the TLC debugger plus 10,000 simulations validate and expose the flaws.
AI-written summary · about
chapters (14)
- 0:00Intro
- 1:20Recap
- 5:40Missing concepts
- 6:37Termination detection
- 8:01Rules
- 10:18EWB998
- 17:13Defining functions
- 19:28Defining records
- 21:33Defining variables
- 22:00Defining system
- 24:15Initiate probe action
- 36:31Choose
- 40:23System
- 47:43Replacing termination detection
related talks
01h 13mDesigning distributed systems with TLA+
41mDesigning software with complex configurations
15mTLC: Temporal Logic of Distributed Components
43mWeeks of Debugging Can Save You Hours of TLA+
31mTurning an Incident Report into a Design Issue with TLA+
34mTLA+ at Microsoft to build planetary-scale systems
14mModel-guided Fuzzing of Distributed Systems
32mTLA + specification of PCR parallel programming pattern