This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd
April 2008 (vol. 57 no. 4)
pp. 462-471
Rounding to odd is a non-standard rounding on floating-point numbers. By using it for some intermediate values instead of rounding to nearest, correctly rounded results can be obtained at the end of computations. We present an algorithm to emulate the fused multiply-and-add operator. We also present an iterative algorithm for computing the correctly rounded sum of a set floating-point numbers under mild assumptions. A variation on both previous algorithms is the correctly rounded sum of any three floating-point numbers. This leads to efficient implementations, even when this rounding is not available. In order to guarantee the correctness of these properties and algorithms, we formally proved them using the Coq proof checker.

[1] D. Stevenson et al., “A Proposed Standard for Binary Floating Point Arithmetic,” Computer, vol. 14, no. 3, pp. 51-62, Mar. 1981.
[2] D. Stevenson et al., “An American National Standard: IEEE Standard for Binary Floating-Point Arithmetic,” ACM SIGPLAN Notices, vol. 22, no. 2, pp. 9-25, 1987.
[3] G. Melquiond and S. Pion, “Formally Certified Floating-Point Filters for Homogeneous Geometric Predicates,” Theoretical Informatics and Applications, vol. 41, no. 1, pp. 57-70, 2007.
[4] S.A. Figueroa, “When Is Double Rounding Innocuous,” SIGNUM Newsletter, vol. 30, no. 3, pp. 21-26, 1995.
[5] J. von Neumann, “First Draft of a Report on the EDVAC,” IEEE Annals of the History of Computing, vol. 15, no. 4, pp. 27-75, 1993.
[6] D. Goldberg, “What Every Computer Scientist Should Know about Floating-Point Arithmetic,” ACM Computing Surveys, vol. 23, no. 1, pp. 5-47, 1991.
[7] M.D. Ercegovac and T. Lang, Digital Arithmetic. Morgan Kaufmann, 2004.
[8] C. Lee, “Multistep Gradual Rounding,” IEEE Trans. Computers, vol. 38, no. 4, pp. 595-600, Apr. 1989.
[9] M. Daumas, L. Rideau, and L. Théry, “A Generic Library of Floating-Point Numbers and Its Application to Exact Computing,” Proc. 14th Int'l Conf. Theorem Proving in Higher Order Logics, pp.169-184, 2001.
[10] Y. Bertot and P. Casteran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag, 2004.
[11] S. Boldo, “Preuves Formelles en Arithmétiques à Virgule Flottante,” PhD dissertation, École Normale Supérieure de Lyon, Nov. 2004.
[12] S. Boldo and G. Melquiond, “When Double Rounding Is Odd,” Proc. 17th IMACS World Congress Computational and Applied Math., 2005.
[13] T.J. Dekker, “A Floating-Point Technique for Extending the Available Precision,” Numerische Mathematik, vol. 18, no. 3, pp.224-242, 1971.
[14] D.E. Knuth, The Art of Computer Programming: Seminumerical Algorithms, vol. 2. Addison Wesley, 1969.
[15] S. Boldo, “Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms,” Proc. Third Int'l Joint Conf. Automated Reasoning, 2006.
[16] N.J. Higham, Accuracy and Stability of Numerical Algorithms. SIAM, 1996.
[17] J.W. Demmel and Y. Hida, “Fast and Accurate Floating Point Summation with Applications to Computational Geometry,” Proc. 10th GAMM-IMACS Int'l Symp. Scientific Computing, Computer Arithmetic, and Validated Numerics, 2002.
[18] T. Ogita, S.M. Rump, and S. Oishi, “Accurate Sum and Dot Product,” SIAM J. Scientific Computing, vol. 26, no. 6, pp. 1955-1988, 2005.
[19] D.M. Priest, “Algorithms for Arbitrary Precision Floating-Point Arithmetic,” Proc. 10th IEEE Symp. Computer Arithmetic, pp. 132-144, 1991.
[20] M. Daumas, “Multiplications of Floating Point Expansions,” Proc. 14th IEEE Symp. Computer Arithmetic, pp. 250-257, 1999.
[21] F. de Dinechin, C.Q. Lauter, and J.-M. Muller, “Fast and Correctly Rounded Logarithms in Double Precision,” Theoretical Informatics and Applications, vol. 41, no. 1, pp. 85-102, 2007.
[22] C.Q. Lauter, “Basic Building Blocks for a Triple-Double Intermediate Format,” Technical Report RR2005-38, LIP, Sept. 2005.
[23] V. Lefèvre and J.-M. Muller, “Worst Cases for Correct Rounding of the Elementary Functions in Double Precision,” Proc. 15th IEEE Symp. Computer Arithmetic, pp. 111-118, 2001.

Index Terms:
Computer arithmetic, Verification
Citation:
Sylvie Boldo, Guillaume Melquiond, "Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd," IEEE Transactions on Computers, vol. 57, no. 4, pp. 462-471, April 2008, doi:10.1109/TC.2007.70819
Usage of this product signifies your acceptance of the Terms of Use.