Data Race Detection by Digest-Driven Abstract Interpretation
summary
Presents a concrete, sound definition of data races in a thread‑modular local trace semantics and implements a digest-driven abstract interpretation in Goblint to check it. Digests summarize thread histories; a generic birectional digest compatibility predicate rules out races, while bespoke checks (for example the lockset digest or a thread id digest) prove more. Evaluation on the Sv-Comp suite shows combining lockset with thread-id and join reasoning increases correctly solved tasks by more than a factor of five, and the implementation scales to real benchmarks.
AI-written summary · about
chapters (14)
- 0:00Data race detection intro
- 1:26Classical data race definition
- 2:49Thread modular abstract interpretation
- 4:12Digest-driven abstract interpretation
- 8:23Paper contributions
- 9:25Generic digest-driven detection
- 14:44Example with thread ID digest
- 16:55Dedicated digest definitions
- 18:37Combining digests for precision
- 20:02Goblin race detection algorithm
- 22:28SV-COMP evaluation
- 24:53Summary
- 25:34Q&A
- 26:57Q&A
related talks
31mRace Conditions - Practical Tools & Techniques for Testing, Preventing, and Debugging C++/C Code
15mSafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
20mData Race Freedom à la Mode
42mUnderstanding Data Races in the Linux Kernel
24mDATA – Differential Address Trace Analysis: Finding Address-based Side-Channels in Binaries
34mDetecting Race Conditions on macOS
27mLightweight Shape Analysis based on Physical Types
10mBacktraces in the mirror: mad science by secrets of elves & dwarves!!