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 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 proves {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 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 provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.