Authors
Xinyu Feng
Rodrigo Ferreira
Zhong Shao
Abstract
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 A-G based 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 type systems.
Published
Technical Report YALEU/DCS/TR-1374 (Extended Version, 22 pages)
Coq Implementaions