NASA Formal Methods
NASA Formal Methods
复制标题
NASA 正式方法
DOI：
10.1007/978-3-319-06200-6_18
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bardsley E
中科院分区：
文献类型：
--
作者：
Bardsley E
我们描述的设计和实现的方法，以支持在GPU内核中的数据竞争的推理，而不是标准的屏障原语用于同步的构造。在一个极端，我们考虑内核利用samewarp中线程之间的隐式粗粒度同步，这是许多架构提供的功能。在另一个极端，我们考虑通过使用原子操作来减少或避免屏障同步的内核。我们讨论了与GPUVerify（OpenCL和CUDA内核的正式验证工具）中提供线程束和原子支持相关的设计决策。我们评估这些设计决策的实际影响，使用一个大的基准集，显示，翘曲可以支持一个可扩展的方式，一个粗略的抽象足以有效的推理原子操作的最实际的用途，一个新颖的，精致的抽象捕捉一个重要的设计模式，原子操作用于计算唯一的数组索引。我们的评估揭示了公开可用的基准测试套件中两个以前未知的错误。
We describe the design and implementation of methods to support reasoning about data races in GPU kernels where constructs other than the standard barrier primitive are used for synchronization. At one extreme we consider kernels that exploit implicit, coarse-grained synchronization between threads in the samewarp, a feature provided by many architectures. At the other extreme we consider kernels that reduce or avoid barrier synchronization through the use ofatomicoperations. We discuss design decisions associated with providing support for warps and atomics in GPUVerify, a formal verification tool for OpenCL and CUDA kernels. We evaluate the practical impact of these design decisions using a large set of benchmarks, showing that warps can be supported in a scalable manner, that a coarse abstraction suffices for efficient reasoning about most practical uses of atomic operations, and that a novel, refined abstraction captures an important design pattern where atomic operations are used to compute unique array indices. Our evaluation revealed two previously unknown bugs in publicly available benchmark suites.