Vous pouvez vous abonner à nos annonces de séminaires
		    http://gallium.inria.fr/seminaires/

			     S E M I N A I R E
			   __
			  / _`  _   /  /  o
			 /   ) __) /  /  / /  / /\/|
			(___/ (_/ (_ (_ / (__/ /   |

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                            Lundi 8 juillet, 14h00

                                  ---------
                                  Cyril Six
                                  ---------

                      Verimag, Université Grenoble Alpes

  =========================================================================
  Certified and modular postpass-scheduling for VLIW processors in CompCert
  =========================================================================


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