Software Verification Lab
Static Verification for Fearless GPU programming
Project description
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.
- We will develop bug prevention techniques that can prove the absence deadlocks/data-races and identify the root cause of concurrency errors. We wil introduce the first techniques that can analyze programs fully symbolically and techniques that mitigate false alarms.
- We will develop static performance-profiling techniques that help identify the major sources of performance degradation, uncoalesced accesses, bank conflicts, divergence, and over-synchronization. Our technique includes an amortization analysis that de- rives a symbolic expression capturing the resource usage bounds of memory transactions, synchronizations, among others.
- We will develop program repair techniques that can fix concurrency bugs without sacrificing performance.
Intellectual Merit
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:
- 2 journal articles,
- 2 conference articles,
- 2 workshop articles, and
- 4 peer-reviewed extended abstracts.
Broader Impacts
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.
Open Source Software
- Faial: a correctness and performance verifier for GPU programs
- Faial-setup: integrate Faial into GitHub CI workflows
Publications
2 Journal papers:
- Sound and partially-complete static analysis of data-races in GPU programs. Dennis Liew, Tiago Cogumbreiro, Julien Lange. PACMPL, 8(OOPSLA), 2024.