Guodong Li
Sreeranga P. Rajan
Abstract
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.
- G. Li and G. Gopalakrishnan, "Scalable SMT-based verification of GPU kernel functions," in SIGSOFT FSE, 2010. Google Scholar
Digital Library
- M. Zheng, V. T. Ravi, F. Qin, and G. Agrawal, "GRace: A low-overhead mechanism for detecting data races in GPU programs," in PPoPP, 2011. Google ScholarDigital Library
- M. Boyer, K. Skadron, and W. Weimer, "Automated dynamic analysis of CUDA programs," in Third Workshop on Software Tools for MultiCore Systems,2008.Google Scholar
- C. Cadar, D. Dunbar, and D. R. Engler, "KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs," in OSDI, 8th USENIX Symposium, 2008. Google ScholarDigital Library
- "SMT-COMP. http://www.smtcomp.org/2011."Google Scholar
- P. Godefroid, N. Klarlund, and K. Sen, "DART: Directed automated random testing," in PLDI, 2005. Google ScholarDigital Library
- "KLEE open projects," http://klee.llvm.org/OpenProjects.html.Google Scholar
- K. Sen, D. Marinov, and G. Agha, "CUTE: a concolic unit testing engine for C," in 10th ESEC/FSE, 2005. Google ScholarDigital Library
- "CUDA zone. www.nvidia.com/object/cuda_home.html."Google Scholar
- OpenCL. http://www.khronos.org/opencl.Google Scholar
- A. Kamil and K. A. Yelick, "Concurrency Analysis for Parallel Programs with Textually Aligned Barriers," in LCPC, 2005. Google ScholarDigital Library
- "The LLVM compiler infrastructure. http://www.llvm.org/."Google Scholar
- "GKLEE Technical Report. http://www.cs.utah.edu/fv/GKLEE."Google Scholar
- "Cuda programming guide version 4.0. http://developer.download.nvidia.com/compute/cuda/4_0/toolkit/docs/CUDA_C_Programming_Guide.pdf."Google Scholar
- J. Sevcik, "Safe Optimisations for Shared-Memory Concurrent Programs," in PLDI, 2011. Google ScholarDigital Library
- S. V. Adve, M. D. Hill, B. P. Miller, and R. H. Netzer, "Detecting data races on weak memory systems," in ISCA, 1991. Google ScholarDigital Library
- D. Shasa and M. Snir, "Efficient and correct execution of parallel programs that share memory," ACM TOPLAS, vol. 10, no. 2, pp. 282--312, 1988. Google ScholarDigital Library
- A. Aiken and D. Gay, "Barrier inference," in POPL, 1998. Google ScholarDigital Library
- NVIDIA, "CUDA-GDB," Jan. 2009, an extension to the GDB debugger for debugging CUDA kernels in the hardware.Google Scholar
- Nvidia, "Parallel Nsight," Jul. 2010.Google Scholar
- Rogue Wave, "Totalview for CUDA," Jan. 2010.Google Scholar
- J. M. Cobleigh, L. A. Clarke, and L. J. Osterweil, "Flavers: A finite state verification technique for software systems," IBM Systems Journal,vol. 41, no. 1, 2002. Google ScholarDigital Library
- S. K. Lahiri, S. Qadeer, and Z. Rakamaric, "Static and precise detection of concurrency errors in systems code using SMT solvers," in 21st Computer Aided Verification (CAV), 2009. Google ScholarDigital Library
- B. Coutinho, D. Sampaio, F. M. Quintao Pereira, and W. Meira Jr., "Divergence analysis and optimizations," in PACT, 2011. Google ScholarDigital Library
- J. Lv, G. Li, A. Humphrey, and G. Gopalakrishnan, "Performance degradation analysis of GPU kernels," in EC2 Workshop, 2011.Google Scholar
- P. Collingbourne, C. Cadar, and P. H. J. Kelly, "Symbolic crosschecking of floating-point and SIMD code," in EuroSys, 2011. Google ScholarDigital Library
- P. Collingbourne, C. Cadar, and P. Kelly, "Symbolic testing of OpenCL code," in Haifa Verification Conference (HVC), 2011. Google ScholarDigital Library
- G. F. Diamos, A. R. Kerr, S. Yalamanchili, and N. Clark, "Ocelot: a dynamic optimization framework for bulk-synchronous applications in heterogeneous systems," in PACT, 2010. Google ScholarDigital Library
Index Terms
- GKLEE: concolic verification and test generation for GPUs
Recommendations
Scalable SMT-based verification of GPU kernel functions
FSE '10: Proceedings of the eighteenth ACM SIGSOFT international symposium on Foundations of software engineeringInterest in Graphical Processing Units (GPUs) is skyrocketing due to their potential to yield spectacular performance on many important computing applications. Unfortunately, writing such efficient GPU kernels requires painstaking manual optimization ...
GKLEE: concolic verification and test generation for GPUs
PPoPP '12: Proceedings of the 17th ACM SIGPLAN symposium on Principles and Practice of Parallel ProgrammingPrograms 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 ...
Practical symbolic race checking of GPU programs
SC '14: Proceedings of the International Conference for High Performance Computing, Networking, Storage and AnalysisEven the careful GPU programmer can inadvertently introduce data races while writing and optimizing code. Currently available GPU race checking methods fall short either in terms of their formal guarantees, ease of use, or practicality. Existing ...
Comments