Barrier Invariants: A Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels

Nathan Chong, Alastair F. Donaldson, Paul H.J. Kelly, Jeroen Ketema, Shaz Qadeer
Imperial College London
28th ACM International Conference on Object Oriented Programming, Systems, Languages, and Applications (OOPSLA 2013), 2013


   title={Barrier Invariants: A Shared State Abstraction for the Analysis of Data-Dependent GPU Kernels},

   author={Donaldson, Nathan Chong Alastair F and Ketema, Paul HJ Kelly Jeroen and Qadeer, Shaz},



Data-dependent GPU kernels, whose data or control flow are dependent on the input of the program, are difficult to verify because they require reasoning about shared state manipulated by many parallel threads. Existing verification techniques for GPU kernels achieve soundness and scalability by using a two-thread reduction and making the contents of the shared state nondeterministic each time threads synchronise at a barrier, to account for all possible thread interactions. This coarse abstraction prohibits verification of data-dependent kernels. We present barrier invariants, a novel abstraction technique which allows key properties about the shared state of a kernel to be preserved across barriers during formal reasoning. We have integrated barrier invariants with the GPUVerify tool, and present a detailed case study showing how they can be used to verify three prefix sum algorithms, allowing efficient modular verification of a stream compaction kernel, a key building block for GPU programming. This analysis goes significantly beyond what is possible using existing verification techniques for GPU kernels.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: