13.3 Evaluation

< Free Open Study >

A more subtle aspect of the treatment of references appears when we consider how to formalize their operational behavior. One way to see why is to ask, "What should be the values of type Ref T?" The crucial observation that we need to take into account is that evaluating a ref operator should do something-namely, allocate some storage-and the result of the operation should be a reference to this storage.

What, then, is a reference?

The run-time store in most programming language implementations is essentially just a big array of bytes. The run-time system keeps track of which parts of this array are currently in use; when we need to allocate a new reference cell, we allocate a large enough segment from the free region of the store (4 bytes for integer cells, 8 bytes for cells storing Floats, etc.), mark it as being used, and return the index (typically, a 32- or 64-bit integer) of the start of the newly allocated region. These indices are references.

For present purposes, there is no need to be quite so concrete. We can think of the store as an array of values, rather than an array of bytes, abstracting away from the different sizes of the run-time representations of different values. Furthermore, we can abstract away from the fact that references (i.e., indexes into this array) are numbers. We take references to be elements of some uninterpreted set L of store locations, and take the store to be simply a partial function from locations l to values. We use the metavariable μ to range over stores. A reference, then, is a location-an abstract index into the store. We'll use the word location instead of reference or pointer from now on to emphasize this abstract quality.^[5]

Next, we need to extend our operational semantics to take stores into account. Since the result of evaluating an expression will in general depend on the contents of the store in which it is evaluated, the evaluation rules should take not just a term but also a store as argument. Furthermore, since the evaluation of a term may cause side effects on the store that may affect the evaluation of other terms in the future, the evaluation rules need to return a new store. Thus, the shape of the single-step evaluation relation changes from t → t′ to t | μ → t′ | μ′, where μ and μ′ are the starting and ending states of the store. In effect, we have enriched our notion of abstract machines, so that a machine state is not just a program counter (represented as a term), but a program counter plus the current contents of the store.

To carry through this change, we first need to augment all of our existing evaluation rules with stores:

Note that the first rule here returns the store μ unchanged: function application, in itself, has no side effects. The other two rules simply propagate side effects from premise to conclusion.

Next, we make a small addition to the syntax of our terms. The result of evaluating a ref expression will be a fresh location, so we need to include locations in the set of things that can be results of evaluation-i.e., in the set of values:

 v  ::=        λx:T.t        unit        l

values:

abstraction value

unit value

store location

Since all values are also terms, this means that the set of terms should include locations.

 t  ::=        x        λx:T.t        t t        unit        ref t        !t        t:=t        l

terms:

variable

abstraction

application

constant unit

reference creation

dereference

assignment

store location

Of course, making this extension to the syntax of terms does not mean that we intend programmers to write terms involving explicit, concrete locations: such terms will arise only as intermediate results of evaluation. In effect, the term language in this chapter should be thought of as formalizing an intermediate language, some of whose features are not made available to programmers directly.

In terms of this expanded syntax, we can state evaluation rules for the new constructs that manipulate locations and the store. First, to evaluate a dereferencing expression !t₁, we must first reduce t₁ until it becomes a value:

Once t₁ has finished reducing, we should have an expression of the form !l, where l is some location. A term that attempts to dereference any other sort of value, such as a function or unit, is erroneous. The evaluation rules simply get stuck in this case. The type safety properties in §13.5 assure us that well-typed terms will never misbehave in this way.

Next, to evaluate an assignment expression t₁ :=t₂, we must first evaluate t₁ until it becomes a value (i.e., a location),

and then evaluate t₂ until it becomes a value (of any sort):

Once we have finished with t₁ and t₂, we have an expression of the form l:=v₂, which we execute by updating the store to make location l contain v₂:

(The notation [l ↦ v₂]μ here means "the store that maps l to v₂ and maps all other locations to the same thing as μ." Note that the term resulting from this evaluation step is just unit; the interesting result is the updated store.)

Finally, to evaluate an expression of the form ref t₁, we first evaluate t₁ until it becomes a value:

Then, to evaluate the ref itself, we choose a fresh location l (i.e., a location that is not already part of the domain of μ) and yield a new store that extends μ with the new binding l ↦ v₁.

The term resulting from this step is the name l of the newly allocated location.

Note that these evaluation rules do not perform any kind of garbage collection: we simply allow the store to keep growing without bound as evaluation proceeds. This does not affect the correctness of the results of evaluation (after all, the definition of "garbage" is precisely parts of the store that are no longer reachable and so cannot play any further role in evaluation), but it means that a naive implementation of our evaluator will sometimes run out of memory where a more sophisticated evaluator would be able to continue by reusing locations whose contents have become garbage.

13.3.1 Exercise [⋆⋆⋆]

How might our evaluation rules be refined to model garbage collection? What theorem would we then need to prove, to argue that this refinement is correct?

^[5]Treating locations abstractly in this way will prevent us from modeling the pointer arithmetic found in low-level languages such as C. This limitation is intentional. While pointer arithmetic is occasionally very useful (especially for implementing low-level components of run-time systems, such as garbage collectors), it cannot be tracked by most type systems: knowing that location n in the store contains a Float doesn't tell us anything useful about the type of location n + 4. In C, pointer arithmetic is a notorious source of type safety violations.

< Free Open Study >