An Asynchronous soundness theorem for concurrent separation logic

07/21/2018
by   Paul-André Melliès, et al.
0

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 π of a judgment Γ{P}C{Q} defines a winning and asynchronous strategy [π]_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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset