Skip to end of metadata
Go to start of metadata

Okay, a couple of people this have been asking me about separation logic, out of the blue, and I am taking it as a sign. This is of interest to me because Andy Gordon and I have been trying to wrap our collective heads around separation logic, a project about which I hope to be able to talk about before long.

So what's the big hoopla? To understand the why of separation logic, you have to first understand the basics of reasoning about programs, Hoare-logic style. Hoare logic is a logical system where the main judgment is of the form {P}C{Q}, where P and Q are first-order logic formulas, and C is a program, generally in some sequential imperative programming language. The interpretation of such a Hoare triple is that when executed in a state satisfying formula P, program C either does not terminate, or terminates in a state satisfying formula Q. Formulas P and Q may refer to program variables. Thus, for instance, the triple {x=0/\y=0}C{res>=0} says that program C, when started in a state where x=y=0, may terminate in a state where res is positive (or it may not terminate). Hoare logic comes with a proof system that lets you derive Hoare triples compositionally from Hoare triples talking about subprograms appearing in C. Thus, for example, if you know {P}C{Q} and {Q}D{R}, then you can derive {P}C;D{R}, where C;D represents the sequential composition of C and D.

This works surprisingly well for simple imperative languages, but does not scale easily to the kind of features found in real programming languages. In particular, programs that manipulate pointers have always been problematic. Dealing with programs that manipulate heap memory itself is not so bad, by simply extending Hoare logic with a heap and allowing formula P and Q in a Hoare triple to refer to values on the heap. The problem is that the heap must be treated as a large unit, while what one really wants to do is to be able to reason locally, taking into account only the part of the heap that a piece of code reads and modifies. Reynolds and O'Hearn, separately, came up with a rather clean way to express this kind of local reasoning by introducing a separation operator into the predicate language, that can be used to say that the heap is separable into two disjoint pieces that do not refer to each other through pointers. Thus, it is possible to reason locally about the heap that a piece of code uses by simply separating out the appropriate portion of the heap, and re-introducing in the postcondition of the code. In other words, if a piece of code C only uses memory cells c1 and c2, then we can use heap separation to separate a heap h into h' * (c1 -> v1, c2 -> v2), have program C act on the local heap (c1 -> v1, c2 -> v2), perhaps producing a new local heap (c1 -> v1', c2 -> v2', c3 -> v3) (here, C has created a new memory cell c3 holding value v3), and the final heap is obtained by reattaching h' to (c1 -> v1', c2 -> v2', c3 -> v3). This works quite nicely, and I will refer you to the following papers for the history of those early days:

Recently, separation logic has been applied to the problem of reasoning about heap-manipulating concurrent programs. New challenges emerge in this context, such as race conditions. It turns out that separation logic has something to say about managing resources (the heap can be viewed as a resource, so this is maybe not very surprising), and it has been used to reason about lock-free programs, that is, programs that attempt to avoid race conditions without overly using locks, if at all. Unfortunately, there appears to be subtle issues with the rules of the logic when concurrency is added to the mix.

A good overview of separation logic for concurrent programs is O'Hearn's survey paper:

O'Hearn credits Steve Brookes with the solution to the problems of separation logic for concurrent programs:

I hope the above reading material makes for a reasonable starting point.