Automatic Synchronization for GPU Kernels

Automatic Synchronization for GPU Kernels
复制标题

GPU 内核自动同步

DOI:
10.23919/fmcad.2018.8602999
复制
发表时间:
2018
期刊:
2018 Formal Methods in Computer Aided Design (FMCAD)
影响因子:
--
通讯作者:
N. Polikarpova
N. Polikarpova
中科院分区:
--
文献类型:
--
作者:
S. Anand;N. Polikarpova

文献摘要

参考文献

被引文献

相似文献

我们提出了一种自动合成GPU内核中有效且可证明正确同步的技术。我们的技术依赖于现成的正确性Oracle,并通过利用Oracle提供的种族位置信息来将最佳同步合成作为MaxSAT问题来实现有效的综合。我们已经在名为AutoSync的工具中实现了我们的技术,该工具可用于用CUDA编写的内核,并使用静态验证者Gpuverify作为正确的Oracle。对来自Gpuverify基准套件的18个现实核的评估表明,AutoSync能够合成最佳同步位置,合成时间是合理的(我们最大的基准为20秒)。
We present a technique for automatic synthesis of efficient and provably correct synchronization in GPU kernels. Our technique relies on an off-the-shelf correctness oracle and achieves efficient synthesis by leveraging the race location information provided by the oracle in order to encode optimal synchronization synthesis as a MaxSAT problem. We have implemented our technique in a tool called AUTOSYNC that works on kernels written in CUDA and uses a static verifier GPUVERIFY as the correctness oracle. An evaluation on 18 realistic kernels from the GPUVERIFY benchmark suite shows that AUTOSYNC is able to synthesize optimal synchronization placements, and synthesis times are reasonable (20 seconds for our largest benchmark).
DOI: 10.1145/2743017
发表时间: 2015
影响因子: 1.3
作者:
Betts A
通讯作者: Betts A