This Article 
 Bibliographic References 
 Add to: 
Formally Verified Argument Reduction with a Fused Multiply-Add
August 2009 (vol. 58 no. 8)
pp. 1139-1145
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, 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, 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, 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$ , 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,, 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,, 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, , 1998.
[16] J. Harrison, “Floating Point Verification in HOL Light: The Exponential Function,” Technical Report 428, Univ. of Cambridge Computer Laboratory,, 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,, 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, 24269101.pdf, 1996.
[23] K.C. Ng, Argument Reduction for Huge Arguments: Good to the Last Bit, work in progress,, 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, 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.
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.