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
                    Salle de conférences du bâtiment 7

                            Lundi 10 juin, 10h30

                            -------------------
                            Arthur Charguéraud
                            -------------------

                                   INRIA

===========================================================================
Verification of Concurrent Programs Targeting the x86-TSO Weak Memory Model
===========================================================================

Pretty much every computer sold today is multi-core. Taking advantage of
more than one core to speed up a program is a nontrivial problem in general.
Nevertheless, it has been shown that many algorithms can be relatively
easily parallelized on shared memory architecture by using appropriate
dynamic load balancing algorithms as well as a small number of classic
concurrent data structures. These components involve a fairly small amount
of code, however this code is extremely error-prone and very hard to debug.
These components are therefore an ideal target for program verification.
In this talk, I will recall the simple weak memory model associated with
Intel and AMD's x86 hardware, and explain how to build on top of this model
a logic for reasoning about concurrent programs. I will present concrete
code examples taken from a realistic scheduling library, show how they
can be verified by hand, and discuss the possibility of mechanizing and
automating the proofs.