BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Barrier Invariants : a Shared State Abstraction for Data-dependent
  GPU Kernels &gt\;  - Nathan Chong\, Imperial College\, London
DTSTART:20130503T150000Z
DTEND:20130503T160000Z
UID:TALK44610@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:Graphics processing units (GPUs) are highly parallel processor
 s that are now commonly used in the acceleration of a wide range of comput
 ationally intensive tasks. The focus of this talk is on verifying race-fre
 edom of data-dependent GPU kernels\, whose data or control flow are depend
 ent on the input of the program. Kernels in this small but important class
  are difficult to verify because they require reasoning about shared state
  manipulated by many parallel threads. Existing verification techniques fo
 r GPU kernels achieve soundness and scalability by using a two-thread redu
 ction and making the contents of the shared state nondeterministic each ti
 me threads synchronise at a barrier\, to account for all possible thread i
 nteractions. This abstraction is too coarse for data-dependent kernels.\n\
 nThis talk will present barrier invariants\, a new abstraction technique t
 hat allows key properties about the shared state of a kernel to be preserv
 ed across barriers during formal reasoning. By integrating this technique 
 into the GPUVerify tool\, we have verified kernels that were previously be
 yond existing verification techniques for GPU kernels.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR