| Autor: |
Soares, Pedro, Ravara, António, de Sousa, Simão Melo |
| Rok vydání: |
2017 |
| Předmět: |
|
| Zdroj: |
Journal of Logical and Algebraic Methods in Programming, Volume 89, 2017, Pages 41-66 |
| Druh dokumentu: |
Working Paper |
| DOI: |
10.1016/j.jlamp.2017.02.004 |
| Popis: |
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. |
| Databáze: |
arXiv |
| Externí odkaz: |
|
