Themis: Detecting Distributed Concurrency Bugs through RPC-Driven Race-Directed Test...
summary
Themis combines static RPC-driven race detection with LLM-based test generation and directed fuzzing and interleaving exploration to find distributed concurrency bugs that involve RPC-triggered concurrent flows. The system statically finds RPC-reachable variables and candidate races, generates harnesses with LLMs, uses targeted fuzzing to satisfy path constraints and force specific interleavings, and verifies symptoms. A prototype on eight real-world systems finds 198 new violations corresponding to 52 new bugs, with confirmed reproductions.
AI-written summary · about
chapters (13)
- 0:00Simu and distributed concurrency bugs
- 1:03Distributed concurrency bugs impact
- 2:28Prior work limitations and Simu's approach
- 3:32Static RPC-driven race detection
- 5:40RPC-reachable variables and access sites
- 7:27Violations and atomicity violations
- 8:49Public interfaces and benign races
- 10:16Test harnesses with real aim
- 11:42Directed fuzzing and interleaving
- 13:51Implicit error conditions checks
- 14:37Evaluation on eight cloud systems
- 15:40Test case generation and violations
- 16:01Conclusion and future work
related talks
24mRacerD - Compositional Static Race Detection
18mPreview: Verification (Correctness & Debugging)
32mEventRacer: Finding Concurrency Errors in Event-Driven Applications
36mStateful property-based testing: with a game logic case study
55mMuch ado about testing
07mWhy Tracing is a Lifesaver for E2E Tests of Distributed Systems?
14mModel-guided Fuzzing of Distributed Systems
23mBeyond Tests What to Verify in AI Generated Code