Compatibilité du code généré avec CompCert

Télécharger le fichier pdf d’un mémoire de fin d’études

Un petit programme flot de données

Nous pouvons à présent écrire notre premier (et dernier) programme en Lustre (ver-sion 4) [53]. Un programme en Lustre se présente comme un système d’équations paramétrées par des suites et définissant des suites. Parmis les suites du systèmes, certaines doivent être retournées afin de pouvoir exploiter la solution du système trouvé. Toutes les autres suites du système sont alors inaccessibles de l’extérieur.
Ces équations doivent respecter les propriétés suivantes :
Cloture Toute suite utilisée dans le système doit être définie par une équation du système à l’exception des paramètres du système.
Concision Toute suite définie dans le système ne peut l’être qu’au plus une fois.
Causalité Tout terme de suite ne peut se calculer à partir de lui même.
La propriété de cloture garantit que tout est sous contrôle et qu’on ne dépend pas d’un facteur extérieur au programme en dehors de ses paramètres.
La propriété de concision n’apporte rien en soi, mais si on la retirait, il faudrait être en mesure de pouvoir décider si les deux équations définissant bien la même suite, ce qui est trop complexe à réaliser, en plus d’être inutile en pratique.
La propriété de causalité assure existence et unicitié d’une solution pour un système clos 3. Elle exclut des équations de la forme un = un, un = un + 1 ou des systèmes comme un = vn + 1 ∧ vn = un − 1, mais autorise des équations de la forme un = 0->pre(1 + un).
Ce programme gère deux compteurs, l’un croissant et l’autre décroissant sur deux sous-suites complémentaires.
Dans le langage Ls qui est le langage source de notre chaîne de compilation, l’opéra-teur ->pre sera remplacé par un l’opérateur fby qui a le même comportement, mais dont l’argument gauche doit impérativement être une constante, et non une suite. L’opérateur current est remplacé par un opérateur merge qui prend en entrée deux suites complé-mentaires, c’est-à-dire ne pouvant pas simultanément définir une valeur au même indice, et retourne une suite qui remplit les trous de l’une avec la valeur de l’autre. Ceci évite, d’une part de se retrouver avec des valeurs indéfinies, et d’autre part de devoir mémoriser la valeur précédente. La traduction naturelle du programme Lustre dans Ls donne le programme défini en figure 1.5.

Compilation d’un petit programme

Le processus de compilation a deux problèmes à traiter. Le premier est de réussir à ne plus avoir de notion de suite afin de ne manipuler que des données que la machine sait utiliser, c’est-à-dire afin de ne traiter que des valeurs simples. Le second est comment organiser les calculs pour les rendre effectifs.

Passer des suites de valeurs aux valeurs simples

Un premier travail consiste à simplifier les équations en jeu, pour que le compilateur puisse traiter par la suite une seule information à la fois.
Pour cela, on va introduire de nouvelles variables, comme montré en figure 1.6.
Bien que ce soit à première vue évident quand on connaît la sémantique du langage, il faut encore se persuader que ce nouveau programme définit bien la même suite delta que l’ancien. C’est la partie II de cette thèse. Ici, il suffit d’utiliser un théorème de référence transparentielle ; en remplaçant toutes les nouvelles suites introduites par leur définition, on retrouve à la virgule près le programme d’origine, et le théorème permet de conclure.
Après cette étape, on peut facilement identifier quelles valeurs sont passées entre les suites, il s’agit des variables dp et dn. Ces deux valeurs auront un statut particulier, celui de mémoires du programme. Une façon d’éliminer les suites pour se focaliser sur les valeurs est d’appeler le programme avec une valeur de la suite et une mémoire reflétant les calculs effectués jusqu’à présent, et de récupérer la sortie correspondante, ainsi que la nouvelle mémoire.
La figure 1.7 illustre cette idée ; on voit en particulier que le calcul de la mémoire suivante ne se fait qu’à partir de la mémoire précédente et de l’entrée. Il n’y a jamais accès ni au futur ni à des mémoires calculées plusieurs étapes auparavant.

Expliquer comment calculer

Maintenant, le compilateur doit transformer le programme pour expliquer à la machine comment calculer. Comme nous avons déjà simplifié les équations et qu’elles sont toutes de la forme x = f(…) où f est une fonction des valeurs à calculer, il suffit d’effectuer un tri topologique des équations en suivant les dépendances de données.
Cependant certaines valeurs peuvent en apparence dépendre d’elles mêmes. C’est no-tamment le cas de dn qui dépend de dn_pre qui dépend de dn_pre0 qui dépend de delta qui dépend de dn. Ce problème est résolu en remarquant que dn est une mémoire, et donc que sa valeur précédente est déjà connue. On peut donc la diviser en deux versions, dn qui est la valeur avant de commencer l’itération et dn0 qui est la valeur à la fin de l’itération.
On part donc du principe selon lequel delta, dp et dn sont déjà définis. La seule équation alors bien définie est delta = merge sign (True -> dp) (False -> dn);. Ce sera donc la première instruction à exécuter.
Maintenant, delta est aussi défini, et les équations dp_pre0 = delta+1; ainsi que dn_pre0 = delta-1; deviennent aussi bien définies et peuvent être exécutées.
Une fois les variables dp et dn devenues inutiles, on peut les écraser avec les nou-velles valeurs de dp0 et dn0. On peut donc ajouter vers la fin du programme les équations dp0 = 0 fby dp_pre et dn0 = 0 fby dn_pre.
Il n’y a pas une unique façon d’ordonner les équations. Le programme donné en fi-gure 1.8 correspond à l’un des multiples ordonnancements possibles.

Traduction vers du code impératif

Le code obtenu n’est pas encore tout à fait impératif. En effet, les opérateurs merge et when n’ont pas d’équivalent dans la plupart des langages de programmation impérative. ; il faut encore les encoder dans des structures de contrôle.
De plus, la compilation doit produire une procédure qui attend des entrées et une mé-moire qu’elle doit modifier à chaque itération. Il est donc nécessaire d’identifier précisément quelle est la mémoire nécessaire et comment l’initialiser.
La compilation doit donc produire une mémoire initiale et une procédure d’itération, que l’on regroupe dans un objet.
Le langage vers lequel est compilé notre langage synchrone s’appelle Obc.
Le code brut après traduction est donné en figure 1.9.
Ce code est séquentiel, et la compilation peut s’arrêter ici. Cependant le code est particulièrement inefficace, et on peut encore lui appliquer des passes d’optimisation pour obtenir un code plus léger et rapide. En particulier, on peut regrouper les switch entre eux et faire de la propagation de constantes pour obtenir le code en figure 1.10.
La chaîne de compilation est résumée en figure 1.11.

Compilation C

La certification s’arrête ici. Certifier formellement vers un langage usuel, tel que C ou Java, impliquerait la définition d’une sémantique formelle de ce langage, ainsi que la formalisation de ce que l’on entendrait par préservation de la sémantique par compilation.
En effet, la compilation présentée ne produit pas un code exécutable, mais une biblio-thèque de fonctions à appeler dans une boucle. Or certains langages compilables, comme le sous ensemble de C utilisé dans CompCert [36] ont bien été formalisés, mais donnent une sémantique non pas à une bibliothèque de fonctions, mais à la fonction principale d’un programme.
De plus, il est préférable de s’arrêter dans un langage qui puisse être facilement traduit dans d’autres, ce qui est le cas de Obc.
Une traduction possible vers C est tout de même donnée dans les figures 1.13 et 1.14. La mémoire du programme se traduit en une structure contenant toutes les valeurs à passer entre appels (ici dp et dn), ainsi qu’une fonction d’initialisation de cette mémoire (qui, ici, met à 0 ces deux valeurs).
La fonction d’itération prend en arguments une référence vers une mémoire, les entrées du programme (ici sign) et des références vers les sorties (ici delta).
Pour utiliser le programme généré, il faut alors commencer par réserver une mémoire et l’initialiser. Ensuite, il faut placer la fonction d’itération dans une boucle qui récupère la suite des valeurs d’entrées et calcule les valeurs de sorties pour les utiliser, comme en figure 1.12.
À titre de comparaison, voici aussi les versions compilées à partir du compilateur Lustre (version 4), et réédité à la main pour le rendre plus lisible et lui donner une interface comparable.
On y voit en particulier que la mémoire doit contenir une information supplémentaire d’initialisation. Avoir une expression à gauche de ->pre au lieu d’une constante à gauche de fby oblige calculer la valeur initiale au bon moment, et donc à tester si on est dans l’instant initial.

Table des matières

Introduction 
0.1 Quel est le titre de cette thèse ?
0.1.1 Langages, systèmes formels, sémantique, compilation
0.1.2 Systèmes critiques et temps réel
0.1.3 Les langages synchrones [5]
0.1.4 Certification, qualification, validation et vérification
0.2 Motivation
0.3 Structure de la thèse
0.4 À propos des dessins
I Architecture générale du compilateur 
1 Exemple introductif 
1.1 Un petit programme flot de données
1.1.1 Définition d’une suite récurrente
1.1.2 Échantillonnement de flots
1.1.3 Un petit programme flot de données
1.2 Compilation d’un petit programme
1.2.1 Passer des suites de valeurs aux valeurs simples
1.2.2 Expliquer comment calculer
1.2.3 Traduction vers du code impératif
1.2.4 Compilation C
2 Notions de base 
2.1 Notations mathématiques
2.2 Types, constantes, opérateurs et interfaces
2.2.1 Interfaces
2.2.2 Types
2.2.3 Valeurs, valeurs non étendues et valeurs étendues
2.2.4 Flots
2.2.5 Produit de types et signatures
2.2.6 Opérateurs
2.3 Noeuds et sémantiques
2.4 Environnement local et horloges
2.5 Typage, causalité et bonne formation
2.5.1 Typage et vérification des horloges
2.5.2 Bonne formation
2.5.3 Causalité
2.6 Conclusion
3 Modèles de compilation préservant la sémantique 
3.1 Sémantique de Kahn
3.1.1 Cadre formel
3.1.2 Machines à états
3.1.3 Machines à états finis
3.2 Unification des sémantiques
3.2.1 Contraintes sur la sémantique instantanée
3.2.2 Contraintes sur la sémantique flots de données
3.2.3 Relèvement de sémantiques
3.3 Préservations de sémantique
3.3.1 Compilateurs
3.3.2 Complétude et correction de compilateurs
3.3.3 Nature des compilateurs
3.3.4 Natures de sémantiques
3.3.5 Lemmes de sémantique élémentaires
3.4 Extraction d’un compilateur certifié
3.4.1 Présentation du langage Coq [7, 11]
3.4.2 Extraction de programmes Coq vers Ocaml
3.4.3 Procédures de décision et de vérification
3.5 Certificats et validations
3.5.1 Certification directe
3.5.2 Une forme de validation
3.5.3 Compilation assistée par serveur certifié
3.6 Conclusion
II Le monde flot de données 
4 Primitives flots de données 
4.1 Primitives sans mémoire
4.2 Primitives avec mémoire
4.3 Conclusion
5 Ls : syntaxe et sémantique 
5.1 Syntaxe du langage Ls
5.1.1 Exemples
5.2 Typage de Ls
5.2.1 Création de l’environnement de typage
5.2.2 Vérification du typage
5.3 Sémantique de Ls
5.3.1 Exemples
6 Lsn : syntaxe et sémantique 
6.1 Syntaxe de Lsn
6.2 Typage de Lsn
6.3 Sémantique de Lsn
7 Normalisation : de Ls à Lsn 
7.1 Schéma de l’algorithme de normalisation
7.2 Création de noms de flots intermédiaires
7.2.1 Présentation de la validation de cette passe
7.2.2 Algorithme d’introduction de nouvelles équations
7.3 Distribution des tuples
7.3.1 Présentation de l’algorithme
7.4 Le changement de syntaxe : de Ls vers Lsn
7.4.1 Présentation de l’algorithme
7.5 Conclusion
III Le monde instantané 
8 Lsni : syntaxe et sémantique 
8.1 Syntaxe de Lsni
8.2 Typage et bonne formantion dans Lsni
8.3 Sémantique de Lsni
8.3.1 Environnement et mémoire d’un noeud
8.3.2 Sémantique des expressions
8.3.3 Sémantique des équations
9 Instantiation et ordonnancement : de Lsn à Lsni 
9.1 L’instanciation
9.1.1 Relation d’instanciation
9.1.2 Preuve de l’algorithme
9.2 L’ordonnancement
9.2.1 Objectifs de l’ordonnancement
9.2.2 Quand lire, quand écrire ?
9.2.3 Certificat, et validation de l’ordonnancement
9.3 Conclusion
10 Obc : syntaxe et sémantique 
10.1 Syntaxe de Obc
10.2 Typage de Obc
10.3 Sémantique de Obc
10.3.1 Sémantique des expressions
10.3.2 Sémantique des instructions et des blocs
11 Génération de code : de Lsni à Obc 
11.1 Traduction de Lsni à Obc
11.1.1 Traduction des expressions simples
11.1.2 Traduction d’une équation
11.1.3 Traduction d’un noeud
11.2 Optimisations
11.2.1 Fusion des blocs de contrôle
11.2.2 Propagation des variables
11.2.3 Réduction du contrôle
11.2.4 Nettoyage des variables locales inutilisées
11.2.5 Déplacement d’instructions
11.2.6 Augmentation du contrôle
11.2.7 Enchaînement des optimisations
11.3 Conclusion
IV Conclusion 
12 Vers du code exécutable 
12.1 Génération de code C
12.2 Connexion avec CompCert
12.2.1 Compatibilité du code généré avec CompCert
12.2.2 Comment réinterpréter la sémantique d’Obc dans CompCert
13 Extensions du langage à considérer 
13.1 Extensions pour exprimer tout programme Lustre
13.1.1 Multi-horloges pour les entrées/sorties
13.1.2 Décalage de flots non initialisés
13.2 Extensions pour exprimer tout programme MiniLs
13.3 Extensions pour exprimer tout programme Heptagon
13.3.1 Automates hiérarchiques
13.4 Conclusion
14 Conclusion 
14.1 Travaux connexes
14.2 Contributions
14.3 Perspectives
Annexes 
A Optimisations
A.0.1 Conclusion
B Codes intermédiaires
B.1 Interface
B.2 Flot de données
B.2.1 Code source (Ls)
B.2.2 Après introduction de nouveaux flots (Ls)
B.2.3 Après distribution (Lsn)
B.3 Instantané
B.3.1 Après instanciation (Lsni)
B.3.2 Après ordonnancement (Lsni)
B.3.3 Après génération de code (Obc)
B.3.4 Après développement (Obc)
B.3.5 Après fusion des branches (Obc)
B.3.6 Après propagation des variables (Obc)
B.3.7 Après élimination de code mort (Obc)
B.3.8 Après élimination de code inutile (Obc)
B.4 Code cible (C)
B.4.1 Interface
B.4.2 Itération
B.4.3 Initialisation
B.5 Exemple d’utilisation (C)
C Références pour le développement en Coq
C.1 common : axiomes et fonctions générales (env. 2000 lignes)
C.1.1 Axioms.v (14 lignes)
C.1.2 CMapPositive.v (1367 lignes)
C.1.3 Coqlib.v (612 lignes)
C.1.4 Autres fichiers
C.2 minils : les structures syntaxiques (env. 1200 lignes)
C.2.1 Utils.v, Clocks.v, Consts.v, Types.v, Operators.v (322 lignes)
C.2.2 Vardec.v, Static.v (163 lignes)
C.2.3 Autres fichiers
C.3 ssemantics : sémantique synchrone (env. 3100 lignes)
C.3.1 SynchronousStreams.v, Primitives.v, DFPrimitives.v, DFPrimitivesFunctionnal.v (1119 lignes)
C.3.2 SSEnv.v, SSEnv_ext.v, SIEnv.v, Dynamic.v (966 lignes)
C.3.3 LSSemantics.v, LSNSemantics.v, LSNISemantics.v, ObcSemantics.v, Memory.v (1219 lignes)
C.4 ls : Propriétés et preuves concernant Ls (env. 4100 lignes)
C.4.1 LSTyped.v, LSTypingValidator.v (1177 lignes)
C.4.2 prop/LSTyped_ext.v, prop/LSTypingCoherency.v, prop/LSTypingUnicity.v, prop/LSDeterminism.v (916 lignes)
C.4.3 LSSubst.v, LSDist.v, LSNorm.v (308 lignes)
C.4.4 LSDistPreservation.v, LSNormPreservation.v LSSubstPreservation.v (1479 lignes)
C.5 ls_to_lsn : compilation de Ls vers Lsn (env. 1000 lignes)
C.5.1 LSSubst_Validator.v, LSDistValidator.v, LSNormValidator.v (788 lignes)
C.5.2 LS2LSN.v (178 lignes)
C.6 lsn : propriétés et preuves concernant Lsn
C.6.1 LSNTyped.v (168 lignes)
C.6.2 LSNInst.v (96 lignes)
C.6.3 LSNInstPreservation.v (1185 lignes)
C.7 Fichiers en Ocaml
C.7.1 Analyse syntaxique de Ls
C.7.2 Affichage des codes produits
C.7.3 Générateurs de certificats
C.7.4 Le compilateur
D Justifications de quelques choix d’implémentation
D.0.5 La relation de substitution
D.0.6 Ajout de valeurs dans un flot
D.0.7 Fonctions et prédicats
D.0.8 Sémantique avec absences et sémantique de Kahn
D.0.9 Inductifs et coinductifs
Index
Notations

Télécharger le rapport complet