Correct Rounding of Elementary Functions in IEEE754 Formats

Publications

The paper by Brisebarre, Hanrot, Muller and Zimmermann, Correctly-rounded evaluation of a function: why, how, and at what cost? (3rd version, Feb. 2025)

The paper by Gladman, Innocente, Mather and Zimmermann, Accuracy of Mathematical Functions in Single, Double, Double Extended, and Quadruple Precision (last version: Feb. 2025)

The paper by Sibidanov and Zimmermann, Correctly rounded cubic root evaluation in double precision

TBD: simple description of main steps

Tools

Sollya: environment and library for safe floating-point code development. It is particularly targeted to the automatized implementation of mathematical floating-point libraries. In particular: certified supremum norm, fast Remez algorithm, and computation of polynomial approximation under special constraints (such as the coefficients being exactly representable as FP numbers). Authors: Chevillard, Lauter and Joldes.

Gappa: helps verifying and formally proving properties on numerical programs and circuits handling floating-point or fixed-point arithmetic. In our context: makes it possible to obtain a certified tight bound on the error committed when evaluating a polynomial that approximates a function. Author: Guillaume Melquiond.

Currently available correctly-rounded function software

The CORE-MATH project: on-the-shelf high performance open-source mathematical functions with correct rounding that can be integrated into current mathematical libraries (contains all binary32 and binary64 functions from the C23 standard except compound and lgamma).Main authors: Sibidanov and Zimmermann

LLVM LibC: the C library that comes with the LLVM compiler. All binary32 functions from the C99 standard except erfc, and the most useful binary64 functions: cbrt, cos, exp, exp2, exp10, expm1, hypot, log, log10, log1p, log2, sin, sincos, and tan

RLIBM: the most useful binary32 functions: acos, asin, atan, cos, cosh, cospi, exp, exp10, exp2, log,
log10, log2, sin, sinh, sinpi, and tan. Authors: the group of Santosh Nagarakatte at Rutgers University

BACSEL: computes worst cases for rounding. Authors: Hanrot, Lefèvre, Stehlé and Zimmermann.

Resources

Correctly-Rounded Logarithm Example

Dr. Christoph Lauter developed a correctly-rounded logarithm implementation prioritizing simplicity for educational purposes rather than maximum performance. His program is available in an archive, and he has recorded lectures explaining the implementation. Video Tutorial (Lecture and Implementation), Presentation, Download Document GitLab Repository with Implementation

Survey on Correct Rounding

A survey on correct rounding, written by Nicolas Brisebarre, Guillaume Hanrot, Paul Zimmermann, and Jean-Michel Muller, is currently under revision. The previous version is available at HAL Archive. An updated version will be shared upon completion.

Survey on Range Reduction

Work is ongoing on a survey covering range reduction techniques. A draft will be made available once it reaches a decent state.

Hardest-to-Round Cases Collection

A central repository for the hardest-to-round cases in common mathematical functions is being compiled. Currently, the largest collected list can be found at Worst Cases for Rounding, compiled by Paul Zimmermann.

In binary64 arithmetic:

they are known in the whole domain for exp, log, exp2, log2, exp10, log10, log1p, log2p1, log10p1, expm1, exp2m1, exp10m1, rsqrt, sinpi, cospi, tanpi, acospi, asinpi, atanpi, cosh, sinh, tanh, acosh, asinh, atanh, acos, asin, atan, cbrt, erf, erfc,
they are known for input values less than 2048 for sin, cos,
they are known for input values less than 10.5*pi for tan