University of Cambridge > > Semantics Lunch (Computer Laboratory) > RESCHEDULED to 20th Feb: GPUVerify: a modular verifier for GPU kernels

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity