Lecture 33: Separation Logic
1 Purpose
Extend Hoare Logic to handle Heaps and Pointers.
2 Outline
First, we add four commands to our language from last time:
V := [E] -- read the value at address E into V |
[E] := E' -- write the value resulting from evaluating E' into address evaluated by E |
V := cons(E1,...,En) -- create n new consecutive memory cells, storing values from E1,...,En |
-- note this means V is a pointer l, but l+1, l+2, ..., l+n-1 are pointers too |
dispose(E) -- evaluate E to pointer, and free memory associated. fails if pointer is not in heap |
e.g.,
X:=cons(0,1,2); [X]:=Y+1; [X+1]:=Z; [X+2]:=Y+Z; Y:=[Y+Z] |
We would like to be able to prove Hoare triples that involve the heap, e.g.,
{T} X:=cons(0); Y:=X; [Y]:=Z; W:=[X] {W = Z} |
This allocates one cell, storing the pointer in the variable X then copies the pointer to Y. It then writes the value of Z into the cell pointed to by Y, and finally reads the value of the cell pointed to by X into W. This should mean that W is equal to Z, but how do we prove it?
3 Separation Logic
Invented around 2000 by Reynolds, O’Hearn, & Yang, Separation Logic adds various constructs to Hoare Logic that allows it to effectively reason about heap programs. One central issue is that distinct pointers can point to the same memory, which can cause problems in reasoning.
e.g., consider a program to reverse a linked list. If each element is two cells in memory: a value followed by the pointer to the next cell (and the final one has nil for the pointer to the next), the following code reverses the list stored at X, leaving the result at Y.
Y:=nil; |
WHILE ¬(X = nil) DO (Z:=[X+1]; [X+1]:=Y; Y:=X; X:=Z) |
Intuitively, we want to prove a Hoare triple that looks like:
{X points to a linked list holding x} |
Y:=nil; |
WHILE ¬(X = nil) DO (Z:=[X+1]; [X+1]:=Y; Y:=X; X:=Z) |
{Y points to a linked list holding reverse(x)} |
The critical additions to Hoare logic, to support this, are the following logical operators:
E → F -- in the current state, the heap contains a mapping from the value E to the value F |
For example X → Y + 1 holds for a heap {20 → 43} if the variable X has value 20 and the variable Y has value 42.
We may also write E → _ to indicate that there exists some value in the heap that E points to, but not specify which. Logically, this is equivalent to ∃X. E → X (where X does not exist in E).
The next operator, which is the critical operator for separation logic, is called the separating conjunction, and is written ⋆.
It allows us to write logical expressions:
P ⋆ Q -- P and Q hold of disjoint sections of the heap |
This is the critical notion: that you can express properties that hold of different parts of the heap. For example, the assertion X → 0 ⋆ X + 1 → 0 holds of the heap {20 → 0, 21 → 0} if X is 20. More interestingly, the statement X → _ ⋆ Y → _ holds of the heap 10 → 0, 20 → 0 (with X as 10, Y as 20), but does not hold if both X and Y are 10, as then there are not disjoint sections of the heap within which X → _ and Y → _ hold.
We can also specify that the heap is empty, with:
emp |
In addition to a separating conjunction, we also have a separating implication:
P -* Q -- holds if given h' disjoint from h, P(h') implies Q(h, h') |
We can use separating conjunction, and existential, to make formal what we mean by a linked list:
list [] e = (e = nil) |
list ([a0,a1,...,an]) e = ∃e'. (e → a0, e') ⋆ list [a1,...,an] e' |
Note the critical use of the separating conjunction: this ensures that there are no loops in the linked list (which would cause it not to be a list, and for the reverse to not work).
Now, given a (logical) list a0 (like used in the definiton above, e.g., [a,b,c]), we can write the precise Hoare triple for the reverse code as:
{list a0 X} |
Y:=nil; |
WHILE ¬(X = nil) DO (Z:=[X+1]; [X+1]:=Y; Y:=X; X:=Z) |
{list reverse(a0) Y} |
The critical part to prove this will be to figure out the loop invariant for the WHILE loop, which ends up being:
∃ a B. list a X ⋆ list B Y ∧ (rev(a0) = rev(a) · β)
where · means append.
4 Proofs in Separation Logic
Now, we need axioms (or proof rules). First, we have a slightly different assignment axiom:
------------------------------ [assign2] |
⊢ {V = v} V := E {V = E[v/V]} |
(where v must not occur in E). If V doesn’t occur in E, this amounts to:
We can fetch from the heap with:
------------------------------------------------------- [fetch] |
⊢ {(V = v1) ∧ E → v2} V :=[E] {(V = v2) ∧ E[v1/V ] → v2} |
For heap assignment, we have:
--------------------------- [heap-assign] |
⊢ {E → _} [E]:=F {E → F} |
And allocation:
----------------------- [alloc] |
⊢ {V = v} V :=cons(E1, . . . , En) {V → E1[v/V ], . . . , En[v/V ]} |
Finally, disposal (freeing):
----------------------- [dispose] |
⊢ {E → _} dispose(E) {emp} |
The key structural rule for separation logic is the so-called "frame" rule:
⊢ {P} C {Q} |
------------------- [frame] |
⊢ {P ⋆ R} C {Q ⋆ R} |
That allows certain portions of the logical state (here R) to be held constant, assuming they are not modified by C. This is how most of the axioms can involve only the actual locations being used, as the rest of the heap can be framed away.
This allows us to, for example, verify the list reversal program, though we won’t do that (it’s quite tedious). See, e.g., https://www.cl.cam.ac.uk/archive/mjcg/HL/Notes/Notes.pdf (p123).
Tedium in the actual proofs has led to plenty of automation, and there are many libraries to enable proofs using separation logic, including some that handle concurrency. One in particular, Iris, was originally created in order to verify unsafe code in the Rust standard library. Rust is a language that promises safe concurrency by borrowing techniques from linear logic: in particular, there can only be a single mutable reference at a given time. While this is a very strong guarantee, it is in some sense overly restrictive, in that many standard library primitives cannot be implemented without violating it. In order to handle this, Rust has an escape hatch to write "unsafe" code, which is allowed to violate the rules, but programmers are supposed to only use it in ways that do not actually violate the memory constraints. Since all logics and type systems are conservative, there can be operations that the Rust type system cannot prove to be safe, but are, in actuallity, okay.
Iris is a concurrent separation logic that was created in order to prove that unsafe Rust library code, despite violating the rules of the Rust type system, does not acutally violate the memory requirements and thus is, indeed, safe. Another way of understanding this is that while it may break the rules temporarily, by the time it has returned, the memory is in a safe state. For example: there is an operation to split a pointer to an array: doing this in safe Rust isn’t possible, because there isn’t a way to ensure that the original pointer no longer has access to the latter half of the array, but in unsafe Rust, it is possible to create two new pointers that have the right bounds, and Iris can prove that the resulting two pointers are, indeed, safe.
5 Concurrent Separation Logic
While being able to prove sequential programs that manipulate programs were the direct contributions of separation logic, it indirectly provided the tools to solve a much harder problem: shared-memory concurrency. As it turned out, pointer manipulation was the primary challenge, and with tools for that, the rest, while not easy, became much more tractable.
In particular, one key rule is parallel composition:
⊢{P1} C1 {Q1} · · · ⊢ {Pn} Cn {Qn} |
------------------------------------ [par-comp] |
⊢{P1 ⋆ · · · ⋆ Pn} C1 || · · · || Cn {Q1 ⋆ · · · ⋆ Qn} |
i.e., to prove a parallel composition correct, we first separate the state into disjoint parts, prove each part separately, and then combine the resulting states. Of course, this requires there is no communication between parts, which is quite restrictive, but a whole series of results (which we will not cover here), stretching from the mid-2000s up to the present, allow various restricted forms of communication. While the fundamental logic is that of separation, there are certain resources that can be shared that allow reasoning about, e.g., locks, that enable safe mutation across threads.
https://read.seas.harvard.edu/~kohler/class/cs260r-17/brookes16concurrent.pdf