Les leçons d’un algorithme délinquant

Le Pentium qui défraya la chronique.

L’étude des algorithmes arithmétiques ne concerne pas que les « savants fous », loin de là. Intel en a fait la cuisante expérience en 1994. La première version de son Pentium s’est certes retrouvée en Une des magazines spécialisés, mais pour une raison peu glorieuse. Le bug de ce nouveau joyau venait d’être révélé par le mathématicien américain Thomas Nicely, de l’université Lynchburg (Virginie). Mais au-delà de l’anecdote, très désagréable pour le constructeur, cet incident a d’une certaine manière bouleversé les pratiques de vérification des algorithmes implantés sur les microprocesseurs. Un gain pour l’informatique en général.

Question de mathématicien

Thomas Nicely est un mathématicien américain qui travaille dans le domaine de la théorie des nombres. Il s’intéresse en particulier aux nombres premiers « jumeaux », c’est-à-dire aux nombres premiers dont la différence vaut 2. Exemples : 5 et 7, 11 et 13… Il travaille également sur le calcul de la constante de Bruin, qui est la somme des inverses des nombres premiers jumeaux. Ses premiers termes sont : (1/3 + 1/5)  + (1/5 + 1/7) +  (1/11 + 1/13) + … On ne sait toujours pas si cette somme comporte un nombre fini ou infini de termes. On en connaît une valeur approchée, sans savoir toutefois si sa valeur exacte est rationnelle, algébrique… On dispose simplement d’une conjecture qui affirme l’existence d’une infinité de nombres premiers jumeaux.

Alerte

Dessin : Olivier Taffin

En juin 1994, Thomas Nicely fut saisi de perplexité. Les très gros calculs qu’il effectuait, dans son domaine de recherche, donnaient des résultats totalement contradictoires avec des calculs antérieurs. Cela venait-il du compilateur ? Celui qu’il utilisait manifestait, il est vrai, un comportement parfois erratique. Il a donc réécrit ses programmes en fonction de ce problème, et a relancé ses calculs en septembre 1994. Surprise : les calculs effectués sur l’un de ses ordinateurs donnaient un résultat différent sur d’autres machines. L’ordinateur en question était équipé du nouveau processeur Pentium d’Intel. Persévérant, le mathématicien découvre alors le pot aux roses : le Pentium donnait un résultat incorrect lors du calcul de 1/824633702441. Ce nombre apparaissait dans ses calculs car 824633702441 et 824633702443 sont jumeaux.

Enquête

Peu de temps après, il dut se rendre à l’évidence. Le microprocesseur Pentium lui-même effectuait parfois des divisions fausses, explique Nicely. Fin octobre, Nicely a averti la compagnie Intel, ainsi que d’autres utilisateurs par le biais des forums électroniques de diffusion. De nombreux ingénieurs et chercheurs se sont penchés sur le problème. Le « pire cas », c’est-à-dire le cas pour lequel l’erreur due au programme de division du Pentium est la plus grande, a été trouvé par Tim Coe. Celui-ci était alors membre de la firme américaine Vitesse Semiconductors. Verdict de Tim Coe : quand on effectuait la division de 4195835.0 par 3145727.0, on obtenait 1.33373906802 au lieu de 1.3338204491.

D’où venait l’erreur ? L’analyse en profondeur a alors montré que l’on ne pouvait invoquer l’implantation de l’algorithme de division sur le microprocesseur. Elle provenait de l’algorithme lui-même. La méthode de division utilisée était littéralement fausse. Pour comprendre ce qui s’est passé, bref retour sur les bancs de l’école.

Retour au calcul élémentaire

Chacun se souvient de la manière dont on pose sur le papier une division, et comment l’opération est effectuée. On l’apprend alors en système décimal, ou système à base 10. Celui-ci utilise neuf chiffres (1 à 9) plus le zéro. Soit à diviser x par y, avec x < y. La méthode consiste à calculer une suite de chiffres du quotient (q1, q2, q3, …) et les restes partiels associés (x(1), x(2), x(3), …), jusqu’à la précision que l’on souhaite si l’opération ne tombe pas juste.

Dans le cas du Pentium, la base utilisée pour effectuer la division n’est pas 10 mais 4. On construit de la même manière une suite qi de chiffres du quotient et une suite x(i) de restes partiels. Mais les chiffres ne peuvent alors valoir que -2, -1, 0, 1 ou 2. Ils sont lus dans une table qui a pour entrée les 5 chiffres les plus significatifs de l’écriture en base 2 de y et les 7 chiffres les plus significatifs de celle de x(i). Aussi curieux que cela puisse paraître, les arithméticiens ont démontré qu’une telle table est une approximation suffisante d’une table parfaite, c’est-à-dire contenant toutes les valeurs possibles.

La faille

Cette propriété résulte en fait de l’emploi d’une « redondance » du système de numération servant à représenter le quotient. Alors qu’en base 4, il suffit théoriquement de 4 chiffres (0, 1, 2, 3) pour représenter tous les quotients possibles, 5 chiffres sont utilisés dans le cas du Pentium (-2, -1, 0, 1 et 2). Le malheur est que le concepteur du diviseur du Pentium connaissait mal les subtilités des algorithmes de division « redondants ». D’où l’introduction de 5 valeurs fausses dans sa table. Cela a suffi. Le Pentium s’est trouvé dans la situation d’un écolier méconnaissant ses tables de multiplication !

Quelques leçons d’un échec

Ce « bug » du Pentium n’est pas le seul raté informatique célèbre (on se souvient de celui qui conduisit à l’explosion de la première fusée Ariane 5). Peut-être même la publicité faite autour de l’échec de la firme américaine était-elle disproportionnée. Elle s’inscrivait dans un contexte de compétition industrielle féroce. Mais son impact sur le comportement des industriels et des universitaires n’en a été que plus constructif.

Tout le monde a perçu concrètement, industriels comme chercheurs, la complexité des algorithmes de l’arithmétique « virgule flottante » (nombres non entiers), et le soin à apporter à leur vérification. Des environnements informatiques d’aide à la preuve sont désormais utilisés pour vérifier les opérateurs de division et de racine carrée des microprocesseurs. Les utilisateurs veulent aujourd’hui des garanties sérieuses sur la justesse des algorithmes, en particulier pour les applications « critiques » (transports terrestres, véhicules spatiaux…).

La firme Intel elle-même publie dorénavant des rapports présentant ses algorithmes arithmétiques (celle du processeur Itanium par exemple), ainsi que leur preuve (en anglais). L’américain AMD a fait de même pour ses processeurs K5 et K7 (voir la page, en anglais, d’un de ses anciens collaborateurs, David Russinoff).

Les limites du secret

Dessin : Olivier Taffin

Autre conséquence, loin d’être anodine : le secret est en grande partie levé sur les algorithmes arithmétiques des industriels. Pour prouver la correction d’un algorithme, il faut en effet pouvoir le décrire. Le Intel Technology Journal publie régulièrement une description des algorithmes arithmétiques d’Intel. Plus généralement, les constructeurs exposent leurs algorithmes à l’occasion du Symposium on Computer Arithmetic qui a lieu tous les deux ans (il a eu lieu à Saint-Jacques de Compostelle en 2003, et se tient dans les environs de Boston en 2005).

Le monde académique n’est pas en reste. L’université de Californie, à Berkeley (États-Unis), a développé des programmes de test d’un environnement arithmétique. L’Action de recherche coopérative (ARC) « Arithmétique des ordinateurs certifiée » de l’INRIA a engagé des travaux dans ce domaine. Ils se poursuivent au sein de plusieurs projets (LEMME, ARÉNAIRE et SPACES) de l’organisme. L’arithmétique est la « brique de base » de l’informatique. Tous les programmes (ou presque) utilisent des opérations arithmétiques. Si même les machines venaient à se tromper, qui assurera la sécurité des humains ?