From the July 2014 Issue
Symbolic Crosschecking of Data-Parallel Floating-Point Code
By Peter Collingbourne, Cristian Cadar, and Paul H.J. Kelly
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 tool based on the symbolic execution engine 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 effective support for integer arithmetic, the situation is different 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 prove the bounded equivalence between scalar and data-parallel versions of floating-point programs and 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 a compiler bug.
Editorials and Announcements
- According to Thomson Reuters' 2013 Journal Citation Report, TSE has an impact factor of 2.292.
- TSE celebrates its 40th Anniversary
- Get Your Journals as eBooks for Free
- eBooks of issues of TSE can now be downloaded from the Computer Society Digital Library
- In Memoriam: Mary Jean Harrold (1947-2013) (Nov 2013)
- Editorial (Sept 2013)
- In Memoriam—David Notkin (1953-2013) (June 2013)
- Editorial (May 2013)
- E-ditorial: State of the Journal (Feb 2013)
- State of the Journal (Jan/Feb 2012)
- Editorial: What Makes a Publication Archival? (March/April 2011)
- Editorial: State of the Journal (Jan/Feb 2011)
- Editorial (Nov/Dec 2010)
- How Special Should Issues Be? (Jul/Aug 2010)
- Special Section on the International Symposium on Software Testing and Analysis (March/April 2012)
- Special Section on the International Conference on Software Engineering (Jan/Feb 2012)
- Special Section on Socio-Technical Environment of Software Development Projects (May/June 2011)
- Search Based Software Engineering: Introduction to the Special Issue of the IEEE Transactions on Software Engineering (Nov/Dec 2010)
- 2008 Conference on the Foundations of Software Engineering (Sept/Oct 2010)
- The Best Papers of ISSTA (Jul/Aug 2010)
Access All Recently Published TSE Articles
Subscribe to the RSS feed of latest TSE content added to the digital library
Sign up to receive email alerts when a new issue of TSE is online.
A PrePrint is an article that has been accepted for publication in a future issue of this journal, but has not been fully edited. Content may change prior to final publication
The IEEE Transactions on Software Engineering (TSE) is an archival journal published bimonthly. We are interested in well-defined theoretical results and empirical studies that have potential impact on the construction, analysis, or management of software.
Read the full scope of TSE