ALPINIST: An Annotation-Aware GPU Program Optimizer
Formal Methods and Tools, University of Twente, Enschede, The Netherlands
Lecture Notes in Computer Science, vol 13244. Springer, TACAS, 2022
@inproceedings{csakar2022annotation,
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},
pages={332–352},
year={2022},
organization={Springer}
}
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.
April 10, 2022 by hgpu
