Checking Data-Race Freedom of GPU Kernels, Compositionally. / Cogumbreiro, Tiago; Lange, Julien; Liew Zhen Rong, Dennis; Zicarelli, Hannah.

International Conference on Computer-Aided Verification. Vol. 12759 Springer-Verlag, 2021.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

E-pub ahead of print
  • Tiago Cogumbreiro
  • Julien Lange
  • Dennis Liew Zhen Rong
  • Hannah Zicarelli

Abstract

GPUs offer parallelism as a commodity, but they are diffi- cult 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.
Original languageEnglish
Title of host publicationInternational Conference on Computer-Aided Verification
PublisherSpringer-Verlag
Volume12759
ISBN (Electronic)978-3-030-81685-8
ISBN (Print)978-3-030-81684-1
DOIs
Publication statusE-pub ahead of print - 15 Jul 2021
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 42271340