Symbolic crosschecking of floating-point and SIMD code
Symbolic crosschecking of floating-point and SIMD code
复制标题
DOI：
10.1145/1966445.1966475
复制
发表时间：
2011-04
期刊：
影响因子：
--
通讯作者：
Peter Collingbourne;Cristian Cadar;P. Kelly
中科院分区：
文献类型：
--
作者：
Peter Collingbourne;Cristian Cadar;P. Kelly
我们提出了一种有效的交叉检查IEEE754浮点程序及其SIMD矢量化版本的技术，并在Klee-FP中实现，Klee-FP是对Klee符号执行工具的扩展，它支持关于浮点值之间等价性的符号推理。我们方法背后的关键见解是，只有当浮点值基本上由相同的操作构建时，它们才能可靠地相等。因此，我们的技术的工作方式是将Intel SIMD流扩展(SSE)指令集降低为原始整数和浮点操作，然后使用基于符号表达式匹配和规范化规则的算法。在符号执行下，我们必须验证每个可行的控制流路径上的等价性。我们通过积极地合并条件句来减少这一过程的分支因子，通过积极的Phi节点折叠变换将分支转换为选择操作。我们将Klee-FP应用于流行的开源计算机视觉库OpenCV。Klee-FP能够成功地交叉检查51个SIMD/SSE实现与其对应的标量版本，证明其中41个实现的有界等价性(即，在特定大小的图像上)，并发现其他10个实现中的不一致。
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.