TY - GEN
T1 - Checking Data-Race Freedom of GPU Kernels, Compositionally
AU - Cogumbreiro, Tiago
AU - Lange, Julien
AU - Rong, Dennis Liew Zhen
AU - Zicarelli, Hannah
N1 - Publisher Copyright:
© 2021, The Author(s).
PY - 2021
Y1 - 2021
N2 - 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 access memory 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.
AB - 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 access memory 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.
KW - Behavioural types
KW - Data-race
KW - GPU
KW - Static analysis
UR - https://www.scopus.com/pages/publications/85113484375
UR - https://www.scopus.com/pages/publications/85113484375#tab=citedBy
U2 - 10.1007/978-3-030-81685-8_19
DO - 10.1007/978-3-030-81685-8_19
M3 - Conference contribution
AN - SCOPUS:85113484375
SN - 9783030816841
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 403
EP - 426
BT - Computer Aided Verification - 33rd International Conference, CAV 2021, Proceedings
A2 - Silva, Alexandra
A2 - Leino, K. Rustan
PB - Springer Science and Business Media Deutschland GmbH
T2 - 33rd International Conference on Computer Aided Verification, CAV 2021
Y2 - 20 July 2021 through 23 July 2021
ER -