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

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