*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle U/V, etage -2                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 11 juillet  2003 **** 14h00 ****************************
(exceptionnellement, salle R, e'tage -2)

Benjamin Goldberg (Department of Computer Science, Courant Institute 
                   of Mathematical Sciences, New York University)

Translation Validation of Loop Optimizations

Re'sume': This talk describes the approach taken by the ACSys group at
NYU to performing translation validation for optimizing compilers that
perform loop reordering optimizations.  Rather than verifying the
compiler, translation validation performs a validation check after
every run of the compiler, producing a formal proof that the produced
target code is a correct implementation of the source code.

We will briefly describe our approach to validating optimizations
which preserve the loop structure of the code, and describe a tool,
VOC-64, which implements this technique.  For more aggressive
optimizations which alter the loop structure of the code, such as loop
distribution and fusion, loop tiling, and loop interchange, we will
then present permutation rules which establish that the transformed
code satisfies all the implied data dependencies necessary for the
validity of the considered transformation.
                          
Finally, we will discuss some preliminary work on run-time validation
of speculative loop optimizations, which involves using run-time tests
to ensure the correctness of loop optimizations of which neither the
compiler nor compiler-validation techniques can guarantee the
correctness. In this work, the theorem prover CVC is used not only to
prove that the verification conditions are satisfied, but to generate
the run-time tests.

This is joint work with Lenore Zuck, Amir Pnueli, Clark Barrett,
Yi Fang, and Ying Hu.

*** Relache du 14 juillet au 26 septembre 2002 *********************

*********************************************************************
Pour recevoir l'annonce par courrier electronique s'enregistrer sur
http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************