Static Verification for Fearless GPU programming

University Of Massachusetts Boston, Dorchester MA

Investigators

Abstract

Programming Graphics 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× performance overhead, and off-by-one errors can silently corrupt their data. The intent of this project is to develop an infrastructure of complementary code analysis techniques that include bug prevention, performance profiling, and bug repairing. The project's novelties are in developing a holistic understanding of performance and safety bugs, which considers the interactions between various classes of bugs. The project's impacts are on making GPU programming more accessible, by providing tools to all programmers that simplify understanding parallel programming and hardware architectures, thus enabling algorithm correctness and more in depth performance analysis. An outcome of this project is improved developer productivity and software sustainability, as the project aids in writing correct and highly efficient GPU programs without sacrificing either objectives. There is an expectation of interest from industry (e.g., autonomous mobility, artificial intelligence applications) as well as from academia and national laboratories. The research lowers the barrier to entry of GPU programming, so it is expected 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. This project advances the state of the art of static verification for GPUs and other accelerator architectures, both in terms of correctness and performance analysis. Static verification aims to assess the requirements of software without executing the program. Existing solutions suffer from a high rate of false alarms, cannot handle large codes, or are unsound. Most importantly, existing approaches either address performance or safety, but not both at once. A key aspect of this project is an underlying static verification infrastructure, a collection of analysis backed by theoretical results, that enables novel and efficient tools that better our understanding of existing software. Such verification infrastructure is built around a novel and general intermediate representation based on behavioral type theory, which codifies, structures, and enforces the meaning of parallel programs. The project expands our formal understanding of GPU programming models, by introducing safety properties, semantics preserving transformations, and behavioral equivalences, all fully mechanized using a proof assistant. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.