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.