To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 16/03/09 - Paris - FR

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

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                         Amphi Turing du bâtiment 1

                            Lundi 16 mars, 10h30

                              ----------------
                              Benoît Robillard
                              ----------------

                               Cedric, ENSIIE

     ==================================================================
     Vérification formelle et optimisation de l'allocation de registres
     ==================================================================

L'allocation de registres est une passe cruciale de compilation. Son
optimisation peut être plus ou moins poussée et fait le plus souvent appel à
des méthodes d'optimisation combinatoire, telles que la théorie des graphes ou
la programmation mathématique. Le modèle le plus classique est celui de la
coloration avec préférences d'un graphe dit graphe d'interférences. Ce
problème étant NP-complet, il peut soit être traité de manière heuristique en
temps polynomial, soit résolu de façon exacte en temps exponentiel.

Dans cet exposé, nous présentons nos travaux en cours visant à l'optimisation
et la vérification formelle d'algorithmes "efficaces" pour l'allocation de
registres. Nous détaillons plus précisément deux points. Tout d'abord, nous
décrivons une première implémentation en Gallina de l'heuristique impérative
actuellement implantée en Ocaml dans CompCert, ainsi que certains problèmes
sous-jacents comme notamment la terminaison de l'algorithme et l'implantation
des graphes. Nous introduisons ensuite un modèle de graphes d'interférence
plus précis ainsi qu'un processus de résolution exponentiel particulier à ces
graphes, combinant un algorithme de réduction du graphe et la programmation
mathématique. Nous évoquons en conséquence les méthodes envisagées pour la
vérification formelle d'algorithmes à base de programmation mathématique,
ainsi que les résultats obtenus sur l'"Optimal Coalescing Challenge".