COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > 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 kernelsAdd 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. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsCU Pakistan Society Switch Off Week CU Nanotechnology SocietyOther talksThe role of myosin VI in connexin 43 gap junction accretion Reconciling centennial-scale climate variation during the last millennium in reconstructions and simulations Huntington´s disease and autophagy - insights from human and mouse model systems Speak white, speak black, speak American Understanding model diversity in CMIP5 projections of westerly winds over the Southern Ocean Cyclic Peptides: Building Blocks for Supramolecular Designs Disease Migration Cambridge - Corporate Finance Theory Symposium September 2017 - Day 1 To be confirmed Protein Folding, Evolution and Interactions Symposium Mothers & Daughters: a psychoanalytical perspective |