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.
@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},
volume = {41},
year = {2007},
pages = {85-102},
doi = {10.1051/ita:2007003},
mrnumber = {2330045},
zbl = {1132.65302},
language = {en},
url = {http://dml.mathdoc.fr/item/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) pp. 85-102. doi : 10.1051/ita:2007003. http://gdmltest.u-ga.fr/item/ITA_2007__41_1_85_0/
[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] and, Interactive Theorem Proving and Program Development. Coq'Art: the Calculus of Inductive Constructions. Texts in Theoretical Computer Science, Springer Verlag (2004). | Zbl 1069.68095
[4] , and, Scientific Computing on Itanium-based Systems. Intel Press (2002).
[5] and, Generating formally certified bounds on values and round-off errors, in 6th Conference on Real Numbers and Computers (2004).
[6] , Cache-optimised methods for the evaluation of elementary functions. Technical Report 2002-38, LIP, École normale supérieure de Lyon (2002).
[7] and, Software carry-save: A case study for instruction-level parallelism, in Seventh International Conference on Parallel Computing Technologies (September 2003).
[8] , and, 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] , and, Towards the post-ultimate libm, in 17th Symposium on Computer Arithmetic. IEEE Computer Society Press (June 2005).
[10] , and, Assisted verification of elementary functions using Gappa, in ACM Symposium on Applied Computing (2006).
[11] , and, A proven correctly rounded logarithm in double-precision, in RNC6, Real Numbers and Computers (November 2004).
[12] , Collapsing dependent floating point operations. Technical report, DALI Research Team, LP2A, University of Perpignan, France (December 2004).
[13] and, Software carry-save for fast multiple-precision algorithms, in 35th International Congress of Mathematical Software (2002). | Zbl 1057.68138
[14] , and, Correctly rounded exponential function in double precision arithmetic, in Advanced Signal Processing Algorithms, Architectures, and Implementations X (SPIE'2000) (August 2001).
[15] , A floating point technique for extending the available precision. Numerische Mathematik 18 (1971) 224-242. | Zbl 0226.65034
[16] , High bandwidth evaluation of elementary functions, in Proceedings of the 5th IEEE Symposium on Computer Arithmetic. IEEE (1981).
[17] , 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 0605.65011
[18] , What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys 23 (1991) 5-47.
[19] and, 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] ,,, and, C-XSC a C++ class library for extended scientific computing. Springer Verlag (1993). | Zbl 0814.68035
[22] , Basic building blocks for a triple-double intermediate format. Technical Report 2005-38, LIP, École normale supérieure de Lyon (September 2005).
[23] , Moyens arithmétiques pour un calcul fiable. Ph.D. Thesis, École normale supérieure de Lyon, Lyon, France (2000).
[24] and, 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] , and, Towards correctly rounded transcendentals. IEEE Transactions on Computers 47 (1998) 1235-1243.
[26] IBM Accurate Portable MathLib, http://oss.software.ibm.com/ mathlib/.
[27] , IA-64 and Elementary Functions: Speed and Precision. Hewlett-Packard Professional Books, Prentice Hall (2000).
[28] , Interval analysis. Prentice Hall (1966). | MR 231516 | Zbl 0176.13301
[29] MPFR, http://www.mpfr.org/.
[30] , Elementary Functions, Algorithms and Implementation. Birkhauser, Boston (1997/2005). | MR 1452106 | Zbl 0892.65005
[31] , Table lookup algorithms for elementary functions and their error analysis, in 10th IEEE Symposium on Computer Arithmetic. IEEE (June 1991).
[32] and, Fast hardware-based algorithms for elementary function computations using rectangular multipliers. IEEE Transactions on Computers 43 (1994) 278-294.
[33] , Fast evaluation of elementary mathematical functions with correctly rounded last bit. ACM Transactions on Mathematical Software 17 (1991) 410-423. | Zbl 0900.65038