Sciweavers

EUROSYS
2011
ACM

Symbolic crosschecking of floating-point and SIMD code

12 years 7 months ago
Symbolic crosschecking of floating-point and SIMD code
We present an effective technique for crosschecking an IEEE 754 floating-point program and its SIMD-vectorized version, implemented in KLEE-FP, an extension to the KLEE symbolic execution tool that supports symbolic reasoning on the equivalence between floating-point values. The key insight behind our approach is that floatingpoint values are only reliably equal if they are essentially built by the same operations. As a result, our technique works by lowering the Intel Streaming SIMD Extension (SSE) instruction set to primitive integer and floating-point operations, and then using an algorithm based on symbolic expression matching augmented with canonicalization rules. 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. We applied KLEE-FP to OpenCV, a popula...
Peter Collingbourne, Cristian Cadar, Paul H. J. Ke
Added 28 Aug 2011
Updated 28 Aug 2011
Type Journal
Year 2011
Where EUROSYS
Authors Peter Collingbourne, Cristian Cadar, Paul H. J. Kelly
Comments (0)