GPUVerify with Barrier Invariants

This webpage accompanies our OOPSLA 2013 paper.

GPUVerify is a tool for verifying race- and divergence-freedom of OpenCL and CUDA kernels. Our paper presents an extension to GPUVerify for reasoning about thread interactions using Barrier Invariants. This allows us to verify data-dependent GPU kernels.

For reproducibility, we give binaries and code for our toolchain and experimental evaluation for the Blelloch, Brent Kung and Kogge Stone prefix sum algorithms discussed in the paper.

Downloads

We recommend you download the artifact, that we prepared for the OOPSLA Artifact Evaluation Committee, which contains a VirtualBox virtual machine image with all the required dependencies installed.

NB: the Linux downloads additionally require glibc 3.4.15 and mono 3.0.4 to be installed.

• GPUVerify toolchain and experiments for Windows 64-bit.
• GPUVerify toolchain and experiments for Ubuntu Linux 64-bit.
• GPUVerify toolchain and experiments for Ubuntu Linux 32-bit.
• Just the experiments if you already have GPUVerify installed.