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 8 octobre, 10h30

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

                                   INRIA

             =================================================
             Sound Optimisations in the C11/C++11 Memory Model
                    and Applications to Compiler Testing
             =================================================

Sometimes compilers introduce bugs: the generated code allows
behaviours forbidden by the semantics of the source program.  Most of
the time these misbehaviours materialise as soon as the code is
executed.  However, in some subtle cases, the compiler generates
perfect sequential code but breaks the memory model of the programming
language: unexpected behaviours become observable only when the
miscompiled function interacts with a concurrent context.  We call
these concurrency compiler bugs.  In this work we present cpptest, a
tool for hunting concurrency compiler bugs in modern C and C++
compilers.  First we prove correct a theory of sound optimisations in
the C11/C++11 memory model, covering most of the optimisations we have
observed testing real compilers (including eliminations, reorderings
and a restricted class of introductions of memory accesses).  Building
on this theory, we show how concurrency compiler bugs can be
identified by comparing the memory trace of compiled code against a
reference memory trace for the source code: this effectively reduces
the hard problem of hunting concurrency compilation bugs to
differential testing of sequential code.  The cpptest tool puts this
idea at work: at the time of writing, preliminary testing of gcc and
clang has already identified some mistaken write introduction
performed by the loop invariant motion optimisation in gcc 4.7.

This is work in progress with Robin Morisset and Pankaj Pawan.