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:
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 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.

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.
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.
An abstract version of separation logic was proposed that works for Hoare triples
where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.
Later, by suitable choice of commutative monoid, 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.

Verification and program analysis tools

Tools for reasoning about programs fall on a spectrum from fully automatic program analysis tools, which do not require any user input, to interactive tools where the human
is intimately involved in the proof process. Many such tools have been developed; the following list includes a few representatives in each category.
The distinction between interactive and in-between verifiers is not a sharp one. For example,
Bedrock strives for a high degree of automation, in what it terms mostly-automatic verification, where
Verifast sometimes requires annotations that resemble the tactics used in interactive verifiers.