论文标题
静态竞赛检测中的可证明的GPU数据率
Provable GPU Data-Races in Static Race Detection
论文作者
论文摘要
我们扩展了FAIAL工具链背后的理论，该链可以很好地证明CUDA程序（又称内核）使用称为内存访问协议（MAP）的专业行为类型免费数据率。 在本文中，我们将地图理论扩展到表征内核，以确定警报为真实警报。 我们引入了CUDA的核心演算，我们将其命名为babycuda，并为其命名为行为类型系统。我们表明，如果可以为BabyCuda程序分配一个地图，那么Faial为此程序提出的任何警报都是一个真正的警报。
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.
