Revisiting concurrent separation logic

DOI10.1016/J.JLAMP.2017.02.004zbMATH Open1370.68056arXiv1712.01631OpenAlexW3100121990MaRDI QIDQ2397039FDOQ2397039

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)

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.

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

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

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)

Cites Work

• A structural approach to operational semantics
• Syntactic control of interference for separation logic
• Title not available (Why is that?)
• A semantics for concurrent separation logic
• An axiomatic basis for computer programming
• Verifying properties of parallel programs
• Resources, concurrency, and local reasoning
• Title not available (Why is that?)
• Title not available (Why is that?)
• A Marriage of Rely/Guarantee and Separation Logic
• Concurrent separation logic and operational semantics
• Title not available (Why is that?)
• A revisionist history of concurrent separation logic

Cited In (14)

• Barriers in concurrent separation logic: now with tool support!
• Oracle Semantics for Concurrent Separation Logic
• An asynchronous soundness theorem for concurrent separation logic
• Precision and the conjunction rule in concurrent separation logic
• On the relation between concurrent separation logic and concurrent Kleene algebra
• CONCUR 2004 - Concurrency Theory
• Convolution as a Unifying Concept
• Concurrent separation logic and operational semantics
• Higher-order ghost state
• Barriers in Concurrent Separation Logic
• Parameterized Memory Models and Concurrent Separation Logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

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)