Parametric flows: Automated behavior equivalencing for symbolic analysis of races in CUDA programs
Parametric flows: Automated behavior equivalencing for symbolic analysis of races in CUDA programs
复制标题
参数流：CUDA 程序中种族符号分析的自动行为等效
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
G. Gopalakrishnan
中科院分区：
文献类型：
--
作者：
Peng Li;Guodong Li;G. Gopalakrishnan
不断增长的并发规模需要自动抽象技术，以减少并发系统分析中的努力。在本文中，我们表明，GPU程序中存在的高度行为对称性允许通过抽象大大简化CUDA种族检测。我们的抽象技术是一种自动创建参数流 - 以相同方式差异的线程类别类别类别 - 仅在每个参数流中检查一对线程的数据种族。我们已经实施了这种方法作为我们最近提出的GKLEE符号分析框架的扩展，并表明我们以前所有的结果都得到了极大的改进，因为（i）基于参数流的分析所花费的时间少得多，并且（ii）由于很多时间）分析的较高可扩展性，我们可以检测到更多的数据竞赛情况，而Gklee先前错过的情况是因为它被迫降低了尺寸的示例以限制分析的复杂性。此外，基于参数流的分析适用于具有SPMD模型的其他程序。
The growing scale of concurrency requires automated abstraction techniques to cut down the effort in concurrent system analysis. In this paper, we show that the high degree of behavioral symmetry present in GPU programs allows CUDA race detection to be dramatically simplified through abstraction. Our abstraction techniques is one of automatically creating parametric flows - control-flow equivalence classes of threads that diverge in the same manner - and checking for data races only across a pair of threads per parametric flow. We have implemented this approach as an extension of our recently proposed GKLEE symbolic analysis framework and show that all our previous results are dramatically improved in that (i) the parametric flow-based analysis takes far less time, and (ii) because of the much higher scalability of the analysis, we can detect even more data race situations that were previously missed by GKLEE because it was forced to downscale examples to limit analysis complexity. Moreover, the parametric flow-based analysis is applicable to other programs with SPMD models.
DOI：
10.1145/1966445.1966475
发表时间：
2011-04
期刊：
--
影响因子：
--
作者：
Peter Collingbourne;Cristian Cadar;P. Kelly
通讯作者：
Peter Collingbourne;Cristian Cadar;P. Kelly