Sound Static Data Race Verification for C: Is the Race Lost?
summary
Paper evaluates SV-COMP race verifiers on real C programs and on extracted micro-benchmarks that codify common multithreaded idioms, measuring soundness and scalability under resource limits. The authors add those micro-benchmarks to SV-COMP and find 8 of 20 idioms are verifiable by some tool, but also report Goblint and Deagle unsound behavior. Most tools choke: 5 of 7 tools failed to return results on any real-world program, and only 2 of 18 programs verified by the remaining tools, exposing clear gaps for non-lock idioms.
AI-written summary · about
chapters (10)
- 0:00Data race verification intro
- 1:06Sound static verification dream
- 2:53Benchmarks vs real-world gap
- 3:55Idioms for data races
- 8:36Idiom extraction method
- 11:32Challenging idioms prevalence
- 13:19Lock vs non-lock sync conclusion
- 14:03Q&A
- 15:15Q&A benign races
- 16:41Benign races in C
related talks
22mData race detection
01h 04mDebugging data races
07mRace Conditions in Details
17mSSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures
01h 11mProgramming language memory models: Problems, solutions, and directions
19mRuntime Detection of Data Races in OCaml with ThreadSanitizer
24mSimuliris: A Separation Logic Framework for Verifying Concurrent Program Optimiz
21mAutomated Robustness Verification of Concurrent Data Structure Libraries Against(…)