Scalable SMT-based verification of GPU kernel functions
Scalable SMT-based verification of GPU kernel functions
复制标题
基于 SMT 的可扩展 GPU 内核功能验证
DOI：
10.1145/1882291.1882320
复制
发表时间：
2010
影响因子：
12.6
通讯作者：
G. Gopalakrishnan
中科院分区：
文献类型：
--
作者：
Guodong Li;G. Gopalakrishnan
对图形处理单元（GPU）的兴趣由于其在许多重要的计算应用中产生壮观性能的潜力而飙升。不幸的是，编写如此有效的GPU内核需要艰苦的手动优化工作，这很容易出错。我们为用Cuda C撰写的内核贡献了第一个综合符号验证器，称为“用户GPU程序的摊子（PUG）”，我们的工具有效地自动地使用满意度模型理论（SMT）工具来自动分析现实世界内核数据竞赛，错误同步的障碍，银行冲突和错误的结果。帕格的创新想法包括一种新颖的方法来象征性编码线程交织，正确的屏障放置的精确分析，避免交织产生的特殊方法，对屏障间隔进行分析以及通过三种方法处理循环：循环归一化，超级抗性，发现不变的发现。 Pug从公共分布和内部项目中分析了一百多个CUDA内核，发现错误以及微妙的无证件假设。
Interest in Graphical Processing Units (GPUs) is skyrocketing due to their potential to yield spectacular performance on many important computing applications. Unfortunately, writing such efficient GPU kernels requires painstaking manual optimization effort which is very error prone. We contribute the first comprehensive symbolic verifier for kernels written in CUDA C. Called the 'Prover of User GPU programs (PUG),' our tool efficiently and automatically analyzes real-world kernels using Satisfiability Modulo Theories (SMT) tools, detecting bugs such as data races, incorrectly synchronized barriers, bank conflicts, and wrong results. PUG's innovative ideas include a novel approach to symbolically encode thread interleavings, exact analysis for correct barrier placement, special methods for avoiding interleaving generation, dividing up the analysis over barrier intervals, and handling loops through three approaches: loop normalization, overapproximation, and invariant finding. PUG has analyzed over a hundred CUDA kernels from public distributions and in-house projects, finding bugs as well as subtle undocumented assumptions.