Symbolic crosschecking of floating-point and SIMD code
Imperial College London, London, United Kingdom
Proceedings of the sixth conference on Computer systems, EuroSys ’11, 2011
@inproceedings{collingbourne2011symbolic,
title={Symbolic crosschecking of floating-point and SIMD code},
author={Collingbourne, P. and Cadar, C. and Kelly, P.H.J.},
booktitle={Proceedings of the sixth conference on Computer systems},
pages={315–328},
year={2011},
organization={ACM}
}
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 popular open source computer vision library. KLEE-FP was able to successfully crosscheck 51 SIMD/SSE implementations against their corresponding scalar versions, proving the bounded equivalence of 41 of them (i.e., on images up to a certain size), and finding inconsistencies in the other 10.
September 12, 2011 by hgpu
