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
- Checkout Boogie from the Mercurial repository here. Ensure that you do not checkout to a network drive otherwise there might be issues with DLLs.
- Download Z3 from here and install it to its default location.
- Load the GPUVerify (Visual Studio) solution found in <path\to\Boogie>\Source and build (Debug).
- 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.
-
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]