Revisiting concurrent separation logic

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

doi:10.1016/j.jlamp.2017.02.004

Revisiting concurrent separation logic

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

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	41-66
Number of pages	26
Journal	Journal of Logical and Algebraic Methods in Programming
Volume	89
DOIs	https://doi.org/10.1016/j.jlamp.2017.02.004
Publication status	Published - Jun 2017

Keywords

Concurrent separation logic
Soundness proof
Structural operational semantics

Access to Document

10.1016/j.jlamp.2017.02.004

Cite this

@article{455c2000fa9143998e99351f7b833d92,

title = "Revisiting concurrent separation logic",

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.",

keywords = "Concurrent separation logic, Soundness proof, Structural operational semantics",

author = "Pedro Soares and Ant{\'o}nio Ravara and {Melo de Sousa}, Sim{\~a}o",

note = "This work was partially funded by Fundacao para a Ciencia e a Tecnologia through AVIACC project, grant PTDC/EIA-CCO/117590, and CITI/FCT/UNL, grant Pest-OE/EEI/UI0527/2014.",

year = "2017",

month = jun,

doi = "10.1016/j.jlamp.2017.02.004",

language = "English",

volume = "89",

pages = "41--66",

journal = "Journal of Logical and Algebraic Methods in Programming",

issn = "2352-2208",

publisher = "Elsevier BV",

}

TY - JOUR

T1 - Revisiting concurrent separation logic

AU - Soares, Pedro

AU - Ravara, António

AU - Melo de Sousa, Simão

N1 - This work was partially funded by Fundacao para a Ciencia e a Tecnologia through AVIACC project, grant PTDC/EIA-CCO/117590, and CITI/FCT/UNL, grant Pest-OE/EEI/UI0527/2014.

PY - 2017/6

Y1 - 2017/6

N2 - 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.

AB - 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.

KW - Concurrent separation logic

KW - Soundness proof

KW - Structural operational semantics

UR - http://www.scopus.com/inward/record.url?scp=85097001393&partnerID=8YFLogxK

U2 - 10.1016/j.jlamp.2017.02.004

DO - 10.1016/j.jlamp.2017.02.004

M3 - Article

AN - SCOPUS:85097001393

VL - 89

SP - 41

EP - 66

JO - Journal of Logical and Algebraic Methods in Programming

JF - Journal of Logical and Algebraic Methods in Programming

SN - 2352-2208

ER -

Revisiting concurrent separation logic

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this