Separation logic


In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs.
It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications. A CACM review article by O'Hearn charts developments in the subject to early 2019.

Overview

Separation logic facilitates reasoning about:
  • programs that manipulate pointer data structures—including information hiding in the presence of pointers;
  • "transfer of ownership" ; and
  • virtual separation between concurrent modules.
Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification and automated parallelization of software.

Assertions: operators and semantics

Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local variables and dynamically-allocated objects in common programming languages such as C and Java. A store is a function mapping variables to values. A heap is a partial function mapping memory addresses to values. Two heaps and are disjoint if their domains do not overlap.
The logic allows to prove judgements of the form, where is a store, is a heap, and is an assertion over the given store and heap. Separation logic assertions contain the standard Boolean connectives and, in addition,,,, and, where and are expressions.
  • The constant asserts that the heap is empty, i.e., when is undefined for all addresses.
  • The binary operator takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I.e., when and is otherwise undefined.
  • The binary operator asserts that the heap can be split into two disjoint parts where its two arguments hold, respectively. I.e., when there exist such that and and and.
  • The binary operator asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I.e,. when for every heap such that, also holds.
The operators and share some properties with the classical conjunction and implication operators. They can be combined using an inference rule similar to modus ponens
and they form an adjunction, i.e., if and only if for ; more precisely, the adjoint operators are and.

Reasoning about programs: triples and proof rules

In separation logic, Hoare triples have a slightly different meaning than in Hoare logic. The triple asserts that if the program executes from an initial state satisfying the precondition then the program will not go wrong, and if it terminates, then the final state will satisfy the postcondition. In essence, during its execution, may access only memory locations whose existence is asserted in the precondition or that have been allocated by itself.
In addition to the standard rules from Hoare logic, separation logic supports the following very important rule:
This is known as the frame rule and enables local reasoning. It says that a program that executes safely in a small state, can also execute in any bigger state and that its execution will not affect the additional part of the state. The side condition enforces this by specifying that none of the variables modified by occur free in, i.e. none of them are in the 'free variable' set of.

Separation algebras

More generally, separation logic can be seen as a way of reasoning about separation algebras. A separation algebra may be defined in several ways, but is often presented as a cancellative, partial commutative monoid. More concretely, it is a set A, partial binary operation and constant u satisfying the following identities, where in the first three laws, if any side of the equation is defined, all sides are defined:
  • Associativity: For all x, y and z,
  • Commutativity: For all x and y,
  • Identity: For all x,
  • Cancellativity: For all x, y and z, if then
It can be shown that the presentation of stacks and heaps above gives rise to a separation algebra: take A to be the set of all heaps, the binary operation to be the union of two heaps, and u to be the empty heap. In some definitions, cancellativity is omitted, but this does not necessarily pose a problem.
Many assertions can be given semantics purely in terms of a separation algebra; in particular, for an assertion P we can assign to it a certain subset of A, denoted, as follows:
The rules for,, and are omitted but are easily derived from the above, while the semantics of are given by the separation algebra in question.

Sharing

Separation logic leads to simple proofs of pointer manipulation for data structures that exhibit regular sharing patterns which can be described simply using separating conjunctions; examples include singly and doubly linked lists and varieties of trees. Graphs and DAGs and other data structures with more general sharing
are more difficult for both formal and informal proof. Separation logic has, nonetheless, been applied successfully to reasoning about
programs with general sharing.
In their POPL'01 paper, O'Hearn and Ishtiaq explained how the magic wand connective could be used to reason in the presence of sharing, at least in principle.
For example, in the triple
we obtain the weakest precondition for a statement that mutates the heap at location, and this works for any postcondition, not only one that is laid out neatly using the separating conjunction. This idea was taken much further by Yang, who used to provide localized reasoning about mutations in the classic Schorr-Waite graph marking algorithm. Finally, one of the most recent works in this direction is that of Hobor and Villard, who
employ not only but also a connective
which has variously been called overlapping conjunction or sepish, and which can be used to describe overlapping data structures: holds of a heap when
and hold for subheaps and whose union is, but which possibly have a nonempty portion in common. Abstractly, can be seen to be a version of the fusion connective of relevance logic.

Concurrent separation logic

A Concurrent Separation Logic,
a version of separation logic for concurrent programs, was originally proposed by Peter O'Hearn,
using a proof rule
which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach of Tony Hoare to reasoning about concurrency,
replacing the use of scoping constraints to ensure separation by reasoning in separation logic. In addition to extending Hoare's approach to apply in the presence of heap-allocated pointers, O'Hearn showed how reasoning in concurrent separation logic could track dynamic ownership transfer of heap portions between processes; examples in the paper include a pointer-transferring buffer, and a memory manager.
Commenting on the early classical work on interference freedom by Susan Owicki and David Gries, O'Hearn says that explicit checking for non-interference isn't necessary because his system rules out interference in an implicit way, by the nature of the way proofs are constructed.
A model for concurrent separation logic was first provided by Stephen Brookes in a companion paper to O'Hearn's. The soundness of the logic had been a difficult problem, and in fact a counterexample of John Reynolds had shown the unsoundness of an earlier, unpublished version of the logic; the issue raised by Reynolds's example is described briefly in O'Hearn's paper, and more thoroughly in Brookes's.
At first it appeared that CSL was well suited to what Dijkstra had called loosely connected processes, but perhaps not to fine-grained concurrent algorithms with significant interference. However, gradually it was realized that the basic approach of CSL was considerably more powerful than first envisaged, if one employed non-standard models of the logical connectives and even the Hoare triples.
By suitable choice of separation algebra, it was surprisingly found that the proof rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding the rely-guarantee technique which had been originally proposed to reason about interference; in this work the elements of the model were considered not resources, but rather "views" of the program state, and a non-standard interpretation of Hoare triples accompanies the non-standard reading of pre and postconditions.
Finally, CSL-style principles have been used to compose reasoning about program histories instead of program states, in order to provide modular techniques for reasoning about fine-grained concurrent algorithms.
Versions of CSL have been included in many interactive and semi-automatic verification tools as described in the next section. A particularly significant verification effort is that of the μC/OS-II kernel mentioned there. But, although steps have been made, as of yet CSL-style reasoning has been included in comparatively few
tools in the automatic program analysis category.
O'Hearn and Brookes are co-recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic.

Fractional permissions

Plain concurrent separation logic is able to describe ownership transfer, wherein one thread may completely gives control over individual heap locations to another thread, but this isn't enough to reason about many concurrent programs—in particular, each heap cell may be shared by many threads so long as each thread only reads from the cell and does not write to it, or alternatively it may be written to so long as only one thread can do the writing.
This may be achieved by annotating each assertion with a fractional permission as. When π = 1, the thread has full ownership of the heap cell and therefore may write to it:
When π < 1, the thread only has shared access, and therefore may only read:
Importantly, permissions may be infinitely split, allowing an arbitrary number of threads to read from the same location :
Note that the actual magnitudes of the permissions less than one are immaterial and only required for tracking purposes; a program should not concern itself over whether any given permission is 0.1 or 0.9, as it is able to read from the heap cell all the same.
To allow for two heaps to both consider the same memory location, some modification is required to the definition of heaps and their disjointness. In particular, every heap location is assigned a fractional permission, and two heaps are disjoint if, for every location that is in both heaps, their values are equal and the sum of their fractional permissions does not exceed one. The operation of merging two heaps will correspondingly add together permissions for those duplicated locations.