BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:RESCHEDULED to 20th Feb:  GPUVerify: a modular verifier for GPU ke
 rnels - Alastair Donaldson\, Imperial
DTSTART:20120220T124500Z
DTEND:20120220T140000Z
UID:TALK34817@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:GPUs are being used to accelerate general-purpose computations
  in diverse domains such as medical imaging\, computational finance\, part
 icle simulation and real-time eye tracking.  Writing GPU kernels in low-le
 vel languages like OpenCL and CUDA can yield high performance\, but is err
 or-prone.  In particular\, GPU kernels are susceptible to nondeterministic
  behaviour arising from unintentional  data races\, and undefined behaviou
 r due to threads diverging on barrier synchronisations.\n\nIn 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 the
 n describe a novel verification technique for proving correctness (with re
 spect to data races and divergence) of GPU kernels.  This method has been 
 implemented as a tool GPUVerify\, built on top of Microsoft’s Boogie ver
 ifier.  I will conclude with a demo of GPUVerify and a discussion of the l
 imitations of the tool and opportunities for future work.
LOCATION:FW26
END:VEVENT
END:VCALENDAR