An Asynchronous soundness theorem for concurrent separation logic

TL;DR

This paper introduces an asynchronous game semantics framework for concurrent separation logic, providing a new conceptual proof of soundness and clarifying the logic's guarantees against data races.

Contribution

It develops a novel asynchronous semantics for CSL inspired by game theory, establishing a soundness theorem with a fibrational property that clarifies the logic's correctness guarantees.

Findings

Defines asynchronous transition systems for programs and their environments.

Establishes that derivation trees correspond to winning strategies in the semantics.

Proves an asynchronous soundness theorem ensuring the absence of 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 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\vdash\{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.