This article'suse ofexternal links may not follow Wikipedia's policies or guidelines. Pleaseimprove this article by removingexcessive orinappropriate external links, and converting useful links where appropriate intofootnote references.(October 2024) (Learn how and when to remove this message)

Incomputer science,separation logic^[1] is an extension ofHoare logic, a way of reasoning about programs.It was developed byJohn C. Reynolds,Peter O'Hearn, Samin Ishtiaq and Hongseok Yang,^[1][2][3][4] drawing upon early work byRod Burstall.^[5] The assertion language of separation logic is a special case of thelogic of bunched implications (BI).^[6] ACACM review article by O'Hearn charts developments in the subject to early 2019.^[7]

Separation logic facilitates reasoning about:

• programs that manipulate pointer data structures—includinginformation hiding in the presence of pointers;
• "transfer of ownership" (avoidance of semantic frameaxioms); and
• virtual separation (modular reasoning) between concurrent modules.

Separation logic supports the developing field of research described byPeter O'Hearn and others aslocal 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 automatedprogram verification (where analgorithm checks the validity of another algorithm) and automatedparallelization of software.

Separation logic assertions describe "states" consisting of astore and aheap, roughly corresponding to the state oflocal (orstack-allocated) variables anddynamically-allocated objects in common programming languages such asC andJava. A store${\displaystyle s}$ is afunction mapping variables to values. A heap${\displaystyle h}$ is apartial function mapping memory addresses to values. Two heaps${\displaystyle h}$ and${\displaystyle h^{\prime }}$ aredisjoint (denoted${\displaystyle h\mathrm{\perp }{h}^{\prime }}$) if their domains do not overlap (i.e., for every memory address${\displaystyle \ell }$, at least one of${\displaystyle h(\ell )}$ and${\displaystyle h^{\prime }(\ell )}$ is undefined).

The logic allows to prove judgements of the form${\displaystyle s,h\models P}$, where${\displaystyle s}$ is a store,${\displaystyle h}$ is a heap, and${\displaystyle P}$ is anassertion over the given store and heap. Separation logic assertions (denoted as${\displaystyle P}$,${\displaystyle Q}$,${\displaystyle R}$) contain the standard Boolean connectives and, in addition,${\displaystyle \mathbf{e}\mathbf{m}\mathbf{p}}$,${\displaystyle e\mapsto e^{\prime }}$,${\displaystyle P\ast Q}$, and${\displaystyle P-\ast Q}$, where${\displaystyle e}$ and${\displaystyle e^{\prime }}$ are expressions.

• The constant${\displaystyle \mathbf{e}\mathbf{m}\mathbf{p}}$ asserts that the heap isempty, i.e.,${\displaystyle s,h\models \mathbf{e}\mathbf{m}\mathbf{p}}$ when${\displaystyle h}$ is undefined for all addresses.
• The binary operator${\displaystyle \mapsto }$ 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.,${\displaystyle s,h\models e\mapsto e^{\prime }}$ when${\displaystyle h([[e]{]}_s)=[[e^{\prime }]{]}_s}$ (where${\displaystyle [[e]{]}_s}$ denotes the value of expression${\displaystyle e}$ evaluated in store${\displaystyle s}$) and${\displaystyle h}$ is otherwise undefined.
• The binary operator${\displaystyle \ast }$ (pronouncedstar orseparating conjunction) asserts that the heap can be split into twodisjoint parts where its two arguments hold, respectively. I.e.,${\displaystyle s,h\models P\ast Q}$ when there exist${\displaystyle h_1,h_2}$ such that${\displaystyle h_1\mathrm{\perp }{h}_2}$ and${\displaystyle h=h_1\cup h_2}$ and${\displaystyle s,h_1\models P}$ and${\displaystyle s,h_2\models Q}$.
• The binary operator${\displaystyle -\ast }$ (pronouncedmagic wand orseparating implication) 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,.${\displaystyle s,h\models P-\ast Q}$ when for every heap${\displaystyle h^{\prime }\mathrm{\perp }h}$ such that${\displaystyle s,h^{\prime }\models P}$, also${\displaystyle s,h\cup h^{\prime }\models Q}$ holds.

The operators${\displaystyle \ast }$ and${\displaystyle -\ast }$ share some properties with the classicalconjunction andimplication operators. They can be combined using an inference rule similar tomodus ponens

${\displaystyle \frac{s,h\models P\ast (P-\ast Q)}{s,h\models Q}}$

and they form anadjunction, i.e.,${\displaystyle s,h\cup h^{\prime }\models P\ast Q\Rightarrow R}$ if and only if${\displaystyle s,h\models P\Rightarrow Q-\ast R}$ for${\displaystyle h\mathrm{\perp }{h}^{\prime }}$; more precisely, the adjoint operators are${\displaystyle \mathrm{\_}\ast Q}$ and${\displaystyle Q-\ast \mathrm{\_}}$.

In separation logic, Hoare triples have a slightly different meaning than inHoare logic. The triple${\displaystyle \{P\}C\{Q\}}$ asserts that if the program${\displaystyle C}$ executes from an initial state satisfying the precondition${\displaystyle P}$ then the program willnot go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition${\displaystyle Q}$. In essence, during its execution,${\displaystyle C}$ may access only memory locations whose existence is asserted in the precondition or that have been allocated by${\displaystyle C}$ itself.

In addition to the standard rules fromHoare logic, separation logic supports the following very important rule:

${\displaystyle \frac{\{P\}C\{Q\}}{\{P\ast R\}C\{Q\ast R\}}\mathsf{m}\mathsf{o}\mathsf{d}(C)\cap \mathsf{f}\mathsf{v}(R)=\mathrm{\varnothing }}$

This is known as theframe rule (named after theframe problem) and enables local reasoning. It says that a program that executes safely in a small state (satisfying${\displaystyle P}$), can also execute in any bigger state (satisfying${\displaystyle P\ast R}$) and that its execution will not affect the additional part of the state (and so${\displaystyle R}$ will remain true in the postcondition). The side condition enforces this by specifying that none of the variables modified by${\displaystyle C}$ occur free in${\displaystyle R}$, i.e. none of them are in the 'free variable' set${\displaystyle \mathsf{f}\mathsf{v}}$ of${\displaystyle R}$.

More generally, separation logic can be seen as a way of reasoning aboutseparation algebras. A separation algebra may be defined in several ways, but is often presented as acancellative,partialcommutative monoid.^[8] More concretely, it is a setA, partial binary operation${\displaystyle \oplus :A\times A\rightharpoonup A}$ and constantu satisfying the following identities, where in the first three laws, if any side of the equation is defined, all sides are defined:

• Associativity: For allx,y andz,${\displaystyle (x\oplus y)\oplus z=x\oplus (y\oplus z)}$
• Commutativity: For allx andy,${\displaystyle x\oplus y=y\oplus x}$
• Identity: For allx,${\displaystyle x\oplus u=x=u\oplus x}$
• Cancellativity: For allx,y andz, if${\displaystyle x\oplus z=y\oplus z}$ then${\displaystyle x=y}$

It can be shown that the presentation of stacks and heaps above gives rise to a separation algebra: takeA to be the set of all heaps, the binary operation${\displaystyle \oplus }$ to be the union of two heaps (only defined when the heaps are disjoint), andu to be the empty heap. In some definitions, cancellativity is omitted, but this does not necessarily pose a problem.^[9]

Many assertions can be given semantics purely in terms of a separation algebra; in particular, for an assertionP we can assign to it a certain subset ofA, denoted${\displaystyle [[P]]}$, as follows:

• ${\displaystyle [[false]]=\mathrm{\varnothing }}$
• ${\displaystyle [[P\Rightarrow Q]]=\{h|h\in [[P]]\Rightarrow h\in [[Q]]\}}$
• ${\displaystyle [[\mathrm{\forall }x.P]]=\{h|\mathrm{\forall }v.h\in [[P[x:=v]]]\}}$
• ${\displaystyle [[\mathbf{e}\mathbf{m}\mathbf{p}]]=\{u\}}$
• ${\displaystyle [[P\ast Q]]=\{h_1\oplus h_2|h_1\in [[P]]\wedge h_2\in [[Q]]\}}$
• ${\displaystyle [[P-\ast Q]]=\{h|\mathrm{\forall }{h}^{\prime }.h^{\prime }\mathrm{\perp }h\wedge h^{\prime }\in [[P]]\Rightarrow h\oplus h^{\prime }\in [[Q]]\}}$

The rules for${\displaystyle \wedge }$,${\displaystyle \vee }$,${\displaystyle \mathrm{\neg }}$ and${\displaystyle \mathrm{\exists }}$ are omitted but are easily derived from the above, while the semantics of${\displaystyle e\mapsto e^{\prime }}$ are given by the separation algebra in question.

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 aboutprograms with general sharing.

In their POPL'01 paper,^[3] O'Hearn and Ishtiaq explained how the magic wand connective${\displaystyle -\ast }$ could be used to reason in the presence of sharing, at least in principle.For example, in the triple

${\displaystyle \{(x\mapsto -)\ast ((x\mapsto 42)-\ast P)\}[x]=42\{P\}}$

we obtain the weakest precondition for a statement that mutates the heap at location${\displaystyle x}$, 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${\displaystyle -\ast }$ to provide localized reasoning about mutations in the classicSchorr-Waite graph marking algorithm.^[10] Finally, one of the most recent works in this direction is that of Hobor and Villard,^[11] who employ not only${\displaystyle -\ast }$ but also a connective${\displaystyle \cup \ast }$which has variously been called overlapping conjunction or sepish,^[12] and which can be used to describe overlapping data structures:${\displaystyle P\cup \ast Q}$ holds of a heap${\displaystyle h}$ when${\displaystyle P}$ and${\displaystyle Q}$ hold for subheaps${\displaystyle h_P}$ and${\displaystyle h_Q}$ whose union is${\displaystyle h}$, but which possibly have a nonempty portion${\displaystyle h_P\cap h_Q}$ in common. Abstractly,${\displaystyle P\cup \ast Q}$ can be seen to be a version of the fusion connective ofrelevance logic.

A Concurrent Separation Logic (CSL),a version of separation logic for concurrent programs, was originally proposed byPeter O'Hearn,^[13]using a proof rule

${\displaystyle \frac{\{P_1\}{C}_1\{Q_1\}\{P_2\}{C}_2\{Q_2\}}{\{P_1\ast P_2\}{C}_1\parallel C_2\{Q_1\ast Q_2\}}}$

which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach ofTony Hoare to reasoning about concurrency,^[14]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 amemory manager.

Commenting on the early classical work oninterference freedom bySusan Owicki andDavid 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.^[15] 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,^[16] 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;^[17] 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.^[18]

Versions of CSL have been included in many interactive and semi-automatic (or "in-between") 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,^[19] as of yet CSL-style reasoning has been included in comparatively fewtools in the automatic program analysis category (and none mentioned in the next section).

O'Hearn and Brookes are co-recipients of the 2016Gödel Prize for their invention of Concurrent Separation Logic.^[20]

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.^[21]

This may be achieved by annotating each${\displaystyle \mapsto }$ assertion with a fractional permission${\displaystyle \pi \in (0,1]}$ as${\displaystyle e\stackrel{\pi }{\mapsto }{e}^{\prime }}$. Whenπ = 1, the thread has full ownership of the heap cell and therefore may write to it:

${\displaystyle \{x\stackrel{1}{\mapsto }\mathrm{\_}\}[x]:=a\{x\stackrel{1}{\mapsto }a\}}$

Whenπ < 1, the thread only has shared access, and therefore may only read:

${\displaystyle \{x\stackrel{\pi }{\mapsto }v\}a:=[x]\{x\stackrel{\pi }{\mapsto }v\ast a=v\}}$

Importantly, permissions may be infinitely split, allowing an arbitrary number of threads to read from the same location (with the fractional permission keeping track of when the number of threads has reduced to one again):

${\displaystyle x\stackrel{{\pi }_1+{\pi }_2}{\mapsto }v⟺x\stackrel{{\pi }_1}{\mapsto }v\ast x\stackrel{{\pi }_2}{\mapsto }v}$

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 thus${\displaystyle s,h⊢e\stackrel{\pi }{\mapsto }{e}^{\prime }}$ semantically means that in heaph, locatione has valuee' with 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.

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 humanis intimately involved in the proof process. Many such tools have been developed; the following list includes a few representatives in each category.

• Automatic Program Analyses. These tools typically look for restricted classes of bugs (e.g., memory safety errors) or attempt to prove their absence, but fall short of proving full correctness.
  • A current example isFacebook Infer, a static analysis tool for Java, C, andObjective-C based on separation logic and bi-abduction.^[22] As of 2015 hundreds of bugs per month were being found by Infer and fixed by developers before being shipped to Facebook's mobile apps.^[23]
  • Other examples includeSpaceInvader (one of the first SL analyzers),Predator (which has won several verification competitions),MemCAD (which mixes shape and numerical properties) andSLAyer (from Microsoft Research, focussed on data structures found in device drivers).
• Interactive Proof. Proofs have been done using embeddings of Separation Logic into interactive theorem provers such asRocq (previously known asCoq) andHOL (proof assistant). In comparison to the program analysis work, these tools require more in the way of human effort but prove deeper properties, up to functional correctness.
  • A proof of the FSCQ file system^[24] where the specification includes behaviour under crashes as well as normal operation. This work won the best paper award at the 2015 Symposium on Operating System Principles.
  • Verification of a large fragment of theRust type system and some of its standard libraries in theRustBelt project using theIris framework for separation logic in Rocq.
  • Verification of an OpenSSL implementation of a cryptographic authentication algorithm,^[25] utilizingverifiable C
  • Verification of key modules of a commercial OS kernel, the μC/OS-II kernel, the first commercialpre-emptive kernel to have been verified.^[26]
  • Other examples include theYnot^[27] library for the Rocq; theHolfoot embedding of Smallfoot in HOL;Fine-grained Concurrent Separation Logic, andBedrock (a Rocq library for low-level programming).
• In Between. Many tools require more user intervention than program analyses, in that they expect the user to input assertions such as pre/post specs for functions or loop invariants, but after this input is given they attempt to be fully or almost fully automatic; this mode of verification goes back to classic works in the 1970s such as J King's verifier, and the Stanford Pascal Verifier. This style of verifier has recently been calledauto active verification, a term which intends to evoke the way of interacting with a verifier via an assert-check loop, analogous to the interaction between a programmer and a type-checker.
  • The very first Separation Logic verifier,Smallfoot, was in this in-between category. It required the user to input pre/post specs, loop invariants, and resource invariants for locks. It introduced a method of symbolic execution, as well as an automatic way to infer frame axioms. Smallfoot included Concurrent Separation Logic.
  • SmallfootRG is a verifier for a marriage of separation logic and the classic rely/guarantee method for concurrent programs.
  • Heap Hop implements a separation logic for message passing, following the ideas inSingularity (operating system).
  • VeriFast is an advanced current tool in the in-between category. It has demonstrated proofs ranging from object-oriented patterns to highly concurrent algorithms and to systems programs.
  • Viper is a state-of-the-art automated verification infrastructure for permission-based reasoning. It mainly consists of a programming language and two verification backends, one based on symbolic execution and another one on verification condition generation (VCG).^[28] Based on the Viper infrastructure, several frontends for various programming languages have emerged:Gobra for Go,Nagini for Python,Prusti for Rust, andVerCors for C, Java, OpenCL, and OpenMP. These frontends translate the frontend programming language into Viper to then use a Viper verification backend for proving the input program's correctness.
  • TheMezzo Programming Language andAsynchronous Liquid Separation Types include ideas related to CSL in the type system for a programming language. The idea to include separation in a type system has earlier examples inAlias Types andSyntactic Control of Interference.

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, whereVerifast sometimes requires annotations that resemble the tactics (little programs) used in interactive verifiers.

The satisfiability problem for a quantifier-free, multi-sorted fragment of separation logic parameterized over the sorts of locations and data can be shown to bePSPACE-complete.^[29] An algorithm for solving this fragment inDPLL(T)-basedSMT solvers has been integrated intocvc5.^[30] Extending this result, satisfiability for an analog of theBernays–Schönfinkel class for separation logic with uninterpreted memory locations can also be shown to be PSPACE-complete, whereas the problem is undecidable with interpreted memory locations (e.g., integers) or further quantifier alternations^[31]

• 2002 introductions
• Program logic
• Substructural logic

• CS1 errors: periodical ignored
• Articles with short description
• Short description matches Wikidata
• Wikipedia external links cleanup from October 2024