- 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).