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 9 mai, 10h30

                          ------------------------
                          Francesco Zappa Nardelli
                          ------------------------

                                   INRIA

                 =========================================
                 Verifying Fence Elimination Optimisations
                 =========================================

We consider simple compiler optimisations for removing redundant memory fences
in programs running on top of the x86-TSO relaxed memory model. While the
optimisations are performed using standard thread-local control flow analyses,
their correctness is subtle and relies on a non-standard global simulation
argument. The implementation and the proof of correctness are programmed in
Coq as part of CompCertTSO, a fully-fledged certified compiler from a
concurrent extension of a C-like language to x86 assembler. In this talk I
will describe the soundness proof of the optimisations and evaluate their
effectiveness.

Avec Viktor Vafeiadis (MPI-SWS).