Specification and verification of GPGPU programs

Stefan Blom, Marieke Huisman, M. Mihelcic

Research output: Book/ReportReportProfessional

34 Downloads (Pure)

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
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages18
Publication statusPublished - 8 Nov 2013

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-13-21
ISSN (Print)1381-3625

Keywords

  • Formal verification
  • GPU programming
  • IR-87747
  • METIS-300133
  • CR-D.2.4
  • EWI-23922
  • EC Grant Agreement nr.: FP7/2007-2013
  • EC Grant Agreement nr.: FP7/287767
  • EC Grant Agreement nr.: FP7/258405
  • Permissions
  • Separation Logic

Cite this

Blom, S., Huisman, M., & Mihelcic, M. (2013). Specification and verification of GPGPU programs. (CTIT Technical Report Series; No. TR-CTIT-13-21). Enschede: Centre for Telematics and Information Technology (CTIT).
Blom, Stefan ; Huisman, Marieke ; Mihelcic, M. / Specification and verification of GPGPU programs. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; TR-CTIT-13-21).
@book{d2553660c57f400e9b1363e5a95d5d41,
title = "Specification and verification of GPGPU programs",
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 = "Formal verification, GPU programming, IR-87747, METIS-300133, CR-D.2.4, EWI-23922, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/287767, EC Grant Agreement nr.: FP7/258405, Permissions, Separation Logic",
author = "Stefan Blom and Marieke Huisman and M. Mihelcic",
note = "eemcs-eprint-23922",
year = "2013",
month = "11",
day = "8",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-21",
address = "Netherlands",

}

Blom, S, Huisman, M & Mihelcic, M 2013, Specification and verification of GPGPU programs. CTIT Technical Report Series, no. TR-CTIT-13-21, Centre for Telematics and Information Technology (CTIT), Enschede.

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; No. TR-CTIT-13-21).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Specification and verification of GPGPU programs

AU - Blom, Stefan

AU - Huisman, Marieke

AU - Mihelcic, M.

N1 - eemcs-eprint-23922

PY - 2013/11/8

Y1 - 2013/11/8

N2 - 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 - 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 - Formal verification

KW - GPU programming

KW - IR-87747

KW - METIS-300133

KW - CR-D.2.4

KW - EWI-23922

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

KW - EC Grant Agreement nr.: FP7/287767

KW - EC Grant Agreement nr.: FP7/258405

KW - Permissions

KW - Separation Logic

M3 - Report

T3 - CTIT Technical Report Series

BT - Specification and verification of GPGPU programs

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Blom S, Huisman M, Mihelcic M. Specification and verification of GPGPU programs. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 18 p. (CTIT Technical Report Series; TR-CTIT-13-21).