Provable GPU Data-Races in Static Race Detection

TL;DR

This paper extends the Faial tool-chain's theoretical framework to accurately identify true data-race alarms in CUDA kernels by using memory access protocols and introduces a core calculus called BabyCUDA with a behavioral type system.

Contribution

It develops a formal theory for soundly proving data-race freedom in CUDA programs and extends it to distinguish true alarms, enhancing static race detection accuracy.

Findings

Faial can reliably identify true data-race alarms.

Introduction of BabyCUDA calculus and behavioral type system.

Extension of MAP theory to practical CUDA kernels.

Abstract

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.