Alpinist: An Annotation-Aware GPU Program Optimizer

Ömer Şakar; Mohsen Safari; Marieke Huisman; Anton Wijs

doi:10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer

Ömer Şakar, Mohsen Safari, Marieke Huisman, Anton Wijs

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

6 Citations (Scopus)

117 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems
Subtitle of host publication	28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II
Editors	Dana Fisman, Grigore Rosu
Place of Publication	Cham
Publisher	Springer
Pages	332–352
Number of pages	21
ISBN (Electronic)	978-3-030-99527-0
ISBN (Print)	978-3-030-99526-3
DOIs	https://doi.org/10.1007/978-3-030-99527-0_18
Publication status	Published - 2022

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	13244
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords

GPU
Optimization
Deductive verification
Annotation-aware
Program transformation

Access to Document

10.1007/978-3-030-99527-0_18Licence: CC BY

Şakar2022alpinistFinal published version, 550 KBLicence: CC BY

Cite this

Şakar, Ö., Safari, M., Huisman, M., & Wijs, A. (2022). Alpinist: An Annotation-Aware GPU Program Optimizer. In D. Fisman, & G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II (pp. 332–352). (Lecture Notes in Computer Science; Vol. 13244). Springer. https://doi.org/10.1007/978-3-030-99527-0_18

Şakar, Ömer ; Safari, Mohsen ; Huisman, Marieke et al. / Alpinist : An Annotation-Aware GPU Program Optimizer. Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. editor / Dana Fisman ; Grigore Rosu. Cham : Springer, 2022. pp. 332–352 (Lecture Notes in Computer Science).

@inbook{9ee3e976c396445badf3e75ac2409ffe,

title = "Alpinist: An Annotation-Aware GPU Program Optimizer",

abstract = "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.",

keywords = "GPU, Optimization, Deductive verification, Annotation-aware, Program transformation",

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

note = "Funding Information: ★ This work is supported by NWO grant 639.023.710 for the Mercedes project and by NWO TTW grant 17249 for the ChEOPS project Publisher Copyright: {\textcopyright} 2022, The Author(s).",

year = "2022",

doi = "10.1007/978-3-030-99527-0_18",

language = "English",

isbn = "978-3-030-99526-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "332–352",

editor = "Dana Fisman and Grigore Rosu",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems",

address = "Germany",

}

Şakar, Ö, Safari, M, Huisman, M & Wijs, A 2022, Alpinist: An Annotation-Aware GPU Program Optimizer. in D Fisman & G Rosu (eds), Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. Lecture Notes in Computer Science, vol. 13244, Springer, Cham, pp. 332–352. https://doi.org/10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer. / Şakar, Ömer; Safari, Mohsen; Huisman, Marieke et al.
Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. ed. / Dana Fisman; Grigore Rosu. Cham: Springer, 2022. p. 332–352 (Lecture Notes in Computer Science; Vol. 13244).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Alpinist

T2 - An Annotation-Aware GPU Program Optimizer

AU - Şakar, Ömer

AU - Safari, Mohsen

AU - Huisman, Marieke

AU - Wijs, Anton

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - GPU

KW - Optimization

KW - Deductive verification

KW - Annotation-aware

KW - Program transformation

U2 - 10.1007/978-3-030-99527-0_18

DO - 10.1007/978-3-030-99527-0_18

M3 - Chapter

SN - 978-3-030-99526-3

T3 - Lecture Notes in Computer Science

SP - 332

EP - 352

BT - Tools and Algorithms for the Construction and Analysis of Systems

A2 - Fisman, Dana

A2 - Rosu, Grigore

PB - Springer

CY - Cham

ER -

Şakar Ö, Safari M, Huisman M, Wijs A. Alpinist: An Annotation-Aware GPU Program Optimizer. In Fisman D, Rosu G, editors, Tools and Algorithms for the Construction and Analysis of Systems: 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2–7, 2022, Proceedings, Part II. Cham: Springer. 2022. p. 332–352. (Lecture Notes in Computer Science). doi: 10.1007/978-3-030-99527-0_18

Alpinist: An Annotation-Aware GPU Program Optimizer

Abstract

Publication series

Keywords

Access to Document

Fingerprint

Cite this