Salle 206
20 septembre 2018 - 14h00
Compilateur CompCert certifié pour processeur VLIW Kalray
par Cyril Six de Kalray & Verimag
Résumé : Les processeurs VLIW [Fisher, 1983], acronyme de « Very Long Instruction Word », sont conçus pour donner aux programmes assembleurs du contrôle sur la façon de paralléliser les ressources de processeur à chaque instruction. Autrement dit, une instruction VLIW représente un certain agrégat de calculs atomiques à exécuter en parallèle sur les unités de calcul (d'où leur très grande taille). Par rapport aux architectures hautes performances classiques (par exemple, les x86 modernes) qui réordonnent et parallélisent les instructions du programme en cours d'exécution, un tel processeur offre une plus grande puissance de calcul, en utilisant moins de ressources (taille spatiale et consommation énergétique), et des temps de calculs plus faciles à borner statiquement (e.g. WCET).
La contrepartie de cette simplicité du processeur est qu’il faut des compilateurs plus complexes pour en exploiter tout le potentiel. Un tel compilateur doit en effet trouver une façon efficace de découper le comportement du programme de haut niveau (typiquement du C) en une séquence de calculs atomiques parallèles.
CompCert [Leroy et al., 2006-2018] est un compilateur C optimisant, développé et certifié en Coq, utilisé dans l'industrie des systèmes embarqués critiques depuis 2015. Ce compilateur génère des programmes assembleurs pour différentes cibles, mais qui ont toutes une sémantique assembleur sans parallélisme.
Cyril Six démarre une thèse CIFRE Kalray/Verimag pour permettre à CompCert de produire des programmes assembleurs optimisés pour le prochain processeur VLIW de Kalray. Il va présenter le contexte scientifique de son sujet de thèse au carrefour de trois thématiques: les processeurs VLIW, les compilateurs optimisants, et la certification de logiciels.
