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 - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                             Lundi 4 juin, 10h30

                                --------------
                                Léo Stefanesco
                                --------------

                                     IRIF

      =================================================================
      An asynchronous soundness theorem for concurrent separation logic
      =================================================================

Concurrent separation logic (CSL) is a specification logic for concurrent
imperative programs with shared memory and locks. In this talk, I will present
a concurrent and interactive account of the logic inspired by asynchronous
game semantics. To every program C, we associate a pair of asynchronous
transition systems [C]S and [C]L which describe the operational behavior of
the Code when confronted to its Environment, both at the level of machine
states (S) and of machine instructions and locks (L). We then establish that
every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and
asynchronous strategy [π] with respect to both asynchronous semantics [C]S and
[C]L. From this, we deduce an asynchronous soundness theorem for CSL, which
states that the canonical map L : [C]S → [C]L from the stateful semantics [C]S
to the stateless semantics [C]L satisfies a basic fibrational property. We
advocate that this fibrational property provide a clean and conceptual
explanation for the usual soundness theorem of CSL, including the absence of
data races.

This is joint work with Paul-André Melliès.