Specification and verification of GPGPU programs.

Stefan Blom, Marieke Huisman, M. Mihelcic

    Research output: Contribution to journalArticleAcademicpeer-review

    18 Citations (Scopus)
    13 Downloads (Pure)

    Abstract

    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
    Pages (from-to)376-388
    Number of pages13
    JournalScience of computer programming
    Volume95
    Issue numberPart 3
    DOIs
    Publication statusPublished - 1 Dec 2014

    Keywords

    • EC Grant Agreement nr.: FP7/258405
    • EC Grant Agreement nr.: FP7/2007-2013
    • EC Grant Agreement nr.: FP7/287767
    • EWI-25485
    • IR-93984
    • Permissions
    • Formal verification
    • GPU programming
    • METIS-309764
    • Separation Logic

    Cite this

    Blom, Stefan ; Huisman, Marieke ; Mihelcic, M. / Specification and verification of GPGPU programs. In: Science of computer programming. 2014 ; Vol. 95, No. Part 3. pp. 376-388.
    @article{2d4a2c40b2b34885a6e4a6fb9f8deeb1,
    title = "Specification and verification of GPGPU programs.",
    abstract = "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.",
    keywords = "EC Grant Agreement nr.: FP7/258405, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/287767, EWI-25485, IR-93984, Permissions, Formal verification, GPU programming, METIS-309764, Separation Logic",
    author = "Stefan Blom and Marieke Huisman and M. Mihelcic",
    note = "eemcs-eprint-25485",
    year = "2014",
    month = "12",
    day = "1",
    doi = "10.1016/j.scico.2014.03.013",
    language = "Undefined",
    volume = "95",
    pages = "376--388",
    journal = "Science of computer programming",
    issn = "0167-6423",
    publisher = "Elsevier",
    number = "Part 3",

    }

    Specification and verification of GPGPU programs. / Blom, Stefan; Huisman, Marieke; Mihelcic, M.

    In: Science of computer programming, Vol. 95, No. Part 3, 01.12.2014, p. 376-388.

    Research output: Contribution to journalArticleAcademicpeer-review

    TY - JOUR

    T1 - Specification and verification of GPGPU programs.

    AU - Blom, Stefan

    AU - Huisman, Marieke

    AU - Mihelcic, M.

    N1 - eemcs-eprint-25485

    PY - 2014/12/1

    Y1 - 2014/12/1

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

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

    KW - EC Grant Agreement nr.: FP7/258405

    KW - EC Grant Agreement nr.: FP7/2007-2013

    KW - EC Grant Agreement nr.: FP7/287767

    KW - EWI-25485

    KW - IR-93984

    KW - Permissions

    KW - Formal verification

    KW - GPU programming

    KW - METIS-309764

    KW - Separation Logic

    U2 - 10.1016/j.scico.2014.03.013

    DO - 10.1016/j.scico.2014.03.013

    M3 - Article

    VL - 95

    SP - 376

    EP - 388

    JO - Science of computer programming

    JF - Science of computer programming

    SN - 0167-6423

    IS - Part 3

    ER -