Les Newsletters Interstices
    Niveau facile
    Niveau 1 : Facile

    MPFR : vers un calcul flottant correct ?

    Sécurité & Vie privée
    Obtenir un seul résultat pour un calcul donné : à première vue, cela semble une évidence ; c'est en fait un vaste sujet de recherche auquel les chercheurs apportent petit à petit leurs contributions. Une nouvelle étape est franchie aujourd'hui grâce à MPFR, une bibliothèque de calcul multi-précision sur les nombres flottants.

    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.

    valeurs du Handbook of Mathematical Functions
    valeurs calculées avec MPFR

    Quelques valeurs : à gauche, celles publiées dans le « Handbook of Mathematical Functions » et à droite, celles calculées avec MPFR.
    Par exemple, en 4e ligne, la valeur de 101/5 sur 22 chiffres vaut 1.584893192461113485202, ce qui arrondi au plus proche donne 1.5848931924611134852 comme indiqué par MPFR, et non 1.5848931924611134853.

     

    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 !

    Précision (en bits) :
    (entrer une valeur entre 64 et 8192)
    Formule :
    La formule s’écrit comme dans une calculette et peut utiliser

    • les fonctions
      sqrt (racine carrée), exp, log, log10, log2,
      sin, cos, tan, sinh, cosh, tanh
    • les opérateurs arithmétiques +, -, *, /, ^
    • ainsi que les constantes numériques ou pi.
     

     

    Le résultat du calcul s’affiche dans une nouvelle fenêtre.

     

    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.

    Si vous souhaitez expliquer votre choix, vous pouvez ajouter un commentaire (Il ne sera pas publié).

    Votre choix a été pris en compte. Merci d'avoir estimé le niveau de ce document !

    Paul Zimmermann

    Directeur de recherche Inria dans l'équipe CACAO.
    Voir le profil

    Ces articles peuvent vous intéresser

    ArticleSécurité & Vie privée
    Algorithmes

    Le « dilemme du fabricant de tables » ou comment calculer juste

    Anita Castiel
    Vincent Lefèvre
    Paul Zimmermann

    Niveau intermédiaire
    Niveau 2 : Intermédiaire