Specification and verification of GPGPU programs

Stefan Blom, Marieke Huisman, M. Mihelcic

    Research output: Book/ReportReportProfessional

    42 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 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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages18
    Publication statusPublished - 8 Nov 2013

    Publication series

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

    Keywords

    • Formal verification
    • GPU programming
    • IR-87747
    • METIS-300133
    • CR-D.2.4
    • EWI-23922
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/287767
    • EC Grant Agreement nr.: FP7/258405
    • Permissions
    • Separation Logic

    Cite this

    Blom, S., Huisman, M., & Mihelcic, M. (2013). Specification and verification of GPGPU programs. (CTIT Technical Report Series; No. TR-CTIT-13-21). Enschede: Centre for Telematics and Information Technology (CTIT).