Informations

Une sémantique dénotationnelle pour un compilateur synchrone vérifié
soutenue le 20 décembre 2024 devant un jury constitué de :

directeurs Timothy Bourke Inria
Marc Pouzet ENS
rapporteurs Sylvain Boulmé Grenoble INP
Christine Paulin-Mohring Université Paris-Saclay
examinateurs Michael Mendler Université de Bamberg
César Muñoz NASA
Xavier Rival Inria
Yannick Zakowski Inria

Résumé

Lustre est un langage synchrone de type flot de données. Sa structure temporelle discrète et son système d'horloges lui permettent de garantir un temps d'exécution et une consommation de mémoire bornés statiquement, favorisant ainsi son adoption dans le domaine de systèmes critiques, notamment au sein de l'outil industriel Scade. Vélus, développé à l'Inria, est un compilateur Lustre vérifié. En s'appuyant sur la définition d'une sémantique formelle pour chaque langage intermédiaire, il apporte une preuve qu'un programme Lustre et sa traduction en Clight (langage pris en charge par CompCert) exhibent des comportements identiques.
Dans cette thèse, nous développons un nouveau modèle du noyau flot de données du langage d'entrée, basé sur une sémantique dénotationnelle synchrone, et donnons les conditions exactes de son équivalence avec le modèle relationnel existant dans Vélus. Cette approche constructive permet d'obtenir une sémantique exécutable, renforçant ainsi le principal théorème de correction de la compilation. Grâce au principe d'induction de Scott, propre à la sémantique dénotationnelle, nous menons des raisonnements très naturels sur la dynamique des programmes, moyennant un traitement explicite des erreurs pouvant survenir à l'exécution. Enfin, nous explorons la possibilité de s'affranchir des contraintes de synchronisation du langage en proposant une correspondance formelle de notre modèle avec celui des réseaux de Kahn. Nous esquissons les principes de l'infrastructure nécessaire à un raisonnement vérifié de bout en bout sur les programmes compilables.

Le code source du développement associé est disponible sous la licence non commerciale Inria à cette adresse.