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.