high performance computing on graphics processing units: hgpu.org

Graphics processing units (GPUs) have become of major importance for highperformance computing due to their high throughput. To get the best possible performance, GPU programs are frequently optimized. However, every optimization carries the risk of introducing bugs. In this thesis, we present a framework for the theorem prover Lean to formally verify transformations of GPU programs. Our formalization generalizes the concepts of GPU programming and follows a layered approach. We define an abstract programming language that captures the essential primitives of GPU programming and construct a logic to relate two implementations of a program. The abstract language forms the basis to formalize Many-Core Levels (MCL), a GPU programming language with a focus on optimizations.