# Comparing Separation Logic vs Dynamic Frames in the context of Frame Problem

In the write-up, we are comparing how [Separation Logic](https://www.cs.cmu.edu/~jcr/seplogic.pdf) (abbreviated as SL) and [Dynamic Frames Theory](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.185.2957&rep=rep1&type=pdf) (abbreviated as DFT) tackle the [frame problem](https://en.wikipedia.org/wiki/Frame_problem). This turned to be a non-trivial, but quite useful exercise, at least, for me.

One problem is that the DFT is not explicit about some of its foundations, so we need to recover details. Another problem is that terminology differs and variable, state, value and address refer to somewhat different notions. Third, underlying logics used to express framing specification are different too.

So, we first clarify the problem, unify terminology and then discuss differences and similarities in tackling the frame problem.

# Frame problem and (absence of) aliasing

The approaches of DFT and SL to tackle the [frame problem](https://en.wikipedia.org/wiki/Frame_problem) are quite similar: one adds necessary annotations (`framing specification`s) and use them to prove absence of aliasing.

However, terminology and details differ significantly. In order to unify approaches, we have developed a simple [model](https://hackmd.io/@ericsson49/model-of-aliasing) of how absence of aliasing can be proved. We will use the model (its terminology and proof principle) to compare the DFT and the SL.

The details are described in a separate [document](https://hackmd.io/@ericsson49/model-of-aliasing). But here is a rough idea of how this works:
- specify a memory `effect` of a `mutator`
- specify a memory `footprint` of a (pure) `expression`
- prove that the `effect` and the `footprint` are `disjoint`
- we now can conclude that the `mutator` has no effect on the `expression`
- thus, the `expression` value can be re-used in the new memory state

# Notes on terminology

There is an inconsistency in how `frame` and `framing` is used in literature, which may confuse a reader. Basically, the idea is to determine a memory region, which can be accessed by a piece of computation (i.e. read, write, allocate of de-allocate). And then state that any access to the rest of (allocated) memory is independent of the computation. So, there are two complimentary regions and `frame` (and `framing`) can be used to refer to both.

That was one of the reason to introduce `footprint` and `effect` instead of `frame`. However, `framing specification` is not confusing, since if one defines a region, then it's complement is implicitly defined too.

## Frame terminology in DFT

The DFT paper seems to use `frame` to refer to a region which is accessed by a piece of computation. For example,
> The modification $\Delta f$ is satisfied by every computation that only touches region `f` or at most allocates new memory.

Here `f` is a `dynamic frame`. In the write-up parlance, `frame` refers to `effect` of a computation here.

Another example is "`f` **frames** `v`" condition:
> In a state $\sigma$ in which this condition is true, we say that `f` **frames** `v` or that `f` is a frame for `v`. When that happens, `v` depends only on locations in `f`, i.e. leaving those locations untouched preserves the value of `v`.

In the write-up parlance, this describes a `footprint` of a variable (which is an expression in the DFT).

However, occasionally the DFT paper uses term `frame` inconsistent with the rest of the paper, e.g.
> When specifying a piece of computation, we should also specify its frame, i.e. the part of the state that it operates upon.

## Other literature

There is also inconsistency of `frame` usage among other texts. For example, the [frame problem](https://en.wikipedia.org/wiki/Frame_problem) wiki page uses `frame` to refer to what is unchanged:
> In the logical context, actions are typically specified by what they change, with the implicit assumption that everything else (the frame) remains unchanged.

Another example is a [Separation Logic
](https://cacm.acm.org/magazines/2019/2/234356-separation-logic/fulltext) article in Communications of the ACM, which also uses `frame` to refer to the untouched memory, e.g. [Figure 3](https://dl.acm.org/cms/attachment/c30ba82f-e1d2-4dd7-8205-ce95f9244d7a/f3.jpg).

[Dafny reference manual](https://dafny-lang.github.io/dafny/DafnyReferenceManual/DafnyRef#framing) uses `framing expressions`:
> Frame expressions are used to denote the set of memory locations that a Dafny program element may read or write.

However, as we noted above regarding `frame specification`s, such use doesn't introduce confusion, since by defining a set, we implicitly define its complement.

# Paradigm

A most prominent difference is that the DFT stems from Object-Oriented [Refinement](https://en.wikipedia.org/wiki/Refinement_(computing)) paradigm, while SL is a low-level imperative paradigm equipped with Hoare triples with assertions about heap.

Thus, it's difficult to compare two approaches directly. They are however complimentary in some sense and can be even combined (e.g. [Implicit Dynamic Frames](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.185.3963&rep=rep1&type=pdf)).

## Refinement

In the context of the frame problem, it directly impacts the form how framing conditions are specified. The DFT supports encapsulation and refinement, which means a specification and its refinements (implementations) are separate entities (called `modules` in DFT). The DFT is more expressive in the sense than vanilla SL.

## Permission Logic

In the semantics of SL's operations, a computation is aborted, if it tries to access an unallocated address. A precondition can contain assertions about heap, which can certify that some locations are allocated. In the sense, SL's preconditions serve as permissions (or capabilities) to access heap locations.
As the assertions about locations are explicit (of the form $addr \mapsto value$), one is able to prove that a code accesses only allocated locations.

## "Global" vs "Local" reasoning

We assume that a program is split in a set of code units. In the DFT that can be methods, functions or expressions, in the SL it's commands `C` of [Hoare-triples](https://en.wikipedia.org/wiki/Hoare_logic) `{P} C {Q}`.

In the DFT, there is a common heap memory for all code units. That means that generally a code unit can affect any other code unit - in the sense, the DFT implies "global" reasoning.

In the SL, a well-specified code (which doesn't lead to `abort` state) should access only the locations of heap, which existence is explicitly stated in its precondition (of the form $a \mapsto b$, i.e. there is a heap cell at address $a$ with content $b$). It thus has the only way to affect other code units: via its effective heap after execution, which is described in its post-condition. Similarly, dependencies (or footprint) of the code are described in its pre-condition. The reasoning is thus "local" as we can concentrate only on the `footprint` and `effect`.

However, such "local" reasoning can be emulated in the DFT too: one can specify for each code unit its footprint and its effect ("`f` **frames** `v`" and "**modifies** `v`" constructs). At the same time, "global" reasoning is more flexible, e.g. one can re-use dynamic frames for several operations or construct a new one from other dynamic frames.

## Pointers and de-allocation

SL supports low-level features, like pointer arithmetics and memory de-allocation, which are absent in the DFT. Explicit heap permissions make it straightforward to prove that a piece of code is well-specified in respect to heap access (i.e. doesn't try to dereference a non-allocated location).

Due to "global" reasoning, it can be more difficult to add pointer arithmetics and de-allocation to the DFT. Basically, when one tries to de-reference an expression, one should prove that it's an allocated address, i.e. $a \in Used$ in the DFT's parlance. When the only way to obtain a location value is to allocate something, then the location value acts as a permission to access it.

It's not so, when one can construct location values using pointer arithmetics or de-allocation is possible. One obviously has to prove that a location points to an allocated address every time a location is accessed. It can be implemented using dynamic frames, but `effect` specifications should be made more expressible, to specify that a code unit can shrink its `footprint`.

# Underlying logical foundation

Besides different paradigms, there are differences in type systems, memory models and underlying logics, which are used to express statements about computations and prove them. Some differences are minor (and perhaps introduced to simplify the narrative), while others are more significant.

## State/memory model

Memory model differ rather significantly among the DFT and SL. However, most of the differences stem from the paradigmatic differences and their intended usages: it looks like the SL is simplified to make it easier to reason about its properties.
A more practical version of SL will likely make its type system more expressive (which is also discussed in the SL paper).

As discussed out, it's perhaps difficult to introduce de-allocation in the DFT. However, as it stems from Object-Oriented paradigm, which typically assumes garbage collection, it doesn't seem to be a severe restriction.

### Addresses and Locations

Both DFT and SL assume an infinite set of memory locations (SL uses `address` where DFT uses `location`), however, sets of used or allocated locations are finite. Actually, an `address` in (a flavor of) SL is an infinite integer, which allows using pointer arithmetics in SL, while `locations` are unordered in DFT.

### Values

Locations are mapped to `value`s in both cases. However, `value`s in SL are very simple compared to `value`s in DFT, i.e. they are just infinite integers. Whereas in DFT, `value`s include at least integers, locations and sets.

The difference is not significant, as there can be (and are) flavors of SL with richer type systems (it's discussed in the SL paper too). It's likely that the type system in the SL paper is simplified to make it easier to reasoning about SL properties.

### Computational state

Memory model is more uniform in DFT: a `state` is a finite mapping from `location`s into `value`s. Whereas is SL, state consists of `store` and `heap`. The latter is a finite mapping from `address`es to `value`s, i.e. the same concept as the `state` in DFT. The former is a finite mapping from `variable`s to `value`s.

De-allocation of heap locations is possible in SL, while it's absent in DFT.

### Variables

Variables in SL are quite distinct from variables in DFT. Actually, DFT uses `specification variable` which is an expression, depending on the `state` (corresponds to a pure function with `state` as a parameter).
DFT also defines a `program variable`, which is a special case of `specification variable`, the values of the `program variable` being the content of the `state` at the constant address of the variable.

A `variable` in SL corresponds to a `program variable` in DFT, however, it's kept in a `store` and is not subject to aliasing, as they are not addressable. SL uses variables from its predicate calculus as a rough analogue of DFT's `specification variable`s.

#### Expressions in SL

Expressions in SL don't depend on `heap`, only on `store`. However, as mentioned before, in SL there are explicit assertions about `heap` of form $a \mapsto b$. And if one wants to safely read a location, it's existence should be stated in a pre-condition. Thus, possibility to access `heap` in expressions is not really required, at least in case of pre-conditions.
In other cases, one can add a read operation, e.g.

{ ... } cmds; tmp = [a] { E(.., tmp, ..) }

## Underlying logic

### Framing specifications

Both DFT and SL allows expressing `framing specification`s, however, their underlying logics are quite different.

The logic in DFT is sets-based. A `dynamic frame` in DFT is a kind of `specification variable`, which value is a set of allocated locations. A `dynamic frame` can be constructed using set comprehensions and set operations. There seems to be two main `framing specification`s in DFT:
- **modifies** `f` - a computation preserves allocated locations other than `f` (`effect`)
- `f` **frames** v - variable `v` is framed by `f`, in the sense that preserving `f` preserves the value of `v` (`footprint`)

SL employs "inductive definition of predicates on abstract data structures", i.e. a form of [inductive types](https://en.wikipedia.org/wiki/Inductive_type) (though there are intuitionistic and classic SL flavors) together with `separating conjunction` $P * Q$, which are used to specify pre- and post-conditions for a computation. Such pre- and post-conditions explicitly split the entire `heap` in disjoint rejoins down to singleton (cell) and empty heaps.

### Disjointness

DFT uses explicit `disjointness` predicate, which can be assumed, asserted and/or proved. In SL, heap assertions are constructed in "disjoint-less" manner. Of course, there still arise proof conditions, i.e. if one states $a \mapsto b * c \mapsto e$, heap fragment disjointness implies $a \neq c$, $a$ and $c$ are addresses of heap cells.

# Framing

Here we illustrate how DFT and SL approach the frame problem. The key problem is to be able to prove that an update of a location preserves content of another syntactically different location, e.g. $a \mapsto b$ in the SL case. Then, if there are several such facts involved in consequent reasoning, one need to construct such proofs for all of them. See [A model to prove absence of aliasing](https://hackmd.io/@ericsson49/model-of-aliasing) for details.

## Framing in DFT

Let's assume there is a spec variable `a` and we want to prove that a modification of a program variable `b` doesn't affect `a` and we can reuse its value in the new state after update.

One can specify a `dynamic frame` `f` for `a`: "`f` **frames** `a`". One also specifies that the effect of the update to `b`: " b = x **modifies** g". If there is an evidence that "**disjoint**[f;g]", one can concude that `a` and `b` are independent, i.e.
$\mathbf {disjoint}[f;g] \land \mathbf {modifies}\, g \land f\, \mathbf {frames}\, a \Rightarrow a' = a$.

In the simple case, when `a` or `b` are program variables, corresponding dynamic frames comprise addresses of them, i.e. $f = \{addr\_a\}$ and $g = \{addr\_b\}$. In the case of a complex type, its dynamic frame can be constructed from dynamic frames of components, since a dynamic frame is a particular case of a specification variable.

## Framing in SL

Let's assume, there is a Hoare-tuple {P} C {Q} and we want to append a write: `{ b -> _ } [b] = x { b -> x}`. `Q` may contain facts about heap, which can be invalidated by such write.

Actually, in SL we do not necessary to prove absence of aliasing explicitly, one just needs to construct a new post-condition for the combined program. This includes both aliasing and non-aliasing cases. In the latter we want to prove we can simply include `Q` in the new post-condition, while in the former, we want an updated version of it.

let's assume that a predicate `allocated(b, Q)` means that assertion `Q` contains a singleton assertion ${b' \mapsto bv}, s.t. {b = b'}$. And `!allocated(b, Q)` means there is no such singleton.

## Aliasing

If there is aliasing that means `alloc(b, Q)`, so there is $b' \mapsto bv$ for some $b'$ and $b = b'$. We can thus construct new `Q'` by substituting $b' \mapsto bv$ with $b' \mapsto x$.

## No aliasing

That means `!alloc(b, Q)`. We want to apply the SL's frame rule. Let's check whether `b` was allocated in `P`.

### allocated(b, P)

In that case `C` deallocates the location `b`, which means `C; [b] = x` is not well-specified (i.e. will abort).

### !allocated(b, P)

We now want to apply frame rule. But we need check that the `C` doesn't modifies `b`. If it does, there is obviously a conflict in how two pieces treat `b` and we need to resolve it with appropriate renaming.

When resolved, $b \notin mod(C)$. Thus, we can apply the frame rule to both pieces: `{ P * b -> _ } C { Q * b -> _ }` and `{ Q * b -> _ } [b] = x { Q * b -> x }`. We can construct a Hoare-triple for our resulting piece of code: `{ P * b -> - } C; [b] = x { Q * b -> x }`