RESCHEDULED to 20th Feb: GPUVerify: a modular verifier for GPU kernels

Add to your list(s) Download to your calendar using vCal

• Alastair Donaldson, Imperial
• Monday 20 February 2012, 12:45-14:00
• FW26.

If you have a question about this talk, please contact Peter Sewell.

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.

This talk is part of the Semantics Lunch (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW26
• Interested Talks
• School of Technology
• Semantics Lunch (Computer Laboratory)
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.