Mon 15 Jun 2015 14:25 - 14:50 at PLDI Main BLUE (Portland 254-255) - Verification Chair(s): Zachary Tatlock

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, {\em warp-specialized} kernels based on producer-consumer {\em 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.

PLDI 2015 Artifact Evaluated Badge

Mon 15 Jun

pldi2015-papers
14:00 - 15:40: Research Papers - Verification at PLDI Main BLUE (Portland 254-255)
Chair(s): Zachary Tatlock
pldi2015-papers143436960000014:00 - 14:25
Talk
Ilya SergeyIMDEA Software Institute, Aleksandar NanevskiIMDEA Software Institute, Anindya BanerjeeIMDEA Software Institute
Link to publication Media Attached
pldi2015-papers143437110000014:25 - 14:50
Talk
Rahul SharmaStanford University, Michael BauerNVIDIA Research, Alex AikenStanford University
Media Attached
pldi2015-papers143437260000014:50 - 15:15
Talk
Peter GammieNICTA, Tony HoskingAustralian National University, Data61, and Purdue University, Kai EngelhardtUNSW and NICTA
Link to publication Media Attached
pldi2015-papers143437410000015:15 - 15:40
Talk
Joseph TassarottiCarnegie Mellon University, Derek DreyerMPI-SWS, Viktor VafeiadisMPI-SWS, Germany
Media Attached