What happens-after the first race? enhancing the predictive power of dynamic race detection
summary
Proposes schedulable happens-before (SHB), a partial order that exactly characterizes which HB-unordered conflicting accesses are actually schedulable races, and gives a linear-time vector clock algorithm that adds an extra per-location vector clock to track last writes. Implements the algorithm in Java, runs on traces up to ~200 million events, and finds HB tools (e.g., ThreadSanitizer/FastTrack) report about twice as many warnings (hundreds of thousands, e.g., ~750k) of which manual inspection shows many false positives; SAT-based feasibility does not scale.
AI-written summary · about
chapters (7)
- 0:00Start
- 0:53Dynamic Race Detection
- 2:52Happens-Before: Soundness Guarantee
- 5:23Why Detect Multiple Races?
- 14:02Vector-clock algorithm for SHB
- 14:45Implementation
- 18:01Concluding Remarks
related talks
23mDynamic Race Detection with O(1) Samples
01h 04mDebugging data races
22mData race detection
07mRace Conditions in Details
19mEfficient Timestamping for Sampling-Based Race Detection
19mRuntime Detection of Data Races in OCaml with ThreadSanitizer
54mStructured Concurrency: Hierarchical Cancellation & Error Handling
17mSSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures