Barrier invariants a shared state abstraction for the analysis of data-dependent GPU kernels
Barrier invariants a shared state abstraction for the analysis of data-dependent GPU kernels
复制标题
屏障不变量是一种共享状态抽象，用于分析数据相关的 GPU 内核
DOI：
10.1145/2544173.2509517
复制
发表时间：
2013
影响因子：
--
通讯作者：
Chong N
中科院分区：
文献类型：
--
作者：
Chong N
数据依赖的GPU内核，其数据或控制流依赖于程序的输入，很难验证，因为它们需要对许多并行线程操纵的共享状态进行推理。GPU内核的现有验证技术通过使用两个线程减少和使共享语句的内容不确定性来实现可靠性和可伸缩性，每次线程在屏障处同步，以考虑所有可能的线程交互。这种粗糙的抽象阻止了对依赖于数据的内核的验证。我们提出了屏障不变量，这是一种新的抽象技术，它允许在形式推理过程中跨屏障保留关于核共享状态的关键属性。我们将屏障不变量与GPUVerify工具集成在一起，并提供了一个详细的案例研究，展示了如何使用屏障不变量来验证三前缀和算法，从而允许对流压缩内核（GPU编程的关键构建块）进行有效的模块化验证。这种分析大大超出了使用现有的GPU内核验证技术的可能性。
Data-dependent GPU kernels, whose data or control flow are dependent on the input of the program, are difficult to verify because they require reasoning about shared state manipulated by many parallel threads. Existing verification techniques for GPU kernels achieve soundness and scalability by using a two-thread reduction and making the contents of the shared statenondeterministiceach time threads synchronise at a barrier, to account for all possible thread interactions. This coarse abstraction prohibits verification of data-dependent kernels. We presentbarrier invariants, a novel abstraction technique which allows key properties about the shared state of a kernel to be preserved across barriers during formal reasoning. We have integrated barrier invariants with the GPUVerify tool, and present a detailed case study showing how they can be used to verify threeprefix sumalgorithms, allowing efficient modular verification of astream compactionkernel, a key building block for GPU programming. This analysis goes significantly beyond what is possible using existing verification techniques for GPU kernels.