Local reasoning about Concurrency

The concept of separation naturally applies to concurrent programs.

TODO disjoint parallel comp rule.

There are a number of approaches of extending sequential separation logic to handle concurrent programs.

• CSL
• RGSep/SAGL/LRG
• Deny-guarantee

CSL (Concurrent Separation Logic)

The place to get started is Resources, Concurrency and Local Reasoning. PW O'Hearn, Theoretical Computer Science 375(1-3) (Reynolds Festschrift), pp271-307, May 2007.

This paper adapted the resource invariants to separation logic and introduced the notion of 'ownership transfer,' whereby the right to access a portion of the heap can be transferred between processes via a shared resource invariant. This enables modular reasoning in the presence of semaphores (e.g., split binary semaphores without maintaining a global invariant).

TODO: Ownership is in the eyer of the beholder.

Important papers:

• Resources, Concurrency and Local Reasoning. PW O'Hearn, Theoretical Computer Science 375(1-3) (Reynolds Festschrift), pp271-307, May 2007.

• A Semantics for Concurrent Separation Logic. SD Brookes, Theoretical Computer Science 375(1-3) (Reynolds Festschrift), pp227-270, May 2007.
• Permission Accounting in Separation Logic. R Bornat, C Calcagno, P O'Hearn and M Parkinson, POPL 2005, pp 59-70.

Important extensions:

• Permissions.
• locks-in-the-heap.

Other papers:

• Modular Verification of a Non-blocking Stack M Parkinson, R Bornat and P O'Hearn, POPL 2007
• Independence and Concurrent Separation Logic Jonathan Hayman and Glynn Winskel, Proceedings of LICS'06

RGSep / SAGL / LRG

• A Marriage of Rely/Guarantee and Separation Logic. V Vafeiadis, M Parkinson. CONCUR 2007.

• On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning. X. Feng, R. Ferreira, Z. Shao. ESOP 2007.

• Local Rely Guarantee Reasoning. X. Feng. POPL 2009.