Verification of Producer-Consumer Synchronization in GPU Programs

Rahul Sharma, Michael Bauer, Alex Aiken
Stanford University
36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI), 2015


   title={Verification of Producer-Consumer Synchronization in GPU Programs},

   author={Sharma, Rahul and Bauer, Michael and Aiken, Alex},



Previous efforts to formally verify code written for GPUs have focused solely on kernels written within the traditional data-parallel GPU programming model. No previous work has considered the higher performance, but more complex, warp-specialized kernels based on producer-consumer named barriers available on current hardware. In this work we present the first formal operational semantics for named barriers and define what it means for a warp-specialized kernel to be correct. We give algorithms for verifying the correctness of warp-specialized kernels and prove that they are both sound and complete for the most common class of warp-specialized programs. We also present WEFT, a verification tool for checking warp-specialized code. Using WEFT, we discover several non-trivial bugs in production warp-specialized kernels.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: