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

De Ensiwiki
Aller à : navigation, rechercher
(Prérequis)
 
Ligne 11 : Ligne 11 :
 
[http://compcert.inria.fr/ 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 [https://coq.inria.fr/ Coq] que tout programme assembleur produit par le compilateur a bien le comportement spécifié par le programme source en C.
 
[http://compcert.inria.fr/ 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 [https://coq.inria.fr/ 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 [https://www.kalrayinc.com/ 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 [https://en.wikipedia.org/wiki/Instruction-level_parallelism 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 [https://hal.archives-ouvertes.fr/hal-02185883 notre pré-publication].
+
Dans l'équipe PACSS, nous avons étendu CompCert pour optimiser l'utilisation du pipeline sur un processeur [https://www.kalrayinc.com/ 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 [https://en.wikipedia.org/wiki/Instruction-level_parallelism 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 [https://hal.archives-ouvertes.fr/hal-02185883 notre pré-publication].
  
 
=== 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.
+
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 ===
 
=== Prérequis ===
Ligne 22 : Ligne 22 :
  
 
Prendre en main un outil comme Coq est assez long, rentrer dans CompCert (des centaines de milliers de lignes de Coq) aussi.  
 
Prendre en main un outil comme Coq est assez long, rentrer dans CompCert (des centaines de milliers de lignes de Coq) aussi.  
Il est possible de contribuer dans ce stage sans faire de Coq: par exemple, en travaillant sur l'oracle.
+
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.

Version actuelle en date du 23 octobre 2019 à 16:38


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.