proposed a concurrent separation logic
(CSL). CSL showed efficient reasoning
about threads that share access to storage, proofs that mirrored design principles espoused by Dijkstra at the birth
of concurrent programming.
16 The correctness of CSL’s proof rules (its ‘
soundness’) turned out to be a formidable
problem, solved eventually by Brookes.
Brookes and O’Hearn were awarded
the 2016 Gödel prize for their papers on
8, 30 the significance of which was
summed up as follows:
"For the last 30 years experts have
regarded pointer manipulation as an
unsolved challenge for program verification and shared-memory concurrency as
an even greater challenge. Now, thanks
to CSL, both of these problems have
been elegantly and efficiently solved;
and they have the same solution."
—2016 Gödel Prize citationa
It is worth remarking that the first
part of this citation, about pointer manipulation, applies to sequential and
not just concurrent SL.
After the early papers, research on SL
expanded rapidly. Starting from a special logic for heaps SL has evolved into
a general theory for modular reasoning.
Non-standard models of SL based on an
abstract model theory due to Pym provided many potential avenues for wider
application, and Gardner and others
realized that there exist non-standard
models that support modular reasoning about intertwined structures as if
they were separate. SL has even been
applied to interfering processes using
fine-grained concurrency, a situation far
removed from the original intuitions of
SL is the basis of numerous auto-
mated proof tools, and it has been used
in significant verification efforts. It has
been used to provide the first verifica-
tion of a crash-proof file system,
to provide the first verification of a com-
mercial, preemptive OS microkernel.
These verification efforts are semi-
automatic, done by a human together
with a proof assistant (in these cases,
the Coq proof assistant). SL has also
been used in static program analysis,
where weaker properties than full cor-
rectness are targeted but with higher
automation, so that the tool can scale
better both in the sizes of codebases
SL for sequential programs reached
maturity in a further paper of O’Hearn,
Reynolds and Yang.
32 In that work
O’Hearn proposed the following prin-
ciple of local reasoning, both as a way to
describe what was special about SL and
as a guiding principle for development
of reasoning methods.
"To understand how a program
works, it should be possible for reasoning and specification to be confined to
the cells that the program actually accesses. The value of any other cell will
automatically remain unchanged."
A proof rule—the frame rule—
allowed to infer that cells remain unchanged when they are not mentioned
in a precondition. The frame rule was
named in homage to the frame problem
from artificial intelligence, which concerns axiomatizing state changes without enumerating all of the things that do
not change. The frame rule is the key to
scalable reasoning in SL.
Reynolds’ influential survey article
summarized the early developments
up to 2002.38 At the end of this early period, O’Hearn circulated a note that
Figure 1. Picture semantics.
x = 10
y = 42
x = 10
y = 42
x = 10
y = 42
Figure 2. Mathematical semantics.