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

Marieke Huisman, Matej Mihelcic

    Research output: Contribution to conferencePaper

    48 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 Dive into the research topics of 'Specification and Verification of GPGPU Programs using Permission-Based Separation Logic'. Together they form a unique fingerprint.

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