Specification and Verification of Atomic Operations in GPGPU Programs

Autor: Amighi, A., Darabi, Saeed, Blom, Stefan, Huisman, Marieke, Calinescu, Radu, Rumpe, Bernhard

Publikováno v: Software Engineering and Formal Methods ISBN: 9783319229683
SEFM
Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015), 69-83
STARTPAGE=69;ENDPAGE=83;TITLE=Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)

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 r

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e4aa266fa27a07dc8c258e91c7bdc895
https://doi.org/10.1007/978-3-319-22969-0_5