Symbolic Testing of OpenCL Code
Symbolic Testing of OpenCL Code
复制标题
OpenCL 代码的符号测试
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
P. Kelly
中科院分区：
文献类型：
--
作者：
Peter Collingbourne;Cristian Cadar;P. Kelly
我们提出了一种有效的技术，用于交叉检查C或c++程序与加速的OpenCL版本，以及检测OpenCL程序中的数据竞争的技术。我们的技术在KLEE- cl中实现，KLEE- cl是一个基于KLEE和KLEE- fp的符号执行引擎，支持对符号值之间的等价性进行符号推理。
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.
DOI：
10.1145/1966445.1966475
发表时间：
2011-04
期刊：
--
影响因子：
--
作者：
Peter Collingbourne;Cristian Cadar;P. Kelly
通讯作者：
Peter Collingbourne;Cristian Cadar;P. Kelly