Specification and Verification of GPGPU programs using Permission-based Separation logic

Marieke Huisman, M. Mihelcic

Research output: Book/ReportReportProfessional

28 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 our ideas how to verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verification approach is modular, based on permission-based separation logic. We first present the main ingredients of our logic, and then illustrate its use on several example kernels. We show in particular how the logic is used to prove data-race- freedom and functional correctness of GPU applications.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages8
Publication statusPublished - Mar 2013

Publication series

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

Keywords

  • EWI-23278
  • METIS-297616
  • IR-86119
  • EC Grant Agreement nr.: FP7/287767
  • EC Grant Agreement nr.: FP7/2007-2013

Cite this

Huisman, M., & Mihelcic, M. (2013). Specification and Verification of GPGPU programs using Permission-based Separation logic. (CTIT Technical Report Series; No. TR-CTIT-13-12). Enschede: Centre for Telematics and Information Technology (CTIT).
Huisman, Marieke ; Mihelcic, M. / Specification and Verification of GPGPU programs using Permission-based Separation logic. Enschede : Centre for Telematics and Information Technology (CTIT), 2013. 8 p. (CTIT Technical Report Series; TR-CTIT-13-12).
@book{4fa22f657b134a27a2f1c5f57520e8c5,
title = "Specification and Verification of GPGPU programs using Permission-based Separation logic",
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 our ideas how to verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verification approach is modular, based on permission-based separation logic. We first present the main ingredients of our logic, and then illustrate its use on several example kernels. We show in particular how the logic is used to prove data-race- freedom and functional correctness of GPU applications.",
keywords = "EWI-23278, METIS-297616, IR-86119, EC Grant Agreement nr.: FP7/287767, EC Grant Agreement nr.: FP7/2007-2013",
author = "Marieke Huisman and M. Mihelcic",
note = "This work was presented at the 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), March 23, 2013, Rome, Italy.",
year = "2013",
month = "3",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-13-12",
address = "Netherlands",

}

Huisman, M & Mihelcic, M 2013, Specification and Verification of GPGPU programs using Permission-based Separation logic. CTIT Technical Report Series, no. TR-CTIT-13-12, Centre for Telematics and Information Technology (CTIT), Enschede.

Specification and Verification of GPGPU programs using Permission-based Separation logic. / Huisman, Marieke; Mihelcic, M.

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

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Specification and Verification of GPGPU programs using Permission-based Separation logic

AU - Huisman, Marieke

AU - Mihelcic, M.

N1 - This work was presented at the 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), March 23, 2013, Rome, Italy.

PY - 2013/3

Y1 - 2013/3

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 our ideas how to verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verification approach is modular, based on permission-based separation logic. We first present the main ingredients of our logic, and then illustrate its use on several example kernels. We show in particular how the logic is used to prove data-race- freedom and functional correctness of GPU applications.

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 our ideas how to verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verification approach is modular, based on permission-based separation logic. We first present the main ingredients of our logic, and then illustrate its use on several example kernels. We show in particular how the logic is used to prove data-race- freedom and functional correctness of GPU applications.

KW - EWI-23278

KW - METIS-297616

KW - IR-86119

KW - EC Grant Agreement nr.: FP7/287767

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

M3 - Report

T3 - CTIT Technical Report Series

BT - Specification and Verification of GPGPU programs using Permission-based Separation logic

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Huisman M, Mihelcic M. Specification and Verification of GPGPU programs using Permission-based Separation logic. Enschede: Centre for Telematics and Information Technology (CTIT), 2013. 8 p. (CTIT Technical Report Series; TR-CTIT-13-12).