Specifying with Separation Logic

Hoare logic works well for programs that involve only local scalar variables on the stack (such as intint): assertions are first-order formulas about variable values, and the assignment axiom and loop invariants suffice for most proofs. Verifying C programs becomes more difficult when they manipulate the heap through pointers, especially in shared mutable data structures such as linked lists, trees, and graphs. We first use an example to show how heap manipulation makes classical Hoare specifications unwieldy and complicates proofs; we then introduce separation logic, which addresses this difficulty with a new logical connective. This section uses mathematical notation; C*‘s concrete specification syntax comes later.

Consider the following C function, which recursively frees all the nodes of a binary tree:

#include <stdlib.h>
struct tree {
  struct tree *l;
  struct tree *r;
};
void free_tree(struct tree *p)
{
  if (p != NULL) {
    struct tree *i = p->l;
    struct tree *j = p->r;
    free_tree(i);
    free_tree(j);
    free(p);
  }
}

#include <stdlib.h>
struct tree {
  struct tree *l;
  struct tree *r;
};
void free_tree(struct tree *p)
{
  if (p != NULL) {
    struct tree *i = p->l;
    struct tree *j = p->r;
    free_tree(i);
    free_tree(j);
    free(p);
  }
}

We want to prove that all nodes of the tree have been freed when the call returns. A seemingly reasonable Hoare-style specification is:

Here means that points to a valid binary tree (nodes are unshared and there are no cycles); means that node is reachable from ; means that is allocated; is an arbitrary auxiliary variable. The specification states that if is any node in the tree , then after free_tree(p)free_tree(p) executes, is no longer allocated.

To verify the function body by following its recursive structure, consider the first recursive call free_tree(i)free_tree(i). Instantiating the specification at gives:

The postcondition says only that the nodes in the subtree have been freed; it says nothing about the rest of memory. In particular, it allows free_tree(i)free_tree(i) to overwrite the subtree as well. From this specification alone, we cannot establish that is still a tree when the call returns, so we cannot establish the precondition of the second call free_tree(j)free_tree(j). The proof must account for every behavior the specification permits.

One remedy is to add frame axioms, which state what remains unchanged in the pre- and postconditions. For example:

To state that any node outside the tree and its fields are unchanged, and that the unallocated remains unallocated, the specification introduces metavariables , , unrelated to the function’s operation; stands for an arbitrary field (such as ll and rr). For every additional kind of resource the program might reference, each function specification has to carry another set of frame axioms. Such specifications are difficult to maintain as programs grow. They also obscure the programmer’s reasoning: free_treefree_tree operates on just one tree.

Separation logic was proposed by Reynolds, O’Hearn and others around the year 2000 to address these two difficulties: assertions describe individual blocks of memory, and the logical connective itself expresses disjointness, reducing the number of conditions that must be stated explicitly.

Separation logic extends Hoare logic: the form of the triple stays the same, while the program state model and assertion language change.

The store corresponds to C’s local variables and can be thought of as the stack; the heap corresponds to dynamically allocated memory. Because the heap is a partial function, it can contain just two or three addresses, allowing an assertion to describe a small block of memory.

The assertion language extends first-order logic with three constructs, collectively called spatial assertions:

• : the empty-heap assertion, i.e. the empemp we saw in Your First C* Program
• : the points-to predicate, meaning address holds exactly the value , i.e. the data_at data_at we saw in Your First C* Program (address holds exactly the value );
• : separating conjunction, meaning the heap can be split into two disjoint blocks satisfying and respectively, i.e. the **** connective we saw in Your First C* Program.

The satisfaction relation is written , read “state satisfies assertion .” Arithmetic assertions between variables (such as ) depend only on the store and have the same semantics as in Hoare logic. Logical constants and connectives are lifted pointwise to the state . Together with the three new constructs, they have the following semantics.

The assertion describes a heap with exactly one location, namely . To express that the heap contains at least the cell described by , write . This exactness supports locality: each describes one memory location, and combines assertions about disjoint parts of the heap.

The figure below shows three memory locations pointing to one another. Each in the assertion describes exactly one location, and combines the three single-cell heaps into the whole heap.

Let us verify each row:

• Row 1: requires the entire heap to be exactly the two cells starting at ; A’s heap has four cells, so it does not hold;
• Row 2: holds for any heap, so relaxes “exactly” to “at least”: the heap need only contain the two cells starting at , with the rest satisfying . Both A and B meet this condition;
• Row 3: A’s heap can be split into two disjoint blocks, each satisfying one conjunct, whereas B’s heap cannot be split into two disjoint blocks;
• Row 4: requires both conjuncts to hold on the same heap, which here requires ;
• Row 5: each conjunct requires the heap to contain at least the two cells it describes. In A, the two blocks can be split off separately; in B, both conjuncts describe the same block. The assertion therefore holds in both states. It is a common weakening of rows 3 and 4 and does not distinguish whether and are aliases.

Thus, requires disjoint parts of the heap, while requires its conjuncts to hold on the same heap. One consequence is that is satisfiable (take ; any nonempty heap satisfies ). As O’Hearn put it: “To understand a separation-logic assertion, always think locally.”

Locality applies to separation logic’s reasoning rules as well as its assertions. We begin with the axioms for heap-manipulating statements. Our mathematical notation uses a minimal instruction set: writes to address (corresponding to C’s *e = f*e = f), allocates contiguous cells and initializes them (corresponding to mallocmalloc), and frees address (corresponding to freefree). Their axioms describe only the memory involved in each operation and are therefore called small axioms:

(Side condition of allocation: does not occur free in .) Each axiom’s precondition describes only the cells the operation touches: writing requires a single cell, and freeing that cell leaves . The frame rule lets us use these small axioms to reason about larger heaps:

If runs correctly on a state satisfying , it also runs correctly on a heap consisting of the memory described by and a disjoint block satisfying , and the memory described by remains unchanged. We can therefore introduce the unchanged memory through the frame rule when needed, without listing it in every specification. This is local reasoning: a specification describes only the memory the program touches (its footprint), and the frame rule accounts for the rest.

Return to the free_treefree_tree example at the start. First, the predicate itself can be defined inductively using spatial assertions:

guarantees that the root node and the left and right subtrees are pairwise disjoint. The absence of sharing and cycles follows from the definition, without an extra axiom. The specification becomes:

The postcondition states that when the function returns, all memory described by the precondition (the entire tree) has been freed. The specification says nothing about memory outside the tree. To verify the recursive call, split the heap into three blocks according to the definition of ; apply the specification to free_tree(i)free_tree(i) (acting on the block ), and the frame rule passes the other two blocks through unchanged:

The subtree belongs to the frame , so the frame rule guarantees that it remains unchanged. This resolves the difficulty with the earlier specification. Three small axioms and one frame rule replace the explicit frame axioms.

Separation logic gives its triples a stronger meaning than partial correctness alone:

The requirement that execution never faults is also needed for the frame rule to hold. If faulting executions were allowed, then would be a valid specification (it imposes no condition on the result state). Applying the frame rule with would give:

This conclusion is invalid: it claims that after writing into , still holds . The problem is that should not hold: does not require the cell to be allocated, so the write might fault. Separation logic therefore requires that the precondition characterize all the memory the program touches. Verification in separation logic thus rules out wild-pointer writes, dangling-pointer dereferences, double frees, and similar errors: memory safety follows from the semantics of the triple.

We can combine the small axioms, the frame rule, and Hoare logic’s original rules to verify a pointer-manipulating program statement by statement. The program below allocates two two-cell blocks, makes them reference each other, then frees one cell and reads through the pointer. The target specification is: