GPURepair：GPU 内核的自动化修复

本文提出一种用于修复 CUDA 或 OpenCL 编写的 GPU 内核中由数据竞争与屏障发散引起的错误的工具。我们对先前工作的新颖扩展还能移除被认定对正确性不必要的屏障。我们在名为 GPURepair 的工具中实现了这些想法，该工具使用 GPUVerify 作为 GPU 内核的验证预言机。我们还扩展了 GPUVerify 以支持 CUDA Cooperative Groups，使 GPURepair 能够对 CUDA 内核执行块间同步。据我们所知，GPURepair 是唯一能为 CUDA 与 OpenCL 内核的块内数据竞争与屏障发散错误提出修复方案、且唯一能修复 CUDA 内核块间数据竞争的工具。我们在约 750 个内核上进行了广泛实验，并与先前工作进行比较。我们通过其修复更多内核的能力以及移除冗余屏障和处理块间数据竞争的唯一能力展示了 GPURepair 的优越性。