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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.356.4 | bibtex | |
Comments and questions to:
![]() |
For website issues:
![]() |