The CORE-MATH project

Average number of clock cycles needed by CORE-MATH functions (revision 55c872b, f5d9e09 for log2l, f8f982e for expl) on an Intel Xeon Silver 4214, with GCC 13.2.0, compared to GNU libc 2.37, the Intel Math Library from icx 2023.2.0 and LLVM libc (revision d099dbb):

Usages of CORE-MATH:

• branch core-math of LibmCS, the Mathematical Library for Critical Systems developed by the European Space Agency

Available CORE-MATH functions (under MIT license):

Caption:

• code: pointer to the main CORE-MATH code foo.c. Note that it might require some header files present in the same directory. For example the log function needs the dint.h header file available from the [git] link on top of this page, then follow src, binary64, and log.
• llvm: pointer to a correctly-rounded implementation in llvm-libc
• proof: a paper proof of the correctness of the algorithm
• (1) tested on hard-to-round cases |x| < 2^-34
• (2) only for rounding to nearest

Notes:

• correct rounding is claimed for all IEEE-754 rounding modes. For univariate binary32 functions it is checked by exhaustive search. For bivariate functions or larger formats it is checked only with respect to known hard-to-round cases. If you find an input which is not correctly rounded, please send it to paul dot zimmermann @ inria dot fr.
• these implementations only care about correct rounding for regular numbers, they do not necessarily correctly deal with NaN, infinities or zero, set the underflow and overflow exceptions, nor the inexact flag.
• these implementations were tested on x86_64-linux, with and without the use of fma (fused multiply add).

Other correctly-rounded implementations:

• CRlibm this is a mirror of the original CRlibm project (which is no more available). CRlibm is no longer maintained, but contains very useful resources: provides binary64 exp, log, cos, sin, tan, cospi, sinpi, tanpi, atan, atanpi, cosh, sinh, log2, log10, asin, acos, asinpi, acospi, expm1, log1p, exp2, pow (only for rounding to nearest for pow).
• RLIBM provides binary32 log, log2, log10, exp, exp2, exp10, sinh, cosh, sinpi, cospi, sin, cos, tan, atan, asin, acos for all rounding modes.
• LLVM-libc provides some correctly rounded functions (see links below): claimed accuracy of LLVM functions
• JuliaIntervals provides elementary functions with directed rounding wrapping CRlibm.