Revisiting concurrent separation logic

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

Research output: Contribution to journalArticlepeer-review

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.

Original languageEnglish
Pages (from-to)41-66
Number of pages26
JournalJournal of Logical and Algebraic Methods in Programming
Volume89
DOIs
Publication statusPublished - Jun 2017

Keywords

  • Concurrent separation logic
  • Soundness proof
  • Structural operational semantics

Fingerprint

Dive into the research topics of 'Revisiting concurrent separation logic'. Together they form a unique fingerprint.

Cite this