To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Cristal - 19/12/02 - Paris - FR

L'exposé de Simon P. Jones à 10h30 a également lieu au Batiment 7
(contrairement à la précédente annonce)

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


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                        Salle de conference du Bat 7

                          Jeudi 19 decembre, 11h30

                               -------------
                               Atsushi Ohori
                               -------------

                                   JAIST

                ===========================================
                Register Allocation by Proof Transformation
                ===========================================


   We  interpret  structural rules  in  a  sequent  style proof  system  as
   register  manipulation  instructions,  and develop  a  proof-theoretical
   framework  for  register allocation.   The  framework  accounts for  the
   entire  process  of register  allocation.   Liveness  analysis is  proof
   reconstruction (similar  to type inference), and  register allocation is
   proof  transformation from  a  proof system  with unrestricted  variable
   accesses to the one with  restricted variable access.  In our framework,
   the set of  registers acts as the ``working set''  of the live variables
   at  each instruction  step, which  changes during  the execution  of the
   code. This eliminates the  ad-hoc notion of ``spilling''.  The necessary
   memory-register  moves  are  systematically  incorporated in  the  proof
   transformation process.   Its correctness is  a simple corollary  of our
   construction;  the resulting  proof is  equivalent to  the proof  of the
   original code modulo  the treatment of structural rules.   This yields a
   simple yet  powerful register  allocation algorithm.  The  algorithm has
   been implemented, demonstrating the feasibility of the framework.

   (The  work  has not  yet  been published,  but  a  technical summary  is
   available. Interested one should contact the speaker.)