Compilation optimisée formellement prouvée : Différence entre versions

De Ensiwiki
Aller à : navigation, rechercher
(Page créée avec « {{Sujet irl | labo = VERIMAG | titre = Compilation optimisée formellement prouvée | equipe = PACSS (Proofs and Code analysis for Safety and Security) | encadrants = sylv... »)
 
(Objectif)
Ligne 14 : Ligne 14 :
  
 
=== Objectif ===
 
=== Objectif ===
 +
 +
L'objectif du stage sera soit d'étudier des améliorations de cette optimisation, soit de contribuer à porter cette optimisation sur 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 ===
 
=== Prérequis ===
  
 
Intérêt pour la vérification formelle, l'algorithmique, la programmation et la compilation.
 
Intérêt pour la vérification formelle, l'algorithmique, la programmation et la compilation.

Version du 23 octobre 2019 à 16:27


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 dans le pipeline. 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 certifié qui optimise le parallélisme d'instruction. Pour les détails: voir notre pré-publication.

Objectif

L'objectif du stage sera soit d'étudier des améliorations de cette optimisation, soit de contribuer à porter cette optimisation sur 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.