Specification and Verification of GPGPU Programs using Permission-Based Separation Logic

Marieke Huisman, Matej Mihelcic

Research output: Contribution to conferencePaperAcademicpeer-review

23 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 specied 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 verication approach is modular, based on permission-based separation logic. We rst 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 languageEnglish
Number of pages8
Publication statusPublished - 2013
Event8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013) - Rome, Italy
Duration: 23 Mar 201323 Mar 2013

Workshop

Workshop8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013)
Abbreviated titleBYTECODE 2013
CountryItaly
CityRome
Period23/03/1323/03/13

Fingerprint

Specifications
Computer programming languages
Energy efficiency
Graphics processing unit

Cite this

Huisman, M., & Mihelcic, M. (2013). Specification and Verification of GPGPU Programs using Permission-Based Separation Logic. Paper presented at 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), Rome, Italy.
Huisman, Marieke ; Mihelcic, Matej. / Specification and Verification of GPGPU Programs using Permission-Based Separation Logic. Paper presented at 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), Rome, Italy.8 p.
@conference{619bf8c0f8424c5aaf87039f70a85fb2,
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 specied and proven correct formally. This paper presents our ideas howto verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verication approach is modular, based on permission-based separation logic. We rst 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.",
author = "Marieke Huisman and Matej Mihelcic",
year = "2013",
language = "English",
note = "8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), BYTECODE 2013 ; Conference date: 23-03-2013 Through 23-03-2013",

}

Huisman, M & Mihelcic, M 2013, 'Specification and Verification of GPGPU Programs using Permission-Based Separation Logic' Paper presented at 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), Rome, Italy, 23/03/13 - 23/03/13, .

Specification and Verification of GPGPU Programs using Permission-Based Separation Logic. / Huisman, Marieke ; Mihelcic, Matej.

2013. Paper presented at 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), Rome, Italy.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Specification and Verification of GPGPU Programs using Permission-Based Separation Logic

AU - Huisman, Marieke

AU - Mihelcic, Matej

PY - 2013

Y1 - 2013

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 specied and proven correct formally. This paper presents our ideas howto verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verication approach is modular, based on permission-based separation logic. We rst 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 specied and proven correct formally. This paper presents our ideas howto verify GPU programs written in OpenCL, a platform-independent low-level programming language. Our verication approach is modular, based on permission-based separation logic. We rst 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.

M3 - Paper

ER -

Huisman M, Mihelcic M. Specification and Verification of GPGPU Programs using Permission-Based Separation Logic. 2013. Paper presented at 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2013), Rome, Italy.