Communications of the ACM

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