Separation logic

Separation logic is a novel kind of mathematical logic which facilitates reasoning about mutations to computer memory. It enables scalability by breaking reasoning into chunks corresponding to local operations on memory, and then composing the reasoning chunks together.

Separation logic is based on a logical connective \( * \) called the separating conjunction and pronounced “and separately”. Separation logic formulae are interpreted over program allocated heaps. The logical formula \( A*B \) holds of a piece of program heap (a heaplet) when it can be divided into two sub-heaplets described by \(A\) and \(B\). For example, the formula

\(x \mapsto y * y \mapsto x \)

can be read “\(x\) points to \(y\) and separately \(y\) points to \(x\)”. This formula describes precisely two allocated memory cells. The first cell is allocated at the address denoted by the pointer \(x\) and the content of this cell is the value of \(y\). The second cell is allocated at the address denoted by the pointer \(y\) and the content of this second cell is the value of \(x\). Crucially, we know that there are precisely two cells because \( * \) stipulates that they are separated and therefore the cells are allocated in two different parts of memory. In other words, \( * \) says that \(x\) and \(y\) do not hold the same value (i.e., these pointers are not aliased). The heaplet partitioning defined by the formula above can visualized like so:

static/images/SepSplit.jpg

The important thing about separating conjunction is the way that it fits together with mutation to computer memory; reasoning about program commands tends to work by updating \(*\)-conjuncts in-place, mimicking the operational in-place update of RAM.

Separation logic uses Hoare triples of the form \( \lbrace pre \rbrace prog \lbrace post \rbrace \) where \(pre\) is the precondition, \(prog\) a program part, and \(post\) the postcondition. Triples are abstract specifications of the behavior of the program. For example, we could take

\( \lbrace r \mapsto open\rbrace \, closeResource(r)\, \lbrace r \mapsto closed\rbrace \;\;\; (spec)\)

as a specification for a method which closes a resource given to it as a parameter.

Now, suppose we have two resources \( r_1 \) and \( r_2 \), described by \(r_1 \mapsto open * r_2 \mapsto open\) and we close the first of them. We think operationally in terms of updating the memory in place, leaving \(r_2 \mapsto open\) alone, as described by this triple:

\( \lbrace r_1 \mapsto open * r_2 \mapsto open\rbrace closeResource(r_1) \lbrace r_1 \mapsto closed * r_2 \mapsto open \rbrace \;\;\; (use)\)

What we have here is the that specification (spec) described how \(closeResource()\) works by mentioning only one piece of state, what is sometimes called a small specification, and in (use) we use that specification to update a larger precondition in place.

This is an instance of a general pattern. There is a rule that lets you go from smaller to bigger specifications

\( \frac{\lbrace pre \rbrace prog \lbrace post \rbrace}{\lbrace pre * frame \rbrace prog \lbrace post * frame \rbrace}\)

Our passage from (spec) to (use) is obtained by taking

  • \(pre\) to be \(r_1 \mapsto open\)
  • \(post\) to be \(r_1 \mapsto closed \), and
  • \(frame\) to be \(r_2 \mapsto open \)

This rule is called the frame rule of separation logic. It is named after the frame problem, a classic problem in artificial intelligence. Generally, the \(frame\) describes state that remains unchanged; the terminology comes from the analogy of a background scene in an animation as unchanging while the objects and characters within the scene change.

The frame rule is the key to the principle of local reasoning in separation logic: reasoning and specifications should concentrate on the resources that a program accesses (the footprint), without mentioning what doesn’t change.

Bi-abduction

Bi-abduction is a form of logical inference for separation logic which automates the key ideas about local reasoning.

Usually, logic works with validity or entailment statements like

\( A \vdash B \)

which says that \(A\) implies \(B\). Infer uses an extension of this inference question in an internal theorem prover while it runs over program statements. Infer’s question

\( A * ?antiframe \vdash B * ?frame \)

is called bi-abduction. The problem here is for the theorem prover to discover a pair of frame and antiframe formulae that make the entailment statement valid.

Global analyses of large programs are normally computational untractable. However, bi-abduction allows to break the large analysis of a large program in small independent analyses of its procedures. This gives Infer the ability to scale independently of the size of the analyzed code. Moreover, by breaking the analysis in small independent parts, when the full program is analyzed again because of a code change the analysis results of the unchanged part of the code can be reused and only the code change needs to be re-analyzed. This process is called incremental analysis and it is very powerful when integrating a static analysis tool like infer in a development environment.

In order to be able to decompose a global analysis in small independent analyses, let’s first consider how a function call is analyzed in separation logic. Assume we have the following spec for a function \( f() \):

\( \lbrace pre_f \rbrace \;\; f() \;\; \lbrace post_f \rbrace \)

and by analyzing the caller function, we compute that before the call of \( f \), the formula \( CallingState \) hold. Then to utilize the specification of \( f \) the following implication must holds:

\( CallingState \vdash pre_f \;\;\;\;\;\;\;\;\;\;\;\; (Function Call)\)

Given that, bi-abduction is used at procedure call sites for two reasons: to discover missing state that is needed for the above implication to hold and allow the analysis to proceed (the antiframe) as well as state that the procedure leaves unchanged (the frame).

To see how this works suppose we have some bare code

\( closeResource(r1); \, closeResource(r2) \)

but no overall specification; we are going to describe how to discover a pre/post spec for it. Considering the first statement and the (spec) above, the human might say: if only we had \(r1 \mapsto open\) in the precondition then we could proceed. Technically, we ask a bi-abduction question

\( emp * ?antiframe \vdash r1 \mapsto open * ?frame \)

and we can fill this in easily by picking \(antiframe = r1 \mapsto open\) and \(frame = emp\), where emp means the empty state. The emp is recording that at the start we presume nothing. So we obtain the trivially true implication:

\( emp * r1 \mapsto open \vdash r1 \mapsto open * emp \)

which, by applying logical rules, can be re-written equivalently to:

\( r1 \mapsto open \vdash r1 \mapsto open \)

Notice that this satisfy the (Function Call) requirement to correctly make the call. So let’s add that information in the pre, and while we are at it record the information in the post of the first statement that comes from (spec).

\( \lbrace r1 \mapsto open \rbrace \) \( closeResource(r1) \) \( \lbrace r1 \mapsto closed \rbrace \) \( closeResource(r2) \)

Now, let’s move to the second statement. Its precondition \(r1 \mapsto closed\) in the partial symbolic execution trace just given does not have the information needed by \(closeResource(r2)\), so we can fill that in and continue by putting \(r2 \mapsto open\) in the pre. While we are at it we can thread this assertion back to the beginning.

\( \lbrace r1 \mapsto open * r2 \mapsto open \rbrace \) \( closeResource(r1) \) \( \lbrace r1 \mapsto closed * r2 \mapsto open\rbrace \) \( closeResource(r2) \)

This information on what to thread backwards can be obtained as the antiframe part of the bi-abduction question

\( r1 \mapsto closed * ?antiframe \vdash r2 \mapsto open * ?frame \)

where the solution picks \(antiframe = r2 \mapsto open\) and \(frame = r1 \mapsto closed\). Note that the antiframe is precisely the information missing from the precondition in order for \(closeResource(r2)\) to proceed. On the other hand, the frame \(r1 \mapsto closed\) is the portion of state not changed by \(closeResource(r2)\); we can thread that through to the overall postconditon (as justified by the frame rule), giving us

\( \lbrace r1 \mapsto open * r2 \mapsto open \rbrace \) \( closeResource(r1) \) \( \lbrace r1 \mapsto closed * r2 \mapsto open\rbrace \) \( closeResource(r2) \) \( \lbrace r1 \mapsto closed * r2 \mapsto closed \rbrace\)

Thus, we have obtained a pre and post for this code by symbolically executing it, using bi-abduction to discover preconditions (abduction of antiframes) as well as untouched portions of memory (frames) as we go along.

In general, bi-abduction provides a way to infer a pre/post specs from bare code, as long as we know specs for the primitives at the base level of the code. The human does not need to write preconditions and postconditions for all the procedures, which is the key to having a high level of automation. This is the basis for how Infer works, why it can scale, and how it can analyze code changes incrementally.

Context: The logical terminology we have been using here comes from AI and philosophy of science. Abductive inference was introduced by the philosopher Charles Peirce, and described as the mechanism underpinning hypothesis formation (or, guessing what might be true about the world), the most creative part of the scientific process. Abduction and the frame problem have both attracted significant attention in AI. Infer uses an automated form of abduction to generate preconditions describing the memory that a program touches (the antiframe part above), and frame inference to discover what isn’t touched. Infer then uses deductive reasoning to calculate a formula describing the effect of a program, starting from the preconditions. In a sense, Infer approaches automated reasoning about programs by mimicking what a human might do when trying to understand a program: it abduces what the program needs, and deduces conclusions of that. It is when the reasoning goes wrong that Infer reports a potential bug.

This description is by necessity simplified compared to what Infer actually does. More technical information can be found in the following papers. The descriptions in the papers are precise, but still simplified; there are many engineering decisions not recorded there. Finally, beyond the papers, you can read the source code if you wish!

Technical papers

The following papers contain some of the technical background on Infer and information on how it is used inside Facebook.

Edit on GitHub