An Asynchronous Soundness Theorem for Concurrent Separation Logic

Authors: Paul-André Melliès and Léo Stefanesco

Paper Information

Title:An Asynchronous Soundness Theorem for Concurrent Separation Logic
Authors:Paul-André Melliès and Léo Stefanesco
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Concurrent Separation Logic, Asynchronous Games, True Concurrency, Data Races

ABSTRACT. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop 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 two basic fibrational properties. We advocate that these two fibrational properties provide a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

Talk:Jul 10 16:00 (Session 57C)