Faithfully Rounded Floating-point Computations

被引:8
|
作者
Lange, Marko [1 ]
Rump, Siegfried M. [1 ,2 ]
机构
[1] Waseda Univ, Fac Sci & Engn, Shinjuku Ku, 3-4-1 Okubo, Tokyo 1698555, Japan
[2] Hamburg Univ Technol, Inst Reliable Comp, Schwarzenberg Campus 3, D-21071 Hamburg, Germany
来源
基金
日本科学技术振兴机构;
关键词
Double-double; inaccurate cancellation; rigorous error bounds; ACCURATE;
D O I
10.1145/3290955
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a pair arithmetic for the four basic operations and square root. It can be regarded as a simplified, more-efficient double-double arithmetic. The central assumption on the underlying arithmetic is the first standard model for error analysis for operations on a discrete set of real numbers. Neither do we require a floating-point grid nor a rounding to nearest property. Based on that, we define a relative rounding error unit u and prove rigorous error bounds for the computed result of an arbitrary arithmetic expression depending on u, the size of the expression, and possibly a condition measure. In the second part of this note, we extend the error analysis by examining requirements to ensure faithfully rounded outputs and apply our results to IEEE 754 standard conform floating-point systems. For a class of mathematical expressions, using an IEEE 754 standard conform arithmetic with base beta, the result is proved to be faithfully rounded for up to 1/root beta u - 2 operations. Our findings cover a number of previously published algorithms to compute faithfully rounded results, among them Horner's scheme, products, sums, dot products, or Euclidean norm. Beyond that, several other problems can be analyzed, such as polynomial interpolation, orientation problems, Householder transformations, or the smallest singular value of Hilbert matrices of large size.
引用
收藏
页数:20
相关论文
共 50 条
  • [1] A general-purpose method for faithfully rounded floating-point function approximation in FPGAs
    Thomas, David B.
    IEEE 22ND SYMPOSIUM ON COMPUTER ARITHMETIC ARITH 22, 2015, : 42 - 49
  • [2] Termination of Floating-Point Computations
    Alexander Serebrenik
    Danny De Schreye
    Journal of Automated Reasoning, 2005, 34 : 141 - 177
  • [3] Termination of floating-point computations
    Serebrenik, A
    De Schreye, D
    JOURNAL OF AUTOMATED REASONING, 2005, 34 (02) : 141 - 177
  • [4] Verified Compilation of Floating-Point Computations
    Sylvie Boldo
    Jacques-Henri Jourdan
    Xavier Leroy
    Guillaume Melquiond
    Journal of Automated Reasoning, 2015, 54 : 135 - 163
  • [5] The pitfalls of verifying floating-point computations
    Monniaux, David
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2008, 30 (03):
  • [6] Verified Compilation of Floating-Point Computations
    Boldo, Sylvie
    Jourdan, Jacques-Henri
    Leroy, Xavier
    Melquiond, Guillaume
    JOURNAL OF AUTOMATED REASONING, 2015, 54 (02) : 135 - 163
  • [7] Symbolic execution of floating-point computations
    Botella, Bernard
    Gotlieb, Arnaud
    Michel, Claude
    SOFTWARE TESTING VERIFICATION & RELIABILITY, 2006, 16 (02): : 97 - 121
  • [8] Floating-point computations on reconfigurable computers
    Morris, Gerald R.
    PROCEEDINGS OF THE HPCMP USERS GROUP CONFERENCE 2007, 2007, : 339 - 344
  • [9] An Interval Compiler for Sound Floating-Point Computations
    Rivera, Joao
    Franchetti, Franz
    Puschel, Markus
    CGO '21: PROCEEDINGS OF THE 2021 IEEE/ACM INTERNATIONAL SYMPOSIUM ON CODE GENERATION AND OPTIMIZATION (CGO), 2021, : 52 - 64
  • [10] A hardware error estimate for floating-point computations
    Lang, Tomas
    Bruguera, Javier D.
    ADVANCED SIGNAL PROCESSING ALGORITHMS, ARCHITECTURES, AND IMPLEMENTATIONS XVIII, 2008, 7074