Fast and correctly rounded logarithms in double-precision
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 1, pp. 85-102.

This article is a case study in the implementation of a portable, proven and efficient correctly rounded elementary function in double-precision. We describe the methodology used to achieve these goals in the crlibm library. There are two novel aspects to this approach. The first is the proof framework, and in general the techniques used to balance performance and provability. The second is the introduction of processor-specific optimization to get performance equivalent to the best current mathematical libraries, while trying to minimize the proof work. The implementation of the natural logarithm is detailed to illustrate these questions.

DOI : 10.1051/ita:2007003
Classification : 26-04, 65D15, 65Y99
Mots-clés : floating-point, elementary functions, logarithm, correct rounding 
@article{ITA_2007__41_1_85_0,
     author = {Dinechin, Florent de and Lauter, Christoph and Muller, Jean-Michel},
     title = {Fast and correctly rounded logarithms in double-precision},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {85--102},
     publisher = {EDP-Sciences},
     volume = {41},
     number = {1},
     year = {2007},
     doi = {10.1051/ita:2007003},
     mrnumber = {2330045},
     zbl = {1132.65302},
     language = {en},
     url = {http://www.numdam.org/articles/10.1051/ita:2007003/}
}
TY  - JOUR
AU  - Dinechin, Florent de
AU  - Lauter, Christoph
AU  - Muller, Jean-Michel
TI  - Fast and correctly rounded logarithms in double-precision
JO  - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 2007
SP  - 85
EP  - 102
VL  - 41
IS  - 1
PB  - EDP-Sciences
UR  - http://www.numdam.org/articles/10.1051/ita:2007003/
DO  - 10.1051/ita:2007003
LA  - en
ID  - ITA_2007__41_1_85_0
ER  - 
%0 Journal Article
%A Dinechin, Florent de
%A Lauter, Christoph
%A Muller, Jean-Michel
%T Fast and correctly rounded logarithms in double-precision
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2007
%P 85-102
%V 41
%N 1
%I EDP-Sciences
%U http://www.numdam.org/articles/10.1051/ita:2007003/
%R 10.1051/ita:2007003
%G en
%F ITA_2007__41_1_85_0
Dinechin, Florent de; Lauter, Christoph; Muller, Jean-Michel. Fast and correctly rounded logarithms in double-precision. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 41 (2007) no. 1, pp. 85-102. doi : 10.1051/ita:2007003. http://www.numdam.org/articles/10.1051/ita:2007003/

[1] CR-Libm, a library of correctly rounded elementary functions in double-precision. http://lipforge.ens-lyon.fr/www/crlibm/.

[2] ANSI/IEEE. Standard 754-1985 for Binary Floating-Point Arithmetic (also IEC 60559). 1985.

[3] 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). | Zbl

[4] M. Cornea, J. Harrison and P.T.P. Tang, Scientific Computing on Itanium-based Systems. Intel Press (2002).

[5] M. Daumas and G. Melquiond, Generating formally certified bounds on values and round-off errors, in 6th Conference on Real Numbers and Computers (2004).

[6] D. Defour, Cache-optimised methods for the evaluation of elementary functions. Technical Report 2002-38, LIP, École normale supérieure de Lyon (2002).

[7] F. De Dinechin and D. Defour, Software carry-save: A case study for instruction-level parallelism, in Seventh International Conference on Parallel Computing Technologies (September 2003).

[8] F. De Dinechin, D. Defour and Ch.Q. Lauter, Fast correct rounding of elementary functions in double precision using double-extended arithmetic. Technical Report 2004-10, LIP, École normale supérieure de Lyon (March 2004).

[9] F. De Dinechin, A. Ershov and N. Gast, Towards the post-ultimate libm, in 17th Symposium on Computer Arithmetic. IEEE Computer Society Press (June 2005).

[10] F. De Dinechin, Ch.Q. Lauter and G. Melquiond, Assisted verification of elementary functions using Gappa, in ACM Symposium on Applied Computing (2006).

[11] F. De Dinechin, C. Loirat and J.-M. Muller, A proven correctly rounded logarithm in double-precision, in RNC6, Real Numbers and Computers (November 2004).

[12] D. Defour, Collapsing dependent floating point operations. Technical report, DALI Research Team, LP2A, University of Perpignan, France (December 2004).

[13] D. Defour and F. De Dinechin, Software carry-save for fast multiple-precision algorithms, in 35th International Congress of Mathematical Software (2002). | Zbl

[14] D. Defour, F. De Dinechin and J.-M. Muller, Correctly rounded exponential function in double precision arithmetic, in Advanced Signal Processing Algorithms, Architectures, and Implementations X (SPIE'2000) (August 2001).

[15] T.J. Dekker, A floating point technique for extending the available precision. Numerische Mathematik 18 (1971) 224-242. | Zbl

[16] P.M. Farmwald, High bandwidth evaluation of elementary functions, in Proceedings of the 5th IEEE Symposium on Computer Arithmetic. IEEE (1981).

[17] S. Gal, Computing elementary functions: A new approach for achieving high accuracy and good performance, in Accurate Scientific Computations, Lect. Notes Comput. Sci. 235 (1986) 1-16. | Zbl

[18] D. Goldberg, What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys 23 (1991) 5-47.

[19] W. Hofschuster and W. Krämer, FI_LIB, eine schnelle und portable Funktionsbibliothek für reelle Argumente und reelle Intervalle im IEEE-double-Format. Technical Report Nr. 98/7, Institut für Wissenschaftliches Rechnen und Mathematische Modellbildung, Universität Karlsruhe (1998).

[20] ISO/IEC. International Standard ISO/IEC 9899:1999(E). Programming languages - C. 1999.

[21] R. Klatte, U. Kulisch, C. Lawo, M. Rauch and A. Wiethoff, C-XSC a C++ class library for extended scientific computing. Springer Verlag (1993). | Zbl

[22] Ch.Q. Lauter, Basic building blocks for a triple-double intermediate format. Technical Report 2005-38, LIP, École normale supérieure de Lyon (September 2005).

[23] V. Lefèvre, Moyens arithmétiques pour un calcul fiable. Ph.D. Thesis, École normale supérieure de Lyon, Lyon, France (2000).

[24] V. Lefèvre and J.-M. Muller, Worst cases for correct rounding of the elementary functions in double precision, http://perso.ens-lyon.fr/jean-michel.muller/Intro-to-TMD.htm (2004).

[25] V. Lefèvre, J.M. Muller and A. Tisserand, Towards correctly rounded transcendentals. IEEE Transactions on Computers 47 (1998) 1235-1243.

[26] IBM Accurate Portable MathLib, http://oss.software.ibm.com/ mathlib/.

[27] P. Markstein, IA-64 and Elementary Functions: Speed and Precision. Hewlett-Packard Professional Books, Prentice Hall (2000).

[28] R.E. Moore, Interval analysis. Prentice Hall (1966). | MR | Zbl

[29] MPFR, http://www.mpfr.org/.

[30] J.-M. Muller, Elementary Functions, Algorithms and Implementation. Birkhauser, Boston (1997/2005). | MR | Zbl

[31] P.T.P. Tang, Table lookup algorithms for elementary functions and their error analysis, in 10th IEEE Symposium on Computer Arithmetic. IEEE (June 1991).

[32] W.F. Wong and E. Goto, Fast hardware-based algorithms for elementary function computations using rectangular multipliers. IEEE Transactions on Computers 43 (1994) 278-294.

[33] A. Ziv, Fast evaluation of elementary mathematical functions with correctly rounded last bit. ACM Transactions on Mathematical Software 17 (1991) 410-423. | Zbl

Cité par Sources :