Nouvelle en rapport avec un thème scientifique, l'analyse automatique de programmes informatiques.
Il fait sombre. Un néon fatigué éclaire la pièce désertée. Tout le monde est parti. Restent le
ronronnement discontinu des unités centrales, le clignotement asynchrone des cartes réseau, et le
défilé bariolé des lignes de log sur l’écran noir de postedien.
Quel bazar. Les bureaux sont encombrés de collections d’écrans de toutes tailles et formes,
débranchés pour la plupart, de modules hardware déballés depuis des semaines, gisant sur les
tables comme des poissons morts sur la plage, et d’antiques impressions d’articles de recherche et
de sujets d’examens, dont l’encre commence à s’estomper. Çà et là, sur les murs nus, un tableau
dégoulinant de formules, de listes de courses et de schémas gribouillés, en strates de couleurs
fanées, sur un fond grisâtre étalé par la brosse sale.
Derrière les bureaux, de larges fauteuils en simili-cuir noir, luisants, incongrus comme des
Lamborghinis sur le parking d’un supermarché hard discount. Fatigués, mais encore étonnamment
confortables. L’Université veille à la santé lombaire de ses personnels. A l’extérieur de la pièce, de
larges couloirs jaune poussin, silencieux et déserts. Un vague murmure flotte dans l’air. Le bruit du
vent sur la tour, ou le râle d’un stagiaire oublié dans un placard ?
Zak fixe l’écran d’un air hébété. Rien ne marche, comme d’habitude. Ce matin, il s’est pourtant levé
avec la conviction de tenir quelque chose. Quelque chose de nouveau. Une idée qui changerait tout,
ou du moins qui sauverait sa thèse, dans l’impasse depuis plusieurs mois. Mais non. Ça n’a pas l’air
de coller.
Abattu, il sort mollement de la pièce, pour traverser le sous-marin jaune des couloirs du labo,
décorés de posters très sérieux sur les automates d’arbres, les algèbres de processus, et la topologie
des réseaux pédophiles pair à pair. Sales crâneurs. Zak sort du labo. La rotonde de la tour 26 est
déserte. Seuls les panneaux luminescents des ascenseurs et des issues de secours luisent dans
l’obscurité. Même les parois vitrées donnant sur la rue semblent opaques, mates, glacées. Zak
marche lentement dans le couloir circulaire, en traînant un peu les pieds. Il frôle légèrement la
paroi intérieure du bout des doigts de la main gauche.
Non, c’est pas normal. Abadi l’avait pourtant assuré que ça marcherait. L’argentin a bien des
défauts, mais pas celui de parler à la légère. Où est-il en ce moment ? Sûrement pas en train de
danser le tango. Il est au comité de programme du Symposium IEEE Security and Privacy, donc il
doit être sur la côte Ouest. Là-bas, ce doit être le milieu de l’après-midi.
Zak termine son tour de rotonde d’un pas décidé, passe son badge, et rentre en trombe dans le labo,
direction le bocal aux thésards. Il se laisse tomber sur son fauteuil, et agite frénétiquement sa
souris jusqu’à ce que l’écran de postedien s’illumine. Il ouvre sa messagerie et commence à écrire :
"Salut Martín, comment ça va à San Francisco ? La météo prétend que la brume se serait levée. J’ai
cru à un canular. 🙂 Ici, rien ne va plus. J’ai essayé tout ce qu’on s’est dit sur l’analyse de portabilité.
Mais y a rien qui marche. Si j’abstrais des ensembles de dépendances à partir d’ensembles de
traces, je perds les dépendances concrètes entre les variables au sein de chaque trace individuelle.
Si je garde des ensembles d’ensembles de traces paramétrées par un ensemble de dépendances
concrètes, j’obtiens des abstractions incomparables pour deux représentations syntaxiques d’un
même programme. Peut-être qu’on a pris le problème à l’envers ?"
Zak joint une archive compressée contenant les derniers logs produits par l’analyseur sur leurs
programmes de test, et envoie le message. "Il va falloir qu’il se grouille de nous sortir de là", grogne
le doctorant pour lui-même. Parce que la deadline de soumission à SBMF, le symposium brésilien
sur les méthodes formelles, est dans deux semaines. Pas d’analyse, pas d’article. Pas d’article, adieu
la virée à Récife. Zak aimerait pourtant bien voir le Brésil. Aux frais de la fac, si possible.
"Ding !" La réponse d’Abadi fait sonner postedien. Zak ouvre fébrilement l’e-mail, plein d’espoir.
"T’as pas la bonne sémantique concrète. Pars d’ensembles de paires d’ensembles de traces pour
représenter les relations entre les exécutions dans les environnements source et destination.
Trouve une formulation dénotationnelle sous forme de point fixe, et essaye une abstraction
relativement expressive, mais qui passe à peu près à l’échelle. Un domaine sous-polyédrique, par
exemple."
Zak se fige, lèvres serrées, sourcils froncés. "Mais c’est pas vrai ! Il se fout carrément de moi, ce c…"
On est à deux semaines de la deadline, et môssieur se prend pour la Pythie ! Et pour l’interprétation
de l’oracle, il faut prendre rendez-vous ? Zak se sent dans la posture du toutou dont on teste la
vaillance en lui jetant un os par dessus le Grand Canyon. Évidemment, il s’en tape, Abadi, de Récife.
Il est déjà allé au Brésil des tas de fois, et il ne se déplacera pas pour la conférence de toute façon,
même si le papier est accepté. Môssieur est bien trop important, môssieur ne se déplace pas pour
des conférences de second rang, sauf s’il est invité à donner une keynote par le banc et l’arrièrebanc
! En plus, il doit avoir déjà une bonne centaine de publications de recherche, dans des
journaux ou actes de colloques avec relecture de premier plan. Alors, un papelard de plus ou de
moins, co-écrit par un obscur Zak Machin-Chose, il en a sûrement rien à cirer. Alors que Zak, lui, ne
peut pas laisser passer une occasion de signer un papier avec une star comme Abadi. C’est une
chance en or pour sa carrière, qui ne se représentera probablement pas de sitôt. Bon. Plus la peine
d’attendre de l’aide à présent. Zak est seul au monde. C’est son problème, son idée, son analyseur,
son papelard. Abadi, c’est qu’une étiquette prestigieuse pour décorer la page de garde. Il faut se
ressaisir. Tout reprendre depuis le début.
Comme toujours dans une situation comme celle-là, Zak exécute son petit rituel. Il commence par se
laver les mains. Évidemment, c’est un peu pénible, car il faut sortir du labo. Il y a bien une arrivée
d’eau dans une pièce, mais il y a eu des fuites. Alors, plutôt que de chercher à réparer, l’Université a
coupé l’eau. Heureusement, il y a des toilettes sur la rotonde de la tour 26. Zak s’y rince
soigneusement les doigts. L’eau est fraîche. Après une quinzaine d’heures de combat contre le
clavier, ça délasse. Il n’y a pas si longtemps, il y avait des urinoirs dans cette pièce. Mais ils ont
commencé à se boucher, alors l’Université les a fait enlever. Moins cher et plus rapide que
d’envisager une réparation. Zak retourne au labo d’un pas lent, mais résolu. Direction la pièce de
détente. Deux tables en T, deux canapés hors d’âge, et une machine Nespresso rutilante. Zak choisit
deux capsules du café le plus corsé de sa réserve personnelle : Ouganda, 100% robusta, intensité 12.
Il se coule un double ristretto. Plus question de flancher maintenant.
Zak retourne s’asseoir face à l’écran de postedien. Allez, c’est parti. Une gorgée. On reprend tout.
Sémantique concrète : on tente le truc d’Abadi, avec les ensembles de paires d’ensembles. Putain,
c’est quoi déjà ? Des ensembles de paires d’ensembles de claques. Penser à en garder un échantillon
pour Abadi si ça ne marche pas. Bon. Maintenant, définir les opérateurs concrets sur le langage. Pas
trop dur : ça ressemble aux 36 tentatives précédentes, qui ont toutes foiré. Tiens, l’union a une
forme sympathique. Ça permettra peut-être de perdre moins de relations entre les exécutions
source et destination, lorsqu’elles suivent des flots de contrôle différents. Bon, pour son histoire de
point fixe, on verra plus tard. Tiens, il n’a qu’à s’asseoir dessus en attendant. Et pour l’abstraction
sous-polyédrique de môssieur, on va pas se casser la tête, y a qu’à mettre des octogones. C’est bon à
toutes les sauces, les octogones. Et la bibliothèque Apron en fournit une implémentation efficace… et
gratoche. Allez, zou, y a plus qu’à implémenter dans l’analyseur. Zak ajuste son casque sur ses
oreilles, et laisse l’ordinateur pêcher au hasard dans sa petite sélection de thèmes de bossa nova.
Tall and tan and young and lovely
The girl from Ipanema goes walking
And when she passes
Each one she passes goes ah
Beaucoup de morceaux de Stan Getz, qui le mettent dans un état de transe lucide proche de
l’euphorie. Parfait pour pisser du code. Banzaï ! Code que je code, Zak fait défiler les lignes colorées
sur l’écran sombre. Il les bricole, il les tripatouille, il les charcute : une vraie boucherie. Ça fait 36
fois qu’il refait tout, mais c’est pas grave. C’est la partie la plus marrante du boulot. Le
programmeur se sent tout-puissant, il a l’impression d’avancer à pas de géant, avec la certitude un
peu naïve d’aller quelque part. Le compilateur est là, rassurant, pour filtrer les plus grosses
conneries. Ce n’est que beaucoup plus tard qu’on découvre avec stupeur qu’on a laissé traîner un
bug toutes les dix lignes.
Pas le temps de finasser. Ça compile, voyons si ça a l’air de tomber en marche. Zak relance son
analyseur sur les cas de test choisis avec Abadi. Le programme tourne longtemps, plusieurs
minutes. "ça ne va encore pas converger !" se dit Zak avec une pointe d’angoisse. Mais les invariants
calculés itérativement semblent progressivement se stabiliser.
Tall and tan and young and lovely
The girl from Ipanema goes walking
And when she passes he smiles
But she doesn’t see, she just doesn’t see
D’une itération à la suivante, ils sont à présent si semblables que Zak n’arrive même plus à les
distinguer dans le fichier de log de l’analyseur. Puis le miracle se produit. Les nouvelles itérations
se mettent à reproduire exactement le résultat des précédentes. Ces éternels retours du calcul, ce
sont des invariants : l’analyseur a trouvé un point fixe !
Zak laisse les analyses se terminer et dépouille les résultats. Hum, c’est pas mal du tout. Dans la
plupart des cas, l’analyseur est arrivé à distinguer automatiquement les programmes portables des
autres. Il n’a échoué que sur les cas les plus difficiles.
"Yessssssss!" Zak se lève d’un bond, et laisse exploser sa joie. Il saute sur place dans la pièce, comme
un gamin de 4 ans le matin de Noël. Cette fois c’est gagné : non seulement sa thèse est sauvée, mais
avec ce papier estampillé Martín Abadi, il a toutes les chances d’obtenir un poste de recherche
permanent. Quelle chance ! Hystérique, Zak tape un long message pour Abadi. Il explique ce qu’il a
fait, et joint le code source de l’analyseur et le brouillon du papier. La réponse arrive deux heures
et demie plus tard, alors que Zak ronfle comme un sapeur dans un canapé de la pièce de détente,
un sourire et la bave aux lèvres : "Joli boulot. Ça va faire un bon papier. Je m’occupe de terminer la
rédaction et de soumettre à SBMF. Repose-toi, tu l’as bien mérité."
Un mois plus tard, ne voyant rien venir de la part du comité de programme, Zak écrit à Abadi pour
savoir si le papier a été accepté. "Bien sûr ! les revues sont excellentes. Je n’ai rien eu a changer
pour la version finale".
Huit semaines plus tard, le printemps déverse sur le labo des nuées de poils de fruits de platanes,
jaunâtres et urticants, et une horde sauvage de stagiaires boutonneux. Dans le bocal aux thésards
plein à craquer, Zak turbine de nouveau à plein régime. Il s’est lancé corps et biens dans la
rédaction de son manuscrit de thèse. Dernière ligne droite avant la soutenance, pas question de
mollir.
"Zak, t’as vu le programme de SBMF ?", s’exclame son condisciple Matthieu par-dessus l’écran de
son ordinateur. Y a l’air d’y avoir un papier pas mal sur la portabilité, pile dans le style de ce que tu
fais ! Tu devrais demander à y aller."
Zak se lève de son fauteuil et contourne le bureau de Matthieu, pour se pencher, goguenard, vers
son écran.
"Ah ouais, fais voir ?"
La page s’affiche. Zak se fige.
Point fixe.
No Comments