I will describe GPUVerify, a collaboration between Imperial College London and Microsoft Research Redmond on the design and implementation of a technique and tool for analysing concurrent software written to run on graphics processing units (GPUs). GPUVerify checks the kernel functions that execute across cores of a GPU architecture and attempts to detect, or verify absence of, two kinds of defects: data races and barrier divergence. To scale to large numbers of threads, GPUVerify exploits the relatively simple nature of the GPU programming model in a way that allows verification of massively parallel kernels to be reduced to a sequential program verification task. In this talk I will describe the defects that GPUVerify checks for, present some details of the verification technique, and discuss open problems in this area.

This is joint work with:

• Adam Betts, Nathan Chong, Peter Collingbourne*, Jeroen Ketema, Paul Thomson (Imperial)

• Shaz Qadeer (Microsoft)

  (*) now at Google