GPUVerify with Barrier Invariants

GPUVerify is a tool for verifying race- and divergence-freedom of OpenCL and CUDA kernels. Our CAV 2013 submission presents an extension to GPUVerify for reasoning about Barrier Invariants.

In the paper we present a detailed case-study of a stream-compaction kernel that uses an exclusive prefix sum algorithm. We describe three experiments inside the paper: (i) verification of data race-freedom of the stream-compaction kernel using the monotonic specification of the prefix sum; (ii) verification of the monotonic specification of the Blelloch prefix sum using concrete binary operators (add, max, bitwise-or); (iii) verification of the monotonic specification of the Blelloch prefix sum using an abstract binary operator. For reproducibility, we give binaries and code for our toolchain and experiments.

Downloads

• GPUVerify toolchain and experiments (self-contained) (Windows 7 64-bit)