About

GPUVerify is a tool for verifying race- and divergence-freedom of GPU kernels that are written in mainstream kernel programming languages such as OpenCL and CUDA. The approach is founded on a novel formal operational semantics for GPU programming termed synchronous, delayed visibility (SDV) semantics. More technical details will be provided in the near future.

Toolchain installation

We have developed a suite of tools to verify GPU kernels using CLANG/LLVM, Boogie, and the Z3 theorem prover. We have only tested our toolchain on Windows 7 64-bit.

The best option is to download the self-contained package containing the GPUVerify toolchain, the benchmark kernels and instructions:

See the included README.txt for instructions.

Alternatively, follow the steps below to manually get the individual components.

Toolchain components

  1. Checkout Boogie from the Mercurial repository here. Ensure that you do not checkout to a network drive otherwise there might be issues with DLLs.
  2. Download Z3 from here and install it to its default location.
  3. Load the GPUVerify (Visual Studio) solution found in <path\to\Boogie>\Source and build (Debug).
  4. Download our frontend and our automated testing tool and place them into a bin directory. Also download essential header files needed by these tools and place them above the directory level of any kernels you want to verify.
  5. Set your environment variable PATH to include:
    • <path\to\Boogie>\Binaries
    • <path\to\Boogie>\Source\GPUVerify\bin\Debug
    • The Z3 bin directory
    • The directory where our frontend and testing tool reside

To test the installation open a Windows command prompt and run:

  • GPUVerify.exe

You should see:

  • *** Error: No input files were specified.

Benchmarks

The open source benchmarks used in our experimental evaluations are found in a zip archive here.

In the zip archive, we provide a Windows command script run_benchmarks.cmd to automatically run our toolchain end to end on all unpacked benchmarks.

Contact

Email:XXXalastair.donaldsonXXX@imperial.ac.uk[remove the XXX]