Testing and Verifying Chain Repair Protocols using Concuerror
summary
Model of Corfu chain repair gets programmed in Erlang and checked with Concuerror; the tool finds a known buggy repair quickly with bounding — about 65 traces in 7 seconds — while full exploration needs ~3.5 million interleavings and ≈1144 hours for that case. Refinements to the model and a receive-aware optimization reduce state space so a third repair method verifies in under ~48 hours exploring under ~4 million traces. The talk shows concrete counterexamples, measured runtimes, and which model changes actually make verification feasible.
AI-written summary · about
chapters (22)
- 0:00Introduction
- 0:30Geography
- 2:10The Tweet
- 2:47Kotlik Fritz
- 3:51Overview
- 4:49Chain Replication Basics
- 6:45Chain Repair
- 9:26CORFU
- 10:41VMware
- 15:05Systematic concurrency testing
- 16:12How does it work
- 17:00Example
- 22:16Concuerror
- 22:51Interleavings
- 23:31Optimal Partial Order Reduction
- 24:46Bounding
- 25:30Testing with Bounding
- 30:40Results
- 38:01Model refinements
- 39:02Verification
- 41:02Concuerror is a tool
- 42:37Questions
related talks
51mFinding Concurrency Errors using Concuerror
51mA CutEr Tool
47mTesting the Hard Stuff and Staying Sane
26mIs this really a refactoring? Automated equivalence checking for Erlang projects
18mPreview: Verification (Correctness)
38mThe Verification of a Distributed System
04mFTFY: Research advances in automatic bug repair
27mBreak It Yourself