Sites Inria

English version

Séminaire des équipes de recherche

An asynchronous soundness theorem for concurrent separation logic

© INRIA Sophie Auvin - G comme Grille

Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks.

  • Date : 4/06/2018
  • Lieu : Inria de Paris, 2 rue Simone Iff, 75012 Paris, bâtiment C, salle J.L. Lions 1 - 10:30 am
  • Intervenant(s) : Léo Stefanesco (IRIF)

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.


Mots-clés : Asynchronous soundness Séminaire Gallium Inria de Paris Léo Stefanesco (IRIF)

Haut de page

Suivez Inria