Note

The URL in the ESOP 2013 submission refers to ESOP 2012 - apologies for this error!

About

GPUVerify is a tool for verifying race- and divergence-freedom of OpenCL and CUDA kernels. Our ESOP 2013 submission presents a lock-step operational semantics for GPU kernels that are described as arbitrary reducible control flow graphs, and describes a new front-end for GPUVerify which uses these semantics to directly analyse kernels at the LLVM bitcode level. In the paper we experimentally compare GPUVerify with this new front-end (GPUVerify II) with the original version of GPUVerify which was restricted to structured kernels (GPUVerify I). To allow reviewers to reproduce our results, this website provides both versions of the tool, together with all our our publicly available evaluation benchmarks. We cannot provide the commercial benchmarks from Rightware, to which we have been given access under an academic license.

Getting the tools and benchmarks

We provide our tools and benchmarks for installation on a Windows 7 64-bit platform.

Please download the following archive which contains both tool chains and the benchmarks. Navigate to the "structured" and "unstructured" directories respectively and look at the README.txt files for instructions on how to run each tool chain on the benchmarks. You will also need to download and install the Z3 SMT solver; the instructions in the archive explain how to do this.

• GPUVerify I and GPUVerify II toolchains and benchmarks (self-contained)

Full version of the paper

Please download the following pdf to obtain a version of the paper which includes all proofs.

• Full version of our ESOP 2013 submission

Contact

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