The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

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

Last modified: Fri Apr 6 16:34:45 2007 GMT.

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

  • Proc. 16th European Symposium on Programming (ESOP'07), Braga, Portugal, March 2007. Lecture Notes in Computer Science Vol. 4421, pages 173-188. © 2007 Springer-Verlag.

  • Technical Report YALEU/DCS/TR-1374 (Extended Version, 22 pages)

  • Coq Implementaions

  • Copyright © 1996-2024 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon