|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Barrier Invariants : a Shared State Abstraction for Data-dependent GPU Kernels >
If you have a question about this talk, please contact Jonathan Hayman.
Graphics processing units (GPUs) are highly parallel processors that are now commonly used in the acceleration of a wide range of computationally intensive tasks. The focus of this talk is on verifying race-freedom of data-dependent GPU kernels, whose data or control flow are dependent 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 for GPU kernels achieve soundness and scalability by using a two-thread reduction and making the contents of the shared state nondeterministic each time threads synchronise at a barrier, to account for all possible thread interactions. This abstraction is too coarse for data-dependent kernels.
This talk will present barrier invariants, a new abstraction technique that allows key properties about the shared state of a kernel to be preserved across barriers during formal reasoning. By integrating this technique into the GPU Verify tool, we have verified kernels that were previously beyond existing verification techniques for GPU kernels.
This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.
This talk is included in these lists:
Note that ex-directory lists are not shown.
Other listsFestival of Ideas: Spotlight Talks Well-being Institute Seminars
Other talksExplorations in structural and functional compensation: Examples from aphasia and dyslexia A never ending journey. Singularities, slip, substrates and structure: challenges of modelling the moving contact line problem From Sea to Shining Sea: The Future of American Education in a post-federalist era. Dr Alessandra Mortellaro - TBC (Human caspase-4/5 role in inflammasome activation) Innate Immunity: The first line of defence Bond-Orientational Order in Metallic and Colloidal Glasses Measured by Limited-Volume Electron and X-ray Diffraction