Abstract

GPUs are being used to accelerate general-purpose computations in diverse domains such as medical imaging, computational finance, particle simulation and real-time eye tracking. Writing GPU kernels in low-level languages like OpenCL and CUDA can yield high performance, but is error-prone. In particular, GPU kernels are susceptible to nondeterministic behaviour arising from unintentional data races, and undefined behaviour due to threads diverging on barrier synchronisations.

In this talk, I will give an overview of the computational model of modern GPUs, and a precise characterisation of data races and barrier divergence. I will then describe a novel verification technique for proving correctness (with respect to data races and divergence) of GPU kernels. This method has been implemented as a tool GPU Verify, built on top of Microsoft’s Boogie verifier. I will conclude with a demo of GPU Verify and a discussion of the limitations of the tool and opportunities for future work.