L'INRIA développe actuellement une bibliothèque mathématique avec arrondi correct : crlibm. Il existe déjà des bibliothèques similaires comme libultim, libmcr ou MPFR, mais elles sont peu performantes. Un arrondi correct signifie que tous les chiffres du résultat sont exacts, alors que les bibliothèques mathématiques standards ne calculent qu'un résultat approché (chiffres les moins significatifs). En l'occurrence, il s'agit des fonctions cos(x), sqrt(x), log(x), etc.

libultim

Abraham Ziv est l'auteur du premier algorithme de calcul avec arrondi correct : la stratégie de l'oignon. Elle consiste à calculer avec une certaine précision : si on peut déterminer l'arrondi correct on s'arrête, sinon on recalcule avec une précision plus importante. On recommence jusqu'à ce qu'on puisse arrondir correctement. Ziv a implémenté cette technique dans la bibliothèque libultim (Accurate Portable Mathlib) pour IBM. La méthode a été publiée en 1991 : Fast evaluation of elementary mathematical functions with correctly rounded last bit.

libultim souffre de plusieurs défauts : le calcul est lent (particulièrement dans les « pires cas »), les algorithmes ne sont pas prouvés, et seul l'arrondi au plus près (nearest) est implémenté (il existe 3 autres modes : zéro, -inf, +inf).

libultim est distribué sous licence LGPL, mais je n'ai pas réussi à retrouver sa trace. Son site web est accessible par les archives du web : http://oss.software.ibm.com/mathlib/ (archives de 2005).

MPFR

La bibliothèque MPFR permet de faire des calculs sur des nombres flottants multi précision. Elle contient les fonctions trigonométriques, la fonction exponentielle, etc. avec arrondi correct. Les calculs utilisent des nombres entiers multi précision (bibliothèque GMP).

MPFR est développé par l'INRIA et distribué sous licence LGPL. La dernière version date de janvier 2009.

scslib

Les processeurs récents ont des unités de calcul en nombre flottant très rapides, parfois plus rapides que les calculs en nombres entiers. La bibliothèque scslib (The Software Carry-Save Multiple-Precision Library) permet de faire des calculs (a + b, a × b, etc.) multi précision sur des nombres flottants en stockant chaque valeur dans plusieurs nombres flottants. La conversion entre un nombre multi précision et un flottant IEEE 754 est très rapide, en comparaison de MPFR (qui utilise des nombres entiers) par exemple. L'article Software carry-save for fast multiple-precision algorithms (2002) présente en détail les concepts et astuces utilisées.

scslib est distribué sous licence LGPL. La dernière version date de 2003.

crlibm

Le travail sur crlibm (correctly rounded mathematical library) a débuté par l'étude des pires cas par Jean-Michel Muller et Vincent Lefèvre. Ils ont par exemple calculé que l'arrondi arrondi correct en double précision (53 bits) nécessite au maximum un calcul sur 118 bits pour le logarithme. crlibm utilise la bibliothèque scslib pour le calcul multi précision sur les nombres flottants. Les algorithmes sont prouvés, un logiciel de génération de preuve a été écrit pour l'occasion. Les performances sont bonnes en comparaison des autres bibliothèques de calcul en arrondi correct, mais restent plus faibles que celles des bibliothèques mathématiques standards (arrondi inexact).

Publications liées à crlibm :

Fin 2007, crlibm a été proposé pour l'inclusion dans GCC, mais a été refusé : Using crlibm as the default math library in GCC sources.

crlibm est distribué sous licence LGPL. La dernière version date d'octobre 2008. Voir aussi la page du projet sur LipForge.