for the second step of the code to wire up
a cyclic linked list described at the start
of the paper.
The ultimate theoretical support for
the small axioms came from a completeness theorem in Yang’s Ph.D. thesis.
42
He showed the small axioms and frame
rule and several other inference rules
(particularly Hoare’s rules for strengthening preconditions and weakening
postconditions, and a rule for existential
quantifiers) can be used to derive all true
Hoare triples for these statements.
Locality properties of program behavior, and their connection to logic,
13, 44
are critical for these results:
"An assertion talks about a heaplet
rather than the global heap, and a spec
{P} C {Q} says that if C is given a heaplet
satisfying P then it will never try to access heap outside of P (other than cells
allocated during execution) and it will
deliver a heaplet satisfying Q if it terminates.
2"
In-place reasoning as with the two-element cyclic list has been applied to
many imperative programs. As an example, consider the insertion of a node
y into a linked list after position x. We
can do this in two steps: first we swing
x’s pointer so it points to y, and then we
swing y to point to z (the node after x).
Here, in the precondition for each
step we write the frame in red; it is the
blue that is updated in place. The reader
can see how, using the small axiom for
free together with the frame rule, we
could reason about the converse case of
removing an element from a list.
This example generalizes to many
other list and tree algorithms: insertion, deletion, reversal, and so on. The
SL proofs resemble the box-and-pointer
arguments that have long been used
informally in describing data structure
mutation.
These ideas extend to concurrent
programs; for example, the second rule
instance in Figure 4 uses the concurrency rule to reasons about our two-element
cyclic list, but wired up concurrently
rather than sequentially. The in the
precondition in this instance ensures
that x and y are not aliases, so there is no
data race in the parallel program.
The second axiom says that if x points
to v and we read x into y, then y will have
value v. Here, we distinguish between
the value in a variable or register (x and
y) and the r-value in a heap cell whose l-value is the value held in x. The second
axiom assumes that x does not appear
in syntactic expression v (see O’Hearn et
al.
32 for a precise description of this and
other variable side conditions).
The allocation axiom says: If you start
with no heap, then you end with a heap
of size 1. Conversely the De-Allocation
axiom starts with a hap of size 1 and
ends with the empty heap. The Application axiom assumes that allocation
always succeeds. To model a case where
allocation might fail we could use a disjunctive postcondition, like x – ∨ x ==
0; this is what tools such as SpaceInvader and Infer, discussed later, do for mal-loc() in C.
The small axioms are so named be-
cause each mentions a small amount
of memory: a single memory cell. When
people first see the axioms they can
come as a shock: aren’t they too sim-
ple? Previous approaches had complex
descriptions accounting for the effect
of mutations on global properties of
graph-like structures.
6
In actuality, there is a sense in which
the small axioms capture all that is
needed to know about the statements
they describe. In intuitive terms, we can
say that imperative computation proceeds by in-place update, where these
primitive statements update or access a
single memory cell at a time; describing
what happens to only that cell should be
enough. The small axioms are thus an
extreme illustration of the principle of
local reasoning.
The frame rule in Figure 3 provides
logical support for this intuition. It allows us to extend reasoning from one
to multiple cells; so the seeming restriction to one cell in the small axioms is not
a restriction at all, but rather a pleasantly
succinct description. For instance, if we
choose x y as our frame then the first
instance in Figure 4 gives the reasoning
Figure 4. Frame and concurrency examples.
Figure 5. deletetree example.
root
r lx y