Differences between revisions 8 and 9
⇤ ← Revision 8 as of 2011-02-03 18:58:52 →
Size: 5742
Editor: viktor
Comment:
← Revision 9 as of 2011-02-03 18:59:48 → ⇥
Size: 5748
Editor: viktor
Comment:
Deletions are marked like this. Additions are marked like this.
Line 5: Line 5:
<<latex($$\frac{ \{ P_1 \}~C_1~\{ Q_1 \} \qquad \{ P_2 \}~C_2~\{ Q_2 \} }{ \{ P_1 * P_2 \}~C_1\|C_2~\{ Q_1 * Q_2 \} }\quad \begin{array}{l}\mathbf{fv}(P_1,Q_1) \cap \mathbf{mod}(C_2) = \emptyset \\ \mathbf{fv}(P_2,Q_2) \cap \mathbf{mod}(C_1) = \emptyset\end{array}$$ )>> <<latex($$\frac{ \{ P_1 \}~C_1~\{ Q_1 \} \qquad \{ P_2 \}~C_2~\{ Q_2 \} }{ \{ P_1 * P_2 \}~C_1\|C_2~\{ Q_1 * Q_2 \} }\quad \begin{array}{l}\mathbf{fv}(P_1,Q_1) \cap \mathbf{mod}(C_2) = \emptyset ~\wedge~ \mathbf{fv}(P_2,Q_2) \cap \mathbf{mod}(C_1) = \emptyset\end{array}$$ )>>

Local reasoning about Concurrency

The concepts of ownership and separation naturally apply to concurrent programs. This is best illustrated by the disjoint parallel composition rule:

$$\frac{ \{ P_1 \}~C_1~\{ Q_1 \} \qquad \{ P_2 \}~C_2~\{ Q_2 \} }{ \{ P_1 * P_2 \}~C_1\|C_2~\{ Q_1 * Q_2 \} }\quad \begin{array}{l}\mathbf{fv}(P_1,Q_1) \cap \mathbf{mod}(C_2) = \emptyset ~\wedge~ \mathbf{fv}(P_2,Q_2) \cap \mathbf{mod}(C_1) = \emptyset\end{array}$$

The rule says that if two threads execute on disjoint portions of the heap, they can safely be run in parallel. 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).

$$\frac{ \Gamma \vdash \{ (P * R)\wedge B \}~C~\{ Q * R \} }{ \Gamma, r: R \vdash \{ P \}~\mathbf{with}~B~\mathbf{do}~C~\{ Q \} }$$

$$\frac{ \Gamma,r:R \vdash \{ P \}~C~\{ Q \} }{ \Gamma \vdash \{ P * R \}~\mathbf{resource}~r~\mathbf{in}~C~\{ Q * R \} }$$

Ownership

In CSL terminology, a thread with a precondition $x \mapsto -$ 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

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.

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

Concurrency (last edited 2011-02-05 12:01:22 by viktor)