Symbolic Crosschecking of Data-Parallel Floating Point Code
Author(s)
Collingbourne, Peter Cyrus
Type
Thesis
Abstract
In this thesis we present a symbolic execution-based technique for cross-checking programs
accelerated using SIMD or OpenCL against an unaccelerated 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 that supports symbolic reasoning on the equivalence
between expressions involving both integer and floating-point operations.
While the current generation of constraint solvers provide good support for integer arithmetic,
there is little support available for floating-point arithmetic, due to the complexity inherent
in such computations. The key insight behind our approach is that floating-point values are
only reliably equal if they are essentially built by the same operations. This allows us to use
an algorithm based on symbolic expression matching augmented with canonicalisation rules to
determine path equivalence.
Under symbolic execution, we have to verify equivalence along every feasible control-flow
path. We reduce the branching factor of this process by aggressively merging conditionals,
if-converting branches into select operations via an aggressive phi-node folding transformation.
To support the Intel Streaming SIMD Extension (SSE) instruction set, we lower SSE instructions
to equivalent generic vector operations, which in turn are interpreted in terms of primitive
integer and floating-point operations.
To support OpenCL programs, we symbolically model the OpenCL environment using an
OpenCL runtime library targeted to symbolic execution. We detect data races by keeping
track of all memory accesses using a memory log, and reporting a race whenever we detect that
two accesses conflict. By representing the memory log symbolically, we are also able to detect
races associated with symbolically indexed accesses of memory objects.
We used KLEE-CL to find a number of issues in a variety of open source projects that use SSE
and OpenCL, including mismatches between implementations, memory errors, race conditions
and compiler bugs.
accelerated using SIMD or OpenCL against an unaccelerated 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 that supports symbolic reasoning on the equivalence
between expressions involving both integer and floating-point operations.
While the current generation of constraint solvers provide good support for integer arithmetic,
there is little support available for floating-point arithmetic, due to the complexity inherent
in such computations. The key insight behind our approach is that floating-point values are
only reliably equal if they are essentially built by the same operations. This allows us to use
an algorithm based on symbolic expression matching augmented with canonicalisation rules to
determine path equivalence.
Under symbolic execution, we have to verify equivalence along every feasible control-flow
path. We reduce the branching factor of this process by aggressively merging conditionals,
if-converting branches into select operations via an aggressive phi-node folding transformation.
To support the Intel Streaming SIMD Extension (SSE) instruction set, we lower SSE instructions
to equivalent generic vector operations, which in turn are interpreted in terms of primitive
integer and floating-point operations.
To support OpenCL programs, we symbolically model the OpenCL environment using an
OpenCL runtime library targeted to symbolic execution. We detect data races by keeping
track of all memory accesses using a memory log, and reporting a race whenever we detect that
two accesses conflict. By representing the memory log symbolically, we are also able to detect
races associated with symbolically indexed accesses of memory objects.
We used KLEE-CL to find a number of issues in a variety of open source projects that use SSE
and OpenCL, including mismatches between implementations, memory errors, race conditions
and compiler bugs.
Date Issued
2012
Date Awarded
2013-02
Copyright Statement
Attribution NoDerivatives 4.0 International Licence (CC BY-ND)
Advisor
Kelly, Paul
Yoshida, Nobuko
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)