Models of Storage

It is a fact that the modelling of store (aka memory) in programming languages is surprisingly difficult.

The history of such models, as well as the state of the art up to the year 2000, are beautifully summarized in Tennent and Ghica 2000.

Styles of models

Pre-history

The earliest models of a store belong to John McCarthy. We read in Tennent and Ghica 2000:

The state of the art in semantic modeling of storage operations before Strachey can be seen in two papers by John McCarthy 23, 24. Commands in simple imperative languages are modeled as transformations of “state vectors” which are intended to record, among other things, the current values of all program variables. Operations for accessing and updating the current value of any variable are axiomatized.

This is of course sufficient to model global variables.

It should be noted that McCarthy's papers of that time simply plaster over recursion, ignoring the problem. However, modified models of this sort (with a little bit of domain theory to deal with recursion) are often taught in old-fashioned courses on program semantics (e.g. in the 1992 book by Nielson and Nielson).

The next models of stores are due to Christopher Strachey. This work introduced notions such as L- and R-values, storable values, and the higher-order store. This early work is beautifully surveyed in Tennent and Ghica 2000.

The main problem with these early approaches is that they cannot model any sort of allocation. For example, in any language able to create new storage cells, the program equivalence

  \textbf{new } x \textbf{ in } C \simeq C

is true operationally, but false in the model. Thus, such models are not fully abstract.

Possible worlds

In the early 1980s John Reynolds and Frank Oles developed an approach to modelling allocation through possible worlds.

Here, the possible worlds w \in \mathcal{W} are all the shapes the memory can have. The accessibility relation w \sqsubseteq w' tells us when the world w' is reachable from the world w through a series of allocations.

Categorically, these models can be thought of as functors from the frame (\mathcal{W}, \sqsubseteq) to either sets or (pre)domains.

However, even these models do not validate certain expected equivalences. Two of the most offensive ones are

\begin{aligned}
  \textbf{new } x \coloneqq V; M &\simeq M \\
  \textbf{new } x \coloneqq V;
    \textbf{new } y \coloneqq W;
    M
  &\simeq
  \textbf{new } y \coloneqq W;
    \textbf{new } x \coloneqq V; M
\end{aligned}

when x does not occur in M or W, and y does not occur in V. Thus, these models are still not fully abstract.

See possible worlds.

Algebraic models

Many effects can be modelled as algebraic effects, and this includes storage.

See also

• Store
• Higher-order store
• Possible worlds (storage).

References

@article{tennent_2000,
	title = {Abstract {Models} of {Storage}},
	volume = {13},
	doi = {10.1023/A:1010022312623},
	journal = {Higher-Order and Symbolic Computation},
	author = {Tennent, Robert D. and Ghica, Dan R.},
	year = {2000},
	pages = {119--129}
}