Sites Inria

Séminaire

Séminaire Gallium

  • Date : 8/07/2019
  • Lieu : Inria de Paris - Salle JLL1
  • Intervenant(s) : Cyril Six
  • Organisateur(s) : Equipe-projet Gallium

Certified and modular postpass-scheduling for VLIW processors in CompCert

Cyril Six (Verimag, Université Grenoble Alpes) 

CompCert  is a C  compiler with a formal, machine-checked, proof of semantic preservation between the source and the target code. It is moderately optimizing; in particular, it does not reorder instructions. In-order processors and, more specifically, VLIW  processors such as the Kalray  core (featuring explicit parallelism at the instruction level), get poor performance if no instruction reordering is done by the compiler.
After briefly introducing VLIW  processors with the example of the Kalray  core, and their interest for safety-critical applications, I will present the formal semantics of a VLIW  assembly that we adopted in CompCert . Then, I will present a scalable, efficient approach for an intra-block scheduling of instructions in the back-end of CompCert. It is inspired by the work of Tristan and Leroy on their list-scheduling verifier [POPL-2008], but uses verified hash-consing to make it scalable.
This is joint work with Sylvain Boulmé and David Monniaux (my academic PhD advisers at Verimag), my PhD is also supervised by Benoît Dupont de Dinechin (Kalray).

CompCert  is a C  compiler with a formal, machine-checked, proof of semantic preservation between the source and the target code. It is moderately optimizing; in particular, it does not reorder instructions. In-order processors and, more specifically, VLIW  processors such as the Kalray  core (featuring explicit parallelism at the instruction level), get poor performance if no instruction reordering is done by the compiler.
After briefly introducing VLIW  processors with the example of the Kalray  core, and their interest for safety-critical applications, I will present the formal semantics of a VLIW  assembly that we adopted in CompCert . Then, I will present a scalable, efficient approach for an intra-block scheduling of instructions in the back-end of CompCert. It is inspired by the work of Tristan and Leroy on their list-scheduling verifier [POPL-2008], but uses verified hash-consing to make it scalable.
This is joint work with Sylvain Boulmé and David Monniaux (my academic PhD advisers at Verimag), my PhD is also supervised by Benoît Dupont de Dinechin (Kalray).

Mots-clés : Séminaire Gallium Séminaire CompCert

Haut de page

Suivez Inria