Revisiting concurrent separation logic

DOI10.1016/J.JLAMP.2017.02.004MaRDI QIDQ2397039zbMATH OpenOpenAlexFDO

Authors Pedro Soares, António Ravara, Simão Melo de Sousa

Publication date 29 May 2017

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

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

zbMATH Keywords

structural operational semanticsconcurrent separation logicsoundness proof

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Semantics in the theory of computing (68Q55)

Abstract: We present a new soundness proof of Concurrent Separation Logic (CSL) based on a structural operational semantics (SOS). We build on two previous proofs and develop new auxiliary notions to achieve the goal. One uses a denotational semantics (based on traces). The other is based on SOS, but was obtained only for a fragment of the logic - the Disjoint CSL - which disallows modifying shared variables between concurrent threads. In this work, we lift such a restriction, proving the soundness of full CSL with respect to a SOS. Thus contributing to the development of tools able of ensuring the correctness of realistic concurrent programs. Moreover, given that we used SOS, such tools can be well-integrated in programming environments and even incorporated in compilers.

Recommendations

• Concurrent separation logic and operational semantics
• An asynchronous soundness theorem for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• A revisionist history of concurrent separation logic
• Oracle Semantics for Concurrent Separation Logic

Cites work

• scientific article; zbMATH DE number 47171 (Why is no real title available?)
• scientific article; zbMATH DE number 3569793 (Why is no real title available?)
• scientific article; zbMATH DE number 1841809 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A revisionist history of concurrent separation logic
• A semantics for concurrent separation logic
• A structural approach to operational semantics
• An axiomatic basis for computer programming
• Concurrent separation logic and operational semantics
• Resources, concurrency, and local reasoning
• Syntactic control of interference for separation logic
• Verifying properties of parallel programs

Cited in

(15)

• Barriers in Concurrent Separation Logic
• \textsc{SecCSL}: security concurrent separation logic
• Precision and the conjunction rule in concurrent separation logic
• On the relation between concurrent separation logic and concurrent Kleene algebra
• An asynchronous soundness theorem for concurrent separation logic
• Oracle Semantics for Concurrent Separation Logic
• Parameterized Memory Models and Concurrent Separation Logic
• Convolution as a Unifying Concept
• Barriers in concurrent separation logic: now with tool support!
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
• Higher-order ghost state
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• scientific article; zbMATH DE number 7233822 (Why is no real title available?)
• Concurrent separation logic and operational semantics

This page was built for publication: Revisiting concurrent separation logic

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