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