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

           Vous pouvez vous abonner à nos annonces de séminaires
                    http://pauillac.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 septembre, 10h30

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

                                   INRIA

              ================================================
              The Semantics of x86 Multiprocessor Machine Code
              ================================================

en collaboration avec M. Myreen, S. Owens, S. Sarkar, P. Sewell (U.
Cambridge) et J. Alglave, T. Braibant (INRIA)

For performance reasons, multiprocessors may reorder memory accesses
in various ways: a shared-memory concurrent program might exhibit
behaviours that cannot be obtained interleaving its memory accesses.
These subtle behaviours are usually described only in ambiguous
prose, leading to widespread confusion.  We develop a rigorous and
accurate semantics for x86 multiprocessor programs, from instruction
decoding to relaxed memory model, mechanized in HOL.  We test the
semantics against actual processors and the vendor litmus-test
examples, and give an equivalent abstract-machine characterisation of
our axiomatic memory model.  For programs that are (in some precise
sense) data-race free, we prove in HOL that their behaviour is
sequentially consistent.  We also contrast the x86 model with some
aspects of PowerPC and ARM behaviour.