Tahina Ramananandro > Recherche >

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

Divers

Dernière modification le 12 septembre 2007