Revisiting concurrent separation logic and operational semantics

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

doi:10.1109/PDP.2015.85

Revisiting concurrent separation logic and operational semantics

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Citation (Scopus)

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 language	English
Title of host publication	Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015
Publisher	Institute of Electrical and Electronics Engineers (IEEE)
Pages	484-491
Number of pages	8
ISBN (Electronic)	978-147998490-9
DOIs	https://doi.org/10.1109/PDP.2015.85
Publication status	Published - 2015
Event	23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015 - Turku, Finland Duration: 4 Mar 2015 → 6 Mar 2015

Conference

Conference	23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015
Country/Territory	Finland
City	Turku
Period	4/03/15 → 6/03/15

Keywords

Concurrency
Operational semantics
Soundness

Access to Document

10.1109/PDP.2015.85Licence: Unspecified

Cite this

@inproceedings{a1941b8507b244f9950090ce0ea7b22d,

title = "Revisiting concurrent separation logic and operational semantics",

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

keywords = "Concurrency, Operational semantics, Soundness",

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

note = "Sem PDF. This work was partially funded by Funda{\c c}{\~a}o para a Ci{\^e}ncia e Tecnologia through AVIACC project, grant PTDC/EIA-CCO/117590, and CITI/FCT/UNL, grant Pest-OE/EEI/UI0527/2014; 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015 ; Conference date: 04-03-2015 Through 06-03-2015",

year = "2015",

doi = "10.1109/PDP.2015.85",

language = "English",

pages = "484--491",

booktitle = "Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015",

publisher = "Institute of Electrical and Electronics Engineers (IEEE)",

address = "United States",

}

Soares, P, Ravara, A & De Sousa, SM 2015, Revisiting concurrent separation logic and operational semantics. in Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015., 7092764, Institute of Electrical and Electronics Engineers (IEEE), pp. 484-491, 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015, Turku, Finland, 4/03/15. https://doi.org/10.1109/PDP.2015.85

Revisiting concurrent separation logic and operational semantics. / Soares, Pedro; Ravara, António; De Sousa, Simão Melo.
Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015. Institute of Electrical and Electronics Engineers (IEEE), 2015. p. 484-491 7092764.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Revisiting concurrent separation logic and operational semantics

AU - Soares, Pedro

AU - Ravara, António

AU - De Sousa, Simão Melo

N1 - Sem PDF. This work was partially funded by Fundação para a Ciência e Tecnologia through AVIACC project, grant PTDC/EIA-CCO/117590, and CITI/FCT/UNL, grant Pest-OE/EEI/UI0527/2014

PY - 2015

Y1 - 2015

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 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 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 - Concurrency

KW - Operational semantics

KW - Soundness

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

U2 - 10.1109/PDP.2015.85

DO - 10.1109/PDP.2015.85

M3 - Conference contribution

AN - SCOPUS:84983123683

SP - 484

EP - 491

BT - Proceedings - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015

PB - Institute of Electrical and Electronics Engineers (IEEE)

T2 - 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015

Y2 - 4 March 2015 through 6 March 2015

ER -

Revisiting concurrent separation logic and operational semantics

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this