Synthesis of certified compilers

es bugs dans les compilateurs, même s'ils sont relativement rares dans les compilateurs de production pour les familles de processeurs les plus répandues, sont particulièrement insidieux : un code source correct peut être compilé en un code assembleur incorrect, et des changements du code source destinés à mieux cerner l'erreur peuvent faire disparaître le bug. Dans certains contextes (p.ex. logiciels de contrôle-commande critiques niveau A en aviation civile), on peut exiger une traçabilité du code source au code objet qui exclut en pratique l'utilisation d'optimisations, d'où une utilisation très sous-optimale du processeur cible. Cela est d'autant plus dommageable que dans ce contexte, mettre un processeur plus rapide, mais plus complexe et potentiellement plus erroné ou nécessitant une forte dissipation thermique, ou encore un processeur multi-cœur, avec des problèmes de programmation concurrente, ne sont pas des options forcément acceptables. Une solution a été apportée par le compilateur CompCert: la traçabilité entre code source et code objet est assurée par une preuve mathématique de raffinement de programmes au travers de toutes les phases de traduction et d'optimisation. Cette preuve est elle-même formellement vérifiée par l'assistant de preuve Coq. Preuve de l'intérêt industriel pour cette solution, CompCert est actuellement commercialisé. Dans le cadre de sa thèse (toujours en cours à Verimag), Cyril Six a étendu CompCert pour lui ajouter comme cible le processeur Kalray KVX, avec réordonnancement d'instructions — CompCert, de base, ne réordonne pas les instructions, ce qui est pénalisant sur les processeurs superscalaires sans réordonnancement dynamique. Il s'avère que lors de l'ajout d'une nouvelle cible, il y a des étapes assez fastidieuses : définition des jeux d'instructions des différentes représentations intermédiaires et de leur sémantique formelle, modélisation du pipeline pour l'algorithme d'ordonnancement, etc., avec des informations transcrites depuis la documentation. Si ce travail a pu être mené manuellement à bien pour un nombre restreint d'instructions, il serait extrêmement pénible pour des jeux d'instructions étendus (que ce soit par des instructions SIMD ou par des extensions particulières destinées à accélérer tel ou tel type de calcul). Idéalement, on aimerait un système qui prenne la description du jeu d'instruction, du pipeline etc. et produirait la plus grande partie de la sélection d'instruction, des combinaisons d'instructions, des ordonnancements etc. et de leur preuve, voire produirait un « superoptimisateur » capable de recombiner des blocs complexes d'instructions. Dans le cadre de l'éco-système RISC-V, dont l'architecture ouverte et extensible va permettre une grande diversité de processeurs, un tel système permettrait de produire efficacement des compilateurs conciliant extrême spécialisation et extrême fiabilité. Le travail de thèse consisterait donc à concevoir un tel système, au besoin en utilisant des techniques telles que la satisfiabilité modulo théorie vérifiée.