Sciweavers

Share
ESOP
2007
Springer

On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning

9 years 6 months ago
On the Relationship Between Concurrent Separation Logic and Assume-Guarantee Reasoning
We study the relationship between Concurrent Separation Logic (CSL) and the assume-guarantee (A-G) method (a.k.a. rely-guarantee method). We show in three steps that CSL can be treated as a specialization of the A-G method for well-synchronized concurrent programs. First, we present an A-G based program logic for a low-level language with built-in locking primitives. Then we extend the program logic with explicit separation of “private data” and “shared data”, which provides better memory modularity. Finally, we show that CSL (adapted for the low-level language) can be viewed as a specialization of the extended A-G logic by enforcing the invariant that “shared resources are well-formed outside of critical regions”. This work can also be viewed as a different approach (from Brookes’) to proving the soundness of CSL: our CSL inference rules are proved as lemmas in the A-G based logic, whose soundness is established following the syntactic approach to proving soundness of ty...
Xinyu Feng, Rodrigo Ferreira, Zhong Shao
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ESOP
Authors Xinyu Feng, Rodrigo Ferreira, Zhong Shao
Comments (0)
books