Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding
Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding
复制标题
通过冲突导向延迟限制对具有原子的 GPU 程序进行形式化分析
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Zvonimir Rakamaric
中科院分区：
文献类型：
--
作者：
Wei;G. Gopalakrishnan;Guodong Li;Zvonimir Rakamaric
近年来，基于GPU的计算取得了长足的进步。不幸的是，GPU程序的优化可能引入微妙的并发错误，因此敏锐的形式狩猎方法至关重要。本文为GPU程序提供了一种新的正式狩猎方法，该方法结合了障碍和原子。我们提出了一种称为C onFlict指导的D Elay结合的调度算法（CD）的算法，该算法利用了原子同步命令之间发生冲突的发生，以触发替代时间表的生成；这些替代时间表以延迟结合的方式执行。我们正式描述CD，并介绍两种正确性检查方法，一种基于最终状态比较，另一个基于用户主张。我们评估了对现实的GPU基准测试的实施，结果令人鼓舞。
GPU based computing has made significant strides in recent years. Unfortunately, GPU program optimizations can introduce subtle concurrency errors, and so incisive formal bug-hunting methods are essential. This paper presents a new formal bug-hunting method for GPU programs that combine barriers and atomics. We present an algorithm called c onflict-directed d elay-bounded scheduling algorithm (CD) that exploits the occurrence of conflicts among atomic synchronization commands to trigger the generation of alternate schedules; these alternate schedules are executed in a delay-bounded manner. We formally describe CD, and present two correctness checking methods, one based on final state comparison, and the other on user assertions. We evaluate our implementation on realistic GPU benchmarks, with encouraging results.
影响因子：
4.6
作者：
J. Xu
通讯作者：
J. Xu