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.