Verification of GPU Program Optimizations in Lean

Björn Fischer
Vrije Universiteit Amsterdam
Vrije Universiteit Amsterdam, 2019


   title={Verification of GPU Program Optimizations in Lean},

   author={Fischer, Bj{"o}rn},



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.
No votes yet.
Please wait...

* * *

* * *

* * *

HGPU group © 2010-2022 hgpu.org

All rights belong to the respective authors

Contact us: