Arithmétique des Ordinateurs Certifiée

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 à:

des algorithmes multi-précision. Le projet POLKA met au point la bibliothèque multi-précision mpfr. Le projet Arénaire met au point une bibliothèque de manipulation d'expansions flottantes (i.e. de nombres représentés comme somme d'un petit nombre de flottants). Nous souhaitons valider les algorithmes arithmétiques implantés dans ces bibliothèques;
des preuves de <<respect de domaine>>. Nous entendons par celà certifier qu'un programme qui implante l'arctangente fournit toujours un résultat compris entre -p/2 et +p/2, qu'un sinus ou un cosinus sera toujours entre -1 et +1, etc. De telles propriétés sont importantes: la plupart du temps elles seront considérées comme <<satisfaites de manière évidente>> par un programmeur. Leur non-satisfaction peut alors rendre imprévisible le comportement d'un programme. On cherche également à garantir qu'une portion de programme de provoquera pas de dépassement de capacité.
gestion d'exceptions flottantes. Un autre point important est de voir si une portion de programme peut générer certaines exceptions, comme l'apparition d'un "Not a Number (NaN)". Ce point est critique pour certaines applications: étant donné que toute opération dont l'une des opérandes est un NaN doit retourner un NaN, un calcul risque très vite de ne produire que des NaNs.

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:

6 stages de niveau DEA ou fin d'études d'élève-ingénieur;
un an de post-doc. Ce point est pour nous le plus important: il va falloir du temps pour former à l'arithmétique flottante quelqu'un qui vient de la preuve (ou inversement);
deux réunions plénières et une dizaine de déplacements individuels (entre URs) par an;
un workshop avec quelques personnalités invitées.

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 L^AT_EX by H^EV^EA.

[Page d'accueil]

Laurent Théry