To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 15/02/10 - Paris - FR

           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 - Rocquencourt
                         Amphi Turing du bâtiment 1

                          Lundi 15 février, 10h30

                                 ----------
                                 Dana N. Xu
                                 ----------

                                   INRIA

             =================================================
             A Practical and Precise Inference and Specializer
                for Array Bound Checks Elimination (PEPM'08)
             =================================================

Arrays are intensively used in many software programs, including those in the
popular graphics and game programming domains.  Although the problem of
eliminating array bound checks has been studied for a long time, there are few
works that attempt to be both aggressively precise and practical. We propose
an inference mechanism that achieves both aims by combining a forward
relational analysis with a backward precondition derivation. Our inference
algorithm works for a core imperative language with assignments, and analyses
each method once through a summary-based approach. Our inference is precise as
it is both path and context sensitive. Through a novel technique that can
strengthen preconditions, we can selectively reduce the sizes of formulae to
support a practical inference algorithm.  Moreover, we subject each inferred
program to a flexivariant specialization that can achieve good tradeoff
between elimination of array checks and code explosion concerns.  We have
proven the soundness of our approach and have also implemented a prototype
inference and specialization system. Initial experiments suggest that such a
desired system is viable.