To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 18/06/07 - 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 18 juin, 10h30

                                ------------
                                Andrew Appel
                                ------------

                            Princeton University

                  =======================================
                  Threads Can Be Implemented As a Library
                  =======================================

Hans Boehm, in "Threads Cannot Be Implemented as a Library" (2005),
writes, "In many environments, multi-threaded code is written in a
language that was originally designed without thread support (e.g. C),
to which a library of threading primitives was subsequently added. There
appears to be a general understanding that this is not the right
approach. We provide specific arguments that a pure library approach, in
which the compiler is designed independently of threading issues, cannot
guarantee correctness of the resulting code."
   This is an inconvenient truth. But I will show how, _almost_
independently of the threading issues, to write compilers, prove them
correct,  prove the soundness of a Separation Logic, or otherwise reason
about operational semantics.  While doing this we can pretend that our
language is deterministic and sequential, extensible with some
yet-to-be-specified pseudodeterministic pseudosequential operations that
implement the threads and concurrency.
    I will describe a specification in Coq of Extensible C Minor, its
operational semantics, and the Coq-checked soundness proof (joint work
with Sandrine Blazy) of its Separation Logic.  The CompCert compiler
could, in principle, be proved correct w.r.t. this specification.  These
proofs can assume determinism and sequentiality.
    With the null extension it is simply (a small-step variant of)
Leroy's C Minor.  With the concurrency extension (joint work with
Aquinas Hobor and Francesco Zappa Nardelli), it is a concurrent C with
threads and locks, but the soundness proofs of the Separation Logic and
the CompCert compiler do not need to be changed.  Other extensions are
also possible.