Specifying with Separation Logic

Hoare logic handles programs that involve only local scalar variables on the stack (such as intint) with ease: assertions are first-order formulas about the values of variables, and the assignment axiom together with loop invariants is enough to carry most proofs through. But the difficulty in verifying C programs lies not in scalars on the stack, but in the heap and pointers—linked lists, trees, graphs, the shared mutable data structures. This section first uses an example to show that once a program starts manipulating the heap, specifications in classical Hoare logic quickly become unwieldy and complicate the proof; it then introduces separation logic and how it resolves this difficulty with a new logical connective. This section uses formalized mathematical notation and does not yet touch C*‘s concrete specification syntax.

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 show that it is correct: after the call returns, all the nodes of the tree have been freed. 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 in the allocated state; is an arbitrary auxiliary variable. The whole specification reads: “if is any node in the tree , then after free_tree(p)free_tree(p) executes, is no longer in the allocated state.”

Verifying the function body along its recursive structure, consider the first recursive call free_tree(i)free_tree(i). Instantiating the specification at :

The postcondition only says “the nodes in the subtree have been freed,” and says nothing about the rest of memory. In particular, it does not rule out the possibility that free_tree(i)free_tree(i) also overwrites the subtree along the way—looking at this specification alone, after the call returns may no longer be a tree, the precondition of the second call free_tree(j)free_tree(j) cannot be established, and the proof gets stuck here. This is not nitpicking: whatever behavior the specification permits, the proof must account for.

One remedy is to add frame axioms: writing “what does not change” into the pre- and postconditions as well. For example:

Just to spell out that “any node outside the tree and its fields are unchanged, and the unallocated remains unallocated,” the specification is stuffed with metavariables , , that have nothing to do with this function, where 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 do not scale, and they run entirely counter to the programmer’s intuition—whoever wrote free_treefree_tree knows perfectly well: “I only touched this one tree.”

Separation logic was proposed by Reynolds, O’Hearn and others around the year 2000 to address these two difficulties head-on: letting assertions by default talk only about “one block” of memory, and building “mutually disjoint” into the logical connective itself, thereby reducing the burden of explicit description.

Separation logic does not replace Hoare logic but extends it: the form of the triple stays the same, the change happens in the model of the program state and in the assertion language.

The store corresponds to C’s local variables and can be thought of as the stack; the heap corresponds to dynamically allocated memory and can be thought of as the heap. Note that the heap is a partial function: a heap can contain just two or three addresses—this leaves room for “an assertion describing only a small block of memory.”

On top of first-order logic, the assertion language adds 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, with semantics identical to Hoare logic; logical constants and connectives are lifted pointwise onto the state ; together with the three new constructs, the semantics are as follows.

Note that the semantics of is “exactly”: the heap has one and only one location, namely . To express “the heap has at least the location ,” one should write . This seemingly strict design is precisely the source of locality: each precisely “claims” one memory location, and then stitches together mutually disjoint claims.

The figure below is a classic example: three memory locations pointing to one another. Each in the assertion describes exactly one location, and stitches the three small heaps characterizing different memory locations 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” into “at least”—as long as one can split off the two cells starting at and assign the rest to , which both A and B satisfy;
• 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 is the opposite: requires both conjuncts to hold on the same heap, which is precisely to assert ;
• Row 5: both conjuncts only require “at least my own two cells”: in A the two blocks can each be split off, in B the same block is shared by both conjuncts, so both hold—it is the common weakening of rows 3 and 4, no longer distinguishing whether and are aliases.

In other words, has “mutually disjoint” built in, while has “the same block” built in. A striking-looking corollary: is satisfiable (take ; any nonempty heap satisfies ). As O’Hearn put it: “To understand a separation-logic assertion, always think locally.”

Separation logic not only lets us characterize heap properties with assertions that have locality, its reasoning rules also let the proof itself benefit from locality. First, the axioms of the heap-manipulating statements. In our mathematical notation, we adopt 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 have very good locality, and so are also called small axioms:

(Side condition of allocation: does not occur free in .) The precondition of each axiom “claims” only the few cells being touched: to write one cell, it talks only about that cell; after freeing, the cell disappears from the heap, leaving . Such small axioms suffice because of the most important rule in separation logic backing them up:

Reading: if runs correctly on the “small” state satisfying , then it runs equally correctly on any “large” state that is “ plus a disjoint block of memory ,” and is left untouched. “What does not change” no longer has to be written into every specification—it is introduced in a single step by the frame rule when needed. This is local reasoning: a specification describes only the memory the program actually touches (called its footprint), and leaves the rest to the frame rule.

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—“nodes are unshared and there are no cycles” no longer needs an extra axiom, but is a direct consequence of the definition. The whole specification accordingly shrinks to:

The postcondition says: when the function returns, the block of memory claimed by the precondition (the entire tree) has all been returned. Note that the specification says nothing at all about the space 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 difficulty of the previous section—“the subtree might be modified”—vanishes here: it sits in the frame , and the rule guarantees it does not budge. Three small axioms plus one frame rule replace the tedious frame axioms.

There is a subtle point worth spelling out. Separation logic reads its triples more strongly than partial correctness:

This semantics is not merely a strengthening of correctness, it is also the condition under which the frame rule holds. Conversely, if we allowed faulting executions, then would be a valid specification (it requires nothing of the result state); applying the frame rule with :

the conclusion does not hold: after writing into , still holds . Notice that the problem here is that should not hold in the first place: did not claim the cell , so the write might fault. Separation logic therefore mandates: the precondition must characterize all the memory the program touches. The benefit this brings: any program verified through separation logic automatically rules out wild-pointer writes, dangling-pointer dereferences, double frees, and the like—memory safety is a natural result of program verification.

Stringing the small axioms, the frame rule, and Hoare logic’s original rules together, we can work through a program that really manipulates pointers, statement by statement. The program below allocates two two-cell blocks, makes them reference each other, then frees one of them and reads through the pointer. The target specification is: