Formal Methods for GPGPU Programming: Is the Demand Met?

Lars van den Haak; Anton J. Wijs; Mark G.J. van den Brand; Marieke Huisman

doi:10.1007/978-3-030-63461-2_9

Formal Methods for GPGPU Programming: Is the Demand Met?

Lars van den Haak, Anton J. Wijs, Mark G.J. van den Brand, Marieke Huisman

Software Engineering and Technology

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

3 Citations (Scopus)

203 Downloads (Pure)

Abstract

Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.

Original language	English
Title of host publication	Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings
Editors	Brijesh Dongol, Elena Troubitsyna
Publisher	Springer
Pages	160-177
Number of pages	18
ISBN (Print)	9783030634605
DOIs	https://doi.org/10.1007/978-3-030-63461-2_9
Publication status	Published - 2020
Event	16th International Conference on Integrated Formal Methods, IFM 2020 - Lugano, Switzerland Duration: 16 Nov 2020 → 20 Nov 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12546 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	16th International Conference on Integrated Formal Methods, IFM 2020
Country/Territory	Switzerland
City	Lugano
Period	16/11/20 → 20/11/20

Keywords

Bugs
CUDA
Formal methods
GPGPU
GPU
OpenCL
Verification

Access to Document

10.1007/978-3-030-63461-2_9

iFM_2020_paper_55Submitted manuscript, 176 KB

Cite this

van den Haak, L., Wijs, A. J., van den Brand, M. G. J., & Huisman, M. (2020). Formal Methods for GPGPU Programming: Is the Demand Met? In B. Dongol, & E. Troubitsyna (Eds.), Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings (pp. 160-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12546 LNCS). Springer. https://doi.org/10.1007/978-3-030-63461-2_9

van den Haak, Lars ; Wijs, Anton J. ; van den Brand, Mark G.J. et al. / Formal Methods for GPGPU Programming : Is the Demand Met?. Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings. editor / Brijesh Dongol ; Elena Troubitsyna. Springer, 2020. pp. 160-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7e7d9f1f6e944f7fa094090c63a9d4ed,

title = "Formal Methods for GPGPU Programming: Is the Demand Met?",

abstract = "Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.",

keywords = "Bugs, CUDA, Formal methods, GPGPU, GPU, OpenCL, Verification",

author = "{van den Haak}, Lars and Wijs, {Anton J.} and {van den Brand}, {Mark G.J.} and Marieke Huisman",

year = "2020",

doi = "10.1007/978-3-030-63461-2_9",

language = "English",

isbn = "9783030634605",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "160--177",

editor = "Brijesh Dongol and Elena Troubitsyna",

booktitle = "Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings",

address = "Germany",

note = "16th International Conference on Integrated Formal Methods, IFM 2020 ; Conference date: 16-11-2020 Through 20-11-2020",

}

van den Haak, L , Wijs, AJ , van den Brand, MGJ & Huisman, M 2020, Formal Methods for GPGPU Programming: Is the Demand Met? in B Dongol & E Troubitsyna (eds), Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12546 LNCS, Springer, pp. 160-177, 16th International Conference on Integrated Formal Methods, IFM 2020, Lugano, Switzerland, 16/11/20. https://doi.org/10.1007/978-3-030-63461-2_9

Formal Methods for GPGPU Programming: Is the Demand Met? / van den Haak, Lars ; Wijs, Anton J.; van den Brand, Mark G.J. et al.
Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings. ed. / Brijesh Dongol; Elena Troubitsyna. Springer, 2020. p. 160-177 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12546 LNCS).

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

TY - GEN

T1 - Formal Methods for GPGPU Programming

T2 - 16th International Conference on Integrated Formal Methods, IFM 2020

AU - van den Haak, Lars

AU - Wijs, Anton J.

AU - van den Brand, Mark G.J.

AU - Huisman, Marieke

PY - 2020

Y1 - 2020

N2 - Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.

AB - Over the years, researchers have developed many formal method tools to support software development. However, hardly any studies are conducted to determine whether the actual problems developers encounter are sufficiently addressed. For the relatively young field of GPU programming, we would like to know whether the tools developed so far are sufficient, or whether some problems still need attention. To this end, we first look at what kind of problems programmers encounter in OpenCL and CUDA. We gather problems from Stack Overflow and categorise them with card sorting. We find that problems related to memory, synchronisation of threads, threads in general and performance are essential topics. Next, we look at (verification) tools in industry and research, to see how these tools addressed the problems we discovered. We think many problems are already properly addressed, but there is still a need for easy to use sound tools. Alternatively, languages or programming styles can be created, that allows for easier checking for soundness.

KW - Bugs

KW - CUDA

KW - Formal methods

KW - GPGPU

KW - GPU

KW - OpenCL

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85097445411&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-63461-2_9

DO - 10.1007/978-3-030-63461-2_9

M3 - Conference contribution

AN - SCOPUS:85097445411

SN - 9783030634605

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 160

EP - 177

BT - Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings

A2 - Dongol, Brijesh

A2 - Troubitsyna, Elena

PB - Springer

Y2 - 16 November 2020 through 20 November 2020

ER -

van den Haak L , Wijs AJ , van den Brand MGJ, Huisman M. Formal Methods for GPGPU Programming: Is the Demand Met? In Dongol B, Troubitsyna E, editors, Integrated Formal Methods - 16th International Conference, IFM 2020, Proceedings. Springer. 2020. p. 160-177. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-63461-2_9

Formal Methods for GPGPU Programming: Is the Demand Met?

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Embargoed Document

Fingerprint

Card sorting data for Formal methods for GPGPU programming: is the demand met?

Cite this

Formal Methods for GPGPU Programming: Is the Demand Met?

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Embargoed Document

Fingerprint

Datasets

Card sorting data for Formal methods for GPGPU programming: is the demand met?

Cite this