IRL - TITRE DU PROJET : 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... »)
 
(avertissement pour étourdis (comme moi).)
 
Ligne 1 : Ligne 1 :
{{Sujet irl
+
Cette page n'est pas censée être modifiée.  
| labo = VERIMAG
+
Pour créer votre page, il faut suivre les recommandations de [[Introduction_A_La_Recherche_En_Laboratoire_2A#Instructions]]
| titre = Compilation optimisée formellement prouvée
+
| equipe = PACSS (Proofs and Code analysis for Safety and Security)
+
| encadrants = sylvain.boulme@univ-grenoble-alpes.fr
+
}}
+
[[Catégorie:IRL]]
+
 
+
=== Contexte ===
+
 
+
[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].
+
 
+
=== Objectif ===
+
 
+
=== Prérequis ===
+
 
+
Intérêt pour la vérification formelle, l'algorithmique, la programmation et la compilation.
+

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

Cette page n'est pas censée être modifiée. Pour créer votre page, il faut suivre les recommandations de Introduction_A_La_Recherche_En_Laboratoire_2A#Instructions