Weeks of Debugging Can Save You Hours of TLA+
summary
A TLA+ spec of a bounded MPMC queue reproduces and explains a surprising deadlock that unit tests miss: TLC finds a violating trace (shortest 9 steps, another case 47 steps) for a 4-producer/3-consumer/buffer-3 configuration and for minimal 2-producer/1-consumer/buffer-1. Modeling waiting threads and scheduling yields two fixes verified by TLC: notify other (wake opposite-type waiters) and using a FIFO wait sequence to prevent starvation. The Toolbox and animated traces expose the exact step sequence so the fixes are checked on small scopes.
AI-written summary · about
chapters (11)
- 0:00Introduction to TLA+
- 0:38What is TLA+?
- 2:16Service outage analysis
- 3:42Analyzing the C++ code
- 6:22Reproducing the deadlock
- 8:52Writing the TLA+ spec
- 13:54Verifying the specification
- 19:25Debugging with trace animation
- 22:25Fixing the deadlock
- 25:16Addressing starvation issues
- 30:46Summary and conclusion
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
41mDesigning software with complex configurations
28mExploring and improving the design of Abaco
40mEverything Will Flow
54mReasoning about Progress of Concurrent Objects
15mTraceLinking Implementations with their Verified Designs
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
28mBounded Model Checking of PLC ST Programs using Rewriting Modulo SMT