Provable GPU Data-Races in Static Race Detection

Dennis Liew
(University of Massachusetts Boston, Boston, USA)
Tiago Cogumbreiro
(University of Massachusetts Boston, Boston, USA)
Julien Lange
(Royal Holloway, University of London, Egham, UK)

We extend the theory behind the Faial tool-chain, which can soundly prove that CUDA programs (aka, kernels) are data-race free using specialized behavioral types called memory access protocols (MAPs). In this paper we extend the theory of MAPs to characterize kernels for which alarms can be identified as true alarms. We introduce a core calculus for CUDA, which we named BabyCUDA, and a behavioral type system for it. We show that if a BabyCUDA program can be assigned a MAP, then any alarm raised by Faial for this program is a true alarm.

In Marco Carbone and Rumyana Neykova: Proceedings of the 13th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2022), Munich, Germany, 3rd April 2022, Electronic Proceedings in Theoretical Computer Science 356, pp. 36–45.
Published: 24th March 2022.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: