Peter Collingbourne
Cristian Cadar
Paul H.J. Kelly
ABSTRACT
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.
- Aharoni 2003 M. Aharoni, S. Asaf, L. Fournier, A. Koifman, and R. Nagel. FPgen - a test generation framework for datapath floating-point verification. In HLDVT '03, 2003. Google Scholar
Digital Library
- Alpern 1988 B. Alpern, M. N. Wegman, and F. K. Zadeck. Detecting equality of variables in programs. In POPL'88, Jan. 1988. Google ScholarDigital Library
- Boldo 2007 Sylvie Boldo and Jean-Christophe Filliatre. Formal verification of floating-point programs. In ARITH'07, 2007. Google ScholarDigital Library
- Boonstoppel 2008 Peter Boonstoppel, Cristian Cadar, and Dawson Engler. RWset: Attacking path explosion in constraint-based test generation. In TACAS'08, Mar.-Apr. 2008. Google ScholarDigital Library
- Botella 2006 Bernard Botella, Arnaud Gotlieb, and Claude Michel. Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16 (2): 97--121, 2006. Google ScholarDigital Library
- Bradski 2008 Gary Bradski and Adrian Kaehler. Learning OpenCV: Computer Vision with the OpenCV Library. O'Reilly Media, 2008.Google Scholar
- Cadar 2008 Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI '08, Dec. 2008. Google ScholarDigital Library
- Chuang 2003 Weihaw Chuang, Brad Calder, and Jeanne Ferrante. Phi-predication for light-weight if-conversion. In CGO 2003, March 2003. Google ScholarDigital Library
- Clarke 2003 Edmund Clarke and Daniel Kroening. Hardware verification using ANSI-C programs as a reference. In ASP-DAC'03, Jan. 2003. Google ScholarDigital Library
- Currie 2006 David Currie, Xiushan Feng, Masahiro Fujita, Alan J. Hu, Mark Kwan, and Sreeranga Rajan. Embedded software verification using symbolic execution and uninterpreted functions. International Journal of Parallel Programming, 34 (1): 61--91, 2006. Google ScholarDigital Library
- Eichenberger 2004 Alexandre E. Eichenberger, Peng Wu, and Kevin O'Brien. Vectorization for SIMD architectures with alignment constraints. In PLDI '04, June 2004. Google ScholarDigital Library
- Ganesh 2007 Vijay Ganesh and David L. Dill. A decision procedure for bit-vectors and arrays. In CAV '07, July 2007. Google ScholarDigital Library
- Godefroid 2007 Patrice Godefroid. Compositional dynamic test generation. In POPL'07, Jan. 2007. Google ScholarDigital Library
- Harrison 2007 John Harrison. Floating-point verification. Journal of Universal Computer Science, 13 (5): 629--638, 2007.Google Scholar
- Holzbaur 1995 Christian Holzbaur. clp(q,r) manual rev. 1.3.2. Technical report, Austrian Research Institute for Artificial Intelligence, Vienna, 1995.Google Scholar
- IEEE Task P754 2008 IEEE Task P754. IEEE 754-2008, Standard for Floating-Point Arithmetic. August 2008.Google Scholar
- Intel Intel and Willow Garage. OpenCV 2.1.0: Open source computer vision library. http://opencv.willowgarage.com/.Google Scholar
- Int 1999 ISO/IEC 9899-1999: Programming Languages-C. International Organization for Standardization, December 1999.Google Scholar
- Int 2003 ISO/IEC 14882:2003(E): Programming Languages-C++. International Organization for Standardization, October 2003.Google Scholar
- King 1975 James C. King. A new approach to program testing. In ICRS'75, April 1975. Google ScholarDigital Library
- klee.llvm.org klee.llvm.org. KLEE website. http://klee.llvm.org.Google Scholar
- Larsen 2000 Samuel Larsen and Saman Amarasinghe. Exploiting superword level parallelism with multimedia instruction sets. In PLDI '00, May 2000. Google ScholarDigital Library
- Lattner 2004 Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis and transformation. In CGO '04, Mar. 2004. Google ScholarDigital Library
- Majumdar 2009} Rupak Majumdar and Ru-Gang Xu. Reducing test inputs using information partitions. In CAV '09, July 2009. Google ScholarDigital Library
- Michel 2002 Claude Michel. Exact projection functions for floating point number constraints. In AMAI '02, 2002.Google Scholar
- Moore 1959 Ramon E. Moore and C. T. Yang. Interval analysis I. Technical Document LMSD-285875, Lockheed Missiles and Space Division, Sunnyvale, CA, USA, 1959.Google Scholar
- Naishlos 2003 Dorit Naishlos, Marina Biberstein, Shay Ben-David, and Ayal Zaks. Vectorizing for a SIMdD DSP architecture. In CASES '03, Oct.-Nov. 2003. Google ScholarDigital Library
- Necula 2000 George C. Necula. Translation validation for an optimizing compiler. May 2000.Google Scholar
- Smith 2008 Eric Whitman Smith and David L. Dill. Automatic formal verification of block cipher implementations. In FMCAD '08, November 2008. Google ScholarDigital Library
Index Terms
- Symbolic crosschecking of floating-point and SIMD code
Recommendations
Use of SIMD Vector Operations to Accelerate Application Code Performance on Low-Powered ARM and Intel Platforms
IPDPSW '13: Proceedings of the 2013 IEEE 27th International Symposium on Parallel and Distributed Processing Workshops and PhD ForumAugmenting a processor with special hardware that is able to apply a Single Instruction to Multiple Data(SIMD) at the same time is a cost effective way of improving processor performance. It also offers a means of improving the ratio of processor ...
Simple, portable and fast SIMD intrinsic programming: generic simd library
WPMVP '14: Proceedings of the 2014 Workshop on Programming models for SIMD/Vector processingUsing SIMD (Single Instruction Multiple Data) is a cost-effective way to explore data parallelism on modern processors. Most processor vendors today provide SIMD engines, such as Altivec/VSX for POWER, SSE/AVX for Intel processors, and NEON for ARM. ...
Retargetable code optimization with SIMD instructions
CODES+ISSS '06: Proceedings of the 4th international conference on Hardware/software codesign and system synthesisRetargetable C compilers are nowadays widely used to quickly obtain compiler support for new embedded processors and to perform early processor architecture exploration. One frequent concern about retargetable compilers, though, is their lack of machine-...
Comments