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 |
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.