What is GPUVerify?
GPUVerify is a tool for formal analysis of GPU kernels written in OpenCL and CUDA
The tool can prove that kernels are free from certain types of defect, including data races:
1 __kernel void add_neighbour(__local int *A, int offset) {
2 int tid = get_local_id(0);
3 int temp = A[tid + offset];
4 barrier(CLK_LOCAL_MEM_FENCE);
5 A[tid] += temp;
6 }
gpuverify --local_size=64 --num_groups=128 add-neighbour-correct.cl
GPUVerify kernel analyser finished with 1 verified, 0 errors
Verified: add-neighbour-correct.cl
- no data races within work groups
- no data races between work groups
- no barrier divergence
- no assertion failures
(but absolutely no warranty provided)
GPUVerify can also find bugs, detecting possible defects in kernels:
1 __kernel void add_neighbour(__local int *A, int offset) {
2 int tid = get_local_id(0);
3 A[tid] += A[tid + offset];
4 }
gpuverify --local_size=64 --num_groups=128 add-neighbour-buggy.cl
add-neighbour-buggy.cl: error: possible read-write race on ((char*)A)[32]:
add-neighbour-buggy.cl:3:3: write by thread 8 group 0
A[tid] += A[tid + offset];
add-neighbour-buggy.cl:3:3: read by thread 4 group 0
A[tid] += A[tid + offset];
Want to quickly try out the GPUVerify tool?
Head over to our online demo page to try it out!
Browse the rest of the web site to find out how to use GPUVerify, how it works, how to download the tool, and how to contribute to its development.
Developers
GPUVerify was originally designed by Alastair Donaldson (Imperial College London) and Shaz
Qadeer (RiSE
group at Microsoft Research) when Alastair visited Shaz at
Microsoft during August and September 2011.
Since then, development of GPUVerify has continued as part of the
CARP project, and the
technique and tool have been additionally contributed to by:
