A semantics for concurrent separation logic
The work
| Authors | Stephen Brookes |
|---|---|
| Editors | |
| Type | article |
| Year | 2007 |
| Citekey | brookes2007semantics |
Where it appeared
| Published in | Theoretical Computer Science |
|---|---|
| Publisher | Elsevier |
| Volume | 375 |
| Issue | 1-3 |
| Pages | 227--270 |
Identifiers
| DOI | 10.1016/j.tcs.2006.12.034 |
|---|---|
| OpenAlex | W2125398300 |
Access
| Landing page | https://doi.org/10.1016/j.tcs.2006.12.034 |
|---|---|
| Free full text | https://www.sciencedirect.com/science/article/pii/S0304397506009248/pdf |
Abstract
We present a trace semantics for a language of parallel programs which share access to mutable data. We introduce a resource-sensitive logic for partial correctness, based on a recent proposal of O’Hearn, adapting separation logic to the concurrent setting. The logic allows proofs of parallel programs in which “ownership” of critical data, such as the right to access, update or deallocate a pointer, is transferred dynamically between concurrent processes. We prove soundness of the logic, using a novel “local” interpretation of traces which allows accurate reasoning about ownership. We show that every provable program is race-free.
A copy is held
pdf, 648.3 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-16 15:25 UTC |
Filed under
Cite it as
@article{brookes2007semantics,
title = {A semantics for concurrent separation logic},
author = {Stephen Brookes},
year = {2007},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
volume = {375},
number = {1-3},
pages = {227--270},
doi = {10.1016/j.tcs.2006.12.034},
}
This record lives at https://refs.drheap.org/brookes2007semantics/ and will keep doing so.