An Asynchronous soundness theorem for concurrent separation logic

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 or Frame --- both at the level of machine states ($S$) and of machine instructions and locks ($L$). We then establish that every derivation tree $\pi$ of a judgment $\Gamma ⊢\{P\}C\{Q\}$ defines a winning and asynchronous strategy $[\pi {]}_{Sep}$ 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 $\mathcal{L}:[C{]}_S\to [C{]}_L$ from the stateful semantics $[C{]}_S$ to the stateless semantics $[C{]}_L$ satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

Full version of an extended abstract published at LICS 2018