An Asynchronous Soundness Theorem for Concurrent Separation Logic

DOI10.1145/3209108.3209116zbMATH Open1497.68349arXiv1807.08117OpenAlexW2798452697WikidataQ130838830 ScholiaQ130838830MaRDI QIDQ5145346FDOQ5145346

Paul-André Melliès, Léo Stefanesco

Publication date: 20 January 2021

Published in: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

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

p i

of a judgment

G a m m a v d a s h P C Q

defines a winning and asynchronous strategy

[p i]_{S e p}

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

m a t h c a l L : [C]_{S} o [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 work available at URL: https://arxiv.org/abs/1807.08117

zbMATH Keywords

concurrent separation logic data races asynchronous game semantics asynchronous machine models separated states stateful-to-stateless translation

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cited In (2)

This page was built for publication: An Asynchronous Soundness Theorem for Concurrent Separation Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5145346)