Barrier invariants
Barrier invariants
复制标题
障碍不变量
DOI：
10.1145/2509136.2509517
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Chong N
中科院分区：
文献类型：
--
作者：
Chong N
依赖数据的GPU内核，其数据或控制流依赖于程序的输入，很难验证，因为它们需要关于由许多并行线程操纵的共享状态的推理。现有的GPU内核验证技术通过使用双线程缩减并使共享状态的内容在每次线程在障碍处同步时具有确定性来实现可靠性和可伸缩性，以考虑所有可能的线程交互。这种粗略的抽象禁止验证依赖于数据的内核。我们提出了障碍不变量，这是一种新的抽象技术，它允许在形式推理过程中跨越障碍保留关于内核共享状态的关键属性。我们将屏障不变量与GPU验证工具集成在一起，并提供了一个详细的案例研究，展示了如何使用它们来验证三前缀求和算法，从而允许对作为GPU编程的关键构建块的ASTREAM压缩内核进行高效的模块化验证。这种分析大大超出了使用现有的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.