Source-to-Source Transformations for GPU Code Generation

GPUs have become essential in modern high performance computing, but programming them correctly remains a significant challenge. This difficulty arises from subtle concurrency bugs that result from the explicit management of synchronization primitives and data movement across intricate hierarchies of memory and parallel threads. At the same time, the ability to control these aspects explicitly is at the core of the performance gains granted by GPUs. These challenges have motivated interest in safe GPU programming: tools and languages that can prevent or detect such bugs statically. However, existing approaches make tradeoffs in three dimensions: the strength of their guarantees, the degree of low-level control they allow, and the amount of additional effort required for the user to achieve these safety guarantees.

This thesis presents OptiGPU, a system for GPU programming with strong safety guarantees, including data race freedom, deadlock freedom, and full functional correctness, that aims to minimize the tradeoffs in the other two dimensions as compared to previous approaches. OptiGPU applies the concept of proof-preserving compilation to GPU programming, allowing verification of low-level, optimized GPU programs through refinement of simple, verified CPU programs. In this way, an OptiGPU user avoids the substantial proof burden required to directly verify complex optimized GPU programs, and instead directs this refinement with source-to-source transformations that automatically preserve proofs. OptiGPU is implemented as a set of extensions to OptiTrust, an existing framework for proof-preserving compilation on CPUs. OptiGPU models essential features of GPU programming, including kernel launches, shared memory, and barrier synchronization, and produces both device and host-side code. We evaluate OptiGPU on two case studies, matrix transposition and tree-based parallel reduction, showing that it can derive CUDA code matching techniques found in handwritten references.