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.
Cite
@article{arxiv.1712.01631,
title = {Revisiting concurrent separation logic},
author = {Pedro Soares and António Ravara and Simão Melo de Sousa},
journal= {arXiv preprint arXiv:1712.01631},
year = {2017}
}