Concurrent Separation Logic

Concurrent Separation Logic (CSL) is an extension to Separation Logic (SL) to reason about concurrent programs, especially those using shared memory concurrency. It was initially developed by Peter W. O'Hearn and later the semantic model with correctness proof was provided by Stephen Brookes.

Separation Logic extends Hoare Logic to efficiently reason about pointer manipulation in programs. One of the main innovations of SL is the new separating conjunction operator *. The main idea is if the state of the program can be captured in a heap, then {P * P'} says that the heap can divided into two separate parts (known as heaplets) such that, one satisfies P and the other satisfies P'.

First, let's use the following syntax for the rest of the examples,

1. x \longmapsto v to represent a pointer x holding a value v.
2. x := v to update a value at pointer x to v.

For example, let's take two pointers x and y holding values 10 and 20 respectively

x \longmapsto 10 \space \space \space \space y \longmapsto 20

Then consider the program x := 30, which can be reasoned using Hoare triplet

\{ x \longmapsto 10 \} x := 30 \{ x \longmapsto 30 \}

As the heap can be split into two disjoint parts, P (which holds memory x) and P' (which holds memory y). The reasoning of above program can be extended to entire heap using the separating conjuction.

\{ x \longmapsto 10 * y \longmapsto 20 \} x := 30 \{
x \longmapsto 30 * y \longmapsto 20\}

Proof Rules

One of the first proof rules of CSL is the Parallel Composition,

 \frac{
 \{P_1\} C_1 \{Q_1\} ... \{P_n\} C_n \{Q_n\}
 }{
 \{P_1 * ... * P_n \} C_1 \parallel ... \parallel C_n \{Q_1 * ... * Q_n\}
 }

where no variable free in P_i or Q_i is changed in C_j when
j\neqi.

The rule says, that if multiple processes are using separate parts of memory, then they can be composed in parallel.

For example, let's consider a program that updates the values at pointers x and y in parallel

x := 10 \parallel y := 30

The reasoning for x := 10 is represented using the following triplet

\{x \longmapsto 30 \} x := 10 \{ x \longmapsto 10 \}

And the reasoning for y:= 30 is represented using the following triplet

\{ y \longmapsto 20 \} y := 30 \{y \longmapsto 30\}

These two programs operate on the disjoint memory locations and neither process modifies the other's memory. These two programs can be composed in parallel and is reasoned using the Parallel Composition.

 \frac{
 \{ x \longmapsto 30 \} x := 10 \{ x \longmapsto 10 \} \quad \{ y \longmapsto 20 \} y := 30 \{ y \longmapsto 30 \}
 }{
 \{x \longmapsto 30 * y \longmapsto 20 \} x := 10 \parallel y := 30 \{x \longmapsto 10 * y \longmapsto 30\}
 }

The above rule is good enough to reason only if there are no interactions between processes. In order to reason about concurrent processes interacting with one another, CSL also provides a rule called Critical Region.

 \frac{
 \{(P * RI_r) \land B\} C \{Q * RI_r\}
 }{
 \{P\} with \space r \space when \space B \space do \space C\{Q\}
 }

The rule says, if a "resource invariant", RI_{r} is defined for a resource r and code C enters into a critical region satisfying code invariants B, then the code gets to access the state associated with the resource and as well as any state local to it.

A resource invariant is a constraint that is defined on a resource such that, it must hold throughout the execution of program.

For example, let's consider a program where two processes share access to a pointer x (one tries to read value at the pointer and other tries to update value at the pointer). As, the both procesee trying to access same memory concurrenlty, these can be synchronized using the two semaphores free and busy. A semaphore is represented by a non-negative integer, where V(s) bumps the value of s up by 1, and P(s) decrements s by 1 whenever it is greater than 0, waiting otherwise.

{semaphore \, free := 1, busy := 0} \\
{P(free) \quad\qquad P(busy)} \\
{x := m \quad \parallel \quad n := x} \\
{V(busy) \quad\qquad V(free)}

And we can define the both semaphore operations in terms of critical regions

P(s) = with s when s > 0 do s := s-1 endwith

V(s) = with s when true do s := s-1 endwith

The resource invariant for the semaphore s can be defined as

RI_s = (s = 0 \land emp) \lor (s = 1 \land x \longmapsto -)

which means either the semaphore is 0 and doesn't own any memory or the semaphore is 1 and owns the memory location that x references to (x \longmapsto - this implies x is not a dangling pointer).

Now, the proof outline for the P(free) on the left of the program is as follows.

 \frac{
 \{(P * RI_{free}) \land (free > 0)\} free := free-1 \{Q * RI_{free}\}
 }{
 \{P\} P(free) \{Q\}
 }

At the start of the program, free is 1 which means this part (free = 1 \land 10 \longmapsto -) of RI holds. This implies semaphore free owns the memoery that x points to, which means P should be empty.

So, the pre-condition

\{(P * RI_{free}) \land (free > 0)\} free := free-1 \{Q * RI_{free}\}

becomes

\{(emp * (free = 0 \land emp) \lor (free = 1 \land x \longmapsto -)) \land (free > 0)\}

which can be reduced to

\{(emp * (free = 1 \land x \longmapsto -))\}

P(free) decrements the semaphore, thus free becomes 0. By decrementing the free in pre-condition, the post-condition becomes

\{(emp * (free = 0 \land x \longmapsto -))\}

But when free is 0, it doesn't own any memory as per the resource invariant RI_{free}.

So, the semaphore free can no longer hold access to memory location that x referencec to. So the memory now gets transferred to the left part of the separating conjuction.

\{(x \longmapsto - * (free = 0 \land emp))\}

which can be reduced to

\{(x \longmapsto - * (free = 0 \land emp) \lor (free = 1 \land x \longmapsto -))\}

And this is in the form \{Q * RI_{free}\}, where Q is {x \longmapsto - }

Using the above premise, we can conclude the triplet

\{emp\} P(free) \{ x \longmapsto -\}

Intuitively, P(free) released the access to memory to the next part of the code x := m.

Principles

There are two important principles of CSL.

Ownership Hypothesis : A code fragment can only access those portions of the state it owns.

Separation Property : At any point in time, the state can be partitioned into that owned by each process and each grouping of mutual exclusion.

In the above example, initially, the semaphore owns the memory location 10, and then P(free) releases the memory to the code outside of it. Similarly, V(busy) acquires access to a memory location for the busy semaphore thus making it available for the P(busy). At any point in time either the semaphore owns memory or it owns nothing.

In the above code, if we observe there are two parts of the state at any point in time. Initially, just before the semaphore operation P(free), the state is partitioned into two parts (emp * (free = 1 \land 10 \longmapsto -)), where the semaphore owns the right part of it. For the next line of code, the state is partitioned into two parts (10 \longmapsto - * (free = 0 \land emp)) such that now the process owns the left part of the memory. And it is the ownership transfer of semaphores operations that holds the separation property throughout the entire program.

Applications of CSL

Different variations of SL and CSL are extensively used in the development of various mechanized verification tools.

1. Mostly-Automatic Verifiers: These tools are used for automatic verification of concurrent programs where the user provides a list of resource invariants and pre/post conditions. SmallFootRG is one of the first automated verification tools built using SL and CSL.
2. Interactive Verification: In these types of tools, interactive proof assistants like Coq, HOL, or Isabelle are used to verify the concurrent programs using CSL proof rules.
3. Automatic Program Analysis Tools: These are more analysis tools than verification. The pre/post conditions are inferred from the code and checked against SL and CSL rules to detect any potential bugs in the code. Infer is one such tool developed at Meta to detect issues like null pointer manipulations, and resource and memory leaks in the Java and C programs.

References

@article{10.1145/2984450.2984457,
author = {Brookes, Stephen and O'Hearn, Peter W.},
title = {Concurrent separation logic},
year = {2016},
issue_date = {July 2016},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {3},
url = {https://doi.org/10.1145/2984450.2984457},
doi = {10.1145/2984450.2984457},
month = {aug},
pages = {47–65},
numpages = {19}
}

@article{10.1016/j.tcs.2006.12.035,
author = {OHearn, Peter W.},
title = {Resources, concurrency, and local reasoning},
year = {2007},
issue_date = {April, 2007},
publisher = {Elsevier Science Publishers Ltd.},
address = {GBR},
volume = {375},
number = {1–3},
issn = {0304-3975},
url = {https://doi.org/10.1016/j.tcs.2006.12.035},
doi = {10.1016/j.tcs.2006.12.035},
month = {apr},
pages = {271–307},
numpages = {37},
keywords = {Separation logic, Logics of programs, Concurrency}
}

@article{10.1145/3211968,
author = {O'Hearn, Peter},
title = {Separation logic},
year = {2019},
issue_date = {February 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {62},
number = {2},
issn = {0001-0782},
url = {https://doi.org/10.1145/3211968},
doi = {10.1145/3211968},
journal = {Commun. ACM},
month = {jan},
pages = {86–95},
numpages = {10}
}

@inproceedings{10.1007/11804192_6,
author = {Berdine, Josh and Calcagno, Cristiano and O'Hearn, Peter W.},
title = {Smallfoot: modular automatic assertion checking with separation logic},
year = {2005},
isbn = {3540367497},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
url = {https://doi.org/10.1007/11804192_6},
doi = {10.1007/11804192_6},
pages = {115–137},
numpages = {23},
location = {Amsterdam, The Netherlands},
series = {FMCO'05}
}