GKLEE: Concolic Verification and Test Generation for GPUs

Guodong Li, Peng Li, Geof Sawaya, Ganesh Gopalakrishnan, Indradeep Ghosh, Sreeranga P. Rajan
Fujitsu Laboratories of America, Sunnyvale, CA 94085, USA
17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), 2012


   title={GKLEE: Concolic Verification and Test Generation for GPUs},

   author={Li, G. and Li, P. and Sawaya, G. and Gopalakrishnan, G. and Ghosh, I. and Rajan, S.P.},



Download Download (PDF)   View View   Source Source   



Programs written for GPUs often contain correctness errors such as races, deadlocks, or may compute the wrong result. Existing debugging tools often miss these errors because of their limited input-space and execution-space exploration. Existing tools based on conservative static analysis or conservative modeling of SIMD concurrency generate false alarms resulting in wasted bug-hunting. They also often do not target performance bugs (non-coalesced memory accesses, memory bank conflicts, and divergent warps). We provide a new framework called GKLEE that can analyze C++ GPU programs, locating the aforesaid correctness and performance bugs. For these programs, GKLEE can also automatically generate tests that provide high coverage. These tests serve as concrete witnesses for every reported bug. They can also be used for downstream debugging, for example to test the kernel on the actual hardware. We describe the architecture of GKLEE, its symbolic virtual machine model, and describe previously unknown bugs and performance issues that it detected on commercial SDK kernels. We describe GKLEE’s test-case reduction heuristics, and the resulting scalability improvement for a given coverage target.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: