Specification and verification of GPGPU programs

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 forma...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2014-12, Vol.95, p.376-388
Main Authors: Blom, Stefan, Huisman, Marieke, Mihelčić, Matej
Format: Article
Language:English
Subjects:
Formal verification
GPU programming
Permissions
Separation logic
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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. •Specification method for OpenCL kernels.•Verification method for OpenCL kernel specifications.•Implementation of tool for verification of OpenCL kernels.•Illustrated with examples.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2014.03.013