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 15 novembre, 10h30

                                 ----------
                                 Mark Batty
                                 ----------

                          University of Cambridge

                       =============================
                       Mathematizing C++ Concurrency
                       =============================

Shared-memory concurrency in C and C++ is pervasive in systems programming,
but has long been poorly defined. This motivated an ongoing shared effort by
the standards committees to specify concurrent behaviour in the next versions
of both languages. They aim to provide strong guarantees for race-free
programs, together with new (but subtle) relaxed-memory atomic primitives for
high-performance concurrent code. However, the current draft standards, while
the result of careful deliberation, are still rather far from clear and
rigorous definitions.

In this talk I will present a mathematical (yet readable) semantics for C++
concurrency.  We aim to capture the intent of the current draft as closely as
possible, but discuss a number of points where this is not straightforward.  I
will show that a proposed x86 implementation of the concurrency primitives is
correct with respect to the x86-TSO model, and describe our CPPMEM tool for
exploring the semantics of examples, using code generated from our
Isabelle/HOL definitions.

This will aid discussion of any further changes to the draft standard, provide
a correctness condition for compilers, and give a much-needed basis for
analysis and verification of concurrent C and C++ programs.

(in collaboration with Scott Owens, Susmit Sarkar, Peter Sewell, Tjark Weber)