An asynchronous soundness theorem for concurrent separation logic

DOI10.1145/3209108.3209116MaRDI QIDQ5145346zbMATH OpenOpenAlexWikidataFDO

Authors 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)

Full work available at URL https://arxiv.org/abs/1807.08117

zbMATH Keywords

concurrent separation logicdata racesasynchronous game semanticsasynchronous machine modelsseparated statesstateful-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)

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 $GammavdashPCQ$ 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 $mathcalL:[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.

Recommendations

• Revisiting concurrent separation logic
• Concurrent separation logic and operational semantics
• CONCUR 2004 - Concurrency Theory
• A semantics for concurrent separation logic
• Precision and the conjunction rule in concurrent separation logic

Cited in

(5)

• Revisiting concurrent separation logic
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• CONCUR 2004 - Concurrency Theory
• Aligning the representation and reality of computation with asynchronous logic automata
• Concurrent separation logic and operational semantics

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)