Static Verification for Fearless GPU programming
Programming Graphical Processing Units (GPUs) is an art currently reserved to a select few experts, as unlocking the full potential of these devices requires mastering an intricate hardware architecture and execution model. Scientists and domain experts need to adapt their algorithms to a programming model where simply changing the order in which data is accessed can have a 10× overhead, and off-by-one errors can silently corrupt data. The aim of this project is to help achieve correct and efficient GPU programming, with a static framework that explains sources of performance degradation and repairs concurrency bugs without loss of performance.
This project consists of three tasks.
Our project advances the state of the art in static verification for GPUs and other accelerator architectures, both in terms of correctness and performance analysis. Existing solutions suffer from a high rate of false alarms, cannot handle large programs, or are unsound. Most importantly, existing approaches either address performance or safety, but not both; our project addresses both complementarily.
A key aspect of this project is an underlying static verification infrastructure, a collection of analysis backed by theoretical results, that enable novel and efficient analysis and tools. Such verification infrastructure is built around a novel and general intermediate representation based on behavioral type theory. Our project expands our formal understanding of GPU programming models, by introducing safety properties, semantics preserving transformations, and behavioral equivalences, fully mechanized using a proof assistant.
Research outputs. This research project produced 10 articles:
This project makes GPU programming more accessible to scientists and domain experts, by furthering their understanding of parallel programming and hardware architectures. An outcome of this project is improved developer productivity and software sustainability, as our project aids in writing correct and highly efficient GPU programs without sacrificing either. We expect an interest from industry (e.g., autonomous mobility, artificial intelligence applications) as well as from academy (e.g., energy national laboratories). Our research lowers the barrier to entry of GPU programming, so we expect to widen the suitability of GPUs to more fields. The tools that result from this project can empower students to understand bugs in their code autonomously, leading to a more focused pedagogical experience between the instructor and the student.
2 Journal papers: