Abstract
GPUs offer parallelism as a commodity, but they are difficult to
program correctly. Static analyzers that guarantee data-race freedom
(DRF) are essential to help programmers establish the correctness
of their programs (kernels). However, existing approaches produce
too many false alarms and struggle to handle larger programs. To
address these limitations we formalize a novel compositional analysis for
DRF, based on memory access protocols. These protocols are behavioral types that codify the way threads interact over shared memory.
Our work includes fully mechanized proofs of our theoretical results,
the first mechanized proofs in the field of DRF analysis for GPU
kernels. Our theory is implemented in Faial, a tool that outperforms
the state-of-the-art. Notably, it can correctly verify at least 1.42×
more real-world kernels, and it exhibits a linear growth in 4 out of
5 experiments, while others grow exponentially in all 5 experiments.
program correctly. Static analyzers that guarantee data-race freedom
(DRF) are essential to help programmers establish the correctness
of their programs (kernels). However, existing approaches produce
too many false alarms and struggle to handle larger programs. To
address these limitations we formalize a novel compositional analysis for
DRF, based on memory access protocols. These protocols are behavioral types that codify the way threads interact over shared memory.
Our work includes fully mechanized proofs of our theoretical results,
the first mechanized proofs in the field of DRF analysis for GPU
kernels. Our theory is implemented in Faial, a tool that outperforms
the state-of-the-art. Notably, it can correctly verify at least 1.42×
more real-world kernels, and it exhibits a linear growth in 4 out of
5 experiments, while others grow exponentially in all 5 experiments.
| Original language | English |
|---|---|
| Journal | Formal Methods in System Design |
| DOIs | |
| Publication status | Published - 26 May 2023 |