Revisiting concurrent separation logic and operational semantics

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 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
Title of host publicationProceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages484-491
Number of pages8
ISBN (Electronic)978-147998490-9
DOIs
Publication statusPublished - 2015
Event23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015 - Turku, Finland
Duration: 4 Mar 20156 Mar 2015

Conference

Conference23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015
CountryFinland
CityTurku
Period4/03/156/03/15

Keywords

  • Concurrency
  • Operational semantics
  • Soundness

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

Cite this