Proving the Correctness of Storage Representations

Mitchell Wand and Dino P. Oliva^{∗}

College of Computer Science Northeastern University

360 Huntington Avenue, 161CN Boston, MA 02115, USA

wand@corwin.ccs.northeastern.edu oliva@corwin.ccs.northeastern.edu

Abstract

Conventional techniques for semantics-directed compiler derivation yield abstract machines that manipulate trees. However, in order to produce a real compiler, one has to represent these trees in memory. In this paper we show how the technique of storage-layout relations (introduced by Hannan [7]) can be applied to verify the correctness of storage representations in a very general way. This technique allows us to separate denotational from operational reasoning, so that each can be used when needed. As an example, we show the correctness of a stack implementation of a language including dynamic catch and throw. The representation uses static and dynamic links to thread the environment and continuation through the stack. We discuss other uses of these techniques.

1 Introduction

Typical semantically-derived compiler systems [2, 3, 7, 18, 19] translate the parse trees of the source language into the language of an abstract byte-code machine. This abstract byte code machine typically manipulates trees that represent the environment, continuation, local stack, etc. However, in order to turn this into a real compiler, one has to represent these trees in machine storage. There are a variety of strategies for doing this [8], but this representation step remains a critical and untrustworthy part of compilerdevelopment technology. Indeed, in two recent compilercorrectness projects [9, 10], it turned out to be the most difficult part of the task.

Hannan [7] has shown how, under certain restrictions, one can automatically transform an abstract machine into a storage machine. In this paper we show how similar techniques can be used to verify the correctness of storage representations in a far more general way. As in [18, 19, 20], we do not attempt to derive these representations automatically.

Instead, our goal is to build a framework in which compiler writers can prove the correctness of arbitrarily clever human-invented representations.

The representations are formalized by the use of representations that we call storage-layout relations. Storagelayout relations allow a compiler writer to specify the representation decisions he or she has made. Storage-layout relations were introduced in [7]. This work extends that of [7] by liberating it from the particular architecture considered there, and by considering more complex representation strategies, such as multiple terms threaded through a single stack.

As an application, we consider a simple (not necessarily functional) language with continuation semantics and catch and throw operators. The language is designed to obey stack discipline: that is, the language can be implemented using only a stack. Our goal is to prove the correctness of this assertion. In fact, we will show that an ordinary stack representation, with static and dynamic chain pointers, constitutes a representation of the three trees (display, local stack, and continuation) of the abstract bytecode machine.

We first give a semantics and a simple byte-code compiler using the techniques of [3]. This compiler produces code for an abstract machine that manipulates combinator trees representing the environment, continuation, and a local stack. We then consider two successively more concrete implementations of this abstract machine. In the first version, we represent the display, local stack, and continuation in a single stack kept in memory, while the program remains as a tree. In the second version, we represent programs linearly as well.

This example shows how we can separate denotational from operational reasoning in a compiler correctness proof, using each to best advantage: the translation from source code to combinator trees is proved correct using structural induction and denotational reasoning; the translation from the abstract machine to the the concrete machines is proved correct using induction on length of execution and operational reasoning. The link between the two regimes is obtained using general results about the completeness of reduction strategies in the λ-calculus. We believe that this strategy will be of general use.

∗Work supported by the National Science Foundation and DARPA under grants CCR-9002253 and CCR-9014603

2 Comparison with Previous Work

Early proofs of compiler correctness, such as [11], did the translation from source to target code in a single step. In modern terminology, such proofs used a source semantics in a direct style and a target semantics in a continuation style or an operational style.

The restriction to direct-style semantics made it infeasible to use these techniques to prove the correctness of compilers for languages with non-local jumps. Therefore, in the 1970’s, attention turned to correctness proofs in which the source language was given using continuation semantics. Such proofs typically involved complex arguments about inclusive predicates that related the domains in the source and target semantics [12, 17]. These proofs were quite complex because they sought to model reasoning that was essentially operational (induction on reduction sequences) by methods that were essentially denotational (induction on approximations to inverse limit domains).

At the beginning of the 1980’s, Wand [18] showed how to avoid the use of inclusive predicates by modelling the target machine in the same semantic domains as the source semantics. In this paradigm, one showed that the meanings of the source and target programs were the same. Because the semantics was compositional, this could be done by a simple structural induction. This approach was refined by Clinger [3] to prove the correctness of a compiler for Scheme.

In this approach, the target language was a sublanguage of the λ-calculus, designed to be closed under reduction. The target machine simply had to simulate the reduction of the target program. One could use any desired mechanism to do this. The simulation proof could use operational reasoning. The reduction strategy was known to be complete, so the machine was guaranteed to reduce the target program to a normal form if one existed.

The Wand-Clinger approach simplified the inclusive-pre-dicate approach in two ways: first, it allowed the denotational reasoning to be done in a single λ-model that gave denotations to both source and target terms, and second, it separated operational from denotational reasoning, so each could be used where appropriate. This paper extends the operational part of the proof by showing how the tree-rewriting systems can be implemented in a conventional storage model, and how that implementation can be proved correct using operational reasoning.

Raoult and Sethi [14] and Schmidt [16] considered the issue of single-threading: when a particular term (or class of terms) could be represented by a single destructivelyupdated quantity, but they did not consider the representation of such quantities in a linear store. Hannan [7] showed how certain classes of tree-rewriting systems could be transformed into a stored-program form, including the linear representation of programs, much like our stored-program machine in Section 8, but he represented all mutable data either in the heap or in multiple stacks, rather than considering the single-stack representation considered here.

3 Source Language

Our source language is a simple language with continuation semantics. Its values are integers, recursive procedures, and continuations. Operations on integers are addition and conditional branch (on zero). Operations on continuations are catch and throw. Catch captures the current continuation and binds it to an identifier. Throw invokes a bound continuation on a value, discarding the current continuation. Procedures are recursive, using a local identifier for selfreference. Any kind of value may be passed to a procedure, but procedures may return only integers, so that the language can be implemented using only a stack. The semantics is given relative to an unspecified domain of command continuations, so that non-functional primitives may be added.

The language is given by

E ::= Id | (E + E) | (if E E E) | (catch Id E)

| (throw Id E) | (E E) | (rec Id(Id) E)

The semantics of the language is given by a valuation E[[−]]. We typically think of E[[−]] as a syntactic transformation, whose output is a λ-term of the appropriate type. That is, if we write \underline{T} for the set of λ-terms of type T, then we think of E as having type E → \underline{U → K → C}, where U, K, and C are types given by

C = Command Continuations
V = Int + [V → K → C] + [V → C]
K = V → C
U = Id → V

The lattice-theoretical details are not relevant, since we are dealing with λ-terms rather than denotations; we assume only the existence of a non-trivial model with this type theory. We write the summands of V as ⟨int, n⟩, ⟨proc, p⟩ or ⟨cont, κ⟩. We assume the existence of combinators that can distinguish these pairwise; this is easy to do by coding.

The semantics is given by

E[[I]] = λρκ.κ(ρ[[I]])
E[[(e_{1} + e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ(λv_{2}. sum v_{1}v_{2}κ))
E[[(if e_{1} e_{2} e_{3})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.v_{1} = ⟨int, 0⟩ →
E[[e_{3}]]ρκ,
E[[e_{2}]]ρκ)
E[[(rec F (I) e)]] = λρκ.κ⟨proc,

(fix(λpλvκ.E[[e]](ρ[⟨proc, p⟩/F, v/I])

(λv. return κv)))⟩
E[[(e_{1} e_{2})]] = λρκ.E[[e_{1}]]ρ(λv_{1}.E[[e_{2}]]ρ
(λv_{2}. apply_{p} v_{1}v_{2}κ))
E[[(catch I e)]] = λρκ.E[[e]]ρ[⟨cont, κ⟩/I]k
E[[(throw I e)]] = λρκ.E[[e]]ρ(λv_{1}.E[[I]]ρ(λv_{2}. apply_{k} v_{1}v_{2}))

The operators sum, apply_{p}, apply_{k}, and return all check their arguments for membership in the appropriate summand. In particular, return only allows procedures to return integers; this prevents upward funargs and allows a stackdiscipline implementation.

sum = λv_{1}v_{2}κ.(v_{1} = ⟨int, n_{1}⟩) →

(v_{2} = ⟨int, n_{2}⟩) → κ(⟨int, n_{1} + n_{2}⟩), (error “Non-integer second arg”),

(error “Non-integer first arg”)

apply_{k} = λv_{1}v_{2}.(v_{2} = ⟨cont, κ⟩) →

(v_{1} = ⟨int, n⟩) → κ(v_{1}),

(error “Non-integer second arg”), (error “Non-continuation first arg”) return = λκv.(v = ⟨int, n⟩) → κ(v),

(error “Non-integer return value”)

apply_{p} = λv_{1}v_{2}κ.(v_{1} = ⟨proc, p⟩) → pv_{2}κ, (error “Non-procedure to apply”)

4 The Byte-Code Compiler

Our compiler is a straightforward byte-code compiler based on [3, 18]. Our abstract machine has three registers: a display u, a local stack ζ (essentially a local register file, which is manipulated as a stack), and a continuation. A program acts on these to produce a command continuation. The machine uses the following domains:

l : L  Lexical Addresses

(Int × Int)

Γ : U_{C} = Id → L  Symbol Tables
u : U_{R} = L → V  Run-Time Environments

(displays)

π : P = U_{R} → V^{∗} → K → C Programs
ζ : V^{∗}  Local Stacks

A program is a term of type P. The compiler takes an expression and a symbol table, and returns a basic block (that is, a function \underline{P} → \underline{P}) for that expression. The goal of the basic block is to execute its sequel in the same runtime environment and continuation, but with the value of the expression pushed on the local stack. This specification will be the induction hypothesis for the compiler correctness proof. We write this specification as follows:

(C[[e]]Γπ)uζκ = E[[e]](u ∘ Γ)(λz.πu(z :: ζ)κ)  (1)

Here we see that the expression is to be evaluated in the environment which is the composition of the symbol table and the display. Given the binding-time annotations suggested for E and C, each side of this equality can be interpreted as a λ-term of type C, so the equality is to be interpreted as equivalence in some suitable λ-theory.

The compiler is defined as follows:

C[[I]]Γπ = fetch(Γ[[I]])π C[[(e_{1} + e_{2})]]Γπ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(add π)) C[[(if e_{1} e_{2} e_{3})]]Γπ = C[[e_{1}]]Γ(brz(C[[e_{2}]]Γπ)(C[[e_{3}]]Γπ)) C[[(rec F (I) e)]]Γπ = close(C[[e]](ext_{C}⟨I, F ⟩Γ) rts)π C[[(e_{1} e_{2})]]Γπ = C[[e_{1}]]Γ(C[[e_{2}]]Γ(jsr π)) C[[(catch I e)]]Γπ = save-cont(C[[e]](ext_{C}⟨I, d⟩Γ) rts)π

(d a fresh identifier ) C[[(throw I e)]]Γπ = C[[e]]Γ(C[[I]]Γ throw)

Thus the code for e_{1} + e_{2} consists of the code for e_{1} followed by the code for e_{2}, followed by an add instruction, followed by the program π that is to follow this basic block. (We leave it to the reader to verify that this definition is consistent with the binding-time annotation given above).

The instructions fetch, add, etc., are combinators that satisfy the following equations:

(fetch l π)uζκ = πu(u(l) :: ζ)κ (add π)u(⟨int, n_{2}⟩ :: ⟨int, n_{1}⟩ :: ζ)κ

= πu(⟨int, n_{1} + n_{2}⟩ :: ζ)κ (brz π_{1}π_{2})u(⟨int, n_{1}⟩ :: ζ)κ

= ((n_{1} = 0) → (π_{2}uζκ), (π_{1}uζκ)) (save-cont π_{1}π_{2})uζκ

= π_{2}(ext_{R}⟨⟨cont, (cont π_{1}uζκ)⟩, ⟨⟩⟩u)⟨⟩(cont π_{1}uζκ) (throw)u(⟨int, n⟩ :: ⟨cont, (cont π′u′ζ′κ′)⟩ :: ζ)κ

= π′u′(⟨int, n⟩ :: ζ′)κ′ (close π′π)uζκ = πu(⟨proc, closure uπ′⟩ :: ζ)κ (rts)u(⟨int, n⟩ :: ζ)(cont π′u′ζ′κ′) = π′u′(⟨int, n⟩ :: ζ′)κ′ (jsr π)u(v :: ⟨proc, closure u′π′⟩ :: ζ)k

= π′(ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′)⟨⟩(cont πuζκ)

In addition, the instructions must also satisfy a set of equations for error conditions in the semantics, such as

(add π)u(v :: ⟨proc, p⟩ :: ζ)κ = error “Non-integer first arg”

Here cont and closure are combinators defined by:

(cont πuζκ) = λz.πu(z :: ζ)κ (closure uπ) = fix(λp.λvκ.π(ext_{R}⟨v, ⟨proc, p⟩⟩u)⟨⟩κ)

and ext_{C} and ext_{R} are combinators such that

(ext_{R}⟨v, v′⟩u) ∘ (ext_{C}⟨I, I′⟩Γ) = (u ∘ Γ)[v/I, v′/I′]

The equations for the instructions are not quite combinators as presented here, but it is straightforward to write combinators that obey these equations.

Now we can state the correctness of the compiler:

Theorem 1 The compiler C is correct, that is, for all source programs e, symbol tables Γ, run-time environments u, stacks ζ, and continuations κ,

(C[[e]]Γπ)uζκ = E[[e]](u ∘ Γ)(λz.πu(z :: ζ)κ)

Proof: By a straightforward structural induction on the expressions of the source language. □

The bytecode machine definition is denotational. However, except for the error rules, each instruction definition is of the form

πuζκ = π′u′ζ′κ′

where π, u, ζ, κ, π′ u′ ζ′ κ′ are given by the following grammar:

π ::= (fetch l π) | (add π) | (brz ππ)

| (save-cont ππ) | (throw) | (close ππ) | (rts) | (jsr π)

u ::= emptydisplay | (ext_{R}⟨v, ⟨proc, closure u′π⟩⟩u′)

| (ext_{R}⟨⟨cont, (cont πu′ζκ)⟩, ⟨⟩⟩u′)

ζ ::= ⟨⟩ | (v :: ζ)
v ::= ⟨int, n⟩ | ⟨proc, closure uπ⟩

| ⟨cont, (cont πuζκ)⟩

k ::= initcont | (cont πuζκ)

(where in the productions for u, the occurrences of u′ are the same; this could be avoided by introducing two new combinators).

Each step in the reduction sequence of πuζκ will have the form π′u′ζ′κ′ for some program π′, display u′, stack ζ′, and continuation κ′ as specified by this grammar. Therefore we can give the bytecode machine an operational semantics by thinking of it as a 4-register machine and regarding each of the equations for the instruction combinators as rewriting rules. The resulting abstract machine is shown in Figure 1. We can state the soundness of this machine as follows:

Theorem 2 If ⟨π, u, ζ, κ⟩ ⟹ ⟨π′, u′, ζ′, κ′⟩, then πuζκ → π′u′ζ′κ′.

It can also be shown that the machine is complete with respect to either call-by-value or call-by-name reduction [13], since these reduction strategies coincide on the terms manipulated by the machine, and the machine emulates these reduction strategies.

So far this is just an example of the method set out in [3, 18] (see also [5] for some more extended examples). We next turn to our main topic: the representation of these trees in a linear store.

5 Stack Representation

This abstract machine simulates the reduction of the terms produced by the compiler. However, it is still a tree manipulation system. In order to implement this abstract machine on a real computer, one must represent these trees in memory. It is the correctness of this representation that is our main concern in this paper.

In particular, our language was carefully designed to obey stack discipline: that is, the language can be implemented using only a stack. Our goal is to prove the correctness of this assertion. In fact, we will show that an ordinary stack representation, with static and dynamic chain pointers, constitutes a representation of the three trees (display, local stack, and continuation) of the abstract bytecode machine.

We will do this in two stages. In the first stage, we will represent the display, local stack, and continuation in a single stack kept in memory, whereas the program π will remain as a tree. In the second stage, we will represent programs linearly as well.

Our concrete machine will be a 5-tuple

⟨π, up, sp, kp, σ⟩

consisting of a program π, a display pointer up, a stack pointer sp, a continuation pointer kp, and a store σ. The pointers are addresses in the store, satisfying sp ≥ kp > up. We assume that each cell of the store can hold a tag (proc or int), a pointer, and occasionally a program. (The program will be condensed to a pointer in the second step).

We now sketch the representation of the abstract machine’s quantities in the concrete machine.

1. Values (integers or closures) are represented as single words in memory, including their tags. Continuations bound by catch are represented as single words containing a tag and a pointer to the continuation structure.

2. A local stack (v_{n} :: v_{n−1} :: …:: v_{1} :: ⟨⟩) is specified by giving upper and lower bounds as indices, and is represented as a series of words in the stack:

ub: v_{n} ; v_{n−1} ; …; v_{1} ; lb:

This notation is intended to mean that ub and lb are pointers into the stack, that ub points higher in the stack than lb, and that the values from position ub, moving downward, are v_{n}, v_{n−1}, …, v_{1}.

3. A run-time environment (display) extension of the form ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′ is specified by a pointer p into the stack:

p :  v
⟨proc, closure p′π′⟩

where p′ is a pointer to the display u′ (ie, a static chain pointer). Here the second slot is used both for the closure that is bound to the local name for the procedure and for the static chain that is in the closure.

4. A run-time environment (display) extension of the form ext_{R}⟨⟨cont, (cont π′uζκ)⟩, ⟨⟩⟩u is specified by a pointer p into the stack:

\begin{aligned}p : & ⟨cont, p′⟩ \\ & p′′ \end{aligned}

where ⟨cont, p′⟩ represents (cont π′uζκ) (according to item 1 above) and p′′ is a pointer to the display u (ie, a static chain pointer).

5. The continuation (cont πuζκ) is represented by a pointer p into the stack as follows:

p : π the saved program (counter)
up pointer to the saved environment
kp dynamic chain (base) pointer

left open for current environment left open for current environment

v_{n} top value in ζ

…

v_{1} bottom value in ζ
kp:  top of frame for next continuation κ

6 Storage Layout Relations

This pictorial specification is adequate for compiler writers, but it is not quite formal enough to allow us to do proofs. We formalize these pictures as a family of relations, called storage layout relations, that tell precisely when a pointer into a stack corresponds to a given abstract structure. In general, a storage layout relation will be a ternary relation σ ⊧ p ≃ m, which means that pointer p corresponds to abstract structure m in store σ. We will consistently put the concrete object on the left of the equivalence, and read ≃ as “corresponds to.”

We will have four storage layout relations, one each for values, stacks, environments, and continuations. These will be defined by simultaneous induction on the terms for values, stacks, environments, and continuations. Since these are relations on terms (not their denotations), the existence of the relations is assured.

The definition of the relations is now a straightforward transcription of the data in the diagrams above.

Abstract machine:

⟨(fetch l π), u, ζ, κ⟩ ⟹ ⟨π, u, (u(l) :: ζ), κ⟩
⟨(add π), u, (⟨int, n_{2}⟩ :: ⟨int, n_{1}⟩ :: ζ), κ⟩ ⟹ ⟨π, u, (⟨int, n_{1} + n_{2}⟩ :: ζ), κ⟩
⟨(brz π′π), u, v :: ζ), κ⟩ ⟹ ⟨(choose v π′π), u, ζ, κ⟩
⟨(save-cont π′π), u, ζ, κ⟩ ⟹ ⟨π, (ext_{R}⟨⟨cont, (cont π′uζκ)⟩, ⟨⟩⟩u),
⟨⟩, (cont π′uζκ)⟩
⟨(throw), u, ⟨cont, (cont π′u′ζ′κ′)⟩ :: ⟨int, n⟩ :: ζ), κ⟩ ⟹ ⟨π′, u′, (⟨int, n⟩ :: ζ′), κ′⟩
⟨(close π′π), u, ζ, κ⟩ ⟹ ⟨π, u, (⟨proc, closure uπ′⟩ :: ζ), κ⟩
⟨(rts), u, (⟨int, n⟩ :: ζ), (cont π′u′ζ′κ′)⟩ ⟹ ⟨π′, u′, (⟨int, n⟩ :: ζ′), κ′⟩
⟨(jsr π), u, (v :: ⟨proc, closure u′π′⟩ :: ζ), κ⟩ ⟹ ⟨π′, ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′,
⟨⟩, (cont πuζκ)⟩

Auxiliaries:

(choose v π′π) = (v = ⟨int, 0⟩) → π, π′

Figure 1: Actions of the abstract machine.

• Relating Pointers and Tagged Values

σ ⊧_{V} p ≃ v ⟺

either v = ⟨int, n⟩ = σ(p)
or  v = ⟨proc, (closure uπ)⟩

and σ(p) = ⟨proc, (closure up π)⟩ and up < p and σ ⊧_{U} up ≃ u

or  v = ⟨cont, (cont πuζκ)⟩

and σ(p) = ⟨cont, p′⟩ and p′ < p and σ ⊧_{K} p′ ≃ (cont πuζκ)

• Relating Pointers and Stacks

σ ⊧_{Z} ⟨p, p′⟩ ≃ ζ ⟺

either ζ = ⟨⟩ and p = p′
or  ζ = (z :: ζ′) and p > p′ and σ ⊧_{V} p ≃ z

and σ ⊧_{Z} ⟨p − 1, p′⟩ ≃ ζ′

• Relating Pointers and Environments

σ ⊧_{U} p ≃ u ⟺

either u = emptydisplay and p = −1
or  u = ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′

and σ ⊧_{V} p ≃ v and σ ⊧_{V} p − 1 ≃ ⟨proc, closure u′π′⟩ and σ(p − 1).u < p and σ ⊧_{U} σ(p − 1).u ≃ u′

or  u = (ext_{R}⟨⟨cont, (cont π′u′ζκ)⟩, ⟨⟩⟩u′)

and σ(p) = ⟨cont, p′⟩ and p′ = p + 3 and σ ⊧_{K} p′ ≃ (cont πuζκ) and σ(p − 1).u < p and σ ⊧_{U} σ(p − 1).u ≃ u′

Here we use the notation σ(p).u to denote the contents of environment-pointer field of location p of σ. We will use similar notation for field selectors throughout. Note that this relation specifies that that the static chain is kept in the same field of the second word of the environment representation, whichever variation (proc or cont) is used. The p+3 case arises when a save-cont instruction is executed: this instruction pushes a new continuation on the stack, using the format in item 5 above, and binds the continuation in the vacant environment frame.

• Relating Pointers and Continuations

σ ⊧_{K} p ≃ κ ⟺

either κ = initcont and p = 0
or  κ = (cont πuζκ′)
and σ(p) = π

and σ(p − 1) < p and σ ⊧_{U} σ(p − 1) ≃ u and σ(p − 2) < p and σ ⊧_{K} σ(p − 2) ≃ κ′

and σ ⊧_{Z} (p − 5, σ(p − 2)) ≃ ζ

7 The Proof

We begin by stating some useful lemmas about these relations. The most important of these lemmas state that the changing locations in the stack above a pointer does not change the quantity that the pointer represents. Let σ =_{p} σ′ denote the proposition ∀x, 0 ≤ x ≤ p ⟹ σ(x) = σ′(x). Then we have the following:

Lemma 1 1. If σ =_{p} σ′ & σ ⊧_{V} p ≃ v then σ′ ⊧_{V} p ≃ v.

2. If σ =_{p} σ′ & σ ⊧_{Z} ⟨p, p′⟩ ≃ ζ then σ′ ⊧_{Z} ⟨p, p′⟩ ≃ ζ.

3. If σ =_{up +3} σ′ & σ ⊧_{U} up ≃ u then σ′ ⊧_{U} up ≃ u.

4. If σ =kp σ′ & σ ⊧_{K} kp ≃ κ then σ′ ⊧_{K} kp ≃ κ.

Proof: By induction on the definition of ≃. For stacks, the condition σ ⊧_{Z} ⟨p, p′⟩ implies p′ ≤ p. For environments, we need to write up +3 because the first slot might contain a continuation, we potentially can point 3 slots up in the stack. □

We can now define the correspondence between abstract and concrete machine states.

Definition 1 We say a concrete machine state ⟨π, up, sp, kp, σ⟩ corresponds to an abstract machine state ⟨π′, u, ζ, κ⟩ (written ⟨π, up, sp, kp, σ⟩ ≃ ⟨π′, u, ζ, κ⟩) if and only if the following conditions are satisfied:

1. π = π′,

2. σ ⊧_{U} up ≃ u,

3. σ ⊧_{Z} (sp, kp) ≃ ζ, and

4. σ ⊧_{K} kp ≃ κ.

This says (among other things) that the local stack ζ is kept at the top of the stack, and is immediately followed by the representation of κ; the display u is threaded through the stack but need not be near the top.

With this definition of correspondence between machine states, we can work out the action of our instructions on the concrete machine. Figure 2 shows the most complex example, the jsr instruction. Here sp′, up′, and kp′ denote the new values of the concrete machine registers. Since sp′ = kp′, the new value of ζ is the empty stack ⟨⟩.

A diagram such as that in Figure 2 can be translated into a formal representation more suitable for formal reasoning, similar to the definition of the abstract machine in Section 4. This is done in Figure 3. Here we use v. kp to extract the continuation field from a stored continuation, and v.π to extract the program field from a stored closure.

We can show that the following invariant is preserved by the machine:

Lemma 2 In all machine states, sp ≥ kp ≥ up +3.

The correctness of the auxiliary find is also shown:

Lemma 3 If σ ⊧_{U} up ≃ u then

σ ⊧_{V} (find l up σ) ≃ u(l)

Now we can show the main theorem, which asserts that the concrete machine correctly simulates the abstract machine:

Theorem 3 Let A_{1} and A_{2} be states of the abstract machine and C_{1} and C_{2} be states of the concrete machine. If C_{1} ≃ A_{1}, A_{1} ⟹ A_{2}, and C_{1} ⟹ C_{2}, then C_{2} ≃ A_{2}.

Proof: By analysis of each instruction. Here we show two cases, fetch and jsr.

• Assume we have ⟨(fetch l π), up, sp, kp, σ⟩ ≃ ⟨(fetch l π), u, ζ, κ⟩ We must show that

⟨π, up, sp +1, kp, σ′⟩ ≃ ⟨π, u, (u(l) :: ζ), κ⟩

where σ′ = σ[(lookup l up σ)/(sp +1)]. We consider each of the conditions for ≃ in turn:

1. π = π

2. We have sp +1 > up +3 and σ ⊧_{U} up ≃ u. Therefore σ′ ⊧_{U} up ≃ u by Lemma 1.

3. We have σ ⊧_{V} (find l up σ) ≃ u(l) and σ ⊧_{Z} ⟨sp, kp⟩ ≃ ζ. Hence σ′ ⊧_{Z} ⟨sp +1, kp⟩ ≃ (u(l) :: ζ)

4. sp +1 > kp and σ ⊧_{K} kp ≃ κ. Therefore σ′ ⊧_{K} kp ≃ κ

• Assume we have ⟨(jsr π), up, sp, kp, σ⟩ ≃ ⟨(jsr π), u, (v :: ⟨proc, closure u′π′⟩ :: ζ), κ⟩. We need

⟨σ(sp − 1).π, sp, sp +3, sp +3, (push-cont up sp kp σ)⟩ ≃ ⟨π′, (ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′), ⟨⟩, (cont πuζκ)⟩

where ζ′ = (v :: ⟨proc, closure u′π′⟩ :: ζ) and σ′ = (push-cont up sp kp σ). By the definition of push-cont, σ and σ′ agree on all locations less than or equal to sp.

1. We have σ ⊧_{Z} ⟨sp, kp⟩ ≃ ζ′ and |ζ′| ≥ 2. Hence

σ(sp − 1).π = π′.

2. σ ⊧_{Z} ⟨sp, kp⟩ ≃ ζ′ and |ζ′| ≥ 2 Hence σ′ ⊧_{U}

sp ≃ (ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′).

3. σ′ ⊧_{Z} ⟨sp +3, sp +3⟩ ≃ ⟨⟩

4. σ′(sp +3) = π

σ′(sp + 2) = up +3 < sp +1 and σ ⊧_{U} up ≃ u
⟹ σ′ ⊧_{U} σ′(sp + 2) ≃ u
σ′(sp + 1) = kp < sp +1 and σ ⊧_{K} kp ≃ κ
⟹ σ′ ⊧_{K} σ′(sp + 1) ≃ κ

σ ⊧_{Z} ⟨sp, kp⟩ ≃ ζ′ and |ζ′| ≥ 2 ⟹ σ′ ⊧_{Z}

⟨sp −2, σ′(sp + 1)⟩ ≃ ζ
⟹ σ′ ⊧_{K} sp +3 ≃ (cont πuζκ)

□

This theorem shows that the concrete machine and the abstract machine compute in the same way: started in corresponding states, they compute by passing through a sequence of corresponding states. Thus the concrete machine will give the same answer as the abstract machine.

This theorem is not surprising, of course. What is new here is a way of formalizing the representation of environments, continuations, etc., so that we can see how even very low-level structures directly represent the quantities in the language definition. Furthermore, this organization allows us to separate denotational from operational reasoning, so that each can be used to best advantage.

8 Code Representation

We can similarly represent the program trees π in a linear program store M. The details here are similar, but easier. Instead of storing a program π in a single word of memory, as we did in the previous machine, we represent π explicitly in a linear program store M. For example, the program (fetch l π′) would be represented as a location p in M:

\begin{aligned}p : & fetch \\ & l \end{aligned}

where p+2 represented π′. We assume that M has a domain that is disjoint from the data store σ and that its range is

Abstract machine:

⟨(jsr π), u, (v :: ⟨proc, closure u′π′⟩ :: ζ), κ⟩ ⟹

⟨π′, (ext_{R}⟨v, ⟨proc, closure u′π′⟩⟩u′), ⟨⟩, (cont πuζκ)⟩

Concrete machine:

Before  After  Comments
sp′, kp′ :  π  return address
up  saved environment pointer
kp  dynamic chain
sp : v up′ : v old top of ζ, now in environment
⟨proc, closure u′π′⟩  ⟨proc, closure u′π′⟩ closure, including static chain
v_{n}  v_{n}  rest of ζ, now saved
…  …
kp :  …  …  representation of κ

Figure 2: Executing a jsr instruction on the abstract and concrete machines.

Concrete machine:

⟨(fetch l π), up, sp, kp, σ⟩ ⟹ ⟨π, up, sp +1, kp, σ[(lookup l up σ)/ sp +1]⟩
⟨(add π), up, sp, kp, σ⟩ ⟹ ⟨π, up, sp −1, kp, σ[(int-add sp(sp −1)σ)/ sp −1]⟩
⟨(brz π′π), up, sp, kp, σ⟩ ⟹ ⟨(choose σ(sp) π′ π), up, sp −1, kp, σ⟩
⟨(save-cont π′π), up, sp, kp, σ⟩ ⟹ ⟨π′, sp +1, sp +5, sp +5, (ext-cp π up sp kp σ)⟩
⟨(throw), up, sp, kp, σ⟩ ⟹ ⟨σ(σ(sp). kp), σ((σ(sp).kp) − 1), σ(sp). kp −4,

σ((σ(sp).kp) − 2), σ[σ(sp −1)/σ(sp).kp − 4]⟩

⟨(close π′π), up, sp, kp, σ⟩ ⟹ ⟨π, up, sp +1, kp, σ[⟨proc, closure up π′⟩/ sp +1]⟩
⟨(rts), up, sp, kp, σ⟩ ⟹ ⟨σ(kp), σ(kp −1), kp −4, σ(kp −2), σ[σ(sp)/kp − 4]⟩
⟨(jsr π), up, sp, kp, σ⟩ ⟹ ⟨σ(sp − 1).π, sp, sp +3, sp +3, (push-cont π up sp kp σ)⟩

Auxiliaries:

(lookup ⟨n, m⟩ up σ) = σ(find ⟨n, m⟩ up σ)

(find ⟨n, m⟩ up σ) = ()(n = 0) → (up −m), (find ⟨n − 1, m⟩(σ(up).up)σ)

(int-add p p′ σ) = ⟨int, (σ(p).int) + (σ(p′).int)⟩

(choose v π′ π) = ((v = ⟨int, 0⟩) → π, π′) (push-cont π up sp kp σ) = σ[kp / sp +1, up / sp +2, π/ sp +3]

(ext-cp π up sp kp σ) = (push-cont π up sp +2 kp σ)[up / sp +1, ⟨cont, sp +5⟩/ sp +2] Figure 3: Actions of the concrete machine. large enough to hold a single opcode or a pointer (either to data or program).

Again, we define a storage layout relation M ⊧_{P} p ≃ π as the least fixpoint of a monotonic operator. (Note the presence of goto, which prevents the use of structural induction. The goto instruction is not necessary, but illustrates the power of the technique).

• Relating pointers and programs

M ⊧_{P} p ≃ π ⟺

either π = (fetch l π′)

and M(p) = fetch and M(p + 1) = l and M ⊧_{P} p + 2 ≃ π′

or  π = (add π′)

and M(p) = add and M ⊧_{P} p + 1 ≃ π′

or  π = (brz π′π′′)

and M(p) = brz and M ⊧_{P} M(p + 1) ≃ π′ and M ⊧_{P} p + 2 ≃ π′′

or  π = (save-cont π′π′′)

and M(p) = save-cont and M ⊧_{P} M(p + 1) ≃ π′ and M ⊧_{P} p + 2 ≃ π′′

or  π = rts and M(p) = rts
or  π = throw and M(p) = throw
or  π = (close π′π′′)

and M(p) = close and M ⊧_{P} M(p + 1) ≃ π′ and M ⊧_{P} p + 2 ≃ π′′

or  π = (jsr π′)

and M(p) = jsr and M ⊧_{P} p + 1 ≃ π′

or  M(p) = goto and M ⊧_{P} M(p + 1) ≃ π

• Relating stored values Stored values correspond if they are alike except for the representation of programs:

M ⊧_{SV} sv ≃ sv′ ⟺

either sv = ⟨proc, (closure up p)⟩

and sv′ = ⟨proc, (closure up π)⟩ and M ⊧_{P} p ≃ π

or  sv = p and sv′ = π and M ⊧_{P} p ≃ π
or  sv = sv′

• Relating data stores Data stores correspond up to pointer p if they correspond location by location for all smaller locations:

\begin{matrix}M ⊧_{p} σ ≃ σ′ ⟺ \\ 0 ≤ p′ ≤ p, M ⊧_{SV} σ(p′) ≃ σ′(p′) \end{matrix}

We call the machine using this linear program store the stored-program machine. In order to describe the machine using simple pattern-matching rules, we specify the storedprogram machine using a fetch-execute cycle. The controller of the machine has two states: fetch and execute. In the fetch state, the machine uses 4 registers: an instruction pointer ip, which is a pointer into the program store, pointers up, sp, and kp, as in the preceding machine. In the execute state, the machine uses in addition an instruction register ir.

In the fetch state, the machine retrieves the opcode to which the instruction pointer points, places it in the instruction register, and goes to the execute state:

F (ip, up, sp, kp, σ) ⟹ E(ip, M(ip), up, sp, kp, σ)

The execute state then performs a rewrite, dispatching on the contents of the instruction register, and returns to the fetch state. The rewriting system for the stored-program machine is shown in Figure 4. This is similar to Figure 3 except for the treatment of pointers to programs.

Now we can define the correspondence between the concrete and stored-program machines. We define the correspondence at the start of the fetch-execute cycle, that is, at the fetch state of the stored-program machine. Since the pointers into the data store are exactly the same, all that is required is that the programs correspond, and that the stores correspond up to sp:

Definition 2 We say a stored-program machine state F (ip, up, sp, kp, σ) corresponds to a concrete machine state ⟨π′, up′, sp′, kp′, σ′⟩ (written M ⊧ F (ip, up, sp, kp, σ) ≃ ⟨π, up, sp, kp, σ′⟩) if and only if:

1. M ⊧_{P} ip ≃ π′

2. up = up′

3. sp = sp′

4. kp = kp′

5. M ⊧sp σ ≃ σ′

Now we can state the main theorem:

Theorem 4 Let C_{1} and C_{2} be states of the concrete machine and L_{1} and L_{2} be fetch states of the stored-program machine. If M ⊧ L_{1} ≃ C_{1}, C_{1} ⟹ C_{2}, and L_{1} ⟹ L_{2}, then M ⊧ L_{2} ≃ C_{2}.

Proof: By analysis of each instruction. This is tedious but straightforward; since M is immutable, we do not need free-location lemmas like Lemma 1. □

If we call the algorithm that translates from program trees π to stored programs the “assembler,” then the correctness of the assembler factors into two parts:

1. Showing that the assembler is correct: that it emits a stored program corresponding to the program tree π.

2. Showing that if a stored program corresponds to a program tree π, then the machines will deliver corresponding outputs.

These two steps are somewhat analogous to the decomposition of the compiler: showing that the compiler is correct by showing it emits code that meets its specification (Theorem 1), and then showing that the bytecode machine simulates reduction of the bytecode term (Theorem 2).

As in the compiler case, the second part of the proof is independent of the assembler algorithm, and that is the part we have shown here; what remains is the first, assemblerdependent part. We hope to report on that elsewhere.

Stored-Program machine:

F (ip, up, sp, kp, σ) ⟹ E(ip, M(ip), up, sp, kp, σ)
E(ip, fetch, up, sp, kp, σ) ⟹ F (ip +2, up, sp +1, kp, σ[(lookup M(ip + 1) up σ)/ sp +1])
E(ip, add, up, sp, kp, σ) ⟹ F (ip +1, up, sp −1, kp, σ[(int-add sp(sp −1)σ)/ sp −1])
E(ip, brz, up, sp, kp, σ) ⟹ F ((choose (σ(sp))(ip +2)(M(ip +1))), up, sp −1, kp, σ)
E(ip, save-cont, up, sp, kp, σ) ⟹ F (M(ip +1), sp +1, sp +5, sp +5, (ext-cp(ip +2) up sp kp σ))
E(ip, throw, up, sp, kp, σ) ⟹ F ((σ(sp). kp), σ(σ(sp).kp − 1), σ(sp). kp −4,

σ(σ(sp).kp − 2), σ[σ(sp −1)/σ(sp).kp − 4])

E(ip, close, up, sp, kp, σ) ⟹ F (ip +2, up, sp +1, kp, σ[⟨proc, closure up M(ip +1)⟩/ sp +1])
E(ip, rts, up, sp, kp, σ) ⟹ F (σ(kp), σ(kp −1), kp −4, σ(kp −2), σ[σ(sp)/kp − 4])
E(ip, jsr, up, sp, kp, σ) ⟹ F (σ(sp − 1). ip, sp, sp +3, sp +3, (push-cont(ip +1) up sp kp σ))

Auxiliaries:

(lookup ⟨n, m⟩ up σ) = σ(find ⟨n, m⟩ up σ)

(find ⟨n, m⟩ up σ) = (n = 0) → (up −m), (find ⟨n − 1, m⟩(σ(up).up)σ)

(int-add p p′σ) = ⟨int, (σ(p).int) + (σ(p′).int)⟩
(choose v ip′ ip) = (v = ⟨int, 0⟩) → ip, ip′

(push-cont ip up sp kp σ) = σ[kp / sp +1, up / sp +2, ip / sp +3] (ext-cp ip up sp kp σ) = (push-cont ip up sp +2 kp σ)[up / sp +1, ⟨cont, sp +5⟩/ sp +2]

Figure 4: The fetch/execute cycle of the stored-program machine.

9 Partial Correctness and Untagged Representations

The stack machine derivation that we have presented is only one application of these proof strategies. In this section we will sketch another such application.

Our implementation still differs from an “ordinary” implementation of a stack-based language such as C or Pascal in that data values in C or Pascal do not include tags like our int or proc. Tags like these would impose a considerable run-time penalty in both time and space.^{1}

In languages like C or Pascal, the compiler typically uses some form of type-checking to ascertain that primitive operations like procedure call or arithmetic are invoked only on legal quantities. For languages that are not type-safe, such as C, these compile-time checks are of course less than foolproof, and may lead to unpredictable consequences (e.g. core dumps).

Here we have a semantic mismatch: the semantics is given using disjoint sums, with specified error behavior (continuations of the form (error …)), but the implementation uses non-disjoint sums and has unspecified error behavior. In what sense can we say that an implementation of such a language is correct?

We can model this situation by using untagged storage layout relations and weakening the requirements on the implementation. To get a storage layout relation for an untagged implementation, we replace pattern-matching in the definition of the storage relation by field selection. Thus we might replace

σ ⊧_{V} p ≃ v ⟺
either v = ⟨int, n⟩ = σ(p)
or  v = ⟨proc, (closure u π_{1})⟩
and σ(p) = ⟨proc, (closure up π_{1})⟩
and up < p and σ ⊧_{U} up ≃ u
…

by

σ ⊧_{V} p ≃ v ⟺

either v = ⟨int, n⟩ and σ(p) = n
or  v = ⟨proc, (closure uπ_{1})⟩
and M ⊧_{P} σ(p).π ≃ π_{1}
and σ(p).u < p and σ ⊧_{U} σ(p).u ≃ u
…

We can weaken the requirement on the implementation by saying that if the abstract machine proceeds without invoking an error, then the concrete machine must do so also. If the abstract machine invokes the error continuation, then the behavior of the concrete machine is unspecified. This contract corresponds to the Scheme notion [4] of “is an error.” With this contract, the correctness theorem becomes:

Theorem 5 Let A_{1} and A_{2} be states of the abstract machine and C_{1} and C_{2} be states of the concrete machine. If C_{1} ≃ A_{1}, A_{1} ⟹ A_{2}, A_{2} is not an error state, and C_{1} ⟹ C_{2}, then C_{2} ≃ A_{2}.

The only change from Theorem 3 is the addition of the phrase “ A_{2} is not an error state.” The proof goes as before.

10 Conclusions and Further Work

We have shown the correctness of a stack implementation of a programming language. The stack was shown to be a data structure that represented three different terms in the bytecode machine. The techniques generalize those introduced by Hannan [7]. We believe that these techniques will generalize to other crucial representation strategies, such as caching portions of the local stack ζ in registers, representing mutable entities with dynamic extent on the stack, and modelling program loops by circular storage structures. These techniques, especially the variant in Section 9, should also be adaptable to model the finite word size of real machines.

1The benefits of tag elimination are less clear for languages that require garbage collection, though even in this case it may be possible to remove all tags [1, 6]

Acknowledgements

Paul Hudak originally suggested the correctness of a stackdiscipline language as a useful exercise. Joshua Guttman, John Ramsdell, Vipin Swarup, Larry Monk, and Bill Farmer of the MITRE Corporation provided useful feedback on our Pure PreScheme compiler, which led us to the questions considered in this paper.

References

[1] Appel, A.W., “Runtime Tags Aren’t Necessary,” Lisp and Symbolic Computation 2 (1989), 153–162.

[2] Clément, D., Despeyroux, J., Despeyroux, T., and Kahn, G. “A Simple Applicative Language: Mini-ML” Proc. 1986 ACM Symp. on Lisp and Functional Programming, 13–27.

[3] Clinger, W. “The Scheme 311 Compiler: An Exercise in Denotational Semantics,” Conf. Rec. 1984 ACM Symposium on Lisp and Functional Programming (August, 1984), 356–364.

[4] Clinger, W., and Rees, J., eds. “Revised^{4} Report on the Algorithmic Language Scheme”, Indiana University Computer Science Department Technical Report No. 341, November, 1991, to appear in LISP Pointers, 1992. See also “Revised^{3} Report on the Algorithmic Language Scheme”, SIGPLAN Notices 21,12 (December, 1986), 37–79.

[5] Friedman, D.P., Wand, M., and Haynes, C.T., Essentials of Programming Languages, MIT Press, Cambridge, MA, and McGraw-Hill, Chicago, 1992.

[6] Goldberg, B. “Tag-Free Garbage Collection for Strongly Typed Programming Languages,” Proc. ACM SIG-PLAN ’91 Symp. on Programming Language Design and Implementation, June, 1991, 165–176.

[7] Hannan, J. “Making Abstract Machines Less Abstract,” Functional Programming Languages and Computer Architecture, 5th ACM Conference (J. Hughes, ed.) Springer Lecture Notes in Computer Science, Vol. 523 (1991), 618–635.

[8] Lee, P. Topics in Advanced Language Implementation, MIT Press, Cambridge, MA, 1991.

[9] Farmer, W.M., Guttman, J.D., Monk, L.G., Ramsdell, J.D., and Swarup, V. “VLISP: A Verified Language Implementation: FY 91 Year-End Report,” The MITRE Corporation Technical Report MTR11232, October, 1991.

[10] Oliva, D.P., and Wand, M., “A Verified Compiler for Pure PreScheme,” Final Report for MITRE Contract Number F19628-89-C-001. Included in [9].

[11] McCarthy, J. and Painter, J. “Correctness of a Compiler for Arithmetic Expressions,” in Proc. Symp. in Appl. Math., Vol. 19, Mathematical Aspects of Computer Science (J. T. Schwartz, ed.) Amer. Math. Soc., Providence, RI, 1967, 33–41.

[12] Milne, R. and Strachey C. A Theory of Programming Language Semantics, Chapman & Hall, London, and Wiley, New York, 1976.

[13] Plotkin, G.D. “Call-by-Name, Call-by-Value and the λ-Calculus,” Theoret. Comp. Sci. 1 (1975) 125–159.

[14] Raoult, J.-C. and Sethi, R. “The Global Storage Needs of a Subcomputation,” Conf. Rec. 11th ACM Symp. on Principles of Programming Languages (1984), 148–157.

[15] Reynolds, J.C. The Craft of Programming, Prentice-Hall International, 1981.

[16] Schmidt, D.A. Denotational Semantics: A Methodology for Language Development Boston: Allyn and Bacon, 1986.

[17] Stoy, J.E. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA., 1977.

[18] Wand, M. “Semantics-Directed Machine Architecture” Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang. (1982), 234–241.

[19] Wand, M. “Loops in Combinator-Based Compilers,” Info. and Control 57, 2–3 (May/June, 1983), 148–164.

[20] Wand, M. “On the Correctness of Procedure Representations in Higher-Order Assembly Language” Proc. MFPS ’91 (S. Brookes, ed.) Springer Lecture Notes in Computer Science, to appear.