Stabilizing Floating-Point Programs Using Provenance Analysis

Stabilizing Floating-Point Programs Using Provenance Analysis
复制标题

使用来源分析稳定浮点程序

DOI:
10.1007/978-3-319-52234-0_13
复制
发表时间:
2017
期刊:
and Abstract Interpretation
影响因子:
--
通讯作者:
Wahl, Thomas
Wahl, Thomas
中科院分区:
--
文献类型:
--
作者:
Gu, Yijia;Wahl, Thomas

文献摘要

参考文献

相似文献

浮点运算是当今许多计算机上可用的真实的运算的松散标准化近似。架构和编译器的差异可能会导致不同平台对相同输入的不同计算。如果不加以处理,平台依赖性,在本文中称为挥发性,严重干扰结果的可重复性,并最终影响程序的可移植性。我们提出了一种方法tostabilizing浮点程序对波动。我们的方法,dubbedprovenance分析,跟踪波动观察到在一个给定的中间expressionE回到波动在前面的声明,并量化个人的贡献波动inE。然后,通过使用表达式重写和控制杂注消除算法的歧义,稳定贡献最大的语句。本地(相对于程序范围)稳定化的好处是编译器可以自由地在程序片段中进行性能或精度增强优化,而不会使E不稳定。我们已经在一个动态分析工具中实现了我们的技术,该工具可以报告波动性和来源信息。我们证明,本地程序稳定往往足以减少平台依赖到一个可接受的水平。
Floating-point arithmetic is a loosely standardized approximation of real arithmetic available on many computers today. Architectural and compiler differences can lead to diverse calculations across platforms, for the same input. If left untreated, platform dependence, calledvolatilityin this paper, seriously interferes with result reproducibility and, ultimately, program portability. We present an approach tostabilizingfloating-point programs against volatility. Our approach, dubbedprovenance analysis, traces volatility observed in a given intermediate expressionEback to volatility in preceding statements, and quantifies individual contributions to the volatility inE. Statements contributing the most are then stabilized, by disambiguating the arithmetic using expression rewriting and control pragmas. The benefit oflocal(as opposed to program-wide) stabilization is that compilers are free to engage performance- or precision-enhancing optimizations across program fragments that do not destabilizeE. We have implemented our technique in a dynamic analysis tool that reports both volatility and provenance information. We demonstrate that local program stabilization often suffices to reduce platform dependence to an acceptable level.
数值程序的硬件相关证明
DOI: --
发表时间: 2011
期刊: Certified Programs and Proofs
影响因子: --
作者:
T. Nguyen;Claude Marché
通讯作者: Claude Marché
通过分析汇编代码来证明浮点数值程序
DOI: --
发表时间: 2011
期刊:
影响因子: --
作者:
Nguyen Thi Mong Tuyen;C. Marché
通讯作者: C. Marché
使用英特尔® 编译器的浮点结果的一致性或为什么我的应用程序不总是给出相同的答案?
DOI: --
发表时间: 2010
期刊:
影响因子: --
作者:
Dr. Martyn J. Corden;David Kreitzer
通讯作者: David Kreitzer