Revisiting concurrent separation logic

TL;DR

This paper introduces a new soundness proof for full Concurrent Separation Logic using structural operational semantics, enabling better integration of correctness tools into programming environments.

Contribution

It extends previous proofs by removing restrictions, proving soundness of full CSL with SOS, and facilitating tool development for concurrent program correctness.

Findings

Proves soundness of full CSL with SOS.

Lifts previous restrictions on shared variable modifications.

Supports integration of correctness tools into programming environments.

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.