Specification and verification of atomic operations in GPGPU programs

A. Amighi, Saeed Darabi, Stefan Blom, Marieke Huisman

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    117 Downloads (Pure)

    Abstract

    We propose a specification and verification technique based on separation logic to reason about data race freedom and functional correctness of GPU kernels that use atomic operations as synchronisation mechanism. Our approach exploits the notion of resource invariant from Concurrent Separation Logic (CSL) to capture the behaviour of atomic operations. However, because of the different memory levels in the GPU architecture, we adapt this notion of resource invariant to these memory levels, i.e., group resource invariants capture the behaviour of atomic operations that access locations in local memory, while kernel resource invariants capture the behaviour of atomic operations that access locations in global memory. We show soundness of our approach and we provide tool support that enables us to verify kernels from standard benchmarks suites.
    Original languageUndefined
    Title of host publicationProceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)
    EditorsRadu Calinescu, Bernhard Rumpe
    Place of PublicationSwitzerland
    PublisherSpringer
    Pages69-83
    Number of pages15
    ISBN (Print)978-3-319-22968-3
    DOIs
    Publication statusPublished - Sep 2015
    Event13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom
    Duration: 7 Sep 201511 Sep 2015
    Conference number: 13
    https://www.cs.york.ac.uk/sefm2015/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing
    Volume9276
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference13th International Conference on Software Engineering and Formal Methods, SEFM 2015
    Abbreviated titleSEFM
    CountryUnited Kingdom
    CityYork
    Period7/09/1511/09/15
    Internet address

    Keywords

    • EC Grant Agreement nr.: FP7/287767
    • EWI-26147
    • METIS-312673
    • EC Grant Agreement nr.: FP7/258405
    • IR-97701
    • EC Grant Agreement nr.: FP7/2007-2013

    Cite this

    Amighi, A., Darabi, S., Blom, S., & Huisman, M. (2015). Specification and verification of atomic operations in GPGPU programs. In R. Calinescu, & B. Rumpe (Eds.), Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015) (pp. 69-83). (Lecture Notes in Computer Science; Vol. 9276). Switzerland: Springer. https://doi.org/10.1007/978-3-319-22969-0_5