5543

Symbolic crosschecking of floating-point and SIMD code

Peter Collingbourne, Cristian Cadar, Paul H.J. Kelly
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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2017 hgpu.org

All rights belong to the respective authors

Contact us: