Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer)
doi:10.4121/16938556.v2
The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future.
For a link that will always point to the latest version, please use
doi: 10.4121/16938556
doi: 10.4121/16938556
Datacite citation style:
Şakar, Ömer; Safari, Mohsen; Huisman, Marieke; Wijs, Anton (2021): Artifact for paper (Alpinist: an Annotation-Aware GPU Program Optimizer). Version 2. 4TU.ResearchData. software. https://doi.org/10.4121/16938556.v2
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software
choose version:
version 2 - 2021-11-26 (latest)
version 1 - 2021-11-22
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.
Abstract of the paper:
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.
Abstract of the paper:
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.
history
- 2021-11-22 first online
- 2021-11-26 published, posted
publisher
4TU.ResearchData
funding
- ChEOPS (NWO TTW grant 17249)
- Mercedes: Maximal Reliability of Concurrent and Distributed Software (grant code 639.023.710) [more info...] Dutch Research Council
organizations
University of Twente, Faculty of Electrical Engineering, Mathematics and Computer ScienceEindhoven University of Technology, Department of Mathematics and Computer Science
DATA
files (1)
- 201,798,653 bytesMD5:
a373484eca53ff9cdff406b6ab1be0ef
TACAS-artifact-submission-109.zip -
download all files (zip)
201,798,653 bytes unzipped