TraceLinking Implementations with their Verified Designs
summary
TraceLink automatically maps runtime traces from PGo-generated Go programs back to their TLA+ designs, uses vector clocks to record causal partial orders, and provides a formal semantics plus a templatization to shrink TLA+ tracing specs. A novel sidestep path-validation checks one-step alternative schedules cheaply. Evaluation on a Raft key-value system records traces up to 100,000 events across 26 processes and counterexamples over 10,000 states; TraceLink finds 9 previously undetected bugs, including a PGo compiler bug.
AI-written summary · about
chapters (11)
- 0:00Trace validation introduction
- 1:26Prior work on trace validation
- 3:10TraceLinking architecture
- 4:36Simple distributed example
- 7:06Pre-sorted traces problem
- 8:28Causal traces and failures
- 9:53Sidestep for model checking
- 11:24Evaluation on RaftKVS
- 12:49Sidestep bug finding
- 13:10Summary and ongoing work
- 13:51Q&A
related talks
24mTLA+: Your Secret Weapon Against Concurrency Hell
41mDesigning software with complex configurations
21mAbstract Debuggers: Exploring Program Behaviors Using Static Analysis Results
19mPete's Footprints
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
39mWeeks of Debugging Can Save You Hours of TLA+
11mFix your hardest bugs with ease with Time Travel Debugging - Session Interview With Greg Law
56mPath Tracing Three Ways: A Study of C++ Style