Détails sur le séminaire

Résumé : Les compilateurs sont des systèmes logiciels très complexes et peuvent donc contenir des bogues. Ces bogues peuvent se traduire par des erreurs au cours du processus de compilation ou, plus ennuyeusement encore, par la génération d’un code incorrect. Les bogues qui altèrent subtilement la sémantique des programmes générés sont souvent très insidieux et difficiles à retracer. Dans certaines applications, en particulier dans les systèmes embarqués critiques pour la sécurité et sujets à des exigences et régulations strictes (par exemple, avionique, trains, etc.), l’élimination de ces bogues est d’une importance capitale.
Bien que la plupart de ces bogues soient typiquement situés dans les passes d’optimisation, la désactivation des optimisations n’est pas une solution viable dans de nombreuses applications. En fait, la simple désactivation des optimisations ne suffit pas à garantir un code exempt de bogues. Les normes réglementaires imposent en général l’utilisation de processeurs simples et prédictibles, dont la performance dépend largement du compilateur.
Une solution alternative est d’employer un compilateur certifié, mécaniquement prouvé correct dans un assistant de preuve. Un tel compilateur assure que le code assembleur généré préserve fidèlement la sémantique du code source. CompCert appartient à cette catégorie, et est le premier compilateur C formellement vérifié et largement utilisé dans l’industrie. Cependant, prouver la correction d’optimisations complexes reste un défi. C’est pourquoi les compilateurs certifiés, y compris CompCert, produisent un code significativement moins performant que les compilateurs classiques tels que GCC ou LLVM.
La validation de traduction est une technique où seul le résultat d’une optimisation est vérifié, plutôt que de prouver la correction de son implémentation. L’algorithme d’optimisation, appelé oracle, reste considéré comme non fiable. Néanmoins, ses résultats sont toujours soumis à la validation par un validateur prouvé et conçu pour rejeter toute erreur.
Dans cette thèse, nous approfondissons le concept de validation de traduction guidée. Le principe est de permettre aux oracles de guider le validateur en lui fournissant des indices qui réduisent l’espace de recherche, minimisant ainsi la complexité du processus de validation. Plus précisément, nous proposons un interpréteur symbolique formellement vérifié capable de valider toute une classe de transformations. Notre outil demande aux oracles des invariants de programme en tant qu’indices pour guider la simulation symbolique du code original et du code optimisé. Le test de simulation prouvé valide défensivement les optimisations appliquées, en garantissant leur cohérence vis-à-vis du code non optimisé.
Nous avons validé avec succès plusieurs nouvelles transformations en utilisant cette approche, dont certaines n’avaient jamais été formellement vérifiées jusqu’alors, grâce à la communication entre les oracles et leur validateur. Notamment, nous avons vérifié une optimisation de ”strength-reduction” (littéralement, ”réduction de force”) ciblant les architectures RISC-V 64 bits, qui sont prometteuses dans le contexte des systèmes embarqués critiques pour la sécurité. En plus de la ”strength-reduction”, notre outil de simulation symbolique supporte l’élimination de redondances partielles, l’élimination du code mort, le déplacement de code, l’ordonnancement, et une forme faible de pipeline logiciel avec renommage.
Nous avons intégré notre mécanisme de validation dans notre version de développement (fork) de CompCert, en développant une nouvelle représentation intermédiaire nommée ”Block Transfer Language”, BTL (littéralement “Langage de Transfert en Blocs”). Les traductions de et vers BTL sont également validées de manière défensive, à l’aide d’un vérificateur dédié, formellement vérifié, et capable de valider de la duplication et factorisation de code en tant que morphismes des graphes de flux de contrôle. Pour évaluer rigoureusement l’impact de nos optimisations et le temps de compilation supplémentaire induit par leur validation, nous avons effectué de multiples mesures expérimentales du temps de compilation et des performances à l’exécution. Les optimisations spécifiques à une architecture cible ont été testées sur des plateformes AArch64 et RISC-V. Les résultats montrent une amélioration significative des performances à l’exécution tout en maintenant un temps de compilation raisonnable.
À l’avenir, cette même méthode pourrait potentiellement être appliquée pour valider d’autres transformations, comme l’insertion automatique de contre-mesures de sécurité. Nos conceptions semblent être applicables au-delà de CompCert.

Les tranparents de la presentation.

Phd defense of Léo Gourdin.
See https://lgourd.in/defense.html for more information (e.g. remote link).