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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Boyer, M., Skadron, K., Weimer, W.: Automated dynamic analysis of CUDA programs. In: STMCS 2008 (April 2008)
Bucur, S., Ureche, V., Zamfir, C., Candea, G.: Parallel symbolic execution for automated real-world software testing. In: EuroSys 2011 (April 2011)
clang: a C language family frontend for LLVM, http://clang.llvm.org/
Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: ASP-DAC 2003 (January 2003)
Collingbourne, P., Cadar, C., Kelly, P.H.: Symbolic crosschecking of floating-point and SIMD code. In: EuroSys 2011 (April 2011)
Coumans, E., et al.: Bullet continuous collision detection and physics library, http://bulletphysics.org/
Flanagan, C., Freund, S.N.: Fasttrack: Efficient and precise dynamic race detection. In: PLDI 2009 (June 2009)
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)
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)
IMPACT Research Group, UIUC. Parboil benchmark suite, http://impact.crhc.illinois.edu/parboil.php
International Organization for Standardization. ISO/IEC 9899-1999: Programming Languages—C (December 1999)
Khronos OpenCL Working Group. The OpenCL Specification, version 1.1, revision 36 (September 2010)
King, J.C.: A new approach to program testing. In: ICRS 1975 (April 1975)
Lattner, C., Adve, V.: LLVM: A compilation framework for lifelong program analysis & transformation. In: CGO 2004 (March 2004)
Li, G., Gopalakrishnan, G.: Scalable SMT-based verification of GPU kernel functions. In: FSE 2010 (November 2010)
Li, G., Li, P., Sawaya, G., Ghosh, I.: GKLEE: Concolic verification and test generation for GPUs. In: PPoPP 2012 (Februery 2012)
Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000 (May 2000)
NVIDIA. NVIDIA CUDA Programming Guide, Version 3.0 (February 2010)
O’Callahan, R., Choi, J.-D.: Hybrid dynamic data race detection. In: PPoPP 2003 (June 2003)
Person, S., Dwyer, M.B., Elbaum, S., Pǎsǎreanu, C.S.: Differential symbolic execution. In: FSE 2008 (November 2008)
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)
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)
Smith, E.W., Dill, D.L.: Automatic formal verification of block cipher implementations. In: FMCAD 2008 (November 2008)
Tripakis, S., Stergiou, C., Lublinerman, R.: Checking non-interference in SPMD programs. In: HotPar 2010 (June 2010)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Collingbourne, P., Cadar, C., Kelly, P.H.J. (2012). Symbolic Testing of OpenCL Code. In: Eder, K., Lourenço, J., Shehory, O. (eds) Hardware and Software: Verification and Testing. HVC 2011. Lecture Notes in Computer Science, vol 7261. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34188-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-34188-5_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34187-8
Online ISBN: 978-3-642-34188-5
eBook Packages: Computer ScienceComputer Science (R0)