ALPINIST: An Annotation-Aware GPU Program Optimizer

Ömer Sakar, Mohsen Safari, Marieke Huisman, Anton Wijs
Formal Methods and Tools, University of Twente, Enschede, The Netherlands
Lecture Notes in Computer Science, vol 13244. Springer, TACAS, 2022


   title={ALPINIST: An Annotation-Aware GPU Program Optimizer},

   author={c{S}}akar, {"O}mer and Safari, Mohsen and Huisman, Marieke and Wijs, Anton},

   booktitle={International Conference on Tools and Algorithms for the Construction and Analysis of Systems},





GPU programs are widely used in industry. To obtain the best performance, a typical development process involves the manual or semi-automatic application of optimizations prior to compiling the code. To avoid the introduction of errors, we can augment GPU programs with (pre- and postcondition-style) annotations to capture functional properties. However, keeping these annotations correct when optimizing GPU programs is labor-intensive and error-prone. This paper introduces Alpinist, an annotation-aware GPU program optimizer. It applies frequently-used GPU optimizations, but besides transforming code, it also transforms the annotations. We evaluate Alpinist, in combination with the VerCors program verifier, to automatically optimize a collection of verified programs and reverify them.
No votes yet.
Please wait...

Recent source codes

* * *

* * *

HGPU group © 2010-2024 hgpu.org

All rights belong to the respective authors

Contact us: