Other: Guest presentation: GPUVerify: a Verifier for GPU Kernels

When: Nov. 15, 2012, 14:00-15:00

Where: Zi 3126

Who: Alastair Donaldson

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