On a parfois tendance à l'oublier : le calcul numérique
est une des briques de base de l'informatique. La précision des
opérateurs et des programmes, leur fiabilité et leur rapidité
sont au cœur de bon nombre d'applications industrielles plus ou moins
critiques.
Il suffit de citer quelques unes des erreurs informatiques célèbres
de ces dernières années comme le " bug " du premier
processeur Pentium en 1994 ou l'explosion de la première fusée
Ariane 5 en 1996 pour rappeler combien la fiabilité et la précision
des calculs par ordinateur sont fondamentales. En première ligne de ces
ratés notoires, les microprocesseurs et les algorithmes dits numériques
qui utilisent l'arithmétique à virgule flottante, le format
implanté dans les ordinateurs pour représenter de façon
approchée les nombres réels (lien encadré sur la virgule
flottante).
À la fin des années 1970, ingénieurs et chercheurs ont
réussi à imposer une solution uniforme normalisée en dépit
d'intérêts commerciaux divergents : à l'époque,
chaque constructeur avait sa propre
représentation des nombres à virgule flottante mais certains choix
visaient juste à calculer plus vite ou avec moins de transistors quitte
à fournir parfois un résultat notoirement inexact ou à
agir à l'opposé des habitudes des programmeurs… D'une
machine à l'autre, des opérations arithmétiques,
même les plus simples conduisaient à des résultats de précisions
variables. À la naissance des ordinateurs personnels, l'idée
de normaliser l'arithmétique à virgule flottante avait fait
son chemin. La volonté d'un nouvel acteur du domaine, Intel, de
se faire une place sur ce marché où il n'avait alors aucune
légitimité et son choix de s'appuyer sur les travaux d'un
scientifique influent sur le sujet ont fait le reste : William Kahan, professeur
à l'université de Californie à Berkeley a fortement
influencé les réflexions sur le sujet et il a depuis reçu
le Turing Award pour ses contributions. Presque toutes ses propositions ont
été acceptées dans la recommandation de l'IEEE
, société savante
qui fait autorité dans les domaines de l'ingénierie informatique.
Connue sous le nom IEEE 754, ce standard a été retenue en 1985 par
l'institut américain de normalisation (ANSI, American national
standards institute). Il définit précisément l'arrondi
correct pour les quatre opérations arithmétiques (addition, soustraction,
multiplication et division) et la racine carrée. La quasi-totalité
des ordinateurs actuels respectent cette norme, même si certaines fonctionnalités
sont seulement implantées grâce à des bibliothèques
à l'exécution ou à la compilation.
La meilleure façon d'être au cœur du sujet
Le projet
ARENAIRE travaille
dans ce domaine depuis sa création en 1999 et la démarche de
standardisation y est totalement intégrée. Les chercheurs sont
impliqués dans les réflexions en cours sur la révision
du standard IEEE 754. Le fonctionnement de ce comité technique de l'
IEEE
est particulièrement pragmatique : le comité de révision
du standard se réunit tous les mois en
Californie et pour plus d'efficacité, un sous-comité travaille à
un rythme hebdomadaire pour préparer les propositions à discuter.
Les membres d'ARENAIRE vont sur place 2 à 3 fois par an et poursuivent
ensuite les discussions à distance. L'INRIA, plusieurs acteurs
américains du domaine (IBM, Intel, HP, Sun Microsystems notamment) et
certains scientifiques anglais et israéliens participent à ces
réunions ouvertes et gratuites.
Le
projet ARENAIRE est réputé dans son domaine. Ses chercheurs
sont par exemple intervenus pour l'Aerospatiale sur le choix de l'utilisation
de la virgule flottante dans l'Airbus A380. D'autres chercheurs
du projet ont développé pour STMicroelectronics des algorithmes
complexes pour réduire les temps de calcul des divisions. Depuis
2002, ils développent une bibliothèque virgule flottante
pour un autre processeur de ST.
De multiples retombées
Les retombées ne sont d'ailleurs pas toujours là où
on les attend. Ainsi, à la suite d'un consensus entre plusieurs
membres du comité technique, il a été décidé
en 2004 de réfléchir à l'intégration de l'arithmétique
à virgule flottante en précision arbitraire dans le futur standard,
un domaine dans lequel l'équipe
SPACES possède un savoir-faire unique. Ce mode de calcul (aussi appelé
" calcul à précision multiple ") est plus précis
que le calcul flottant, mais en contre-partie plus long à réaliser.
L'équipe SPACES a développé un logiciel baptisé
MPFR
(Multiprecision floating-point arithmetic with exact rounding) qui pourra
être compatible avec le standard IEEE, dès qu'elle sera définitive,
pour un surcoût fort raisonnable en termes de temps de calcul. L'expérience
acquise par SPACES la place ici clairement en avance sur les autres équipes,
y compris sur les réflexions des experts du comité de révision
du standard.
Autre domaine clé de l'amélioration de la précision
des calculs : la certification des programmes et de leurs algorithmes avec des
outils automatiques basés sur les preuves formelles. Ces techniques commencent
à s'imposer quand des vies humaines seraient menacées par
un dysfonctionnement. Parce qu'elle deviennent de plus en plus puissantes
et de plus en plus automatisées, elles intéressent aussi de plus
en plus d'industriels. Grâce aux développements du projet de recherche
ARENAIRE, ces techniques peuvent maintenant être appliquées aux
programmes qui ont recours à des calculs numériques. L'objectif
de cette démarche est de valider les programmes et de s'assurer
que leur implantation est correcte. L'INRIA a engagé en 2000 une
action de recherche coopérative sur le sujet (baptisée AOC, Arithmétique
des ordinateurs certifiée) dans laquelle ont été impliqués
plusieurs projets de recherche (LEMME, ARENAIRE et SPACES). Dans le cadre des méthodes
formelles, l'INRIA développe depuis longtemps un logiciel d'assistant
de preuve baptisé
Coq qui vérifie en détail les démonstrations
et depuis 2002, des chercheurs d'ARENAIRE travaillent sur ces sujets aux
côtés de chercheurs de la Nasa au centre de recherches de Langley
et au national institute of aerospace (Virginie). Historiquement, la
Nasa soutient
fortement un autre assistant de preuve formelle baptisée PVS, très
utilisé aux Etats-Unis et en milieu industriel. L'arithmétique
à virgule flottante y est utilisée dans un projet visant à
automatiser le contrôle aérien de petits aérodromes. Grâce
à une collaboration financée par le CNRS et la Nasa, une spécification commune en Coq et PVS verra le jour.
Celle-ci deviendra du même coup une référence mondiale incontournable.
