Parameterized Verification of GPU Kernel Programs

Parameterized Verification of GPU Kernel Programs
复制标题

GPU内核程序参数化验证

DOI：
10.1109/ipdpsw.2012.302
复制
发表时间：
2012
期刊：
2012 IEEE 26th International Parallel and Distributed Processing Symposium Workshops & PhD Forum
影响因子：
--
通讯作者：
G. Gopalakrishnan
G. Gopalakrishnan
中科院分区：
--
文献类型：
--
作者：
Guodong Li;G. Gopalakrishnan

文献摘要

被引文献

相似文献

我们提出了一个自动的符号验证器，用于参数化地检查GPGPU内核的功能正确性，对于任意数量的线程。我们的工具检查内核及其优化版本的功能等价性，帮助调试在内存合并和银行冲突消除相关优化过程中引入的错误。我们工作的关键特征包括：(1)跨两个内核版本编码比较断言的符号方法，以及(2)通过过度近似克服SMT求解器限制的技术，从而产生有效的bug搜索方法。
We present an automated symbolic verifier for checking the functional correctness of GPGPU kernels parametrically, for an arbitrary number of threads. Our tool checks the functional equivalence of a kernel and its optimized versions, helping debug errors introduced during memory coalescing and bank conflict elimination related optimizations. Key features of our work include: (1) a symbolic method to encode a comparative assertion across two kernel versions, and (2) techniques to overcome SMT solver restrictions through over-approximations, yielding an efficient bug-hunting method.