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: | 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. |
Pages: | 11 |
Talk: | Jul 10 16:00 (Session 57C) |
Paper: |