|
Size: 7423
Comment:
|
Size: 8832
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 38: | Line 38: |
| The CCR proof rule allows the ownership of a memory cell to be transferred in and out of the resource invariant, <<latex($R$)>>. For example, let <<latex($R = (\lnot b \land \textbf{emp} \lor b \land x \mapsto 5$)>>. Then a thread can execute the CCR <<latex($\mathbf{when}\ \lnot b\ \mathbf{do}\ b := \mathit{true}$)>> to add a memory cell to the critical region or <<latex($\mathbf{when}\ b\ \mathbf{do}\ b := \mathit{false}$)>> to remove it from the region. | The CCR proof rule allows the ownership of a memory cell to be transferred in and out of the resource invariant, <<latex($R$)>>. For example, let <<latex($R = (\lnot b \land \textbf{emp} \lor b \land x \mapsto 5)$)>>. Then a thread can execute the CCR <<latex($\mathbf{when}\ \lnot b\ \mathbf{do}\ b := \mathit{true}$)>> to add a memory cell to the critical region or <<latex($\mathbf{when}\ b\ \mathbf{do}\ b := \mathit{false}$)>> to remove it from the region. |
| Line 56: | Line 56: |
| ==== Criticism ==== Though the notion of ownership transfer introduced by CSL has been rather useful, CSL itself has been criticized for two important shortcomings. 1. Because resource invariants are assertions of a single state, CSL proofs of intricate concurrent algorithms often require many auxiliary variables. This leads to ugly, un-modular proofs, an important part of which is spent working around the limitations of the logic. A good example of such an ugly proof by [http://www.eecs.qmul.ac.uk/~ohearn/papers/non-blocking-stack.pdf|Parkinson, Bornat, and O'Hearn (2007)]. Vafeiadis argued that RGSep is a better –albeit not perfect– logic for reasoning about intricate concurrent algorithms. [[http://people.cs.kuleuven.be/~bart.jacobs/popl2011.pdf|Jacobs and Piessens (2011)]] showed that modularity can be reinstated by writing specifications up to auxiliary variable insertion in a higher-order style. Nevertheless, the proofs in CSL of intricate concurrent algorithms remain ugly and impractical. 2. The sheer number of CSL extensions for each different concurrent primitive suggests that CSL itself the wrong formalism, because ideally the specifications for these constructs should be derivable within the same logic. [[http://dx.doi.org/10.1007/978-3-642-15057-9_12|Parkinson (2010)]] argued that deny-guarantee with (concurrent) abstract predicates might be the 'correct' formalism. |
|
| Line 62: | Line 71: |
| * Independence and Concurrent Separation Logic Jonathan Hayman and Glynn Winskel, Proceedings of LICS'06 | * Independence and Concurrent Separation Logic Jonathan Hayman and Glynn Winskel. LICS 2006 |
Concurrency & Local Reasoning
The concepts of ownership and separation from separation logic naturally apply to concurrent programs. This is best illustrated by the disjoint parallel composition rule:
The rule says that if two threads execute on disjoint portions of the heap, they can safely be run in parallel. The side-condition states that each thread does not modify the variables mentioned by the other thread, thereby ensuring that there are no race conditions on program variables. This rule allows us to reason about simple parallel programs such as parallel merge sort without requiring rely-guarantee conditions; each thread simply minds its own business.
To handle concurrent programs where threads do interact with each other, a number of extensions have been proposed:
- CSL
- RGSep/SAGL/LRG
- Deny-guarantee
CSL (Concurrent Separation Logic)
CSL (O'Hearn 2007) adapted 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).
CSL specifications consist of a precondition, a postcondition, and a resource environment Γ mapping resource names to resource invariants (which are separation logic assertions). The resource environment, Γ, is simply threaded through all the standard SL rules, and gets used in the following two rules:
The first rule declares a new resource, 
, with invariant 
. Naturally, the invariant must hold separately of the precondition and is guaranteed to remain true in the postcondition. The second rule allows us to use the state protected by the resource, . To do so, we must execute a conditional critical region (CCR), within which we can assume that its resource invariant holds initially and have to reestablish it when exiting the CCR.
Ownership
In CSL terminology, a thread with a precondition 
owns the memory cell pointed to by x. Ownership is a promise that the program will not access any portion of the heap outside its ownership domain and an assumption that the program is the sole owner of the portion of the heap described by its precondition. This concept that appears only in the correctness proof of a program and is enforced by the CSL proof rules. In O'Hearn's terms, Ownership is in the eyer of the beholder.
Permissions (due to Boyland) are an extension of notion of ownership with the concept of a partial owner. In CSL with permissions, full ownership of a memory cell can be decomposed (with the separating conjunction) into two half permissions, each allowing its beholder to read from the memory cell, but not to update it. A half permission can further be decomposed in two quarter permissions, each of which still allows one to read from the memory cell, and so on. Finally, two half permissions can be recombined (with the separating conjunction) into a full permission, allowing both read and write access to the memory cell.
Deny-guarantee further refines the notion of ownership and permissions so that the ability to do any particular change (such as change the value of x from 0 to 1) is subject to ownership, full or partial. Moreover, in deny-guarantee there are two kinds of partial ownership, one which allows everybody to do the change, and one which forbids everybody to do the change.
Ownership transfer
The CCR proof rule allows the ownership of a memory cell to be transferred in and out of the resource invariant, . For example, let 
. Then a thread can execute the CCR 
to add a memory cell to the critical region or 
to remove it from the region.
Further examples can be found in O'Hearn (2007).
Soundness
Proving the soundness of CSL has historically been quite tricky. O'Hearn writes: "... At that time [Jan. 2002] I had no model and was scared about soundness. Then John Reynolds showed surprising subtleties regarding soundness, and we were facing an extremely difficult problem in the semantics of concurrency. We needed expert help, and it arrived in Steve Brookes who rode in and saved the day (and the whole approach)." The subtleties that O'Hearn refers to are the interaction of the conjunction, frame, and CCR rules, which can lead to unsoundness of the logic (cf. the Reynold's counterexample in O'Hearn (2007)). The usual remedy is to require resource invariants to be precise assertions. An alternative is to drop the conjunction rule.
The first proof of soundness was due to Brookes over a denotational trace semantics for programs and using an intermediated instrumented semantics for carrying out the proof. Later proofs have been done by Hayman, Gotsman, Hobor, and others. Recently, Vafeiadis has proposed a simpler operational proof with dispenses the need of an intermediate semantics.
Moderate Extensions
- Permissions
- Locks-in-the-heap (Gotsman et al., Hobor et al.)
- Reentrant locks
- Message-passing synchronization
- Barriers
Criticism
Though the notion of ownership transfer introduced by CSL has been rather useful, CSL itself has been criticized for two important shortcomings.
Because resource invariants are assertions of a single state, CSL proofs of intricate concurrent algorithms often require many auxiliary variables. This leads to ugly, un-modular proofs, an important part of which is spent working around the limitations of the logic. A good example of such an ugly proof by [http://www.eecs.qmul.ac.uk/~ohearn/papers/non-blocking-stack.pdf|Parkinson, Bornat, and O'Hearn (2007)]. Vafeiadis argued that RGSep is a better –albeit not perfect– logic for reasoning about intricate concurrent algorithms. Jacobs and Piessens (2011) showed that modularity can be reinstated by writing specifications up to auxiliary variable insertion in a higher-order style. Nevertheless, the proofs in CSL of intricate concurrent algorithms remain ugly and impractical.
The sheer number of CSL extensions for each different concurrent primitive suggests that CSL itself the wrong formalism, because ideally the specifications for these constructs should be derivable within the same logic. Parkinson (2010) argued that deny-guarantee with (concurrent) abstract predicates might be the 'correct' formalism.
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.
- 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. LICS 2006
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.