Frame problems and frame properties

One of the ideas that has been important to me as I’ve worked on LVars is the notion of a frame property. A frame property captures the idea of local reasoning about programs that alter state. Written as an inference rule (where the truth of the stuff above the line allows us to infer the truth of the stuff below), it might look something like this frame rule, due to O’Hearn, Reynolds, and Yang from their work on separation logic:

\[ \frac{\lbrace p \rbrace~C~\lbrace q \rbrace}{\lbrace p * r \rbrace~C~\lbrace q * r \rbrace} \]

Here, $C$ is a program, and $\lbrace p \rbrace ~ C ~ \lbrace q \rbrace$ is a Hoare triple (in the style of Hoare logic) specifying the behavior of $C$: it says that if the assertion $p$ is true before $C$ runs, then the assertion $q$ will be true afterwards. For example, $p$ and $q$ might respectively describe the state of the heap before and after a heap location is updated by $C$. More generally, $p$ and $q$ could be assertions about any resources that $C$ uses as it runs.

Suppose we have a program $C$ that runs starting from a state satisfying $p$ and and ends in a state satisfying $q$. Then, the frame rule tells us that running $C$ starting from a state satisfying the assertion $p * r$ will result in a state satisfying the assertion $q * r$. These last two assertions use the separating conjunction connective $*$, which combines two assertions that can be satisfied in a non-overlapping manner. For instance, the assertion $p * r$ is satisfied by a heap if the heap can be split into two non-overlapping parts satisfying $p$ and $r$, respectively.

So, what does all this mean? It means that, if $C$ can run starting from a state satisfying $p$ and end in a state satisfying $q$, then it does not do any harm to also have the disjoint property $r$ be true when $C$ runs: the truth of $r$ will not interfere with the execution of $C$. Furthermore, if $r$ is true to begin with, running $C$ will not interfere with the truth of $r$. We can think of the resources (such as heap locations) actually used by $C$ as the “footprint” of $C$, and so $r$ is an assertion about resources outside of that footprint.

When I first encountered separation logic and the frame rule several years ago, I didn’t really understand what was so interesting about it. If a program doesn’t use a piece of the heap, then of course running the program won’t change that piece of the heap! It wasn’t until the last couple of years that I realized that the power of the frame rule is that it cuts both ways: not only will the running of the program not interfere with the piece of the heap in question, but that piece of the heap will also not interfere with the running of the program! To me, this is a very powerful principle of modularity: all kinds of other stuff may be going on, say, elsewhere in the heap, but $C$ can just do its thing, blissfully oblivious to all that. To me, that’s the essence of what’s meant by “local reasoning”.

The frame problem

The frame rule gets its name from the fact that $r$ is a sort of “frame” around $C$: everything that is not explicitly changed by $C$ is part of the frame and is inviolate. To my knowledge, the “frame” terminology was originally introduced in 1969 by McCarthy and Hayes, in their paper “Some Philosophical Problems from the Standpoint of Artificial Intelligence”. They observed that specifying only what is changed by an action does not generally allow an intelligent agent to conclude that nothing else is changed. They give a (charmingly dated) example:

[…] in proving that one person could get into conversation with another, we were obliged to add the hypothesis that if a person has a telephone he still has it after looking up a number in the telephone book. If we had a number of actions to be performed in sequence we would have quite a number of conditions to write down that certain actions do not change the values of certain fluents. In fact with $n$ actions and $m$ fluents we might have to write down $mn$ such conditions. […]

They called this dilemma the frame problem. Peter O’Hearn has a nice characterization of it, too: “when specifying what changes, an inordinate amount of effort usually needs to be spent saying what doesn’t change.” So, in a formal system, one solution to the frame problem is to add a rule like the frame rule.

Fictional separation

In the setting of LVars, we can establish a frame property that captures the idea that independent effects commute with each other. Consider an expression $e$ that runs starting in store $S$ and steps to the expression $e’$, updating the store to $S’$. Our frame property, which we call the “Independence” property, provides a double-edged guarantee about what will happen if we evaluate $e$ starting from a larger store $S \sqcup R$, where $\sqcup$ is the least upper bound operation and $R$ is some other store that we are “framing on” to $S$. If we run $e$ starting from $S \sqcup R$, then $e$ will update the store to $S’ \sqcup R$, and we also know that that $e$ will step to $e’$ as it did before. Intuitively, the “frame” store $R$ is a store resulting from some other independently-running computation.¹

What’s interesting about the Independence property is that we don’t actually need $S$ and $R$ (or $S’$ and $R$) to be disjoint — we’re combining them with $\sqcup$, not with $*$. If they did have to be disjoint, then that would be unfortunate indeed — it would mean that concurrent operations would only be okay as long as they didn’t touch the same parts of the store. In some settings, those are in fact the only kinds of concurrent operations that are allowed. But the whole point of LVars is that this kind of total disjointness is unnecessary, since updates commute! Instead, we can behave as though $S$ and $R$ are disjoint, even though they might not be. We can reason locally, regardless of what is actually going on under the hood.

It’s common to want to allow this kind of “physical” overlap between resources, while retaining “logical” or “fictional” separation. Jensen and Birkedal’s recent work on fictional separation logic explores the notion of fictional separation in detail, generalizing traditional separation logic to allow much more sophisticated kinds of sharing. An even more recent contribution is the “Views” framework, which brings the notion of fictional separation to a concurrent setting. The Views framework is a metatheory of concurrent reasoning principles that generalizes a variety of concurrent program logics and type systems, including concurrent separation logic. It provides a generalized frame rule, which is parameterized by a function $f$ that is applied to the pre- and post-conditions in the conclusion of the rule:

\[ \frac{\lbrace p \rbrace ~ C ~ \lbrace q \rbrace}{\lbrace f(p) \rbrace ~ C ~ \lbrace f(q) \rbrace} \]

In this formulation of the rule, we can’t point concretely to the “footprint” and the “frame” as distinct from one another; rather, the “frame” is an abstract piece of knowledge that is not violated by the execution of $C$.

In fact, in my dissertation, there’s a more general version of the above Independence property that ends up looking a lot like the generalized frame rule from the Views framework! We need to do this because we generalize from allowing only least-upper-bound writes (which take the least upper bound of the value being written to a data structure and that already in the data structure) to allowing arbitrary “update operations”, which have to be commutative and inflationary, but don’t necessarily have to compute a least upper bound. In the presence of these arbitrary update operations, the original Independence property actually no longer holds — but we can prove another property, which we call Generalized Independence, which is based on the idea of a “store update operation” that’s analogous to the function $f$ in the generalized frame rule above. For more details, take a look at my most recent dissertation draft!