Sound and partially-complete static analysis of data-races in GPU programs
summary
A sound static verifier and a partially-complete race finder named FaialAA implements memory-access protocols, SMT encoding, and mechanized proofs to guarantee that alarms on a specific class of programs are true via a True Positive Theorem. Evaluation shows 1.9× fewer potential alarms than prior tools, confirms 5 of 6 real-world bug-fix commits, and finds 10 undocumented races; analysis is exact on 59.5% CI/DI of 2,770 kernels.
AI-written summary · about
chapters (10)
- 0:00Data races in GPU programs
- 1:26Soundness vs completeness in verification
- 3:55Introducing FileA analyzer
- 4:36Evaluating FileA on open-source projects
- 6:46FileA’s false alarms vs state-of-the-art
- 7:50Sources of false alarms in GPU analysis
- 10:18Control flow in GPU programs
- 11:45True positives theorem
- 12:07Conclusion and future work
- 13:09Q&A
related talks
24mRacerD - Compositional Static Race Detection
22mData race detection
44m"go test -race" Under the Hood
19mRuntime Detection of Data Races in OCaml with ThreadSanitizer
32mMaTSa: Race Detection in Java
17mSSRD: Shapes and Summaries for Race Detection in Concurrent Data Structures
18mPreview: Verification (Correctness & Debugging)
32mEventRacer: Finding Concurrency Errors in Event-Driven Applications