Depuis quelques années, une partie de mes recherches porte sur la compilation certifiée, qui s’inscrit dans un but plus global de produire des logiciels dont la fiabilité puisse être justifiée pour des applications critiques (aviation, ferroviaire…). On m’a suggéré d’expliquer ce dont il s’agit.

Les développeurs de logiciels rédigent ceux-ci dans un ou plusieurs langages de programmation, en général textuels (d’où le « code » effrayant que l’on montre parfois lorsque l’on évoque ce sujet dans les médias), parfois graphiques. Le programme ainsi rédigé n’est pas directement exécutable par la machine, dont la circuiterie ne sait exécuter que des opérations très simples (une addition, un déplacement de données…). Il faut donc une étape de traduction. On distinguait naguère pour celle-ci les interpréteurs (qui traduisent les instructions au fur et à mesure) et les compilateurs (qui traduisent le programme une fois pour toutes), mais les frontières sont maintenant floues. Toujours est-il qu’on traduit, et que comme pour toute traduction, celle-ci peut être fidèle ou infidèle. Et une traduction infidèle, pour un logiciel, peut conduire à des bugs.

Remarquons le caractère particulièrement vicieux de cette infidélité. Le logiciel tel que développé peut très bien être correct, mais la phase de traduction rajouter des bugs qui ne se verront pas dans le texte du logiciel. Comme la phase de traduction est influencée par de très nombreux facteurs, il est possible que les bugs ne soient introduits que dans certaines circonstances (par exemple, seulement dans la version de production destinée aux utilisateurs) et pas dans d’autres (par exemple, dans la version instrumentée pour faire des tests).

Dans la plupart des applications, il y a bien d’autres sources de bugs que les compilateurs. Lorsque l’on parle d’applications critiques, où il faut justifier que le programme exécuté met bien en œuvre les fonctionnalités qu’il est censé mettre en œuvre, la question est différente. On peut utiliser des arguments tels que « ce compilateur a été utilisé pour de nombreuses applications critiques et on n’a pas constaté de problèmes », on peut organiser des relectures partielles de la correspondance entre le logiciel tel que rédigé et celui exécuté par la machine, mais il s’agit là de solutions très partielles. En effet, ce n’est pas parce qu’un compilateur n’a pas eu de comportement incorrect détectable sur d’autres applications qu’il n’en aura pas sur une application donnée. Quant aux relectures, elles exigent souvent qu’on demande au compilateur de faire une traduction « mot à mot » qui produit du code inefficace pour la machine.

Il faut ici évoquer la notion d’optimisation. Pour un programme rédigé par un humain donné, il existe de multiples façon de le traduire fidèlement en un programme exécutable sur la machine, fidèles au sens que le sens (on dit : la sémantique) du programme est préservé. Pourtant, toutes ne se valent pas : certaines vont mettre plus de temps que d’autres pour s’exécuter. Un compilateur optimisant va donc transformer le programme, faire une traduction moins littérale, afin de produire du code efficace. Je ne vais pas rentrer dans le détail de toutes les optimisations possibles, mais en voici quelques-unes :

  1. Le programmeur a pu mettre un calcul qui se répète de façon inutile, parce qu’à chaque fois il donne le même résultat. On peut calculer celui-ci une fois pour toutes. (Le programmeur pourrait faire cette transformation lui-même, mais parfois, pour des raisons de lisibilité, ce n’est pas souhaitable.)

  2. L’ordre d’exécution n’est pas forcément optimal. J’ai parlé d’opérations pour déplacer des données ; ces opérations prennent un certain temps et il vaut mieux l’anticiper. C’est un peu comme dans une bibliothèque où il faut commander des documents : si l’on a besoin de 3 documents pour travailler successivement sur chacun d’entre eux, il est plus rapide deême commander les 3 documents en une fois, plutôt que de ne commander que le premier, l’attendre, travailler dessus, le rendre, commander le suivant… Les gros processeurs pour PC ou Mac ont donc dans leur électronique des dispositifs leur permettant d’exécuter les instructions dans le désordre, et lanceront les trois commandes de données en avance ; mais ces dispositifs d’exécution dans le désordre sont complexes, parfois eux-mêmes buggués, et on les évite dans les systèmes critiques. Un compilateur optimisant va donc placer les opérations de façon à anticiper les délais d’attente.

Un compilateur optimisant est un logiciel complexe, il va donc contenir des bugs donc potentiellement introduire des bugs dans les programmes qu’il traduit ; mais sans optimisation, il va produire des programmes inefficaces, ce qui est intolérable dans de nombreuses applications.

La solution proposée par Xavier Leroy (alors directeur de recherche à l’INRIA, maintenant professeur au Collège de France) et ses collaboratrices et collaborateurs a été de démontrer mathématiquement la correction de leur compilateur CompCert.

Il convient ici de préciser certaines idées. Un compilateur est une sorte de traducteur dont on exige la fidélité, c’est-à-dire la préservation du sens du programme. Ce sens peut être défini mathématiquement, tant pour le langage de programmation manipulé par le programmeur que pour les instructions exécutables directement par la machine. Les transformations effectuées par le compilateur peuvent elles aussi être définies sous une forme mathématique. Il « suffit » alors de démontrer un théorème de préservation.

Il serait très difficile, voire impossible, de démontrer à la main (avec du papier et des crayons) un tel théorème, tant un compilateur est complexe, et évolue d’une version à l’autre. Qui plus est, les preuves à la main sont elles-mêmes sujettes à bugs — divers algorithmes de la littérature scientifique, où était publiées des démonstrations de leur correction, se sont révélés in fine incorrects. Aussi la preuve mathématique sera elle-même vérifiée par un logiciel, un assistant de preuve ; dans le cas de CompCert, il s’agit de l’assistant Coq.

La nécessité de justifier minutieusement la fidélité de chaque étape de traduction rend CompCert assez différent d’un compilateur traditionnel ; par exemple, il vaut mieux plusieurs étapes simples qu’une grosse étape complexe. L’effort de preuve est considérable, et on structure le logiciel par rapport à celui-ci : est-il rentable d’implanter une optimisation difficile à justifier rigoureusement si celle-ci ne gagne en général pas grand-chose en efficacité ?

Il faut ici relever que les preuves à rédiger sont considérablement plus délicates et minutieuses que celles que l’on donne dans les publications scientifiques en ce qui concerne les algorithmes d’optimisation. En effet, dans les preuves sur papier, on peut se permettre d’omettre certains « détails » fastidieux et s’en tenir aux grands principes ; ce n’est pas le cas ici (et heureusement, car parfois l’erreur est dans le détail fastidieux).

Depuis près de deux ans, Sylvain Boulmé, moi-même et notre doctorant Cyril Six travaillons à l’ajout d’optimisations dans CompCert, notamment afin d’adapter ce compilateur à des processeurs sans exécution dans le désordre, et en premier lieu le MPPA3 de la société Kalray.

Nous appliquons en cela une idée que nous avons mise en œuvre depuis des années dans d’autres contextes (calcul sur les polyèdres convexes, test de satisfaisabilité booléenne…) et d’ailleurs déjà mise en œuvre dans CompCert (allocation de registres) : nous décomposons notre optimisation en un oracle (un morceau de programme qui fournit un résultat sans qu’on n’ait à démontrer quoi que ce soit sur la correction de ce résultat) et un vérificateur (qui vérifie que ce qui a été fourni par l’oracle était correct), et nous ne démontrons formellement que la correction du vérificateur. Ceci offre plusieurs avantages :

  1. Il est plus simple de démontrer que le vérificateur ne se trompe jamais que de démontrer que l’oracle va toujours produire une solution correcte. (Dans certains cas l’oracle met en jeu un algorithme de recherche complexe ; dans d’autres, l’argument de correction est global, tandis que la vérification de correction peut se faire localement.)

  2. On peut parfois changer l’oracle sans changer le vérificateur.

  3. Le même vérificateur peut parfois servir à plusieurs optimisations.

Nous utilisons notamment des vérificateurs qui vont symboliquement exécuter des fragments de programme et s’assurer que la traduction est fidèle en constatant qu’in fine les deux fragments de programme calculent la même chose.

Le problème scientifique derrière tout cela est : quelles définitions, quels invariants poser pour justifier la correction de ces transformations ? La preuve formelle nous oblige à affiner les concepts. On peut s’apercevoir que certaines hypothèses traditionnellement utilisées sont en fait inutiles (comme par exemple dans mon travail sur les opérateurs d’élargissement), ou que certains concepts sont en fait mal définis…