# A model to prove absence of aliasing

In the context of formal reasoning about imperative programs, one often faces [frame problem](https://en.wikipedia.org/wiki/Frame_problem). However, literature, addressing the problem that we have read, lacks simple and concise intuition of how the problem is solved.

In particular, while comparing two papers, [Dynamic Frames](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.185.2957&rep=rep1&type=pdf) and [Separation Logic](https://www.cs.cmu.edu/~jcr/seplogic.pdf), it becomes clear the papers use varying terminology. While their approaches look rather similar, it was not evident how their actually can be compared.

We address the problems by developing a simple unified model, which solves the framing problem (in the context of formal reasoning about imperative programs). We intend to use the model to compare approaches of Dynamic Frames and of Separation Logic. Hopefully, it will also serve as a relatively simple description of how the frame problem can be tackled.

The write-up is also a follow up to [Why pure functional form matters](https://hackmd.io/8UosBtxfQc6kzj94mWUSpg), which discusses an approach to avoid "dangerous" aliasing (less expressive obviously).

# Frame problem

We are starting from the following understanding of the frame problem (from [Frame problem's wiki page](https://en.wikipedia.org/wiki/Frame_problem)):
> The frame problem is that specifying only which conditions are changed by the actions does not entail that all other conditions are not changed. This problem can be solved by adding the so-called “frame axioms”, which explicitly specify that all conditions not affected by actions are not changed while executing that action.

In the case of imperative programs, one typically uses different terminology. We assume that there is a `memory`, which can be affected by actions. An action corresponds to a modification of the `memory`. Finally, a condition corresponds to an expression, which value depends on the `memory` contents.

## Aliasing

Depending on programing language semantics, it sometimes can be quite easy to determine, which expressions are affected by a particular memory update. For example, it can be the case that two different syntactic names imply that they reference disjoint memory locations. So, if a variable `a` is modified, only expressions depending on `a` are affected.

However, practical languages are more expressive and two syntactically different names may reference two overlapping locations. The situation is called [aliasing](https://en.wikipedia.org/wiki/Aliasing_(computing)).

For example, a reference to a location can be copied to another variable:

a = new A
b = a

`a` and `b` refer to the same location after the program is executed.

Another typical case is arrays:
- `a[i]` is an alias to `a[j]`, if `i == j`
- `a[i]` and `b[j]` can share memory locations, if there is an aliasing between `a` and `b`

## Aliasing and formal reasoning

In presence of aliasing, reasoning about imperative programs can become complicated or even impossible without additional assumptions (so called "frame axioms").

For example, there are two variables: `a` and `b`, and there is some fact about `a`. After some statement modifies `b`, can we still assume that the fact is sill valid? In presence of aliasing, we cannot, as `a` and `b` can share memory locations.

This was a "write-after-read" example: a write following a read can invalidate the value just read (and stored somewhere, e.g. in a register or in a fact store).

One can imagine a "write-after-write" example. However, memory semantics typically mean that once we wrote to a location, a consequent read of it will return the value written. So, in semantic sense, there is an implicit read. Thus, it's typically enough to consider the "write-after-read" case only.

### Split case reasoning

One way to deal with the problem is to consider two cases: there is aliasing between `a` and `b`, and there is no aliasing. In the latter case, one can re-use the fact about `a`, while in the former case, one has to prove a new version of the fact (based on the effect that the update of `b` caused on `a`). Obviously, when there are many variables, facts and updates, such split case reasoning can become very complicated.

### Absence of aliasing

A more promising way is to make sure there is no aliasing. One typically needs to introduce frame axioms. Then one can prove absence of aliasing between variables of interest. There are two important cases:
- restricting language semantics, to prevent aliasing (e.g. in certain cases)
- introducing necessary framing pre-conditions

Of course, a caller of such preconditioned code need to prove that the precondition holds before invocation (this is also true in the case of restricting language semantics: e.g. one may need to reject programs violating restrictions). To be able to do that, one may also need necessary framing post-conditions.

Restricted language semantics is a quite popular way, as it's typically much easier to implement (especially, when dealing with low level languages, like C, where there are plenty of ways to introduce aliasing), and easier to use (less annotation and prove burden). However, it can rule out many interesting implementations.

In the write up, we follow the harder route of specifying and proving absence of dependencies between memory accesses.

### Proving absence of aliasing

Here is a rough idea of how such proof can be preformed.
First, an effect of a memory mutator is specified. Second, a memory footprint of an expression is specified. If the effect and the footprint are disjoint, i.e. consist of different memory locations, one can conclude that the mutator has no effect on the expression. And thus, the expression can be re-used in the new memory state, which occurs after the mutation is performed.
There can be other specification and proving activity, which is discussed further.

# Model to prove absence of aliasing

Without loss of generality, we assume that one need to prove absence of aliasing between two references (to memory), and at least one of them is used to modify the memory.

**NB** We use `reference` instead of `variable`, as the latter notion differ between the DF and SL papers.

## Memory model

There is an infinite set of memory `location`s. A `state` is a finite mapping from `location`s to `value`s. A `location` in the domain of the `state` is called allocated (in the `state`).
Typically, a `location` is a `value` and can be dereferenced (and stored in memory), then we refer to it as an `address`.

`Value`s can be composite (e.g. tuples, records, etc), however, we assume that they are immutable.

**NB** A memory can be non-addressable, i.e. there is no dereference operation on address-valued expressions. One can still access locations of such memory, though aliasing is not possible as any access to the same location looks the same way. Such memory can still be useful to describe parts of a mixed memory model, like store + heap in the SL paper. Another example is stack variables in a language like Java or registers in an assembly language.

Apart from operations to read from and write to a `location` (either directly or via dereferencing), there can be allocation and (optional) de-allocation operations. An allocation is performed from a set of non-allocated locations, and de-allocation is a reverse procedure.

## Framing specifications

A `framing specification` describes how a mutator or an expression is related to memory locations. There are two aspects od such specifications:
- a memory `effect` of a mutator (allocation, modification or de-allocation)
- a memory `footprint` of a (pure) expression - memory locations that its value depends on

The specifications need not be exact, i.e. an upper bound can be specified in practice.

Both `effect` and `footprint` refer to an allocated memory region (sets of allocated locations).

**NB** While we use term `set` here, in practice one need a way to reason about regions and construct them. This is straightforward, when a logic has built-in sets. For example, it's the case for the DF theory. However, the SL paper uses inductively defined predicates (over algebraic data structure), which is an alternative to sets.

An informal meaning of the `effect` is that if an allocated location doesn't belong to the `effect` than its content is not affected by the mutator. An informal meaning of the `footprint` is that if no location from the `footprint` has been modified, then the expression value has not changed.

In simple cases, one doesn't need to specify a `footprint` or an `effect` explicitly. However, a variable's value can be an object, which consists of many memory locations, some of them can be hidden. For example, it's the case in the DF theory, which supports object oriented and refinement features.

Actual `framing specification`s can combine `footprint` and `effect` in one statement. For example, "m **reads** a" may mean that method `m` can read `a` (footprint) and it doesn't modify the heap (effect). Similarly, "m **modifies** a" may mean that method `m` can read/modify `a`. However, we ignore them in our model.

## Programming language assumptions

For convenience, computational state can be split in an addressable and a non-addressable parts. The former is usually called `heap`, while latter can be called `store` (e.g. in the SL paper) or `stack` or `registers`. Though, stack in C *is* addressable, so it's an unsafe term.

Without loss of generality, we assume that each imperative (i.e. impure) statement consists of several pure expressions (which can read memory) and one mutator. So, it has both `footprint` and `effect`.

It's likely that a logic used to prove correctness of a program, follows the [Hoare-style](https://en.wikipedia.org/wiki/Hoare_logic), like the SL. Or inspired from it, like [Refinement calculus](https://en.wikipedia.org/wiki/Refinement_(computing)#Refinement_calculus). A `footprint` of a statement can be seen as a part of its precondition. Indeed, if a statement reads a memory location, which is not allocated, then such program is not "well-specified" and should be either rejected or aborted (though returning some default value is an option too). Similarly, an `effect` can be a part of its post-condition.

## Disjointness

One may also need a `disjointness` statement, to prove that an `effect` and a `footprint` regions are disjoint.

There can be an explicit `disjoint` predicate, as in the DF theory, while SL employs `separating conjunction` $P * Q$. The SL's frame rule also uses a precondition that a computation's `effect` on `store` variables is disjoint with the set of free `store` variables of the frame.

## Proof activity

We now describe sketches of proof activity. Concrete details can vary depending on programming language semantics and underlying logic/theories.

### Absence of aliasing

Now, there are all ingredients (to attempt) to construct a proof of absence of aliasing. Let's assume there is an imperative statement and a (pure) expression about some memory region.
We also assume that both the statement and the expression reference syntactically different memory regions, which can alias though.

After execution of the statement, the memory `state` will become different, so if one re-evaluate the expression, its value may change. Therefore, one cannot use it as a fact in the new state.

Our goal is to be able to prove absence of aliasing, so that the expression can be re-used, when it's required. Else one has to derive the value of the expression in the new state, which can be costly (especially, if there are many such expressions).

In our model, it's sufficient to prove that the `effect` of the statement is disjoint with the `footprint` of the expression. Indeed, if the `footprint` is disjoint with the `effect` then content of every `footprint`'s location is not changed by the statement. Thus, the expression value has not changed in the new state.

### Framing specification proofs

One may also need to prove that a program or an expression obeys their `framing specification`s, i.e. that a statement doesn't modify already allocated locations beyond its `effect` (it may modify freshly allocated locations). And that an expression doesn't read memory beyond its `footprint`.

#### Permission logics

Programming language semantics may require aborting a program execution, when it dereferences or de-allocates an unallocated memory location. This is the case for the SL. In such case, an assertion about heap in a precondition can certify that memory locations are allocated. So, such assertion acts as a permission to access the locations. Such logics are sometimes called permission logics.

In order to avoid implementing the aborting semantics in runtime, one may need to prove that a statement or an expression access only locations, for which there exist permissions in their pre-conditions.

### Auxiliary proofs

There, of course, may be required more or less traditional proofs, like proving that a pre-condition of a statement is fulfilled, proving that sets/regions are disjoint or proving that two address-valued expressions are equivalent.

# Composite memory models

One can combine several kinds of addressable and non-addressable memories, which can have different location/address and value types. Memory states can be stored in memory too, as states are values.
We assume that all memory kinds are disjoint, i.e. pairwise intersections of their sets of locations are all empty.

Combined with dereferencing operations that becomes a quite expressive framework to express various memory models and control aliasing. Here are some simple examples.

## Dynamic Frames' memory model

In the [Dynamic Frames](https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.185.2957&rep=rep1&type=pdf), there is only one kind of memory. Locations can be dereferenced. Values are not specified precisely, however, they at least contain integers, locations and sets. De-allocation is not mentioned.

## Separation Logic

In Separation Logic (as described in the [paper](https://www.cs.cmu.edu/~jcr/seplogic.pdf)), there are two kinds of memory: Store and Heap.
Store is non-addressable, it's a mapping from variables to values. Heap is addressable, it's a mapping from addresses to values.
There are several flavors of SL logic and its memory model. In a simple variant, values are infinite integers and addresses are a subset of integers. Of course, one can introduce more expressible type system (which is also discussed in the paper).
Integer addresses together with dereference operations allow pointer arithmetics. There is also a de-allocation operation.

## Strict aliasing rule

A simple approach to restrict aliasing is to forbid aliasing between references of fundamentally different types (e.g. [strict aliasing rule in C/C++](https://en.wikipedia.org/wiki/Pointer_aliasing#Aliasing_and_re-ordering)). In Java, references to objects of incompatible types cannot alias too. Such memory model is employed in formal verification too (e.g. see [Frama-C/WP, section 3.6](http://frama-c.com/download/frama-c-wp-manual.pdf)).

## Modeling mutable data structures

Values are immutable in our model. However, memory states (i.e. mappings from locations to values) are immutable and can be stored in memory. We thus can model mutability by introducing a dedicated memory kind for a data structure and store its states in memory, since a memory state is an immutable value.
A location of a (mutable) data structure and a location of its state are thus distinct notions and we can keep them in different memory kinds. In order to associate the data structure's location with its state's location, we can introduce handles, which is a value, containing a pointer to a data state (and perhaps some additional information like tags).
For example, a data structure update `a.f = b` can look something like this:

handle = *addr_a
currState = *handle // handle is a pointer to state in the example
newState = currState.copy(f = b)
*handle = newState

This is a somewhat verbose example, to illustrate using of dereferencing (i.e. `*` operation) and handles. The `o.copy(f = b)` creates a new copy of `o` value, where field `f` is replaced with value `b`.

A more concise version can look like (for a variable in an addressable heap):

*a = (*a).copy(f = b)

Or just (for a variable in a non-addressable store):

a = a.copy(f = b)

## Java-like memory model

Since we can model mutable data structures, we can express a Java-like memory model too. E.g. one can introduce two kinds of stores for each class to hold states of static fields and object fields. And stores to hold states of arrays. There also should be stores to keep states of stack frames of methods.