Specification and verification of GPGPU programs
Specification and verification of GPGPU programs
复制标题
GPGPU程序的规范和验证
DOI：
10.1016/j.scico.2014.03.013
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
M. Mihelčić
中科院分区：
文献类型：
--
作者：
S. Blom;M. Huisman;M. Mihelčić
图形处理单元（gpu）由于其低廉的价格、高能效和强大的计算能力而越来越多地用于通用应用程序。考虑到GPU应用程序的重要性，GPU程序的行为可以被指定并正式证明是正确的是至关重要的。本文提出了一种验证用OpenCL编写的GPU内核的逻辑，OpenCL是一种平台无关的底层编程语言。该逻辑可用于证明内核的数据竞争自由和功能正确性。验证是模块化的，基于基于权限的分离逻辑的思想。我们给出了逻辑及其可靠性证明，然后讨论了工具支持并说明了其在复杂示例内核上的使用。
Graphics Processing Units (GPUs) are increasingly used for general-purpose applications because of their low price, energy efficiency and enormous computing power. Considering the importance of GPU applications, it is vital that the behaviour of GPU programs can be specified and proven correct formally. This paper presents a logic to verify GPU kernels written in OpenCL, a platform-independent low-level programming language. The logic can be used to prove both data-race-freedom and functional correctness of kernels. The verification is modular, based on ideas from permission-based separation logic. We present the logic and its soundness proof, and then discuss tool support and illustrate its use on a complex example kernel.