Vérification formelle d'une implémentation d'un gestionnaire de mémoire pour un compilateur certifié
J'ai effectué mon stage de DEA (M2, ou master) du 19 février au 27 juillet 2007 à l'INRIA Rocquencourt, au sein de l'équipe Gallium, sous la direction de Xavier Leroy, que je remercie ainsi que tous les membres de l'équipe Gallium.
L'équipe Gallium travaille sur la compilation certifiée : prouver que la sémantique du code objet produit par le compilateur est la même que la sémantique du code source. Pour cela, elle développe, à l'aide de l'assistant de preuve Coq, un compilateur certifié, CompCert. Il compile des programmes en langage Clight, un sous-ensemble de C, pour produire du code machine pour l'architecture PowerPC, via le langage intermédiaire Cminor. Le compilateur est obtenu par extraction de sa preuve de correction.
On voudrait rajouter un deuxième langage d'entrée, MiniML, un langage fonctionnel sous-ensemble d'OCaml. L'idée est donc de développer un compilateur certifié de MiniML vers Cminor, puis de réutiliser la partie du compilateur CompCert de Cminor vers PowerPC (que l'on appelle backend). C'est l'objet des travaux de Zaynah Dargaye. Comme MiniML est un langage de haut niveau, il faut intégrer à ce compilateur l'environnement d'exécution de MiniML, et notamment le gestionnaire de mémoire. Ces parties peuvent être des morceaux de code Cminor qui viendront compléter la traduction du programme MiniML vers Cminor.
Le but de mon stage est donc de prouver en Coq la correction et la terminaison d'implémentations en Cminor de gestionnaires de mémoire. J'ai choisi de traiter le cas d'un GC mark and sweep.
Ainsi, à long terme, à la suite des travaux de Stéphane Glondu destinés à certifier la procédure d'extraction de Coq vers MiniML, alors l'ensemble du compilateur et sa génération seront entièrement certifiés.
Fichiers du stage
- Diaporama de la soutenance (PDF) au MPRI, le 5 septembre 2007. Également au format OpenDocument Presentation (ODP).
- Rapport de stage (PDF).
- Fiche de synthèse (PDF).
- Sources Coq de la preuve du GC. À lire
avec le rapport. Vous pouvez également télécharger l'archive compressée aux
formats TAr.GZ.
La compilation de ces sources requiert les sources de CompCert ; or celles-ci ne sont pas intégralement disponibles librement au public. Merci d'écrire à Xavier Leroy pour de plus amples informations.
Divers
Dernière modification le 12 septembre 2007