No CrossRef data available.
Article contents
Fast and correctly rounded logarithmsin double-precision
Published online by Cambridge University Press: 24 April 2007
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.
Information
- Type
- Research Article
- Information
- RAIRO - Theoretical Informatics and Applications , Volume 41 , Issue 1: Real Numbers , January 2007 , pp. 85 - 102
- Copyright
- © EDP Sciences, 2007
References
CR-Libm, a library of correctly rounded elementary functions in double-precision. http://lipforge.ens-lyon.fr/www/crlibm/.
ANSI/IEEE. Standard 754-1985 for Binary Floating-Point Arithmetic (also IEC 60559). 1985.
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).
M. Cornea, J. Harrison and P.T.P. Tang, Scientific Computing on Itanium-based Systems. Intel Press (2002).
M. Daumas and G. Melquiond, Generating formally certified bounds on values and round-off errors, in 6th Conference on Real Numbers and Computers (2004).
D. Defour, Cache-optimised methods for the evaluation of elementary functions. Technical Report 2002-38, LIP, École normale supérieure de Lyon (2002).
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).
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).
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).
F. de Dinechin, Ch.Q. Lauter and G. Melquiond, Assisted verification of elementary functions using Gappa, in ACM Symposium on Applied Computing (2006).
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).
D. Defour, Collapsing dependent floating point operations. Technical report, DALI Research Team, LP2A, University of Perpignan, France (December 2004).
D. Defour and F. de Dinechin, Software carry-save for fast multiple-precision algorithms, in 35th International Congress of Mathematical Software (2002).
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).
Dekker, T.J., A floating point technique for extending the available precision.
Numerische Mathematik
18 (1971) 224–242.
CrossRef
P.M. Farmwald, High bandwidth evaluation of elementary functions, in Proceedings of the 5th IEEE Symposium on Computer Arithmetic. IEEE (1981).
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.
Goldberg, D., What every computer scientist should know about floating-point arithmetic.
ACM Computing Surveys
23 (1991) 5–47.
CrossRef
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).
ISO/IEC. International Standard ISO/IEC 9899:1999(E). Programming languages – C. 1999.
R. Klatte, U. Kulisch, C. Lawo, M. Rauch and A. Wiethoff, C-XSC a C++ class library for extended scientific computing. Springer Verlag (1993).
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).
V. Lefèvre, Moyens arithmétiques pour un calcul fiable. Ph.D. Thesis, École normale supérieure de Lyon, Lyon, France (2000).
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).
Lefèvre, V., Muller, J.M. and Tisserand, A., Towards correctly rounded transcendentals.
IEEE Transactions on Computers
47 (1998) 1235–1243.
CrossRef
IBM Accurate Portable MathLib, http://oss.software.ibm.com/mathlib/.
P. Markstein, IA-64 and Elementary Functions: Speed and Precision. Hewlett-Packard Professional Books, Prentice Hall (2000).
R.E. Moore, Interval analysis. Prentice Hall (1966).
MPFR, http://www.mpfr.org/.
J.-M. Muller, Elementary Functions, Algorithms and Implementation. Birkhauser, Boston (1997/2005).
P.T.P. Tang, Table lookup algorithms for elementary functions and their error analysis, in 10th IEEE Symposium on Computer Arithmetic. IEEE (June 1991).
Wong, W.F. and Goto, E., Fast hardware-based algorithms for elementary function computations using rectangular multipliers.
IEEE Transactions on Computers
43 (1994) 278–294.
CrossRef
Ziv, A., Fast evaluation of elementary mathematical functions with correctly rounded last bit.
ACM Transactions on Mathematical Software
17 (1991) 410–423.
CrossRef
- 29
- Cited by