This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formally Verified Argument Reduction with a Fused Multiply-Add
August 2009 (vol. 58 no. 8)
pp. 1139-1145
ASCII Text
x 
 
Sylvie Boldo, Marc Daumas, Ren-Cang Li, "Formally Verified Argument Reduction with a Fused Multiply-Add," IEEE Transactions on Computers, vol. 58, no. 8, pp. 1139-1145, August, 2009.
 
 
BibTex
x
 
@article{ 10.1109/TC.2008.216,
author = {Sylvie Boldo and Marc Daumas and Ren-Cang Li},
title = {Formally Verified Argument Reduction with a Fused Multiply-Add},
journal ={IEEE Transactions on Computers},
volume = {58},
number = {8},
issn = {0018-9340},
year = {2009},
pages = {1139-1145},
doi = {http://doi.ieeecomputersociety.org/10.1109/TC.2008.216},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Computers
TI - Formally Verified Argument Reduction with a Fused Multiply-Add
IS - 8
SN - 0018-9340
SP1139
EP1145
EPD - 1139-1145
A1 - Sylvie Boldo,
A1 - Marc Daumas,
A1 - Ren-Cang Li,
PY - 2009
KW - Argument reduction
KW - fma
KW - formal proof
KW - Coq.
VL - 58
JA - IEEE Transactions on Computers
ER -
 
Sylvie Boldo, INRIA Saclay, Orsay
Marc Daumas, ELIAUS, UPVD, Perpignan
Ren-Cang Li, University of Texas at Arlington, Arlington
The Cody and Waite argument reduction technique works perfectly for reasonably large arguments, but as the input grows, there are no bits left to approximate the constant with enough accuracy. Under mild assumptions, we show that the result computed with a fused multiply-add provides a fully accurate result for many possible values of the input with a constant almost accurate to the full working precision. We also present an algorithm for a fully accurate second reduction step to reach full double accuracy (all the significand bits of two numbers are accurate) even in the worst cases of argument reduction. Our work recalls the common algorithms and presents proofs of correctness. All the proofs are formally verified using the Coq automatic proof checker.

[1] P. Markstein, IA-64 and Elementary Functions: Speed and Precision. Prentice Hall, 2000.
[2] N. Brisebarre, D. Defour, P. Kornerup, J.-M. Muller, and N. Revol, “A New Range-Reduction Algorithm,” IEEE Trans. Computers, vol. 54, no. 3, pp. 331-339, Mar. 2005.
[3] J.-M. Muller, Elementary Functions, Algorithms and Implementation. Birkhauser, http://www.springer.com/west/home/birkhauser computer+ science?SGWID=4-40353-22-72377986-0 , 2006.
[4] R.-C. Li, “Near Optimality of Chebyshev Interpolation for Elementary Function Computations,” IEEE Trans. Computers, vol. 53, no. 6, pp. 678-687, June 2004.
[5] W.J. Cody and W. Waite, Software Manual for Elementary Functions. Prentice Hall, 1980.
[6] P.W. Markstein, “Computation of Elementary Functions on the IBM RISC System/6000 Processor,” IBM J. Research and Development, vol. 34, no. 1, pp.111-119, http://www.research.ibm.com/journal/rd/341 ibmrd3401N.pdf, 1990.
[7] S. Story and P.T.P. Tang, “New Algorithms for Improved Transcendental Function on IA-64,” Proc. 14th IEEE Symp. Computer Arithmetic (ARITH'99), I. Koren and P. Kornerup, eds., pp. 4-11, http://computer.org/proceedings/arith/0116 0116toc.htm, 1999.
[8] R.-C. Li, S. Boldo, and M. Daumas, “Theorems on Efficient Argument Reductions,” Proc. 16th IEEE Symp. Computer Arithmetic (ARITH '03), J.-C.Bajard and M. Schulte, eds., pp. 129-136, http://hal.archives- ouvertes.frhal-00156244 , 2003.
[9] W. Kahan, Minimizing $q \times m - n$ , http://www.cs.berkeley.edu/~wkahan/testpi nearpi.c, 1983.
[10] J. Harrison, “A Machine-Checked Theory of Floating Point Arithmetic,” Proc. 12th Int'l Conf. Theorem Proving in Higher Order Logics (TPHOLs '99), Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, eds., pp.113-130, http://www.cl.cam.ac.uk/users/jrh/papers fparith.ps.gz, 1999.
[11] J. Harrison, “Formal Verification of Floating Point Trigonometric Functions,” Proc. Third Int'l Conf. Formal Methods in Computer-Aided Design (FMCAD '00), W.A. Hunt and S.D. Johnson, eds., pp. 217-233, 2000.
[12] 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 (TPHOLs '01), pp. 169-184, http://hal.archives-ouvertes.frhal-00157285 , 2001.
[13] Y. Bertot and P. Castéran, “Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions,” Texts in Theoretical Computer Science. Springer, 2004.
[14] V.A. Carreño and P.S. Miner, “Specification of the IEEE-854 Floating-Point Standard in HOL and PVS,” Proc. 1995 Int'l Workshop Higher Order Logic Theorem Proving and Its Applications, http://shemesh.larc.nasa.gov/fm/ftp/larc/ vachug95.ps, 1995.
[15] D.M. Russinoff, “A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division and Square Root Algorithms of the AMD-K7 Processor,” LMS J. Computation and Math., vol. 1, pp. 148-200, http://www.onr.com/user/russ/davidk7-div-sqrt.ps , 1998.
[16] J. Harrison, “Floating Point Verification in HOL Light: The Exponential Function,” Technical Report 428, Univ. of Cambridge Computer Laboratory, http://www.cl.cam.ac.uk/users/jrh/papers tang.ps.gz, 1997.
[17] P.H. Sterbenz, Floating Point Computation. Prentice Hall, 1974.
[18] D. Goldberg, “What Every Computer Scientist Should Know about Floating Point Arithmetic,” ACM Computing Surveys, vol. 23, no. 1, pp. 5-47, http://doi.acm.org/10.1145103162.103163, 1991.
[19] S. Boldo and M. Daumas, “Properties of Two's Complement Floating Point Notations,” Int'l J. Software Tools for Technology Transfer, vol. 5, nos. 2/3, pp.237-246, http://hal.archives-ouvertes.frhal-00157268 , 2004.
[20] 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.
[21] W.J. Cody, R. Karpinski et al., “A Proposed Radix and Word-Length Independent Standard for Floating Point Arithmetic,” IEEE Micro, vol. 4, no. 4, pp. 86-100, 1984.
[22] Pentium Pro Family: Developer's Manual, Programmer's Reference Manual, Intel, ftp://download.intel.com/design/pro/manuals 24269101.pdf, 1996.
[23] K.C. Ng, Argument Reduction for Huge Arguments: Good to the Last Bit, work in progress, http://www.validgh.comarg.ps, 1992.
[24] S. Boldo and J.-M. Muller, “Some Functions Computable with a Fused-MAC,” Proc. 17th IEEE Symp. Computer Arithmetic (ARITH '05), P. Montuschi and E. Schwarz, eds., pp. 52-58, http://csdl.computer. org/comp/proceedings arith/, 2005.
[25] A.H. Karp and P. Markstein, “High-Precision Division and Square Root,” ACM Trans. Math. Software, vol. 23, no. 4, pp. 561-589, Dec. 1997.
[26] J.F. Reiser and D.E. Knuth, “Evading the Drift in Floating Point Addition,” Information Processing Letters, vol. 3, no. 3, pp. 84-87, 1975.

Index Terms:
Argument reduction, fma, formal proof, Coq.
Citation:
Sylvie Boldo, Marc Daumas, Ren-Cang Li, "Formally Verified Argument Reduction with a Fused Multiply-Add," IEEE Transactions on Computers, vol. 58, no. 8, pp. 1139-1145, Aug. 2009, doi:10.1109/TC.2008.216
Usage of this product signifies your acceptance of the Terms of Use.