Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer)

Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer) submitted to TACAS '22 conference. For a full description on how to use the artifact, please see the README.txt file. The artifact contains the Alpinist tool, all its dependencies and documentation for the VerCors tool.<br><br>Abstract of the paper:<br>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.<br>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.

提交至TACAS '22会议的论文《Alpinist：感知注解的GPU程序优化器》配套工件。关于该工件的完整使用说明，请参阅README.txt文件。

本工件包含Alpinist工具、其所有依赖项，以及VerCors工具的相关文档。

论文摘要：
GPU程序在工业界应用广泛。为获得最优性能，典型的开发流程需在代码编译前，通过手动或半自动方式应用各类优化手段。为避免引入错误，我们可以为GPU程序添加（前置条件与后置条件风格的）注解以捕获其功能属性。然而，在优化GPU程序的同时保持这些注解的正确性，既耗时费力又极易出错。

本文提出了Alpinist——一款感知注解的GPU程序优化器。其不仅支持常用的GPU优化操作，在转换代码的同时，还能同步更新对应注解。本文结合VerCors程序验证器对Alpinist进行了评估：通过自动优化一批已验证的程序，并对优化后的程序进行重新验证。