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,
For example, let's take two pointers and holding values 10 and 20 respectively
Then consider the program := 30, which can be reasoned using Hoare triplet
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.
One of the first proof rules of CSL is the Parallel Composition,
where no variable free in or is changed in when
ji.
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 and in parallel
The reasoning for is represented using the following triplet
And the reasoning for is represented using the following triplet
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.
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.
The rule says, if a "resource invariant", 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 (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 bumps the value of up by 1, and decrements by 1 whenever it is greater than 0, waiting otherwise.
And we can define the both semaphore operations in terms of critical regions
P(s) = with when 0 do endwith
V(s) = with when do endwith
The resource invariant for the semaphore can be defined as
which means either the semaphore is 0 and doesn't own any memory or the semaphore is 1 and owns the memory location that references to ( this implies x is not a dangling pointer).
Now, the proof outline for the on the left of the program is as follows.
At the start of the program, free is 1 which means this part of RI holds. This implies semaphore free owns the memoery that points to, which means P should be empty.
So, the pre-condition
becomes
which can be reduced to
decrements the semaphore, thus free becomes 0. By decrementing the free in pre-condition, the post-condition becomes
But when free is 0, it doesn't own any memory as per the resource invariant .
So, the semaphore can no longer hold access to memory location that referencec to. So the memory now gets transferred to the left part of the separating conjuction.
which can be reduced to
And this is in the form , where Q is
Using the above premise, we can conclude the triplet
Intuitively, released the access to memory to the next part of the code .
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 (), where the semaphore owns the right part of it. For the next line of code, the state is partitioned into two parts () 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.
Different variations of SL and CSL are extensively used in the development of various mechanized verification tools.
Stephen Brookes and Peter W. O'Hearn. 2016. Concurrent separation logic. ACM SIGLOG News 3, 3 (July 2016), 47–65. https://doi.org/10.1145/2984450.2984457
@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}
}
Peter W. OHearn. 2007. Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 1–3 (April, 2007), 271–307. https://doi.org/10.1016/j.tcs.2006.12.035
@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}
}
Peter O'Hearn. 2019. Separation logic. Commun. ACM 62, 2 (February 2019), 86–95. https://doi.org/10.1145/3211968
@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}
}
Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn. 2005. Smallfoot: modular automatic assertion checking with separation logic. In Proceedings of the 4th international conference on Formal Methods for Components and Objects (FMCO'05). Springer-Verlag, Berlin, Heidelberg, 115–137. https://doi.org/10.1007/11804192_6
@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}
}