Advertisement

Symbolic Testing of OpenCL Code

  • Peter Collingbourne
  • Cristian Cadar
  • Paul H. J. Kelly
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7261)

Abstract

We present an effective technique for crosschecking a C or C++ program against an accelerated OpenCL version, as well as a technique for detecting data races in OpenCL programs. Our techniques are implemented in KLEE-CL, a symbolic execution engine based on KLEE and KLEE-FP that supports symbolic reasoning on the equivalence between symbolic values.

Our approach is to symbolically model the OpenCL environment using an OpenCL runtime library targeted to symbolic execution. Using this model we are able to run OpenCL programs symbolically, keeping track of memory accesses for the purpose of race detection. We then compare the symbolic result against the plain C or C++ implementation in order to detect mismatches between the two versions.

We applied KLEE-CL to the Parboil benchmark suite, the Bullet physics library and the OP2 library, in which we were able to find a total of seven errors: two mismatches between the OpenCL and C implementations, three memory errors, one OpenCL compiler bug and one race condition.

Keywords

Address Space Memory Error Symbolic Execution Race Condition Kernel Execution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Boyer, M., Skadron, K., Weimer, W.: Automated dynamic analysis of CUDA programs. In: STMCS 2008 (April 2008)Google Scholar
  2. 2.
    Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys 2011 (April 2011)Google Scholar
  3. 3.
    clang: a C language family frontend for LLVM, http://clang.llvm.org/
  4. 4.
    Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: ASP-DAC 2003 (January 2003)Google Scholar
  5. 5.
    Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys 2011 (April 2011)Google Scholar
  6. 6.
    Coumans, E., et al.: Bullet continuous collision detection and physics library, http://bulletphysics.org/
  7. 7.
    Flanagan, C., Freund, S.N.: Fasttrack: Efficient and precise dynamic race detection. In: PLDI 2009 (June 2009)Google Scholar
  8. 8.
    Giles, M.B., Mudalige, G.R., Sharif, Z., Markall, G.R., Kelly, P.H.J.: Performance analysis of the OP2 framework on many-core architectures. SIGMETRICS Performance Evaluation Review 38(4), 9–15 (2011)CrossRefGoogle Scholar
  9. 9.
    Grewe, D., O’Boyle, M.F.P.: A Static Task Partitioning Approach for Heterogeneous Systems Using OpenCL. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 286–305. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  10. 10.
    IMPACT Research Group, UIUC. Parboil benchmark suite, http://impact.crhc.illinois.edu/parboil.php
  11. 11.
    International Organization for Standardization. ISO/IEC 9899-1999: Programming Languages—C (December 1999)Google Scholar
  12. 12.
    Khronos OpenCL Working Group. The OpenCL Specification, version 1.1, revision 36 (September 2010)Google Scholar
  13. 13.
    King, J.C.: A new approach to program testing. In: ICRS 1975 (April 1975)Google Scholar
  14. 14.
    Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004 (March 2004)Google Scholar
  15. 15.
    Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: FSE 2010 (November 2010)Google Scholar
  16. 16.
    Li, G., Li, P., Sawaya, G., Ghosh, I.: GKLEE: Concolic verification and test generation for GPUs. In: PPoPP 2012 (Februery 2012)Google Scholar
  17. 17.
    Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000 (May 2000)Google Scholar
  18. 18.
    NVIDIA. NVIDIA CUDA Programming Guide, Version 3.0 (February 2010)Google Scholar
  19. 19.
    O’Callahan, R., Choi, J.-D.: Hybrid dynamic data race detection. In: PPoPP 2003 (June 2003)Google Scholar
  20. 20.
    Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: FSE 2008 (November 2008)Google Scholar
  21. 21.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.E.: Eraser: A dynamic data race detector for multithreaded programs. In: SOSP 1997 (October 1997)Google Scholar
  22. 22.
    Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using model checking with symbolic execution to verify parallel numerical programs. In: ISSTA 2006 (July 2006)Google Scholar
  23. 23.
    Smith, E.W., Dill, D.L.: Automatic formal verification of block cipher implementations. In: FMCAD 2008 (November 2008)Google Scholar
  24. 24.
    Tripakis, S., Stergiou, C., Lublinerman, R.: Checking non-interference in SPMD programs. In: HotPar 2010 (June 2010)Google Scholar
  25. 25.
    Zheng, M., Ravi, V.T., Qin, F., Agrawal, G.: GRace: A low-overhead mechanism for detecting data races in GPU programs. In: PPoPP 2011 (February 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Peter Collingbourne
    • 1
  • Cristian Cadar
    • 1
  • Paul H. J. Kelly
    • 1
  1. 1.Department of ComputingImperial College LondonUK

Personalised recommendations