The Design and Implementation of a Verification Technique for GPU Kernels
The Design and Implementation of a Verification Technique for GPU Kernels
复制标题
GPU内核验证技术的设计与实现
DOI：
10.1145/2743017
复制
发表时间：
2015
影响因子：
1.3
通讯作者：
Betts A
中科院分区：
文献类型：
--
作者：
Betts A
我们提出了一种技术的GPU内核的正式验证，解决两类正确性属性：数据竞赛和障碍发散。我们的方法是建立在一个新的正式的操作语义的GPU内核termedsynchronous，延迟可见性（SDV）的语义，它捕获执行的GPU内核的多组线程。SDV语义为屏障发散以及组间和组内数据竞争提供了操作定义。我们建立的语义开发一种方法，用于减少验证大规模并行GPU内核的验证顺序程序的任务。这完全避免了对线程交错进行推理的需要，并且允许利用现有的顺序程序验证技术。我们描述了一个有效的数据竞争检测编码，并提出了一种方法，自动推断的循环不变的验证所需的。我们已经实现了这些技术作为一个实用的验证工具，GPUVerify，可以直接应用于OpenCL和CUDA源代码。我们评估GPUVerify相对于一组162内核从公共和商业来源。我们的评估表明，GPUVerify能够高效，自动验证大量的现实世界的内核。
We present a technique for the formal verification of GPU kernels, addressing two classes of correctness properties: data races and barrier divergence. Our approach is founded on a novel formal operational semantics for GPU kernels termedsynchronous, delayed visibility (SDV)semantics, which captures the execution of a GPU kernel by multiple groups of threads. The SDV semantics provides operational definitions for barrier divergence and for both inter- and intra-group data races. We build on the semantics to develop a method for reducing the task of verifying a massively parallel GPU kernel to that of verifying a sequential program. This completely avoids the need to reason about thread interleavings, and allows existing techniques for sequential program verification to be leveraged. We describe an efficient encoding of data race detection and propose a method for automatically inferring the loop invariants that are required for verification. We have implemented these techniques as a practical verification tool, GPUVerify, that can be applied directly to OpenCL and CUDA source code. We evaluate GPUVerify with respect to a set of 162 kernels drawn from public and commercial sources. Our evaluation demonstrates that GPUVerify is capable of efficient, automatic verification of a large number of real-world kernels.
登录
查看更多内容
异构多核处理器暂存器代码的自动分析
DOI：
--
发表时间：
2010
期刊：
International Conference on Tools and Algorithms for Construction and Analysis of Systems
影响因子：
--
作者：
Alastair F. Donaldson;D. Kroening;P. Rümmer
通讯作者：
P. Rümmer
使用无干扰检查 SPMD 程序的等价性
影响因子：
0.8
作者：
S. Tripakis;C. Stergiou;Roberto Lublinerman
通讯作者：
Roberto Lublinerman
GPGPU程序的规范和验证
DOI：
10.1016/j.scico.2014.03.013
发表时间：
2013
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
S. Blom;M. Huisman;M. Mihelčić
通讯作者：
M. Mihelčić
单项式和从句谓词抽象的复杂性和算法
DOI：
10.1007/978-3-642-02959-2_18
发表时间：
2009
期刊：
Cardiovascular revascularization medicine : including molecular interventions
影响因子：
--
作者：
Shuvendu K. Lahiri;S. Qadeer
通讯作者：
S. Qadeer
通过冲突导向延迟限制对具有原子的 GPU 程序进行形式化分析
DOI：
--
发表时间：
2013
期刊：
NASA Formal Methods
影响因子：
--
作者：
Wei;G. Gopalakrishnan;Guodong Li;Zvonimir Rakamaric
通讯作者：
Zvonimir Rakamaric