Compilation optimisée formellement prouvée

De Ensiwiki
Aller à : navigation, rechercher


Compilation optimisée formellement prouvée

Labo VERIMAG
Equipe PACSS (Proofs and Code analysis for Safety and Security)
Encadrants sylvain.boulme@univ-grenoble-alpes.fr

Contexte

CompCert est le premier compilateur C optimisant qui soit formellement vérifié (ce compilateur est notamment utilisé pour produire du code embarqué critique, comme celui dans les systèmes de pilotage des Airbus, ou des alimentations de secours dans les centrales nucléaires). Pour chacun des processeurs cibles, il y a en effet une preuve mathématique formelle réalisée dans l'assistant de preuves Coq que tout programme assembleur produit par le compilateur a bien le comportement spécifié par le programme source en C.

Dans l'équipe PACSS, nous avons étendu CompCert pour optimiser l'utilisation du pipeline sur un processeur Kalray. Plus précisément, cette optimisation, qui se situe à la fin de la chaîne de compilation, change l'ordre des instructions du programme assembleur, sans changer la sémantique du programme, de manière à maximiser le parallélisme d'instruction. Techniquement, le réordonnancement est calculé par un oracle non prouvé: un vérificateur (vérifié en Coq) se charge de garantir que le réordonnancement proposé ne change pas la sémantique. A notre connaissance, ce compilateur est le premier compilateur formellement vérifié qui optimise le parallélisme d'instruction. Pour les détails: voir notre pré-publication.

Objectif

Le sujet du stage sera soit d'étudier des améliorations de cette optimisation, soit de contribuer à adapter cette optimisation pour d'autres architectures (comme ARM ou RISC-V). L'objectif sera précisé en fonction des goûts du stagiaire et de l'avancement des travaux de l'équipe. Dans tous les cas, le travail du stagiaire s'effectuera en collaboration avec l'équipe.

Prérequis

Intérêt pour la vérification formelle, l'algorithmique, la programmation et la compilation.

Prendre en main un outil comme Coq est assez long, rentrer dans CompCert (des centaines de milliers de lignes de Coq) aussi. Il sera possible de contribuer dans ce stage sans faire de Coq: par exemple, en travaillant sur l'oracle de réordonnancement. Cela supposera quand même de comprendre le fonctionnement du vérificateur de réordonnancement et sa preuve. Mais il sera bien sûr aussi possible de contribuer côté Coq.