Introduction To Separation Logic
Step 0: Basic reasoning about code with Hoare triples
To start with, consider the following program whose job is to take two pointers and to set the first to be the sum of the two pointed-to values, and the second to be their difference:
fn f(int *a, int *b) {
c = *a
d = *b
*a = c+d
*b = c-d
}Does this work? How would we prove it?
Well, it might not work. What if a or b isn’t a valid pointer?
There isn’t a generic programmatic check for “pointer validity”
(though usually “not NULL” is used in practice as a guard at least
against the most common kind of accidental invalid pointer).
So we can only really reason about this function under the
precondition that a and b are valid pointers. This calls for some
notation: We will write “a -> x” to mean “a is a valid
pointer, and points to the valid x.”
Moreover, following the conventions of the community, we will denote conditions on program execution by surrounding them in curly braces:
{a -> x AND b -> y}Finally, the convention for describing the behaviour of code is that we write
{precondition} code {postcondition}if, when precondition is true and we execute code, it becomes the
case that afterwards, postcondition is true.
So what we’d like to show is that:
{a -> x AND b -> y}
fn f(int *a, int *b) {
let c = *a
let d = *b
*a = c+d
*b = c-d
return
}
{a -> x+y AND b -> x-y}So how do we prove this?
You might already see how we can work our way down the code, one line at a time. We’ll do it slowly, however, to make clear the structure of the logic we’re using, since this will be important and more challenging later.
What we need to know is, for various statements in our programming
language like variable = *pointer_variable, what post-conditions
follow from this code in various pre-conditions. For example, for the
line c = *a, what pre-conditions are required to even run this line?
What post-conditions follow? The answers to these questions for the
various statement types in our programming language are called the
operational semantics of the language.
For example, one proposition in the operational semantics of our pseudo-C language should be:
{a -> x} let c = *a {c = x AND a -> x} (S1)Now we meet with an immediate problem: Our pre-condition doesn’t actually have the required shape to apply this rule.
Of course, the fact that our precondition includes extra conditions shouldn’t really matter. Indeed, the way these pre-/post-condition statements (generally referred to as Hoare triples) work should include some axiom like:
({P} code {Q}) AND ({R} code {R}) => {P AND R} code {Q AND R}That is, if code transforms pre-condition P into Q but leaves
R unchanged, then it transforms the pre-condition P AND R into Q AND R. We shall collect axioms like this one as we go. Usually, all
the axioms are frontloaded into a rather chaotic looking early page in
most programming languages papers, even before the terms needed to
understand them are introduced. For the sake of helping to read such
papers, however, we will note here that the usual way of writing
axioms like this is:
{P} code {Q} {R} code {R}
------------------------------- (A1)
{P AND R} code {Q AND R}(This particular axiom is sometimes called the “frame rule” on account of its noting that any “context frame” that is untouched by that code can be freely added to the pre- and post-conditions of that code.)
The set of all the primitives comprising our language (for example,
points-to—i.e. a -> b, variable values—i.e. a = b, Hoare
triples) as well as the axioms governing those primitives, all
together define a program logic. The specific subspecies of logic
that we will be constructing is called separation logic.
Now we’re prepared to take our first steps through the program:
{a -> x AND b -> y}
let c = *a
{c = x AND a -> x AND b -> y}follows from A1 and S1 and a liberal use of commutativity and
associativity of AND.
Likewise, we can continue:
{a -> x AND b -> y}
let c = *a
{c = x AND a -> x AND b -> y}
d = *b
{d = y AND c = x AND a -> x AND b -> y}If S1 is a semantic rule governing reads, it is not surprising we
should have one governing writes as well:
{a -> x} *x = y {a -> y} (S2)Along with a fairly trivial axiom saying that if a pointer points to a value, then it also points
This gets us through the rest of our program:
{a -> x AND b -> y}
c = *a
{c = x AND a -> x AND b -> y}
d = *b
{d = y AND c = x AND a -> x AND b -> y}
*a = c+d
{d = y AND c = x AND a -> x+y AND b -> y}
*b = c-d
{d = y AND c = x AND a -> x+y AND b -> x-y}But this is not the post-condition we claimed! It has extra stipulations!
For some definitions of the logic, we could have a rule that allows us to drop conditions:
{P AND Q}
---------
{P}However, permitting this will make it challenging to reason about
concurrency and about memory leakage. If {a -> x} means “we have a
resource a that points to x, but we might have other resources
also”, then we cannot conclude that it is safe for any other code to
use, say, b. Moreover, we cannot conclude that b has been properly
cleaned up, or whether we have simply dropped b from our
propositions using the above axiom.
So if we are only designing a logic that will handle straight-line
code in a single thread, particularly in a garbage-collected language
where memory-leaks are handled outside the code, this might be
fine. To reason about concurrency, however, it will be much more
conducive to define {a -> x} to mean “we have a resource a that
points to x, and no other resources.” In consequence, however, it is
then false that from {a -> x AND b -> y} we can conclude {a -> x}.
So what is going on in our code above?
You might recognise that what really makes our conclusion possible
should be some notion of our exiting the function’s scope, causing c
and d to drop because they are attached to this scope. If we are
explicit about scope in our writing the program, then, we might write
it something like:
{a -> x AND b -> y}
begin_scope(f)
let c = *a
let d = *b
*a = c+d
*b = c-d
end_scope(f)Where the result
{a -> x AND b -> y}
begin_scope(f)
let c = *a
{c = x AND a -> x AND b -> y}
d = *b
{d = y AND c = x AND a -> x AND b -> y}
*a = c+d
{d = y AND c = x AND a -> x+y AND b -> y}
*b = c-d
{d = y AND c = x AND a -> x+y AND b -> x-y}
end_scope(f)Step 1: Taming the complexity of Hoare triples–the starting point of separation logic
In the previous program, we used some auxiliary variables to ensure things were done carefully, but we need not have done so if we were just a little more clever:
fn f(int *a, int *b) {
*a = *a + *b
*b = *a - 2 * (*b)
}Not needing all the local variables at least helps us avoid the troublesome reasoning about scope management from the previous step. However, does this program actually work the same way? We can start with the same pre- and post-conditions:
{a -> x AND b -> y}
*a = *a + *b
*b = *a - 2 * (*b)
{a -> x+y AND b -> x-y}What about the proof?
Certainly, we can try to apply our rules for reads and writes as before, but to be careful about it, let’s slow up the first line a little (noting that, as this line does in fact do two reads and a store, it is in reality three operations):
temp1 = *a
temp2 = *b
*a = temp1+temp2Then we can apply our rules to get as far as:
{a -> x AND b -> y}
temp1 = *a
{a -> x AND b -> y AND temp1 = x}
temp2 = *b
{a -> x AND b -> y AND temp1 = x AND temp2 = y}
*a = temp1+temp2Now we want to conclude the post-condition
{a -> x+y AND b -> y AND temp1 = x AND temp2 = y}How do we do this? Remember (S1) that to reason about a store operation, we need pre- and post-conditions shaped like:
{ a -> ? } *a = z { a -> z }While we do have the precondition a -> x+y, we also have a lot of
other preconditions. Recall that it is the “frame rule” (A1) that
allows us to add unaffected “frame” hypotheses to the pre- and
post-conditions. So to apply this, we need:
{b -> y AND temp1 = x AND temp2 = y} *a = temp1+temp2 {b -> y AND temp1 = x AND temp2 = y}That is, that this line of code leaves the truthfulness of every
statement not about a unchanged.
So does it? Well, we don’t yet have an axiom that tells us so. In fact
this is because it may not be so: if a and b point to the same
location, then a write to a may in fact change the value pointed to
by b!
The axiom we are looking for, then, would look something like:
{b -> x AND a != b} *a = y {b -> x AND a != b}However, a logistical problem quickly presents itself: If we had three pointers, we would need to tote around up to 8 extra conditions expressing which pairs of the two pointers may or may not, at any given time, point to the same location. For a more realistically-sized program which might have up to 30 pointers live at some points, we would technically require over a billion conditions to track any possible aliasing. So some better method of bookkeeping is needed.
Now of course, most of the time, pointer aliasing is not
expected. Probably, if we wrote a function like the above, we intend
that it always be called with two separate pointers, and probably if
we had 30 pointers running around our code, we would expect (perhaps
even rely on) that all of them are different. This motivates the
bookkeeping trick that is often used to solve this problem: a new
coordinating conjunction to replace AND–one that doesn’t just say
that two pointers point somewhere, but that explicitly denotes that
they are not aliased. This conjunction, which is usually written as
* and read as “separate from”: a -> x * b -> y (“a points to x;
separately, b points to y”) is the statement that a and b are
valid and non-overlapping pointers, pointing to values x and y
respectively.
The frame rule then states:
{P} code {Q}
--------------------
{P * R} code {Q * R}(Where we no longer need to qualify that R is unaffected, because the
use of * already necessitates that R is disjoint from P and Q.
Then the deduction above becomes not only simpler, but actually correct: If we start with the pre-condition that
{a -> x * b -> y}Then we will be justified in using the frame rule to deduce:
{a -> ? * b -> y} *a = x+y {a -> x+y * b -> y}So our code written this way, has the pre-condition that not only must
a and b be valid pointers, but they must be separate:
{a -> x * b -> y}
*a = *a + *b
{a -> x + y * b -> y}
*b = *a - 2 * (*b)
{a -> x + y * b -> (x + y) - 2*y}
{a -> x+y * b -> x-y}It concludes that a and b take on the requisite values, and are
still separate.