Hidden assumptions in static verification of data-race free GPU programs

on YouTube ↗19m

" summary

Faial is a static analyzer for GPU kernels that checks data-race freedom and delegates checks to an SMT solver, running most kernels in under a minute. On a 191-kernel dataset, 98% require a specific thread/grid configuration to be analyzable and 27% need user-provided assumptions (assume/early-return). When those assumptions are missing Faial reports true data races in at least 92% of cases, finds several misconfigured kernels, and exposes six limitations in its interprocedural and loop-pointer handling.

AI-written summary · about

" chapters (16)

1. 0:00Static verification of GPU data races
2. 6:42Verification tool for data-race free kernels
3. 7:43Tool defaults and assumptions
4. 8:51Thread configuration impact
5. 9:31True versus potential data races
6. 10:15Workarounds for thread issues
7. 10:57Evaluating assumptions in experiment
8. 11:18Grid synchronization and data races
9. 12:22Experiment design and dataset
10. 13:51Grid sync impact on analysis
11. 14:35Effect of user assumptions
12. 15:18Static detection of missing assumptions
13. 16:22Tool limitations and findings
14. 17:23Patterns overlooked by tool
15. 17:44Key findings and conclusions
16. 18:09Q&A: Analysis time