Specification and verification of atomic operations in GPGPU programs

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

  • 4 Citations

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 International Publishing
Pages69-83
Number of pages15
ISBN (Print)978-3-319-22968-3
DOIs
StatePublished - Sep 2015
Event13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom

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

Fingerprint

Synchronization
Specifications

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 International Publishing. DOI: 10.1007/978-3-319-22969-0_5

Amighi, A.; Darabi, Saeed; Blom, Stefan; Huisman, Marieke / Specification and verification of atomic operations in GPGPU programs.

Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015). ed. / Radu Calinescu; Bernhard Rumpe. Switzerland : Springer International Publishing, 2015. p. 69-83 (Lecture Notes in Computer Science; Vol. 9276).

Research output: Scientific - peer-reviewConference contribution

@inbook{92927e6ff165433d93cd9dfeca3201fc,
title = "Specification and verification of atomic operations in GPGPU programs",
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.",
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",
author = "A. Amighi and Saeed Darabi and Stefan Blom and Marieke Huisman",
note = "eemcs-eprint-26147",
year = "2015",
month = "9",
doi = "10.1007/978-3-319-22969-0_5",
isbn = "978-3-319-22968-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
pages = "69--83",
editor = "Radu Calinescu and Bernhard Rumpe",
booktitle = "Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)",

}

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). Lecture Notes in Computer Science, vol. 9276, Springer International Publishing, Switzerland, pp. 69-83, 13th International Conference on Software Engineering and Formal Methods, SEFM 2015, York, United Kingdom, 7-11 September. DOI: 10.1007/978-3-319-22969-0_5

Specification and verification of atomic operations in GPGPU programs. / Amighi, A.; Darabi, Saeed; Blom, Stefan; Huisman, Marieke.

Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015). ed. / Radu Calinescu; Bernhard Rumpe. Switzerland : Springer International Publishing, 2015. p. 69-83 (Lecture Notes in Computer Science; Vol. 9276).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Specification and verification of atomic operations in GPGPU programs

AU - Amighi,A.

AU - Darabi,Saeed

AU - Blom,Stefan

AU - Huisman,Marieke

N1 - eemcs-eprint-26147

PY - 2015/9

Y1 - 2015/9

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

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

KW - EC Grant Agreement nr.: FP7/287767

KW - EWI-26147

KW - METIS-312673

KW - EC Grant Agreement nr.: FP7/258405

KW - IR-97701

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

U2 - 10.1007/978-3-319-22969-0_5

DO - 10.1007/978-3-319-22969-0_5

M3 - Conference contribution

SN - 978-3-319-22968-3

T3 - Lecture Notes in Computer Science

SP - 69

EP - 83

BT - Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)

PB - Springer International Publishing

ER -

Amighi A, Darabi S, Blom S, Huisman M. Specification and verification of atomic operations in GPGPU programs. In Calinescu R, Rumpe B, editors, Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015). Switzerland: Springer International Publishing. 2015. p. 69-83. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-22969-0_5