Technical Report:DCC-2014-11

An Operational Semantics for Concurrent Separation Logic

Pedro Soares

António Ravara

Simão Melo de Sousa

LIACC CITI, DI-FCT LIACC, DI-FE
Universidade do Porto Universidade Nova de Lisboa Universidade da Beira Interior
Portugal
June 2014

Abstract

The deductive verification of concurrent programs gained new tools with the advent of Concurrent Separation Logic (CSL). This program logic is a compositional method that combines the Owicki-Gries method with Separation Logic, allowing to reason and prove correct concurrent programs manipulating shared mutable data structure. The soundness of Concurrent Separation Logic had been established using a denotational semantics (based on traces). An alternative proof based on structural operational semantics 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 Concurrent Separation Logic with respect to an operational semantics.