Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4951421 | Journal of Logical and Algebraic Methods in Programming | 2017 | 26 Pages |
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
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Pedro Soares, António Ravara, Simão Melo de Sousa,