A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers

From LRDE

Abstract

Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10. This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.

Documents

Bibtex (lrde.bib)

@InProceedings{	  boldo.18.arith,
  title		= {A Formally-Proved Algorithm to Compute the Correct Average
		  of Decimal Floating-Point Numbers},
  author	= {Boldo, Sylvie and Faissole, Florian and Tourneur,
		  Vincent},
  booktitle	= {25th IEEE Symposium on Computer Arithmetic},
  address	= {Amherst, MA, United States},
  year		= {2018},
  month		= jun,
  pdf		= {https://hal.inria.fr/hal-01772272/file/article-HAL.pdf},
  lrdedate	= {2017-05-22},
  abstract	= {Some modern processors include decimal floating-point
		  units, with a conforming implementation of the IEEE-754
		  2008 standard. Unfortunately, many algorithms from the
		  computer arithmetic literature are not correct anymore when
		  computations are done in radix 10. This is in particular
		  the case for the computation of the average of two
		  floating-point numbers. Several radix-2 algorithms are
		  available, including one that provides the correct
		  rounding, but none hold in radix 10. This paper presents a
		  new radix-10 algorithm that computes the correctly-rounded
		  average. To guarantee a higher level of confidence, we also
		  provide a Coq formal proof of our theorems, that takes
		  gradual underflow into account. Note that our formal proof
		  was generalized to ensure this algorithm is correct when
		  computations are done with any even radix.}
}