Arithmétique des Ordinateurs Certifiée
AOC

Proposition d'Action de Recherche Coopérative
Promoteur: projet LEMME

Novembre 1999








Résumé

La conception de logiciels numériques certifiés n'a de sens que si l'arithmétique élémentaire utilisée par ces logiciels est, elle aussi, certifiée. Des exemples récents montrent que ceci n'est pas forcément évident et que de la recherche reste à faire dans ce domaine. On désire faire collaborer des équipes travaillant dans le domaine de la preuve et des équipes concevant et/ou implantant des algorithmes arithmétiques.



1  Projets collaborant à l'action AOC

Projet Lemme
(UR Sophia, responsable Loïc Pottier). Le projet LEMME s'intéresse à l'introduction des méthodes formelles dans la construction de logiciels pour le calcul scientifique. Les personnes participant à l'action seraient Loïc Pottier (CR Inria), Laurent Théry (CR Inria);
Projet Polka
(UR Lorraine, responsable Paul Zimmermann). Le projet Polka est consacré à la manipulation de polynômes, à l'arithmétique et à la combinatoire. Il développe actuellement une bibliothèque, mpfr, de calcul multi-précision avec arrondi correct. Les personnes collaborant à l'action seraient Paul Zimmermann (DR Inria) et Guillaume Hanrot (CR Inria);
Projet Arénaire
(UR Rhône-Alpes, responsable Jean-Michel Muller). Le projet Arénaire est consacré à l'arithmétique des ordinateurs. Les personnes participant à l'action seraient Marc Daumas (CR CNRS), Claire Finot (doctorante), Vincent Lefèvre (doctorant) et Jean-Michel Muller (DR CNRS).

2  Buts scientifiques de l'action

On cherchera aussi bien à certifier des algorithmes implantant des opérateurs arithmétiques qu'à vérifier que des algorithmes utilisant de tels opérateurs satisfont certaines propriétés. Donnons quelques exemples.



2.1  Certification d'opérateurs arithmétiques

Faire une addition ou une soustraction virgule flottante est une opération simple dans les grandes lignes, mais il faut tenir compte d'un grand nombre de cas particuliers (entrées ou sorties dénormalisées, arrondi final provoquant un changement d'exposant du résultat, dépassements éventuels de capacité, etc.). Les grands constructeurs ont un grand nombre d'utilisateurs, assurant un <<retour>> suffisant pour vite corriger des problèmes. Ce n'est pas le cas des concepteurs de circuits spécialisés (le processeur 1750, largement embarqué à bord de satellites, a une soustraction flottante fausse). Il semble également d'après des tests récents, que la soustraction et la racine carrée posent quelques problèmes sur des processeurs alpha sous linux.

De plus en plus, la division et la racine carrée sont implantées en utilisant un <<multiplieur-accumulateur>> flottant (c'est-à-dire un opérateur qui effectue avec arrondi correct un calcul de la forme ax+b). Obtenir des algorithmes rapides et certifiés pour de tels opérateurs est un problème sur lequel travaillent des constructeurs comme AMD [MLK98], Hewlett-Packard ou Intel [CGM99].



2.2  Formalisation complète de la norme IEEE 754

La plupart des plate-formes actuelles implantent (plus ou moins bien !) le standard IEEE-754 d'arithmétique flottante, qui spécifie les formats de représentation des nombres, ainsi que le comportement des quatre opérations arithmétiques et de la racine carrée. Nous souhaitons formaliser ce standard, afin de pouvoir prouver (voir section suivante) le comportement d'algorithmes.



2.3  Garantie de propriétés d'un algorithme

En supposant que les <<briques de base>> que constituent les opérateurs arithmétiques répondent bien aux spécifications de la norme IEEE 754, on peut chercher à prouver qu'un algorithme utilisant ces opérateurs satisfait à certaines propriétés. Nous songeons tout particulièrement à:

3  Méthodologie

Pour la certification formelle on se servira principalement de l'assistant de preuve Coq. Coq permet de prouver des théorèmes, de décrire des programmes et enfin d'exécuter efficacement ces programmes grâce à un mécanisme d'extraction. On se propose d'utiliser ces trois aspects dans cette action. La première étape sera de définir dans Coq les objets sur lesquels vont travailler nos programmes et prouver leurs propriétés de base. Pour cela on s'inspirera du travail de John Harrison [JRH]. Ensuite on s'attaquera sur des cas d'étude à la formalisation de certains algorithmes et de leur preuve de correction. Enfin on s'intéressera à l'efficacité des programmes extraits pour évaluer la possibilité de fournir des librairies de programmes portables certifiés.



4  Nos besoins

Nous désirons pouvoir financer:
Post-Doc (1 an) 222 KF
Stages 133 KF
Voyages 150 KF
Worskhop 25 KF
Total 530 KF

References

[CGM99]
M. A. Cornea-Hasegan, R. A. Golliver, and P. Markstein. Correctness proofs outline for Newton-Raphson based floating-point divide and square root algorithms. In I. Koren and P. Kornerup, editors, Proceedings of the 14th IEEE Symposium on Computer Arithmetic (Arith-14, Adelaide, Australia, April 1999), pages 96--105. IEEE Computer Society Press, Los Alamitos, CA, 1999.

[JRH]
J. Harrison. A Machine-Based Theory of Floating Poing. TPHOLs'99 LNCS 1690, Septembre 1999.

[MLK98]
J S. Moore, T.W. Lynch, and M. Kaufmann. A Mechanically Checked Proof of the AMDK5 Floating Point Division Program. IEEE Transactions on Computers, Vol. 47 No. 9, Septembre 1998.

This document was translated from LATEX by HEVEA.

[Page d'accueil]
Laurent Théry