Fast and correctly rounded logarithms in double-precision
Open Access
- 1 January 2007
- journal article
- Published by EDP Sciences in RAIRO - Theoretical Informatics and Applications
- Vol. 41 (1), 85-102
- https://doi.org/10.1051/ita:2007003
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.Keywords
This publication has 11 references indexed in Scilit:
- Assisted verification of elementary functions using GappaPublished by Association for Computing Machinery (ACM) ,2006
- Interactive Theorem Proving and Program DevelopmentTexts in Theoretical Computer Science. An EATCS Series, 2004
- SOFTWARE CARRY-SAVE FOR FAST MULTIPLE-PRECISION ALGORITHMSPublished by World Scientific Pub Co Pte Ltd ,2002
- Correctly rounded exponential function in double-precision arithmeticPublished by SPIE-Intl Soc Optical Eng ,2001
- Toward correctly rounded transcendentalsIEEE Transactions on Computers, 1998
- Fast hardware-based algorithms for elementary function computations using rectangular multipliersIEEE Transactions on Computers, 1994
- Fast evaluation of elementary mathematical functions with correctly rounded last bitACM Transactions on Mathematical Software, 1991
- What every computer scientist should know about floating-point arithmeticACM Computing Surveys, 1991
- High bandwidth evaluation of elementary functionsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1981
- A floating-point technique for extending the available precisionNumerische Mathematik, 1971