Sound Deadlock Prediction
summary
Claims a first sound deadlock predictor for Java that models prediction as a decidable SMT-backed decision problem and actually builds it: a recorder Wiretap and predictor Dirk that add request events and executability constraints plus a data-flow consistency check. Evaluation on 11 programs finds no false positives, discovers deadlocks missed by DeadlockFuzzer, and reports slightly more real data races than RVPredict (average over ~100 runs), while sometimes running 7× to 250× slower on large benchmarks.
AI-written summary · about
chapters (4)
related talks
15mSound Dynamic Deadlock Prediction in Linear Time
15mSoundness of Predictive Concurrency Analyses
55mJava PathFinder: going to Mars without bugs and deadlocks
01h 08mSimplifying Concurrent Programming via Synchronization Synthesis
28mEnd-to-end Deadlock Debugging Tools at Facebook
28mAutomated Correctness Analysis for core.async
47mUsing Java 8 Lambdas and Stampedlock to manage thread safety
35mPredictable Latency