Symbolic Testing of OpenCL Code

Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
Department of Computing, Imperial College London
Haifa Verification Conference, 2011


   title={Symbolic testing of OpenCL code},

   author={Collingbourne, P. and Cadar, C. and Kelly, P.},

   booktitle={Haifa Verification Conference (HVC)},



Download Download (PDF)   View View   Source Source   Source codes Source codes




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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2021 hgpu.org

All rights belong to the respective authors

Contact us: