Alastair F. Donaldson (Imperial College, London), GPUVerify: a Verifier for GPU Kernels



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: