Fast and correctly rounded logarithms in double-precision

Florent de Dinechin; Christoph Lauter; Jean-Michel Muller

RAIRO - Theoretical Informatics and Applications (2007)

  • Volume: 41, Issue: 1, page 85-102
  • ISSN: 0988-3754

Abstract

top
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.

How to cite

top

de Dinechin, Florent, Lauter, Christoph, and Muller, Jean-Michel. "Fast and correctly rounded logarithms in double-precision." RAIRO - Theoretical Informatics and Applications 41.1 (2007): 85-102. <http://eudml.org/doc/250078>.

@article{deDinechin2007,
abstract = { 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. },
author = {de Dinechin, Florent, Lauter, Christoph, Muller, Jean-Michel},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Floating-point; elementary functions; logarithm; correct rounding.},
language = {eng},
month = {4},
number = {1},
pages = {85-102},
publisher = {EDP Sciences},
title = {Fast and correctly rounded logarithms in double-precision},
url = {http://eudml.org/doc/250078},
volume = {41},
year = {2007},
}

TY - JOUR
AU - de Dinechin, Florent
AU - Lauter, Christoph
AU - Muller, Jean-Michel
TI - Fast and correctly rounded logarithms in double-precision
JO - RAIRO - Theoretical Informatics and Applications
DA - 2007/4//
PB - EDP Sciences
VL - 41
IS - 1
SP - 85
EP - 102
AB - 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.
LA - eng
KW - Floating-point; elementary functions; logarithm; correct rounding.
UR - http://eudml.org/doc/250078
ER -

References

top
  1. CR-Libm, a library of correctly rounded elementary functions in double-precision. .  URIhttp://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).  
  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).  
  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 Mathematik18 (1971) 224–242.  
  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.  
  18. D. Goldberg, What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys23 (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).  
  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, (2004).  URIhttp://perso.ens-lyon.fr/jean-michel.muller/Intro-to-TMD.htm
  25. V. Lefèvre, J.M. Muller and A. Tisserand, Towards correctly rounded transcendentals. IEEE Transactions on Computers47 (1998) 1235–1243.  
  26. IBM Accurate Portable MathLib, .  URIhttp://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).  
  29. MPFR, .  URIhttp://www.mpfr.org/
  30. J.-M. Muller, Elementary Functions, Algorithms and Implementation. Birkhauser, Boston (1997/2005).  
  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 Computers43 (1994) 278–294.  
  33. A. Ziv, Fast evaluation of elementary mathematical functions with correctly rounded last bit. ACM Transactions on Mathematical Software17 (1991) 410–423.  

NotesEmbed ?

top

You must be logged in to post comments.