Book ChapterHidden Assumptions in Static Verification of Data-race Free GPU ProgramsCogumbreiro, Tiago (ORCID:0000000232099258); Lange, Julien (ORCID:0000000196971378)GPUs are massively parallel devices that promise a great return of investment at a cost: GPUs are notably difficult to get right. We discuss a static analysis tool for GPU programs, called Faial, that can detect data-races and data-race freedom. We studied a dataset of 191 data-race free programs and found that 98% needs specific thread configuration to be analyzable, and that 27% needs user-provided assertions to be analyzable. We also report that Faial was able to find data-races in at least 92% of the kernels with missing assumptions.Springer Nature Switzerland2025-01-011066831955 to 63https://doi.org/10.1007/978-3-031-97492-2_62204986National Science Foundation