Reynolds), in 2004, proved the theorem,
which justified the logic.
Abstraction and
the Fiction of Separation
There was considerable work on extending SL after those early papers. Some of it
concentrated on different programming
paradigms, such as object-oriented programming or scripting languages, or
on additional programming primitives
such as message passing, reentrant lock
and fork/join concurrency. Besides extensions to cover an ever-greater variety
of programming, two conceptual developments opened major new directions.
•In his Ph.D. thesis, Parkinson
showed how abstract predicates (
predicate variables) fit together nearly with *
in the description of classes and other
stateful data abstractions.
33
• Gardner and others emphasized a
concept of fictional separation, where
strong separation properties could be
assumed of data abstractions, even for
implementations relying on sharing.
These ideas were first described in
a sequential setting. Dinsdale-Young,
Gardner and Wheelhouse described
an implementation of a module of sequences in terms of linked lists and noted a mismatch: at the abstract level an
operation might affect a small part of a
sequence, where at the implementation
level its footprint could involve the entire list; conversely, locality can increase
with abstraction.
19 Meanwhile, Parkinson initially targeted a sequential subset
of Java. Subsequent work showed how
abstract predicates could be understood
using higher-order versions of SL.
5
While they could be expressed in a
sequential setting, the ideas took flight
when transported to concurrency. The
CAP logic18 combined insights on abstract predicates and fiction, along
with those of CSL, to reason about data
abstractions with interference in their
implementations. The views theory17
provided a foundation where separation does not appear in the normal execution semantics of programs, but only
in an abstraction of it. Views showed
that a simple version of CSL can embed
many other techniques including even
the classic rely-guarantee method;
27
this is surprising because rely-guarantee was invented for reasoning about
interference, almost the opposite of
the basis of original SL.
ditions for each process. The rule supports completely independent reasoning about processes. This rule can be
used to provide straightforward proofs
of processes that don’t share access to
storage. We mentioned parallel quick-sort earlier, and deletetree() provides another illustration: we can run
the two recursive calls in parallel rather
than sequentially, as presented in the
proof outline ( 1) in Figure 6.
In work on CSL, proof outlines are
often presented in a spatial fashion like
this: this outline shows the premises of
the concurrency rule in the left and right
Hoare triples, the overall precondition
(the pre1 pre2) at the beginning, and
the post at the end.
While this reasoning is simple, if CSL
had only been able to reason about disjoint concurrency, where there is no inter-process interaction, then it would have
rightly been considered rather restrictive.
An important early example done with CSL
was a pointer-transferring buffer, where
one thread allocates a pointer and puts it
into a buffer while the other thread reads it
out and frees it. Crucially, not only is the
pointer deemed to transfer from one process to another, but the “knowledge that it
is allocated” transfers with the proof. The
proof establishing absence of memory errors is shown in ( 2) of Figure 6. A way to
implement the buffer code for put and
get is to use locks to synchronize access to
a shared variable and a Boolean to signal
when the buffer is full. We will not delve
into the subproofs of buffer operations
here—for that, consult O’Hearn30—but
we want to talk about a shift in perspective on the meanings of logical assertions
that the proof ( 2) led to.
Notice the assertion emp after the
put(x) statement in the left process.
We could not prove a mutation were
we to place it there, because emp is not
a sufficient precondition for any mutation; that is fortunate as such a mutation could lead to a race condition. But
it is not the case that we know the global heap is empty, because the pointer
x could still persist. Rather, the knowledge that it points to something has
been forgotten, transferred to the second process where it materializes as
y –. A reading of assertions began
to form based on the “right to dereference” or “ownership” (taken as synonymous with right to dereference).
On this reading emp says “I don’t have
permission to dereference any heap,”
or “I own nothing,” rather than “the
heap is empty.” Similarly, x – says “I
own x” (where “I” is the process from
which the assertion is made).
The ownership transfer example
made it clear that quite a few concurrent programs would have much simpler proofs than before. Modular proofs
were provided of semaphore programs,
of a toy memory manager, and programs
with interacting resources. It seemed as
if the proofs mirrored design principles
used to simplify reasoning about concurrent processes, such as in Dijkstra’s
idea of loosely connected processes:
“[A]part from the (rare) moments of
explicit intercommunication, the individual processes are to be regarded as
completely independent of each other.”
16
However, the very feature that gave
rise to the unexpected power, ownership
transfer, made soundness (whether the
rules prove only true statements) nonobvious. O’Hearn worked on soundness
during 2001 and 2002, without success.
In May of 2002 he turned to Brookes who
eventually (with important input from
Figure 6. Concurrency proofs.
