MPFR : vers un calcul flottant correct ?
Qui n’a jamais vu s’afficher sur sa calculatrice 2,9999 ou 3,0001 ? Voici un des avatars du calcul avec des nombres à virgule flottante, plus couramment appelés nombres flottants. De tels résultats peuvent cependant s’expliquer. En effet, le résultat d’un calcul flottant, par exemple 1.0/3.0, n’est pas toujours représentable exactement ; il faut choisir entre 0,33333 et 0,33334. C’est ce qu’on appelle un arrondi. Plus gênant est le fait que le même calcul donne 0,33333 sur une machine et 0,33334 sur une autre. Imaginons les dérives que cela peut engendrer pour des calculs d’intérêt portant sur des milliards d’euros ! C’est le problème de la portabilité.
Ce problème peut être illustré par l’exemple « classique » du calcul de sin 1022 en double précision, qui donne des résultats très différents suivant le processeur, le système ou le compilateur qui l’exécute.
Pour en savoir plus sur ce sujet, voir le livre (en anglais) de Jean-Michel Muller, Elementary Functions. Algorithms and Implementation (Birkhauser, 1997).
En double précision, la norme IEEE 754 régit la manière dont les calculs flottants sont effectués sur le processeur, en particulier l’arrondi. La conséquence majeure est que les programmes utilisant l’arithmétique flottante du processeur sont globalement plus précis et plus portables, et des algorithmes basés sur cette norme peuvent être écrits et prouvés facilement.
En précision arbitraire, il n’existe pour l’instant aucune norme. Depuis 1999, plusieurs chercheurs du Loria ont entrepris de développer une bibliothèque, nommée MPFR, de calcul flottant en précision arbitraire.
 |
 |
|
Quelques valeurs : à gauche, celles publiées dans le « Handbook of Mathematical Functions » et à droite, celles calculées avec MPFR. |
|
Cette bibliothèque, diffusée sous forme de logiciel libre, sous la licence LGPL, reprend la philosophie de la norme IEEE 754, notamment la notion d’arrondi. Les calculs effectués via MPFR donnent ainsi un même résultat, quel que soit l’environnement (processeur, compilateur ou système d’exploitation).
La licence sous laquelle est diffusée MPFR est la GNU Lesser General Public License, plus connue sous le nom de LGPL. Comme sa grande sœur GPL, cette licence permet l’utilisation, la modification et la redistribution de MPFR, et est héréditaire, c’est-à-dire qu’elle interdit de priver les utilisateurs de versions modifiées de ces droits. La différence principale avec GPL est que la LGPL permet l’utilisation dans un logiciel non libre, en particulier un logiciel commercial. Par exemple, on pourrait imaginer qu’Excel utilise MPFR, ce qui serait impossible avec la licence GPL.
Concilier exactitude et efficacité
Il faut souligner que lorsqu’on dispose d’une spécification formelle comme dans MPFR, il n’y a qu’un seul résultat correct pour un calcul donné. En effet, à toute entrée (fonction, nombre flottant, précision, arrondi) correspond une et une seule sortie correcte (et non pas à plus ou moins 1 ou 2 chiffres comme le font la plupart des logiciels). Cela rend plus difficile l’obtention de ce résultat, mais cela facilite la recherche de « bugs », et surtout cela permet d’avoir des fondations solides pour construire d’autres logiciels.
Une bibliothèque telle que MPFR a de nombreuses applications. On peut s’en servir pour vérifier les résultats obtenus en double précision (voir le fameux « bug du Pentium »). MPFR permet aussi d’effectuer avec une plus grande précision certains calculs critiques : cela permet d’estimer la stabilité numérique d’un algorithme, ou d’évaluer l’erreur d’arrondi d’un calcul en double précision. Enfin, MPFR permet aussi de calculer avec arrondi correct les fonctions mathématiques qui ne sont pas standardisées par la norme IEEE 754, telles que le sinus, l’exponentielle ou le logarithme. C’est pour cette dernière application que MPFR est depuis peu utilisée dans le compilateur GNU GFORTRAN.
Supposons un programme contenant l’instruction d = sin(1.234), où d est une variable flottante, et supposons que le mode d’arrondi pour cette instruction peut être déterminé à la compilation, alors la valeur stockée dans d sera la même pour toutes les exécutions du programme. (On dit alors qu’elle peut être déterminée statiquement ou à « compile-time » en anglais).
Jusqu’alors, le compilateur faisait appel à la bibliothèque mathématique de la machine (LIBM pour le langage C), ce qui a l’inconvénient de donner des résultats différents suivant la machine utilisée, car la norme IEEE 754 ne spécifie pas ces fonctions.
Maintenant, le compilateur (GFORTRAN et bientôt GCC) appelle la bibliothèque MPFR, qui elle garantit un résultat indépendant de la machine, donc la valeur stockée dans la variable d sera bien la même, quelle que soit la machine utilisée.
Testez MPFR !
Cette applet a été écrite avec GMP et MPFRpar Tomonori Kouya
avec le soutien du Research Institute of Systems Planning Inc.
La principale motivation pour développer MPFR était de montrer qu’il est possible de calculer sur des flottants en précision arbitraire avec une spécification formelle, comme c’est déjà le cas en double précision grâce à la norme IEEE 754, sans perte notable d’efficacité par rapport à d’autres outils sans spécification formelle. Il semble que ce pari soit réussi. Il reste cependant beaucoup à faire, notamment à convaincre les développeurs (et surtout les utilisateurs !) d’outils de calcul flottant en précision arbitraire de l’intérêt d’une spécification formelle.
Newsletter
Le responsable de ce traitement est Inria. En saisissant votre adresse mail, vous consentez à recevoir chaque mois une sélection d'articles et à ce que vos données soient collectées et stockées comme décrit dans notre politique de confidentialité
Niveau de lecture
Aidez-nous à évaluer le niveau de lecture de ce document.
Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !
