Specification and verification of GPGPU programs.

Stefan Blom, Marieke Huisman, M. Mihelcic

Research output: Contribution to journalArticleAcademicpeer-review

18 Citations (Scopus)
12 Downloads (Pure)

Abstract

Abstract Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform-independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.
Original languageUndefined
Pages (from-to)376-388
Number of pages13
JournalScience of computer programming
Volume95
Issue numberPart 3
DOIs
Publication statusPublished - 1 Dec 2014

Keywords

  • EC Grant Agreement nr.: FP7/258405
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/287767
  • EWI-25485
  • IR-93984
  • Permissions
  • Formal verification
  • GPU programming
  • METIS-309764
  • Separation Logic

Cite this

Blom, Stefan ; Huisman, Marieke ; Mihelcic, M. / Specification and verification of GPGPU programs. In: Science of computer programming. 2014 ; Vol. 95, No. Part 3. pp. 376-388.
@article{2d4a2c40b2b34885a6e4a6fb9f8deeb1,
title = "Specification and verification of GPGPU programs.",
abstract = "Abstract Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform-independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.",
keywords = "EC Grant Agreement nr.: FP7/258405, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/287767, EWI-25485, IR-93984, Permissions, Formal verification, GPU programming, METIS-309764, Separation Logic",
author = "Stefan Blom and Marieke Huisman and M. Mihelcic",
note = "eemcs-eprint-25485",
year = "2014",
month = "12",
day = "1",
doi = "10.1016/j.scico.2014.03.013",
language = "Undefined",
volume = "95",
pages = "376--388",
journal = "Science of computer programming",
issn = "0167-6423",
publisher = "Elsevier",
number = "Part 3",

}

Specification and verification of GPGPU programs. / Blom, Stefan; Huisman, Marieke; Mihelcic, M.

In: Science of computer programming, Vol. 95, No. Part 3, 01.12.2014, p. 376-388.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Specification and verification of GPGPU programs.

AU - Blom, Stefan

AU - Huisman, Marieke

AU - Mihelcic, M.

N1 - eemcs-eprint-25485

PY - 2014/12/1

Y1 - 2014/12/1

N2 - Abstract Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform-independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.

AB - Abstract Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform-independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.

KW - EC Grant Agreement nr.: FP7/258405

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/287767

KW - EWI-25485

KW - IR-93984

KW - Permissions

KW - Formal verification

KW - GPU programming

KW - METIS-309764

KW - Separation Logic

U2 - 10.1016/j.scico.2014.03.013

DO - 10.1016/j.scico.2014.03.013

M3 - Article

VL - 95

SP - 376

EP - 388

JO - Science of computer programming

JF - Science of computer programming

SN - 0167-6423

IS - Part 3

ER -