LISP AND SYMBOLIC COMPUTATION: An International Journal, ?, ??–??, 1993 \begin{matrix}c \\ ◯ \end{matrix} 1993 Kluwer Academic Publishers – Manufactured in The Netherlands

VLISP: A Verified Implementation of Scheme^{∗}

JOSHUA GUTTMAN (guttman@mitre.org)

VIPIN SWARUP (swarup@mitre.org)

JOHN RAMSDELL (ramsdell@mitre.org)

Abstract. vlisp has produced a rigorously verified compiler from Scheme to byte codes, and a verified interpreter for the resulting byte codes. The official denotational semantics for Scheme provides the main criterion of correctness. The Wand-Clinger technique was used to prove correctness of the main compiler step. Then a state machine operational semantics is proved to be faithful to the denotational semantics. The remainder of the implementation is verified by a succession of state machine refinement proofs. These include proofs that garbage collection is a sound implementation strategy, and that a particular garbage collection algorithm is correct.

Contents

1 Introduction 2 1.1 What is Scheme? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2 Structure of the VLISP Implementation . . . . . . . . . . . . . . . 4

1.2.1 The Extended Byte Code Compiler . . . . . . . . . . . . . . 4 1.2.2 The Virtual Machine . . . . . . . . . . . . . . . . . . . . . . 6

2 The Byte-Code Compiler 8 2.1 The Scheme Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2 The Byte Code Semantics . . . . . . . . . . . . . . . . . . . . . . . 16 2.3 Multiple Values in the Scheme Semantics . . . . . . . . . . . . . . 19 2.4 Faithfulness of the Alternative Semantics . . . . . . . . . . . . . . 24 2.5 Compiler Correctness for Single-valued Semantics . . . . . . . . . . 26

3 Operational Semantics: Faithfulness and Refinement 30 3.1 Operational Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 30

∗The work reported here was carried out as part of The MITRE Corporation’s Technology Program, under funding from Rome Laboratories, Electronic Systems Command, United States Air Force, through contract F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation. Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford, MA 01730-1420.

Draft of September 29, 1993

3.2 Proving Faithfulness . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.2.1 Denotational Semantics of the Tabular Byte Code . . . . . 32 3.2.2 Operational Semantics of the Tabular Byte Code . . . . . . 32 3.2.3 Faithfulness: Form of the Proof . . . . . . . . . . . . . . . . 36

3.3 Refinement and Storage Layout Relations . . . . . . . . . . . . . . 40

4 The Flattener 43 4.1 The Tabular Byte Code in More Detail . . . . . . . . . . . . . . . 44 4.2 Flattened Byte Code Syntax . . . . . . . . . . . . . . . . . . . . . 45 4.3 Flattened Byte Code Operational Semantics . . . . . . . . . . . . . 46 4.4 The Flattener . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.5 Code Correspondence . . . . . . . . . . . . . . . . . . . . . . . . . 47 4.6 State Correspondence . . . . . . . . . . . . . . . . . . . . . . . . . 51

5 State Observers and Mutators 53

6 Garbage Collection 57 6.1 State Similarity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 6.2 Legitimacy of Garbage Collection . . . . . . . . . . . . . . . . . . . 60 6.3 The Correctness of a Copying Garbage Collector . . . . . . . . . . 64

7 The Finite Stored Program Machine 72

8 The VLISP Scheme Implementation 72 8.1 The VLISP Bootstrap Process . . . . . . . . . . . . . . . . . . . . 72 8.2 VLISP Virtual Machine Performance . . . . . . . . . . . . . . . . . 74 8.3 Unverified Aspects of VLISP . . . . . . . . . . . . . . . . . . . . . 75 8.4 Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76

1. Introduction

The primary goal of the vlisp project has been to produce a rigorously verified implementation of the Scheme programming language.

An implementation for a programming language consists of the ensemble of software required to make a program written in that language execute on a digital computer. A programming implementation may be a compiler, which translates programs in the given language to programs in a lower level language; or it may be an interpreter, which is a program that executes the higher level language directly; or it may be a combination of the two. The vlisp implementation, being modeled on Scheme48 [13], is of this mixed type. It consists of:

Draft of September 29, 1993

• A simple compiler that translates programs in the source language to target programs in an intermediate level byte code language;

• An interpreter (written in a systems-programming oriented dialect called PreScheme [13]) to execute the resulting byte code programs;

• A second compiler to translate the PreScheme code of the interpreter into assembly language code for commercial workstations (either a Sun 3 with an mc68020 cpu or a Sun 4 with a sparc processor).

This paper focuses on the first two items, which make up the implementation of Scheme. The third item, which implements PreScheme, is discussed in the accompanying paper [16]. A third paper [11] discusses results and conclusions of the effort as a whole. The present paper is intended to serve has two main purposes:

• To provide a detailed account of the techniques used in the vlisp Scheme verification; and

• To show the decomposition of layers that made the verification process tractable, that is, to display the “formal methods engineering” decisions we have made.

The vlisp effort has focused on algorithm-level rigorous verification. By this we mean to emphasize two things.

First, the proofs we have produced are about algorithms, rather than being about concrete program text. Reasoning about the concrete program text (under its formal semantics) is considerably more cumbersome. Far from providing deeper insight, in our opinion, the mass of detail involved frequently obscures the essential reasons why the program is correct. Naturally, the actual program text must be carefully constructed so that it is a patently faithful embodiment of the algorithm.

Second, our proofs are rigorous mathematical arguments, i.e., what most mathematicians mean by proofs. We have not produced derivations in a particular formal deductive system (which might be assisted by mechanical proof tools). Formal derivations would, again in our opinion, provide less real insight than mathematical proofs, unless the derivations were accompanied by carefully written, humanly understandable mathematical proofs. We return to this point in [11].

Draft of September 29, 1993

1.1. What is Scheme?

The Scheme programming language, “an UnCommon Lisp,” is defined by the language Report (currently in its fourth revision [3]), and by an ieee standard [12]. We have taken [12] as our definition.

However, the definition consists, for our purposes, of two radically different parts. The first and much larger part provides a carefully written but non-rigorous description of the lexical and syntactic structure of the language, and of its standard procedures and data structures. Many of the standard procedures are conceptually complex; they are generally implemented in Scheme itself, using a smaller set of procedures as data manipulation primitives.

The short, second portion consists of Appendix A, which provides an abstract syntax and a formal denotational semantics for the phrases in that abstract syntax. The semantics is concise and relatively abstract; however, for this reason, it provides only a loose specification for the implementer. Most of the standard procedures, even the data manipulation primitives, correspond to nothing in the denotational semantics; the denotations of constants are mostly unspecified; moreover, the semantics contains no treatment of ports and i/o.

The vlisp verification has taken Appendix A, in the slightly modified form given in [9], as its starting point. We have therefore concentrated on verifying those aspects of the language that it characterizes; some other aspects have only been introduced into our specifications at lower levels in the process of specifying and verifying our implementation.

1.2. Structure of the VLISP Implementation

The vlisp Scheme implementation derives from Scheme48 [13], and is thus a byte-coded implementation. That is, a compiler phase transforms Scheme source programs into an intermediate level language; the resulting target programs are executed by an interpreter, which we refer to as the “virtual machine” vm. The compiler phase is coded in Scheme, while the interpreter is coded in PreScheme.

1.2.1. The Extended Byte Code Compiler

The extended compiler acts on source programs in the Scheme language, and ultimately produces programs in a linearized byte code that we call “stored byte code” [20]. Its input programs consist of abstract syntax trees in a format only slightly different from the format used in the Scheme Standard [12]. The stored byte code output is in a binary form suitable for execution in the vm.

Draft of September 29, 1993

The extended compiler consists of a sequence of procedures which rewrite the original source program in a succession of intermediate languages.

• The byte code compiler [9] (properly so called, as distinguished from the extended compiler, of which it forms the first stage) rewrites the Scheme source code into a tree-structured byte code based on Clinger’s target language [2]. We will refer to this tree-structured byte code as the basic byte code or bbc. The bbc makes the flow of control in the Scheme program explicit, including procedure call and return, the order of argument evaluation, and the operations involved in building environment structures for local variables. bbc uses nested subtrees to represent constants, nested lambda expressions, conditionals, and procedure calls (when not in tail recursive position) in the source code. Successive phases of the compiler eliminate these nested structures in favor of linear layouts.

• The tabulator [9] transforms bbc procedures into templates in a tabular byte code or tbc. A template consists of some code, together with a table listing global variables, constants, and embedded templates (representing locally defined procedures). Instructions using these objects reference them by a numerical index.

• The flattener [10] transforms code in the tbc into a form that is linear rather than tree-structured. We call the output language of the linearizer the flattened byte code (fbc).

• The next stage of the extended compiler is the linker [6]. Its job is to transform a collection of (nested) constants and templates in the fbc into a single linear structure representing the full program.

• Finally the image builder [21] writes out the image to a file. The image builder is responsible for transforming the syntax of the linked code into a succession of bytes, with inetrnal references represented by 32-bit pointers.

The verification of the byte code compiler is closely based on Clinger’s, although some work, described in Section 2.5, had to be done to massage the official Scheme denotational semantics into a suitable form. The theorem establishes that a Scheme program and its compiled image compute that same computational answer, when started with appropriate initial values. The proof that the tabulator leaves the denotation of a program unchanged is straightforward.

The proofs of the remaining phases are based on an operational semantics, using state machines. Thus, there must be a proof that the operational semantics is faithful to the denotational one. For our purposes, it is enough to prove what may be regarded as a “partial correctness” assertion, namely that when the operational semantics predicts a computational answer (rather than non-termination, or an error condition), then the denotational semantics predicts the same answer. For this proof we devised a simple and easily mechanized method, described in Section 3.2.

Draft of September 29, 1993

We consider this approach far more tractable than those that have been devised to prove total correctness [14]. Total correctness would also ensure the converse: whenever the denotational semantics predicts a nonbottom answer, the operational semantics delivers that answer. However, the Scheme semantics predicts more answers than any implementation can actually deliver, simply because any implementation will have finite bounds, for instance on the height of the stack, and the semantics does not fully express this.

For the succeeding stages, we prove correctness by showing that one state machine is faithfully refined by another. As refinement is defined in Section 3.3, when the relation holds between an abstract state machine and a more concrete one, the latter can be used to compute the same results as the former. In practice, in order to prove refinement, we actually prove something more specific, namely that there is a storage layout relation between the machines. A storage layout relation (also as defined in Section 3.3) simplifies the task of proving refinement, because the comparison between state machines involves only states adjacent to one another under the transition relation. We have used this method repeatedly, defining the needed storage layout relations using various different techniques. The flattener (Section 4) provides a clean example of the method.

The other phases of the extended byte code compiler, namely the tabulator, linker and image builder, do not raise essentially new issues, so that we will focus our attention in this paper on the Clinger-style compiler phase, on the faithfulness proof, and on the flattener.

1.2.2. The Virtual Machine

Unlike the compiler phase, which consists of a sequence of essentially separate algorithms, the interpreter comprises a single program. However, the interpreter design is built up by a succession of refinement steps.

These refinement steps are designed to display the successive implementation decisions in a sort of rational reconstruction of the Scheme48 virtual machine. At each stage it must be shown that the new implementation decisions provide a state machine faithful to the behavior of the previous machine. There are three steps, the first two of which are strong refinements, while the last is a weak refinement in the “partial correctness” sense mentioned above. The three refinements interconnect the following four machines, of which the first provides the operational semantics for the output of the extended compiler, and of which the last is implemented directly using the PreScheme primitives.

Draft of September 29, 1993

• The stored program machine, or spm, which executes the byte code images produced by the image builder;

• The microcoded stored program machine, or mspm, which defines the steps of the spm as compositions of atomic state observer and state modifier operations;

• The garbage-collected state machine, or gcsm, which may nondeterministically stop and copy its live data to a fresh heap. The heaps of this state machine (and its predecessors) are of unbounded size, and each location may store an unbounded integer or pointer (among other objects);

• The finite garbage-collected state machine, or fgcsm, which has heaps of bounded size and has a bound on the width of an integer or pointer.

Naturally the fgcsm can not carry out all of the computations of the gcsm; it is correct only in the sense that when it does compute an answer, that is the same value that the gcsm would have computed.

These successive abstract machines are all visible in the code of the vlisp vm. The primitive notions of each machine are shown as procedures or constants, which are in turn implemented in terms of the primitives of the next machine (or primitives of PreScheme, in the case of the last). Thus, each state machine in the sequence of refinements corresponds closely to the program text above a particular abstraction barrier.

There is, however, one complication in matching the program to the specification. It is due to the fact that vlisp PreScheme compiles to a language in which all procedure calls are in tail recursive position. The Front End must substitute the code for a called procedure in line wherever there is a call in the source that is not tail recursive. There are several instructions in the spm that cause memory to be allocated, and each of them, when coded in the obvious way, contains a call to an allocation routine, which in turn calls the garbage collector if the allocation would exceed a bound. These calls are not tail recursive, as the original procedure must normally do some initializations within the new memory object after it has been allocated. Rather than have the code for the garbage collector duplicated in line at each of the original call sites, we have programmed the calls to the allocation procedure and garbage collector in a partial continuation passing style. Because this programming decision affects only a small number of call sites, and only one subroutine, the implementation has lost very little lucidity as a consequence of this programming approach.

Draft of September 29, 1993

Of the three main correctness assertions for the virtual machine, the first and third need relatively little scrutiny, provided in the short Sections 5 and 7.

The interesting step (see Section 6) is to show that the garbage collected state machine refines its predecessor, the mspm. To prove this we provide a storage layout relation ∼ between the mspm and the gcsm. The relation ∼ expresses that the stores of the two states, when regarded as directed graphs and restricted to the portion reachable from abstract machine registers, are isomorphic. There are then conceptually two assertions to be proved:

1. When each of the two machines makes an ordinary (non-GC) transition, related states evolve to related states; and

2. When s_{mspm} ∼ s_{gcsm} and garbage collection produces sgcsm^{′} from s_{gcsm}, then s_{mspm} ∼ sgcsm^{′}.

Of these the former establishes that garbage collection is a valid implementation strategy for the mspm, i.e., that the eventual result of the computation depends only the isomorphism class of the reachable part of the store. The second assertion shows that the particular garbage collection algorithm used is a correct algorithm.

2. The Byte-Code Compiler

The vlisp implementation is a byte-coded one, and the task of the compiler is to produce byte codes from a Scheme source program. The denotation of the resulting byte code program is equivalent to the denotation of the Scheme source program in a sense made precise in Section 2.5.

The byte code compiler itself is based on algorithms used by Clinger [2] and Kelsey and Rees [13]. Its purpose is to analyze the procedural structure of the source code. It distinguishes tail-recursive procedure calls from non-tail-recursive ones; it puts conditional expressions into a more explicit procedural form; and it calculates ⟨over, back⟩ lexical addresses for lexical variables, which it distinguishes from global variables.

The algorithm itself is a syntax-directed recursive descent, based on the abstract syntax shown in Table 1. We regard this bnf as determining a set of tree-like abstract syntax objects, rather than as recognising a set of flat character strings. The tree-like abstract syntax objects are represented by nested sequences. Thus for instance, a concrete program of the form (lambda (x . y) body) has as its abstract syntax:

Draft of September 29, 1993

e, E ::= i | c_{sq} | ⟨quote c⟩ | e^{+} | ⟨begin⟩^{⌢}e^{+}

            | ⟨lambda i* e⟩ | ⟨dotted lambda i^{+} e⟩

| ⟨if e_{1} e_{2} e_{3}⟩ | ⟨if e_{1} e_{2}⟩ | ⟨set! i e⟩
c, K ::= c_{pr} | strings | lists, dotted lists, and vectors of c
c_{pr} ::= numbers, booleans, characters, symbols and nil
c_{sq} ::= numbers, booleans, characters and strings
i, I ::= identifiers (variables)
Γ ::= e  (commands)

Table 1: Scheme Abstract Syntax

     ⟨dotted lambda ⟨xy⟩ e⟩

where e represents the abstract syntax of the body. This abstract syntax is only slightly more abstract than the result of the normal Scheme reader, when lists are regarded as representing mathematical sequences. Dotted lambda forms are the main case in which the abstract syntax differs; we find this form slightly more explicit.

The compiler’s target language is the byte code language abstract syntax defined in Table 2. Expressions of the Basic Byte Code language (bbc) are nested sequences constructed according to the bnf grammar given in Table 2 from natural numbers, Scheme identifiers, Scheme constants, and the keywords shown. We will use n-like variables for natural numbers, i-like variables for identifiers, and c-like variables for constants. Similarly for the classes defined by the grammar, with

t for (bbc) templates,

b for (bbc) closed instruction lists (conjecturally < Eng. block), z for (bbc) neutral instructions, y for (bbc) open instruction lists, w for (bbc) (general) instruction lists, and m for (bbc) (machine) instructions.

This syntax is a little more complex than might have been expected. The distinction between open and closed instruction lists captures a pattern in the code produced by the compiler. When a conditional expression is the last Scheme expression in the block being compiled, the compiler can ar-

Draft of September 29, 1993

t ::= ⟨lap c b⟩
b ::= ⟨⟨return⟩⟩ | ⟨⟨call n⟩⟩ | ⟨⟨unless-false b_{1} b_{2}⟩⟩
| ⟨make-cont b_{1} n⟩:: b_{2} | z:: b_{1}

   z ::= ⟨unless-false y_{1} y_{2}⟩
       | ⟨literal c⟩ | ⟨closure t⟩
       | ⟨global i⟩ | ⟨local n_{1} n_{2}⟩
       | ⟨set-global! i⟩ | ⟨set-local! n_{1} n_{2}⟩
       | ⟨push⟩ | ⟨make-env n⟩
       | ⟨make-rest-list n⟩ | ⟨unspecified⟩
       | ⟨checkargs= n⟩ | ⟨checkargs>= n⟩

| ⟨i⟩
y ::= ⟨make-cont y_{1} n⟩:: b | ⟨make-cont ⟨⟩ n⟩:: b | z:: y_{1} | ⟨z⟩
w ::= b | y

   m ::= z | ⟨return⟩ | ⟨call n⟩ | ⟨unless-false b_{1} b_{2}⟩
       | ⟨make-cont w_{1} n⟩

Table 2: Grammar for the Basic Byte Code

range that the code of each branch will contain a call or return instruction, so that there need be no common code to be executed after either branch has completed. On the other hand, when the conditional expression is not the last Scheme expression in the block, the compiler arranges that neither branch is terminated by a call or return. Thus, execution “drops into” the following code when the selected branch is completed.

After taking cases based on the abstract syntax class of the expression being compiled, the algorithm combines the code produced by its recursive calls with some additional instructions. The main dispatch and one typical case are shown in slightly simplified form in Figure 1. The parameters are:

• The expression being compiled;

• A “compile-time environment,” which associates identifiers serving as lexical variables with their lexical addresses. It is enriched when the algorithm traverses a lambda;

• The “after code” to be attached at the end of the code generated from the current expression; it represents the result of a recursive call.

The Scheme code implementing the algorithm can be safely regarded as a presentation of a mathematical algorithm. It is purely applicative; it makes no use of call/cc; and it has the form of a primitive recursion

Draft of September 29, 1993

(define (comp exp cenv after)
(cond ((id? exp)
 (compile-id exp cenv after))
((self-quoting-constant? exp)
 (compile-constant exp cenv after))
((pair? exp)
 (case (car exp)
   ((lambda) (compile-lambda exp cenv after))
   ((if) (compile-if exp cenv after))
   ...
   (else
    (compile-application exp cenv after))))
(else (compiler-error ...))))
(define (compile-application exp cenv after)
(if (return? after)
(let* ((proc (car exp))
     (args (cdr exp))
     (nargs (length args)))
(comp-args args cenv
           (comp proc cenv
                 (instruction->code-sequence
                  (make-instruction 'call nargs)))))
(compiler-prepend-instruction
(make-instruction 'make-cont after)
(compile-application exp cenv return-code))))
(define (comp-args args cenv after)
(if (null? args)
after
(comp (car args) cenv
    (compiler-prepend-instruction
     (make-instruction 'push)
     (comp-args (cdr args) cenv after)))))

Figure 1: Compiler dispatch procedure, and case for procedure call. on its expression argument, so that it is guaranteed to terminate. In the procedure to compile a procedure call, the call is tail recursive just in case the the “after code” consists of a bare return instruction. If the call is not tail recursive, then the resulting code will consist of a make-continuation instruction prepended in front of the corresponding tail recursive code. In the tail recursive case, it emits code to evaluate each argument, followed by a push instruction, and followed by code to evaluate the procedure. At the very end, a call instruction applies the procedure value to its evaluated arguments.

Draft of September 29, 1993

Syntactic correctness. If e is a Scheme expression, then C(e, ρ_{C}, n, i, w) will refer to the result of calling the procedure comp on e together with the compile-time environment ρ_{C} and the after-code w (assumed to be a bbc instruction sequence). We will also use C(e) to refer to the result of calling the procedure comp on e with the initial values of the other parameters.

Theorem 1 (Compiler syntactic correctness)

1. C(e) is a bbc template t;

2. C(e, ρ_{C}, b_{0}) is a bbc closed instruction sequence b_{1};

3. C(e, ρ_{C}, y_{0}) is a bbc open instruction sequence y_{1};

4. C(e, ρ_{C}, ⟨⟩) is a bbc open instruction sequence y_{1}.

The proof is a bulky but routine simultaneous structural induction on the Scheme syntax.

Since the algorithm is so straightforward a recursive descent, it is natural to use induction on the structure of expressions as a proof technique. Clinger [2] provides us with three suitable induction hypotheses which jointly establish the correctness of the algorithm. They appear below as Lemma 11. However, there is a striking difference between the official Scheme semantics and the simplified (and historically earlier) semantics that Clinger used in his paper, deriving from the fact that the official Scheme semantics makes provision for procedures that may return more than one value.

2.1. The Scheme Semantics

In this section we will briefly describe the official Scheme semantics, in the slightly modified form we have used in the vlisp project. Apart from a few cosmetic changes of notation, our version differs from the standard one in three ways. See [19] for a description of the underlying approach, and [9] for additional details.

Draft of September 29, 1993

⟨ … ⟩  finite sequence formation, commas optional
#s  length of sequence s
⟨ x … ⟩  sequence s with s(0) = x
⟨ … x ⟩  sequence s with s(#s − 1) = x
rev s  reverse of the sequence s
s^{⌢}t  concatenation of sequences s and t
s † k  drop the first k members of sequence s
s ‡ k  the sequence of only the first k members of s
p → a, b  if p then a else b
ρ[x/i]  the function which is the same as ρ

except that it takes the value x at i

x in D  injection of x into domain D
x | D  projection of x to domain D
x, y, …: D true if the type of x, y, … is a disjoint sum

and x, y, … are injected from elements of D

Table 3: Some Notation

• The domains have been made somewhat more concrete. In particular, L has been identified with N, and S has been identified with E*. Note that this entails that, at the current level of modeling, memory is conceived as unbounded.

• We have removed tests from the semantics to check whether a new storage location can be allocated in S. The official Scheme semantics uses conditionals that raise an “out of memory” error if there is no unallocated location; when memory is conceived as unbounded, this situation will not arise. Moreover, it does not seem that all situations in which a real Scheme interpreter can run out of memory are represented in the official semantics, for instance, overflowing the stack by too many nested, non-tail-recursive procedure calls. Thus, we have chosen to represent all memory exhaustion errors uniformly at a much lower level in the formal specification.

• The constraints on K given in the section on Semantics of Constants has been added. It was needed in our work on the faithfulness of an operational semantics for the bbc to its denotational semantics.

The domains used in the denotational semantics of Scheme are presented in Table 4. Note that exactly one “domain equation” is actually not an equation. It implicitly introduces an isomorphism between E and a disjoint

Draft of September 29, 1993

14 GUTTMAN, SWARUP, RAMSDELL

α ^{∈} L = N  locations
ρ ^{∈} U = Ide → L  environments
ν ^{∈} N  natural numbers
T = {false, true}  booleans
T_{L} = {mutable, immutable} mutability flags
Q  symbols
H  characters
R  numbers
E_{p} = L × L × T_{L}  pairs
E_{v} = L* × T_{L}  vectors
E_{s} = L* × T_{L}  strings
M = T + T_{L} + {null, empty, unspecified}

miscellaneous

ϕ ^{∈} F = L × (E* → K → C)  procedure values
ϵ ^{∈} E  ≅ Q + H + R + E_{p} + E_{v} + E_{s} + M + F

expressed values

σ ^{∈} S = E*  stores
θ ^{∈} C = S → A  command continuations
κ ^{∈} K = E* → C  expression continuations
A  answers
X  errors

Table 4: Domains for the Semantics of Scheme

K : Con → E
E : Exp → U → K → C
E* : Exp* → U → K → C
C : Com* → U → C → C

Table 5: Scheme Semantic Functions sum, say ψ_{E} : E≅ E_{Σ}. Although A is not explicitly defined, we will stipulate throughout the remainder of this paper that it is some domain containing a ⊥ and also numbers.

Draft of September 29, 1993

Semantics of Constants. The semantics of constants, given by a function K, will not be completely defined. Rather, we will give constraints on this function. In essence, we consider its actual value to be a parameter to the semantics of Scheme. We do explicitly define its behavior on primitive constants, i.e. constants not requiring storage at run-time.

c : Q ∨ c : H ∨ c : R ⇒ K[[c]] = c

K[[nil]] = null in E; K_{0}[[#f]] = false in E; and K_{0}[[#t]] = true in E

In addition, we constrain its behavior on objects, namely strings, vectors, and pairs, that do require storage and can be named by constants. There are three conditions:

1. Types and lengths are correct:

(a) If c is a string of length n, and K[[c]] is a non-bottom value ϵ, then ϵ : E_{s}, and #(ϵ | E_{s} 0) = n;

(b) If c is a vector of length n, and K[[c]] is a non-bottom value ϵ, then ϵ : E_{v}, and #(ϵ | E_{v} 0) = n;

(c) If c is a pair (and thus also if it is list or dotted list), and K[[c]] is a non-bottom value ϵ, then ϵ : E_{p}.

2. The immutability bit is set: if c is a string or vector, and K[[c]] is a non-bottom value ϵ, then (ϵ | D) 1 = immutable, where D is either E_{s} or E_{v}. Similarly, if c is a pair, and K[[c]] is a non-bottom value ϵ, then (ϵ | E_{p}) 2 = immutable.

3. Subexpressions are well-defined: if c_{0} is a vector or pair, and K[[c_{0}]] is a non-bottom value ϵ, and c_{1} is a subexpression of c_{0}, then K[[c_{1}]] is also non-bottom.

As an inductive consequence of the first condition, we may infer that in no case does K[[c]] : F hold. It also follows that the only real freedom in the definition of K concerns which locations are occupied by storage-requiring objects such as lists and vectors.

Semantics of Expressions. We give the clauses associated with procedure call as a sample of the Scheme semantics. Permute and unpermute are functions that determine the order of evaluation; they are fully specified in [9].

Draft of September 29, 1993

ψ ^{∈} K_{1} = E → C  one argument expression continuations
ρ_{R} ^{∈} U_{R} = N → N → L runtime environments
π ^{∈} P = E → E* → U_{R} → K_{1} → C

code segments

Table 6: Byte Code Semantics: Additional Domains

E[[E_{0} :: E*]] =

λρκ . E*(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) κ)

(unpermute ϵ*)))

E*[[⟨⟩]] = λρκ . κ⟨ ⟩

E*[[E_{0} :: E*]] = λρκ . E[[E_{0}]] ρ (single(λϵ_{0} . E*[[E*]] ρ (λϵ* . κ (⟨ϵ_{0}⟩^{⌢}ϵ*))))

single : (E → C) → K single =

λψϵ* . #ϵ* = 1 → ψ(ϵ* 0),

wrong “wrong number of return values”

applicate : E → E* → K → C applicate =

λϵϵ*κ . ϵ : F → ((ϵ | F) 1)ϵ*κ, wrong “bad procedure”

2.2. The Byte Code Semantics

One can understand a byte code program as operating on a state with four “registers”, so to speak. These are a value register, containing an element of E, an argument stack, an environment register, and a continuation register, where the continuations here take only a single value, unlike the multiple value continuations of the official Scheme semantics. A program, when applied to values of these four kinds, yields a command continuation θ ∈ C. This in turn, if given a store σ, determines an answer. Thus, a code segment determines a computational answer if four registers and a store are given.

This view is expressed formally in the signature of the domain π of code segments, as it appears in Table 6. Representative semantic clauses stated

Draft of September 29, 1993

B : b ∪ {⟨⟩} → U → P
Z : z → U → P → P
Y : y ∪ {⟨⟩} → U → P → P
T : t → U → P

(The variable y′ will range over y ∪ {⟨⟩}.)

Table 7: Byte Code Semantic Functions

B[[⟨⟩]] = λρϵϵ*ρ_{R}ψσ . ϵ : R → ϵ | R in A, ⊥ B[[z:: b]] = λρ . Z[[z]]ρ (B[[b]]ρ) B[[⟨make-cont b_{1} n⟩:: b_{2}]] = λρ . make cont (B[[b_{1}]]ρ)n(B[[b_{2}]]ρ) B[[⟨⟨return⟩⟩]] = λρ . return B[[⟨⟨call n⟩⟩]] = λρ . call n Y[[⟨make-cont y′ n⟩:: b]] = λρπ . make cont (Y[[y′]]ρπ) n (B[[b]]ρ) Y[[z:: y′]] = λρπ . Z[[z]]ρ (Y[[y′]]ρπ) Y[[⟨⟩]] = λρπ . π Z[[⟨literal c⟩]] = λρ . literal (K[[c]]) Z[[⟨closure t⟩]] = λρ . closure (T [[t]]ρ) Z[[⟨global i⟩]] = λρ . global (lookup ρ i) Z[[⟨set-global! i⟩]] = λρ . set global (lookup ρ i) T [[⟨lap c b⟩]] = B[[b]]

Table 8: Byte Code Semantical Clauses

in terms of these semantic functions are presented in Table 8.

The clause for a null code sequence defines the “answer function,” that is, the way that a computational answer in A is determined when the “program register” contains no more code and the program has thus completed execution.

The auxiliary functions (among them, those in Table 9) follow the Wand-Clinger style of byte code specification. In each case, the auxiliary function takes as arguments:

• the denotations of the arguments to the instruction (if necessary);

• the denotation of the code following the current instruction; make cont : P → N → P → P make cont =

Draft of September 29, 1993

λπ′νπ . λϵϵ*ρ_{R}ψ . #ϵ* = ν → πϵ⟨⟩ρ_{R}(λϵ . π′ϵϵ*ρ_{R}ψ),

wrong “bad stack”

call : N → P

call = λν . λϵϵ*ρ_{R}ψ . #ϵ* = ν → applicate ϵϵ*(single ψ),

wrong “bad stack”

return : P

return = λϵϵ*ρ_{R}ψ . ψϵ

push : P → P

push = λπ . λϵϵ*ρ_{R}ψ . πϵ(ϵ*^{⌢}⟨ϵ⟩)ρ_{R}ψ

lookup : U → Ide → L lookup = λρI . ρI

Table 9: Byte Code Auxiliary Functions

• a sequence of four arguments, ϵ, ϵ*, ρ_{R}, ψ, representing the contents of the value register, the argument stack, the environment register, and the continuation register respectively.

In typical cases, such as for instance make cont, the definition returns a value of the form πϵ′ϵ_{1}*ρ′_{R}ψ′ for non-erroneous arguments. In effect, the instruction has invoked the remainder of the code in a new state, computed from the arguments given. Thus one may view the semantic computation of a final result as consisting of a sequence of terms of this form. The first term in the sequence is determined directly by applying the semantic clauses to the byte code program, together with some initial values. Each successive term is the result of expanding the definition for the auxiliary function used in the head instruction, followed by β-reductions and evaluations of conditionals.

Some auxiliaries, such as return, by contrast, do not take this form. However, if the continuation argument ψ has been created by a make cont, then ψ has the form (λϵ . π′ϵϵ*ρ_{R}ψ′), so that ψϵ β-reduces to a term of the requisite form π′ϵϵ*ρ_{R}ψ′. A similar relation links call to the auxiliary closure, which creates procedure values.

These observations were a basic part of the motivation for the Wand-

Draft of September 29, 1993

Variable Value
ρ  F ↦ ℓ_{1}
σ  ℓ_{1} ↦ ϕ_{1}; ℓ_{2} ↦ unspecified
κ  λϵ*σ . #ϵ*
ϕ_{1}  ⟨ℓ_{2}, λϵ*κσ . κ⟨1, 2, 3⟩⟩

Table 10: Naïve Counterexample to Single-Valued Implementations

Clinger approach, and they served to motivate our approach to proving the faithfulness of the operational semantics. They can also serve as the basis for a proof of adequacy, such as is given in [16, Theorem 6], which would establish that an operational semantics computes all the non-erroneous, non-bottom answers predicted by the denotational semantics.

2.3. Multiple Values in the Scheme Semantics

The official semantics for Scheme allows a procedure to return several values to its caller, as would be needed to model the Common Lisp values construct or the T return form. However, ieee standard Scheme has no construct that allows a programmer to construct a procedure that would return more than one value. Assuming that a program is started with an initial store that hides no “multiple value returners,” then an implementation may assume that there will never be any in the course of execution. So, many implementations of Scheme, among them vlisp, do not support multiple return values. This contrast may be seen at the formal level in the contrast between the domain of expression continuations K, as used in Scheme semantics, and the domain of one argument expression continuations K_{1} which plays a corresponding role in the semantics of the byte code.

However, as a consequence, in the most literal sense, an implementation is unfaithful to the formal semantics as written if it makes no provision for multiple-value returners.

We can make this point clear with an example. Consider the program (F), which calls a procedure with no arguments. Given the values described in Table 10, we can easily see that the semantics predict that the correct computational answer is 3. However, saying that an implementation makes no provision for multiple-value returners is in effect to say that if κ is implemented at all, then it always results in a computational answer of 1.

In the next section, we will formalize the reasoning that justifies an implementation in assuming it need implement only “single-valued” objects,

Draft of September 29, 1993

ϕ_{p} ^{∈} F_{p} = E* → K → C pure (untagged) procedure values

Table 11: Pure Procedure Objects

and need make no provision for multiple value returns.

In essence our approach is to introduce a new, “smaller” semantics for Scheme. In this semantics, it is clear that there is no mechanism for multiple return values. With this alternate semantics, called (sva E), in place, there are two separate facts that must be proved to justify the compiler algorithm.

1. The alternate semantics is faithful to the standard semantics, at least in the intended case in which the initial givens harbor no multiple value returns:

E[[e]]ρ κ σ = (sva E)[[e]]ρ κ σ,

when κ and σ, the halt continuation and the initial store respectively, are unproblematic, single-valued objects in a sense to be defined.

2. The compiled byte code is faithful to the alternate semantics, in the

sense that

(sva E)[[e]]ρ and B[[C(e)]]ρ

yield the same answer when applied to suitable initial values.

We will introduce for convenience a new explicitly defined domain of pure procedure objects. Unlike the procedure objects in F (which equals L × (E* → K → C)), those in F_{p} contain only the function-like part (namely E* → K → C), without the location that serves as a tag (see Table 11). The location tags are used to decide whether two procedure objects are the same in the sense of the Scheme standard procedure eqv?. So F = L × F_{p}. It will also be convenient to define a few auxiliary functions:

Definition 1 (Auxiliaries)

1. zeroth : E* → E is the strict function returning ⊥_{E} if its argument ϵ* is either ⊥_{_{E}*} or ⟨⟩, and which returns (ϵ* 0) otherwise.

2. truncate : E* → E* is the non-strict function which takes its argument ϵ* to ⟨zeroth ϵ*⟩. Hence #(truncate ϵ*) = 1, even for ϵ* = ⊥_{_{E}*}.

3. one arg : K → K_{1} is defined to equal λκϵ . κ⟨ϵ⟩

Draft of September 29, 1993

4. multiple : K_{1} → K is defined to equal λψϵ* . ψ(zeroth ϵ*)

The auxiliaries one arg and multiple coerce from K to K_{1} and back. The name truncate is quite long, and we sometimes prefer to truncate it as trunc. Expanding the definitions, we have:

Lemma 2 1. one arg(multiple ψ) = ψ;

2. multiple(one arg κ) = λϵ* . κ(truncate ϵ*).

We define next the function sva, which, given any object in Ω, returns the single-valued object that approximates it. As we will see, sva ω always belongs to the same summand of Ω as ω. Moreover, sva is idempotent, so that we can think of its range as determining the single-valued objects. We will extend sva immediately after defining it so that it may be applied to elements of the disjoint summands of Ω, in addition to the elements of Ω itself.

The heart of sva is its behavior on pure procedure objects ϕ_{p}. A pure procedure object ϕ_{p} is altered to another function ϕ′_{p}, such that ϕ′_{p} calls ϕ_{p} with the same expressed value arguments and the same store. Only the continuation argument is altered, to ensure that the modified continuation can access only one expressed value, and only a single-valued approximation to that. Similarly, only a single-valued approximation to the contents of the new store is made available to the continuation. Crudely put, ϕ′_{p} cannot pass anything infected with multiple values to its continuation, whether in the store, or by making available more than one return value itself, or by hiding it in a procedure value that would later, when applied, make more than one value available to its continuation.

As for the uncontroversially given domains that do not involve E, sva is the identity. For all other domains, sva commutes in the obvious way with the constructor of the domain.

Recall that we write E_{Σ} for Q + H + R + E_{p} + E_{v} + E_{s} + M + F, and ψ_{E} for the isomorphism from E to E_{Σ}. We assume E to be indecomposable in the sense that that it is not produced by any of the domain-constructing operators →, +, ^{∗}, and ×, which produce function domains, disjoint union domains, sequence domains, and product domains respectively. We also assume these operators are formalized so that given a domain, we can read off at most one operator and one list of argument domains that produced it.

We define Ω to be the disjoint sum (in any order) of a set C_{Ω} of domains, where C_{Ω} is the least set containing all of the Scheme denotational domains (including E_{Σ}) and such that 1. every argument of every element of C_{Ω} is an element of C_{Ω}, and

Draft of September 29, 1993

2. if D is constructed by a basic constructor from a finite sequence of arguments in C_{Ω}, then D is an element of C_{Ω}.

Given f : Ω → Ω, say that f respects types if f is strict and for every D in C_{Ω} and every x in Ω such that x : D, we have fx : D; also, for each D in C_{Ω}, let f^{D} : D → D be defined, for d ∈ D, to be

f^{D}d = (f(d in Ω)) |D.

As a preliminary step towards single-valued approximations, define an operator α : (Ω → Ω) → (Ω → Ω) as follows. Let f : Ω → Ω and ω ∈ Ω be arbitrary. Then αfω is

(a) if ω = ⊥_{Ω}, then ω

(b) if ω : D for an indecomposable D other than E, then ω,

(c) if ω : E, then

(ψE^{−1}(f(ψ_{E}(ω|E) in Ω)|E_{Σ})) in Ω,

(d) if ω : D for a decomposable D other than F_{p}, then associate with each argument D_{i} of D the functional f^{D_{i}} : D_{i} → D_{i}, lift these to g : D → D, and take g(ω|D) in Ω, and

(e) if ω : F_{p}, then

(λϵ*κ . (ω | F_{p}) (f^{^{E}*} ϵ*) (λϵ* . (f^{C}(κ (truncate (f^{E} ∘ ϵ*)))))) in Ω,

(here (f^{E} ∘ ϵ*) is taken to be ⊥_{_{E}*} for ϵ* = ⊥_{_{E}*})

All of the real work of α is done by the truncation in the last case. In all cases, if ω : D, then αfω : D; because in addition αf is strict, for all f : Ω → Ω, αf respects types.

Definition 2 (Single-valued approximation) sva : Ω → Ω is the least fixed point of the above α.

For D ∈ C_{Ω} and d ∈ D, we will abuse notation by writing sva d for sva^{D} d, i.e., for (f(d in Ω)|D). The following lemma provides the crucial justification for regarding sva as providing an alternative semantics.

Lemma 3 sva is idempotent.

Draft of September 29, 1993

Proof: If we let f_{0} = ⊥_{Ω→Ω}, and f_{n+1} = αf_{n}, then sva is the supremum of the f_{n} for n ∈ N. Define a strict g_{0} : Ω → Ω by letting g_{0} ω = ⊥_{D} in Ω whenever ω : D (so each g_{0}^{D} = ⊥_{D→D}). Then g_{0} is least type-respecting element of Ω → Ω. Let g_{n+1} = αg_{n}. As g_{1} respects types, g_{0} ⊑ g_{1} and by the monotonicity of α, g_{n} ⊑ g_{n+1}. Since f_{1} respects types, f_{0} ⊑ g_{0} ⊑ f_{1}, so that the supremum of the g_{n}’s is also sva. For h : Ω → Ω, let P (h) mean that

(i) h respects types; (ii) each h^{D} is strict; and (iii) h is idempotent.

Since the supremum of idempotent elements of Ω → Ω is idempotent, and P (g_{0}) holds, it suffices to establish that α preserves the property P. Take an arbitrary f such that P (f) and let h be αf. We already know that (i) holds, and (ii) follows easily taking cases on D. For idempotence of h, pick an arbitrary ω ∈ Ω; the only interesting case is (e). Let ω : F_{p}; we must show that (α f)(α f ω) = (α f ω). By (e), the former (projected into F_{p} for convenience) equals:

λϵ*κ . (λϵ*κ . (ω | F_{p})(fE*ϵ*)(λϵ_{0}* . fC(κ(trunc(fE ∘ ϵ_{0}*)))))
(fE*ϵ*)(λϵ_{1}* . fC(κ(trunc(fE ∘ ϵ_{1}*))))
= λϵ*κ . (ω | F_{p})(fE*(fE*ϵ*))
(λϵ_{0}* . fC(fC(κ(trunc(fE ∘ (trunc(fE ∘ ϵ_{0}*)))))))
= λϵ*κ . (ω | F_{p})(fE*ϵ*)
(λϵ_{0}* . fC(κ(trunc(fE ∘ (trunc(fE ∘ ϵ_{0}*)))))),

We have used β-reduction twice in the first step, and the idempotence of f and therefore also f^{D} in the second. So it suffices to prove that

trunc(fE ∘ (trunc(fE ∘ ϵ_{0}*))) = trunc(fE ∘ ϵ_{0}*),

which follows easily taking cases on whether 0 < #ϵ_{0}*.

By the convention that (svax) = x when x belongs to a syntactic domain such as the Scheme expressions, we may apply sva to the semantic functions K, E, E*, and C. Since Scheme has no syntax for constants denoting procedure objects, both c and K[[c]] are necessarily single-valued, so that (sva K) = K. However, the remaining semantic functions are not single valued, and the alternative semantics consists in replacing them with their single-valued approximations (sva E), (sva E*), and (sva C).

Draft of September 29, 1993

2.4. Faithfulness of the Alternative Semantics

The alternative semantics is faithful in the sense that, for every Scheme expression e, it delivers the same computational answer as the official semantics, provided that a single-valued initial continuation and store are supplied. As mentioned previously, it is reasonable for a Scheme implementation to provide a single-valued store. Moreover, many natural initial continuations (which, intuitively, say how to extract the computational answer if the program finally halts) are single-valued. For instance, the vlisp operational semantics for the Tabular Byte Code Machine is justified against the denotational semantics using the initial continuation:

halt = λϵ*σ . (ϵ* 0) : R → (ϵ* 0) | R in A, ⊥

which is single-valued.

Theorem 4 (Faithfulness of Alternative Semantics)

1. For all Scheme expressions e, environments ρ, expression continuations κ, and stores σ,

(sva E)[[e]]ρ κ σ = E[[e]]ρ (sva κ) (sva σ)  (1)

2. Let κ = sva κ and σ = sva σ. Then

E[[e]]ρ κ σ = (sva E)[[e]]ρ κ σ

Proof: 1. We simply use the definition of sva, together with the fact that the domain of Scheme expressions, the domain of environments, and the domain of answers do not involve E:

(sva E)[[e]]ρ κ σ = (sva(E[[sva e]]))ρ κ σ
= (sva(E[[e]](sva ρ))) κ σ
= (sva(E[[e]]ρ (sva κ))) σ
= (sva(E[[e]]ρ (sva κ) (sva σ)))
= (E[[e]]ρ (sva κ) (sva σ))

2. We use the assumption that κ and σ are single-valued, followed by Equation 1, from right to left:

E[[e]]ρ κ σ = E[[e]]ρ (sva κ) (sva σ)
= (sva E)[[e]]ρ κ σ

Draft of September 29, 1993

Corollary 5 For all values of e, ρ, κ, and σ:

(sva E)[[e]]ρ κ σ = (sva E)[[e]]ρ (sva κ) σ
= (sva E)[[e]]ρ κ (sva σ)
= (sva E)[[e]]ρ (sva κ) (sva σ)

Proof: Use Equation 1 and the idempotence of sva repeatedly.

A further partial justification for the single-valued semantics that we have introduced is that it allows us to eliminate the operator single from the semantic clauses in which it occurs, and to truncate any continuation. These two facts are intuitively significant, as they amount to saying that the meaning of a Scheme expression, if it invokes its expression continuation at all, applies it to a sequence ⟨ϵ⟩ of length 1. Hence they justify the claim that the alternate semantics ensures that procedures never return multiple values.

Theorem 6 (Truncate Continuations)

(sva E)[[E]]ρ κ = (sva E)[[E]]ρ (λϵ* . κ (trunc ϵ*))

Proof: The proof is by induction on E. The cases where E is a constant, an identifier, a lambda expression, a dotted lambda expression, or an assignment are immediate from the definitions of send and hold. The cases for two- and three-expression if, and for begin, are immediate from the induction hypothesis. Hence the only case of interest is for procedure call, which is as it should be. Using the semantics of procedure call, we must show

(sva E*)(permute(⟨E_{0}⟩^{⌢}E*))ρ κ_{1} = (sva E*)(permute(⟨E_{0}⟩^{⌢}E*))ρ κ_{2}

where

κ_{1} = λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) κ)(unpermute ϵ*)) κ_{2} = λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) (λϵ* . κ (trunc ϵ*)))(unpermute ϵ*))

Pushing svas through κ_{1}, we obtain:

λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (svaκ)(trunc ϵ*))))

(sva(unpermute (svaϵ*))))

Pushing svas throughκ_{2} yields:

λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (λϵ* . sva(κ (sva(trunc ϵ*))))

(trunc ϵ*))))

(sva(unpermute (svaϵ*)))).

Draft of September 29, 1993

For these two expressions to be equal, it certainly suffices that for all κ,

λϵ* . (svaκ)(trunc ϵ*) = λϵ* . (λϵ* . sva(κ (sva(trunc ϵ*))))(trunc ϵ*)

Using the definition of sva and the idempotence of trunc, we have:

λϵ* . (svaκ)(trunc ϵ*)
= λϵ* . sva(κ (sva(trunc ϵ*)))
= λϵ* . sva(κ (sva(trunc (trunc ϵ*))))

Theorem 7 (“Single” eliminable)

(sva E)[[E]]ρ (single ψ) = (sva E)[[E]]ρ (λϵ* . ψ (ϵ* 0))

The very similar proof is also by induction on E.

2.5. Compiler Correctness for Single-valued Semantics

We will prove that if e is any Scheme program and b is the result of compiling it, then e and b are equivalent in the following sense:

Definition 3 (Computational equivalence ≡)

A Scheme program e and a byte code program b are computationally equivalent if, for every environment ρ and expression continuation κ,

(sva E)[[e]]ρκ = (svaB)[[b]]ρ unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

Definition 4 (Environment Composition) Consider ρ : Ide → L, ρ_{C} : Ide → (N × N ∪ {not lexical}), and ρ_{R} : N → N → L. Their environment composition ρ◁_{ρ_{C}}^{ρ_{R}} is the environment:

λi . ρ_{C} i = not lexical → ρ i, (λp . ρ_{R} (p 0)(p 1))(ρ_{C} i)

We will refer to objects like ρ_{C} and ρ_{R} as “compile-time environments” and “run-time environment” respectively.

Lemma 8 ρ◁mt_{C}^{ρ_{R}} = ρ.

Proof: For all i, mt_{C} i = not lexical. Hence, ρ◁mt_{C}^{ρ_{R}} i = ρ i, and, by
extensionality, ρ◁mt_{C}^{ρ_{R}} = ρ.

Draft of September 29, 1993

VLISP SCHEME 27

We state the main theorem next, and we will give its (short) proof using Lemma 11, which is due to Will Clinger [2]. A portion of the (longer) proof of Clinger’s lemma, for the vlisp compiler, is given below. Theorem 9 (Compiler correctness)

For any Scheme expression e and environment ρ,

e ≡ C(e).

Proof: The theorem is a direct consequence of Clinger’s lemma (Lemma 11 below), Clause 1. Since

C(e) = C(e, mt_{C}, 0, false, ⟨⟨return⟩⟩),

we let (svaB)[[C(e)]]ρ = π_{2}, (svaB)[[⟨⟨return⟩⟩]]ρ = return = π_{1}, and ψ = one arg κ. Substituting the initial values in the right hand side, we infer:

(svaE)[[e]] (ρ◁mt_{C}^{ρ_{R}}) (multiple λϵ . return ϵ⟨⟩ρ_{R}(one arg κ))
= π_{2} unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

Since return = λϵϵ*ρ_{R}ψ . ψϵ,

λϵ . return ϵ⟨⟩ρ_{R}(one arg κ) = λϵ . (one arg κ)ϵ
= (one arg κ),

and it follows that

(svaE)[[e]] (ρ◁mt_{C}^{ρ_{R}}) (multiple (one arg κ))

= π_{2} unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

By Lemmas 2 and 8, the left hand side equals:

(svaE)[[e]] ρ (λϵ* . κ(trunc ϵ*))

By Theorem 6, the latter equals (svaE)[[e]] ρ κ.

Lemma 10 (Compiled expressions set value register)

1. Let π = (svaB)[[C(e, ρ_{C}, n, i, b)]]ρ. For all ϵ, ϵ′, πϵ = πϵ′.

2. Let π = (svaY)[[C(e, ρ_{C}, n, i, y)]]ρπ_{0}. For all ϵ, ϵ′, πϵ = πϵ′.

3. Let π = (svaB)[[Cargs(e*, ρ_{C}, n, i, b)]]ρ, and let π_{1}(svaB)[[b]]ρ. If for all ϵ, ϵ′, π_{1}ϵ = π_{1}ϵ′, then for all ϵ, ϵ′, πϵ = πϵ′.

Draft of September 29, 1993

Proof: The proof is by simultaneous induction on e and e*. We show one case from the (very routine) induction. Clause 3: If e* = ⟨⟩, then Cargs(e*, ρ_{C}, n, i, b) = b. Otherwise, it is of the form:

C(e, ρ_{C}, n, i, ⟨push⟩:: Cargs(e_{1}*, ρ_{C}, n + 1, i, b)),

so that the result follows by Clause 1.

Lemma 11 (Clinger’s Lemma)

1. Consider any Scheme expression e, bbc closed instruction list b, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial value ϵ. Let π_{1} = (svaB)[[b]]ρ and π_{2} = (svaB)[[C(e, ρ_{C}, #ϵ*, i, b)]]ρ. Then

(svaE)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (multiple λϵ . π_{1}ϵϵ*ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ.

2. Consider any Scheme expression e, bbc open instruction list y, segment π, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial value ϵ. Let π_{1} = (svaY)[[y]]ρπ and π_{2} = (svaY)[[C(e, ρ_{C}, #ϵ*, i, y)]]ρπ. Then

(svaE)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (multiple λϵ . π_{1}ϵϵ*ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ.

3. Consider any sequence of Scheme expressions e*, bbc closed instruction list b, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial values ϵ and ϵ_{1}. Let π_{1} = (svaB)[[b]]ρ and π_{2} = (svaB)[[Cargs(e*, ρ_{C}, #ϵ*, i, b)]]ρ. Suppose that the after code sets the value register before it reads it, in the sense that, for all values ϵ′, π_{1} ϵ = π_{1} ϵ′. Then

(svaE*)[[e*]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ.

Proof: The proof is by a simultaneous induction on e and e*. That is, in proving 1 and 2, we assume that 1 and 2 hold for any proper subexpression of e, and that 3 holds when each expression in e* is a proper subexpression of e. When proving 3, we assume that 1 and 2 hold for each e occurring in e*, and that 3 holds of any proper subsequence of e*. To emphasize the treatment of the single-valued semantics, we give the proof of clause 3 in detail; the proofs of clauses 1 and 2 are very similar in manner to Clinger’s original proof [2].

3. Here we argue by induction on e*, assuming that 1 and 2 hold of the expressions occurring in e*.

Draft of September 29, 1993

Base Case Suppose that e* = ⟨⟩. Then, by the semantic clause for E*,

(svaE*)[[⟨⟩]](ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)
= sva((λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)⟨⟩)
= sva(π_{1}ϵ_{1}(ϵ*^{⌢}⟨⟩)ρ_{R}ψ)
= sva(π_{1}ϵ_{1}ϵ*ρ_{R}ψ).

Since π_{1} is single-valued, the latter equals π_{1}ϵ_{1}ϵ*ρ_{R}ψ. Examining the compiler’s code, Cargs(⟨⟩, ρ_{C}, #ϵ*, i, b) = b, so that π_{1} = π_{2}. Since, by assumption, π_{1} ϵ = π_{1} ϵ_{1}, the case is complete.

Induction Step Suppose that 3 holds for e* and and 1 holds for e, and consider e:: e*. Using the semantic clause for E*, and writing κ for λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ, the left hand side of our goal takes the form:

(sva E)[[e]](ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0}.(sva E)*[[e*]](ρ◁_{ρ_{C}}^{ρ_{R}})(λϵ*.κ(⟨ϵ_{0}⟩^{⌢}ϵ*))))

Applying κ,

(λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)(⟨ϵ_{0}⟩^{⌢}ϵ*)
= π_{1}ϵ_{1}(ϵ*^{⌢}(⟨ϵ_{0}⟩^{⌢}ϵ*))ρ_{R}ψ
= π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ

Hence, the left hand side equals:

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple (λϵ_{0} . (sva E*)[[e*]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ* . π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ)))

Applying the induction hypothesis with (ϵ*^{⌢}⟨ϵ_{0}⟩) in place of ϵ*, with the other variables unchanged, and letting

π_{3} = (svaB)[[Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ,

Lemma 10 shows (for all ϵ_{0}):

(sva E*)[[e*]](ρ◁_{ρ_{C}}^{ρ_{R}})(λϵ*.π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ) = π_{3}ϵ(ϵ*^{⌢}⟨ϵ_{0}⟩)ρ_{R}ψ

Plugging this in this, followed by Lemma 10, then the definition of push, and finally the semantics of push, we have:

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . π_{3} ϵ (ϵ*^{⌢}⟨ϵ_{0}⟩) ρ_{R} ψ))
= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . π_{3} ϵ_{0} (ϵ*^{⌢}⟨ϵ_{0}⟩) ρ_{R} ψ))
= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . (push π_{3}) ϵ_{0} ϵ* ρ_{R} ψ))
= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} .

(svaB)[[⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ

ϵ_{0} ϵ* ρ_{R} ψ))

Draft of September 29, 1993

We will apply Clause 1 with

b = ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b),

and thus with

π_{2} = (svaB)[[C(e, ρ_{C}, #ϵ*, i, ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ*+1, i, b))]]ρ.

Hence,

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})

(multiple(λϵ_{0} . (svaB)[[⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ

ϵ_{0} ϵ* ρ_{R} ψ))
= π_{2} ϵ ϵ* ρ_{R} ψ

But, by the code for Cargs, π_{2} is in fact equal to

(svaB)[[Cargs(e:: e*, ρ_{C}, #ϵ*, i, b)]],

as the latter is the code:

C(e, ρ_{C}, #ϵ*, i, ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)).

3. Operational Semantics: Faithfulness and Refinement

In this section we describe and justify the transition from the denotational method of the Wand-Clinger style proof of the byte code compiler to the operational framework that will be used for the state machine refinement proofs of the succeeding layers.

3.1. Operational Semantics

To equip a language with an operational semantics, we define a particular state machine and a function that maps programs p, possibly with additional parameters x⃗, to initial states. The machine may compute a computational answer of type A from this initial state. We will continue to assume that A is a fixed domain of which R is a summand. The denotation of p may then be taken to be the function which maps x⃗ to the unique value that results, if there is a unique value, and to ⊥_{A} otherwise.^{1}

1 For some kinds of non-deterministic state machines this definition would not be subtle enough. However, the state machine we shall use in our proof of faithfulness is deterministic. In a later stage of our work, we will need a state machine which is nondeterministic but “answer deterministic” as described below. An answer deterministic machine may have different computations starting from a particular state, but they all eventually produce the same computational result.

We would expect that only answer deterministic state machines would play a role as faithful operational refinements of a language with a deterministic denotational semantics, as Scheme’s essentially is.

Draft of September 29, 1993

We choose one convenient way of pinning down details among many which would suffice. First we define (possibly non-deterministic) state transition machines, these are 9-tuples

⟨states, inits, halts, inputs, null-in, outputs, null-out, acts, ans⟩

such that

(a) states, inputs, and outputs are disjoint sets with inits ⊆ states, halts ⊆ states, null-in ∈ inputs, and null-out ∈ outputs;

(b) acts ⊆ (states × inputs) × (states × outputs);

(c) for no pair ⟨s, i⟩ in the domain of actions is s ∈ halts; and

(d) ans : halts → A.

A state s is called a halt state if s ∈ halts, which is equivalent to ans(s) being well defined. If acts is actually a function, then the machine is deterministic.

Given such a machine M, let C be a non-empty, finite or infinite sequence of elements of states × inputs × outputs. Then C_{S} (the state history), C_{I} (the input history), and C_{O} (the output history), of C are, respectively, the derived sequences of states, inputs, and outputs components of C. C is a computation if C_{S}(0) ∈ inits, C_{O}(0) = null-out, and, for every i such that C(i + 1) is defined,

⟨⟨C_{S}(i), C_{I}(i)⟩, ⟨C_{S}(i + 1), C_{O}(i + 1)⟩⟩ ∈ acts.

A transition takes a pair of a current state and a current input and produces a next state and a next output. A state is accessible if it is C_{S}(i) for some computation C and integer i.

Call a state-input pair proceedable if it is in the domain of acts. A computation is maximal if it is infinite or its last state and last input comprise a non-proceedable pair. A finite, maximal computation is successful if its last state is a halt state; other finite, maximal computations are erroneous.

A computation is inputless if every element of its input history is null; it is outputless if every element of its output history is null; it is pure if it is both inputless and outputless. We will focus on pure computations, partly for simplicity, and partly because the official Scheme semantics does not impose a particular treatment of i/o on us. In the case of a pure computation, we will not distinguish between the computation C and the derived sequence of states C_{S}, as the former contains no real additional information.

Draft of September 29, 1993

3.2. Proving Faithfulness

The vlisp faithfulness proof works at the level of the tabular byte code tbc. This differs from the bbc only in that constants, embedded closures obtained from lambda expressions, and global variables have been gathered, along with disambiguating tags, into a sequence of entries (each of syntactic type d) called a “template table” (of syntactic type e). An index into the template table appears in place of their occurrences in the byte code.

The syntax of the tbc is presented in Table 12. The tokens of the tbc are the same as those of the bbc, with the addition of constant, and global-variable, and with lap being replaced by template. The defining productions are very similar to the ones given for bbc, but note that:

• in a template, the block now precedes an important table, instead of following an unimportant constant, and

   • literal, closure, global, and set-global! take integer arguments

here.

We will use n-like variables for natural numbers, i-like variables for identifiers, and c-like variables for constants.

3.2.1. Denotational Semantics of the Tabular Byte Code

The denotational semantics of the tbc, which is given in full in [9], is very similar to the semantics of the bbc. The main difference is that the semantic functions take an additional parameter—namely the template table e to be used—and the semantics of instructions that use the template table make reference to it. We expect the relevant template table entry to be of one of the forms:

     ⟨constant c⟩, ⟨global-variable i⟩, or ⟨template b e′⟩.

Naturally, in the first two cases, it is the value c or i that interests us, which we extract by applying the entry (a sequence) to the argument 1. The clause for closures takes the whole entry, which is an embedded template. The relevant instructions are shown in Table 13.

3.2.2. Operational Semantics of the Tabular Byte Code

The operational semantics of the tbc, which is given in full in [10], is determined by a state machine. That state machine uses, as the components of its states, objects from a syntax extending the tbc; we will call this the augmented byte code or abc.

The new abc tokens are locations (which are actually the same as natural numbers, but which for clarity we indicate by l-like variables when used as

Draft of September 29, 1993

z ::= ⟨unless-false y_{1} y_{2}⟩
| ⟨literal n⟩ | ⟨closure n⟩
| ⟨global n⟩ | ⟨local n_{1} n_{2}⟩
| ⟨set-global! n⟩ | ⟨set-local! n_{1} n_{2}⟩
| ⟨push⟩ | ⟨make-env n⟩
| ⟨make-rest-list n⟩ | ⟨unspecified⟩
| ⟨checkargs= n⟩ | ⟨checkargs>= n⟩

| ⟨i⟩

m ::= z | ⟨return⟩ | ⟨call n⟩ | ⟨unless-false b_{1} b_{2}⟩
| ⟨make-cont w_{1} n⟩

b ::= ⟨⟨return⟩⟩ | ⟨⟨call n⟩⟩ | ⟨⟨unless-false b_{1} b_{2}⟩⟩

| ⟨make-cont b_{1} n⟩:: b_{2} | z:: b_{1} y ::= ⟨make-cont y_{1} n⟩:: b | ⟨make-cont ⟨⟩ n⟩:: b | z:: y_{1} | ⟨z⟩ w ::= b | y

d ::= ⟨constant c⟩ | ⟨global-variable i⟩ | t

e ::= d^{∗}

t ::= ⟨template b e⟩

Table 12: Grammar for the Tabular Byte Code

B_{τ} : b ∪ {⟨⟩} → e → U → P
Z_{τ} : z → e → U → P → P
Y_{τ} : y ∪ {⟨⟩} → U → P → P  (The variable y′ ranges over y ∪ {⟨⟩})
T_{τ} : t → U → P

T_{τ} [[⟨template b e⟩]] = B_{τ} [[b]]e Z_{τ} [[⟨literal n⟩]] = λeρ . literal (K[[(e(n))(1)]]) Z_{τ} [[⟨closure n⟩]] = λeρ . closure (T_{τ} [[e(n)]]ρ) Z_{τ} [[⟨global n⟩]] = λeρ . global (lookup ρ ((e(n))(1)))

Table 13: Partial Semantics for the Tabular Byte Code

Draft of September 29, 1993

v ::= c | ⟨closure t u l⟩ | ⟨escape k l⟩

| ⟨mutable-pair l_{1} l_{2}⟩ | ⟨string l^{∗}⟩ | ⟨vector l^{∗}⟩ | unspecified | undefined

a ::= v^{∗}

u ::= empty-env | ⟨env u l^{∗}⟩
k ::= halt | ⟨cont t b a u k⟩
s ::= v^{∗}

Table 14: abc Syntactic Definition

locations) and the constructors appearing in small capotals in Table 14. The new abc syntactic categories, which will be defined by bnf, are

v for (abc) values,

a for (abc) argument stacks u for (abc) environments, k for (abc) continuations, and s for (abc) stores.

All of the categories (templates, blocks etc.) and productions given for tbc are included here. However, although we are extending the syntax, the additional productions do not feed back into the recursive construction of the old categories. Thus, the meanings of the old categories (as sets of tree-like objects) in the abc are exactly the same as in the tbc. The new productions are given in Table 14.

The states of a byte code state machine are the sequences of the form

⟨t, b, v, a, u, k, s⟩,

with the abuse of notation that b is allowed to be ⟨⟩. The components of a state are called, in order, its template, code, value, argument stack, environment, continuation, and store, and we may informally speak of them as being held in registers. The halt states in this machines are the states such that b = ⟨⟩. The answer function ans is defined for s ∈ halts by

ans(⟨t, ⟨⟩, v, a, u, k, s⟩) = v : R → v | R, ⊥_{A}.

Form of the Rules. We present acts as the union of subfunctions called (action) rules. The action rules are functions from disjoint subsets of states × inputs into states × outputs. Because their domains are disjoint, the union is in fact a function, and the resulting machine is a deterministic one.

Draft of September 29, 1993

For each rule we give a name, one or more conditions determining when the rule is applicable (and possibly introducing new locally bound variables for later use), and a specification of the new values of some state components (“registers”). Often the domain is specified by equations giving “the form” of certain registers, especially the code. In all specifications the original values of the various registers are designated by conventional variables used exactly as in the above definition of a state: t, b, v, a, u, k, and s. Call these the original register variables. The new values of the registers are indicated by the same variables with primes attached: t′, b′, v′, a′, u′, k′, and s′. Call these the new register variables. New register variables occur only as the left hand sides of equations specifiying new register values. Registers for which no new value is given are tacitly asserted to remain unchanged. Additionally, we use e for t(2); thus e must always be a template table no matter what the original state is, just because it is a valid state.

It may help to be more precise about the use of local bindings derived from pattern matching. The domain conditions may involve the original register variables and may introduce new variables (other than e and not among the new or old register variables). If we call these new, “auxiliary” variables x_{1}, …, x_{j}, then the domain conditions define a relation of j + 7 places

(†) R(t, b, v, a, u, k, s, x_{1}, …, x_{j}).

The domain condition really is this: the rule can be applied in a given state if there exist x_{1}, …, x_{j} such that (†). Furthermore, in the change specifications we assume for these auxiliary variables a local binding such that (†). Independence of the new values on the exact choice (if there is any choice) of the local bindings will be unproblematic.

Some Rules of the Tabular Byte Code Machine. We will present the rules connected with make-cont, call, and return. We will refer to all the rules R given in [10] as the abc rules. Each of them is a partial function from states to states; the domains of the rules are pairwise disjoint; hence, they may be combined to form a unique smallest common extension acts.

Draft of September 29, 1993

Rule 1: Return-Halt Domain conditions:

     b = ⟨⟨return⟩⟩

k = halt Changes: b′ = ⟨⟩

Rule 2: Return Domain conditions:

     b = ⟨⟨return⟩⟩

k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ Changes: t′ = t_{1} u′ = u_{1} b′ = b_{1} k′ = k_{1} a′ = a_{1} Rule 3: Call Domain conditions: b = ⟨⟨call #a⟩⟩ v = ⟨closure t_{1} u_{1} l_{1}⟩ t_{1} = ⟨template b_{1} e_{1}⟩ Changes: t′ = t_{1} u′ = u_{1} b′ = b_{1}

Rule 4: Make Continuation Domain conditions: b = ⟨make-cont b_{1} #a⟩:: b_{2} Changes: b′ = b_{2} a′ = ⟨⟩ k′ = ⟨cont t b_{1} a u k⟩

3.2.3. Faithfulness: Form of the Proof

The main idea of the faithfulness proof, which is contained in [5], is to associate a denotation in the domain A with each state. If s is an initial state with template t = ⟨template b e⟩, then the denotation of s agrees with the denotational value of

T_{τ} [[t]]ρ unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ_{0})

where κ_{0} = λϵ* . (ϵ* 0) : R → (ϵ* 0) | R in A, ⊥. This ensures that the denotation of an initial state containing t matches its value as used in the compiler proof. For a halt state s, the denotation is equal to its computational answer ans(s), which has been defined to be compatible with κ_{0}.

Moreover, for each rule, it is proved that when that rule is applicable, the denotation of the resulting state is equal to the denotation of the preceeding state.

Thus in effect the denotation of an initial state equals the expected denotational answer of running the program on suitable parameters, and the process of execution leaves the value unchanged. If a final state is reached, then since the ans function is compatible with κ_{0}, the computational answer matches the denotational answer, so that faithfulness is assured.

Denotational and Operational Answers. We define in this section the notions of the denotational and operational answers associated with an abc state. Our definition requires the new semantic functions shown in Table 15

Draft of September 29, 1993

D_{v} : v → E
D_{a} : v^{∗} → E^{∗}
D_{u} : u → N → N → L
D_{k} : k → E → C
D_{s} : v^{∗} → E^{∗}

Table 15: Semantic Functions for the Faithfulness Proof

The definitions of the functions take a parameter, namely a function ρ_{G} : Ide → L known as globals. Moreover, for f : A → B, f^{(∗)} : A^{∗} → B^{∗} is defined by

f^{(∗)}(⟨a_{1}, …, a_{n}⟩) = ⟨f(a_{1}), …, f(a_{n})⟩,

and f^{[∗]} : A^{∗} → B^{∗} is defined by

f^{[∗]}(⟨a_{1}, …, a_{n}⟩) = ⟨f(a_{n}), …, f(a_{1})⟩.

The semantic functions are defined by the equations shown in Table 16.

Definition 5 (Denotational and Operational Answer) The denotational answer of an abc state Σ = ⟨t, b, v, a, u, k, s⟩, denoted D[[Σ]], is the value of

B_{τ} [[b]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]].

The operational answer of Σ, denoted O[[Σ]], is defined inductively to be the smallest partial function such that:

1. If Σ is a halt state, then O[[Σ]] = ans(Σ) [= D_{v}[[v]]|R in A];

2. Otherwise, O[[Σ]] is O[[acts(Σ)]].

Note that, by the definition of K on R (see Section 2.1), if v ∈ R, then D_{v}[[v]] : R.

Let Σ = ⟨⟨template b_{0} e⟩, b, v, a, u, k, s⟩ be an abc state. The functions L_{glo}, L_{env}, L_{mp}, L_{ip}, which map abc states to finite sets of locations, are defined by the following equations:

L_{glo}(Σ) = ran(ρ_{G}).
L_{env}(Σ) = {env-reference(u′, n_{0}, n_{1}) : u′ occurs in Σ, n_{0}, n_{1} ∈ N,
and env-reference(u′, n_{0}, n_{1}) is defined.}.

Draft of September 29, 1993

D_{v}[[c]] = K[[c]]. D_{v}[[⟨closure t u l⟩]] = fix(λϵ.⟨l, (λϵ^{∗}κ.T_{τ} [[t]]ρ_{G}ϵϵ^{∗}D_{u}[[u]](λϵ.κ⟨ϵ⟩))⟩) in E. D_{v}[[⟨escape k l⟩]] = ⟨l, single arg(λϵκ.D_{k}[[k]]ϵ)⟩ in E. D_{v}[[⟨mutable-pair l_{1} l_{2}⟩]] = ⟨l_{1}, l_{2}, mutable⟩ in E. D_{v}[[⟨string l^{∗}⟩]] = ⟨l^{∗}, mutable⟩ in E. D_{v}[[⟨vector l^{∗}⟩]] = ⟨l^{∗}, mutable⟩ in E. D_{v}[[not-specified]] = unspecified in E. D_{v}[[undefined]] = empty in E.

D_{a} = D_{v}^{[∗]}.

D_{u}[[empty-env]] = (λν_{1}ν_{2}.⊥). D_{u}[[⟨env u l^{∗}⟩]] = extend_{R} D_{u}[[u]](rev l^{∗}).

D_{k}[[halt]] = (λϵσ.ϵ : R → ϵ|R in A, ⊥). D_{k}[[⟨cont ⟨template b_{0} e⟩ b a u k⟩]] = λϵ.B_{τ} [[b]]eρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]].

D_{s} = D_{v}^{(∗)}.

Table 16: Semantic Clauses for the Faithfulness Proof

L_{mp}(Σ) = {l_{1}, l_{2} ∈ L : ⟨mutable-pair l_{1} l_{2}⟩ occurs in Σ}.
L_{ip}(Σ) = {l_{1}, l_{2} ∈ L : p = ⟨immutable-pair c_{1} c_{2}⟩ occurs Σ and
(K[[p]]|L × L × {immutable}) = ⟨l_{1}, l_{2}, immutable⟩}.

Definition 6 (Normal States, Initial States)

Σ is normal if the following conditions hold:

(1) L_{glo}(Σ) ∪ L_{env}(Σ) ∪ L_{ip}(Σ) ∪ L_{mp}(Σ) ⊆ dom(s).

(2) L_{glo}(Σ), L_{env}(Σ), L_{ip}(Σ), L_{mp}(Σ) are pairwise disjoint.

(3) For each p = ⟨immutable-pair c_{1} c_{2}⟩ occurring in Σ, there are l_{1}, l_{2} ∈ L such that (K′[[p]]|L × L × {immutable}) = ⟨l_{1}, l_{2}, immutable⟩, s(l_{1}) = c_{1}, and s(l_{2}) = c_{2}.

A store s is codeless if it contains no value v of the form ⟨closure t u l⟩ or the form ⟨escape k l⟩.

A initial state for a tbc template t = ⟨template b e⟩ is any normal abc state of the form

⟨t, b, not-specified, ⟨⟩, empty-env, halt, s⟩

Draft of September 29, 1993

where s is codeless.

The restriction of initial states to those containing codeless stores plays no role in proving faithfulness, but simplifies the proof of the flattener below.

Theorem 12 The operational semantics for tbc is faithful: for all tbc templates t and all initial states Σ for t, if O[[Σ]] is defined, then D[[Σ]] = O[[Σ]].

Proof: The proof is a straightforward induction on the length of the computation sequence determining O[[Σ]]. It uses the following lemmas.

Lemma 13 If Σ is a normal abc state, R is an abc rule, and Σ′ = R(Σ), then Σ′ is also a normal abc state.

The proof examines the individual rules.

Lemma 14 If Σ = ⟨t, ⟨⟩, v, a, u, k, s⟩ is a normal abc state with v ∈ R, then D[[Σ]] = D_{v}[[v]]|R in A.

The proof is a simple calculation.

Lemma 15 If Σ and Σ′ are normal abc states such that O[[Σ]] is defined and Σ′ = R(Σ) for some abc rule R, then D[[Σ]] = D[[Σ′]].

Proof: (Selected Case) The full proof is a lengthy examination of 34 cases, one for each rule. Let Σ and Σ′ be normal abc states such that O[[Σ]] is defined and Σ′ = R(Σ) for some special rule R. To prove Lemma 15, we must show that, for each special rule R, if Σ satisfies the domain conditions of R, then D[[Σ]] = D[[Σ′]]. The individual cases require, almost exclusively, definitional expansion and β-reduction. A typical case concerns the rule for a return instruction: Case 2: R = Return.

Let Σ = ⟨⟨template b e⟩, ⟨⟨return⟩⟩, v, a, u, k, s⟩, where k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ and t_{1} = ⟨template b′ e_{1}⟩.

Then R(Σ) = Σ′ = ⟨t_{1}, b_{1}, v, a_{1}, u_{1}, k_{1}, s⟩.

D[[Σ]] = B_{τ} [[⟨⟨return⟩⟩]]eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λeρ.return)eρ_{G}D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= returnD_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= (λϵϵ^{∗}ρ_{R}ψ.ψϵ)D_{v}[[v]]D_{a}[[a]]D_{u}[[u]]D_{k}[[k]]D_{s}[[s]]
= D_{k}[[k]]D_{v}[[v]]D_{s}[[s]]
= (λϵ.B_{τ} [[b_{1}]]e_{1}ρ_{G}ϵD_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]])D_{v}[[v]]D_{s}[[s]]
= B_{τ} [[b_{1}]]e_{1}ρ_{G}D_{v}[[v]]D_{a}[[a_{1}]]D_{u}[[u_{1}]]D_{k}[[k_{1}]]D_{s}[[s]]
= D[[Σ′]]

Draft of September 29, 1993

Although not all of the cases are as straightforward as this (see [5] for all the details), the proof is a perfect illustration of the observation that much formal verification requires long but exquisitely tedious arguments. A proof tool in which it is possible to reason effectively about denotational domains would ease the burden of constructing these proofs, and would increase confidence that no error is hidden within the bulky LaTeX source.^{2}

Theorem 12 is a conditional: it asserts on that if the machine computes an answer, then that is the correct answer. This property also holds of less useful machines than the tbcsm, for instance a machine whose transition relation is empty. However, the technique of [16, Theorem 6] is available to prove the converse. The converse establishes the adequacy of the operational semantics, asserting that the machine succeeds in computing an answer when the denotational semantics predicts a non-⊥, non-erroneous answer.

3.3. Refinement and Storage Layout Relations

In the remainder of this paper, we will show how some state machines refine others. Refinement allows us to substitute a more easily implemented state machine (a more “concrete” machine) in place of another (a more “abstract” machine) which we already knew would be acceptable. We will give the definitions in the context of pure computations (those involving neither input nor output), although it is not difficult to modify them for impure computations. We will however state our definitions for non-deterministic machines. The garbage collected state machine is in fact non-deterministic, although it does have the weaker property of answer determinism, meaning that any two successful computations that start at the same initial state produce the same answer.

When C is a successful computation, that is, a finite computation terminating with a halt state s, we will write ans(C) to mean ans(s). Otherwise, ans(C) is undefined. We will say that M can compute a from s if there exists a C such that C(0) = s and ans(C) = a.^{3} Definition 7 (Refinement) Suppose that M^{A} and M^{C} are state machines and ∼_{0} ⊆ inits^{C} × inits^{A}.

2In fact the actual vlisp faithfulness proof as described in [5] is somewhat more complex. The operational semantics and the denotational semantics differ in the order in which they copy the values on the argument stack into the store when making a new environment rib after a procedure call. One order simplified the denotational reasoning, while the other order is more natural to implement. For this reason we have split the faithfulness proof into two parts. The first part has exactly the form described in this section, but uses a state machine with a reversed variant of the Make Environment rule.

The second part uses a simple storage layout relation to demonstrate that the machine with the implemented Make Environment rule refines the one used in the first part.

3The reader may want to pronounce the relations ∼_{0}, ∼, and ≈ in this section using

Draft of September 29, 1993

M^{C} weakly refines M^{A} via ∼_{0} iff, whenever s^{C} ∼_{0} s^{A} and M^{C} can compute a from s^{C}, then M^{A} can compute a from s^{A}.

M^{C} strongly refines M^{A} via ∼_{0} iff:

1. Every abstract initial state corresponds to at least one concrete initial

state:

∀s^{A} : inits^{A} . ∃s^{C} : inits^{C} . s^{C} ∼_{0} s^{A}

2. Whenever s^{C} ∼_{0} s^{A} and M^{C} can compute a from s^{C}, then M^{A} can compute a from s^{A};

3. Whenever s^{C} ∼_{0} s^{A} and M^{A} can compute a from s^{A}, then M^{C} can compute a from s^{C}.

Naturally, weak refinement is an interesting relation between state machines only when enough abstract initial states correspond to concrete initial states, and when enough abstract computations can be simulated on the concrete machine. As we use weak refinement, these are the states and computations in which all values can be stored in a machine word of fixed width.

Our standard approach [22] for proving that one state machine refines another is to prove that there is a storage layout relation between them.

Definition 8 (Storage layout relation) Suppose that M^{A} and M^{C} are state machines.

1. If ∼ ⊆ states^{C} × states^{A}, then the sequential extension of ∼, written here as ≈, is the relation between sequences of states of M^{C} and M^{A} defined inductively by the conditions:

(a) If s^{C} ∼ s^{A}, then ⟨s^{C}⟩ ≈ ⟨s^{A}⟩;

(b) If γ_{1} ≈ ⟨s^{A}⟩ and γ_{2} ≈ ⟨s^{A}⟩, then γ_{1}^{⌢}γ_{2} ≈ ⟨s^{A}⟩;

(c) If γ_{1} ≈ α_{1} and γ_{2} ≈ α_{2}, then γ_{1}^{⌢}γ_{2} ≈ α_{1}^{⌢}α_{2}.

2. ∼ ⊆ states^{C} × states^{A} is a storage layout relation for M^{C} and M^{A} iff:

(a) ∀s^{A} : inits^{A} . ∃s^{C} : inits^{C} . s^{C} ∼ s^{A}; (b) ∀C^{C}, s^{A} . C^{C} is finite ∧ C^{C}(0) ∼ s^{A} ⇒

terms such as “refines” or “implements.” This motivates the order of the arguments, with the more concrete argument always appearing on the left.

Draft of September 29, 1993

∃C^{A} . C^{A}(0) = s^{A} ∧ C^{C} ≈ C^{A};

(c) ∀C^{A}, s^{C} . C^{A} is finite ∧ C^{A}(0) ∼ s^{C} ⇒

∃C^{C} . C^{C}(0) = s^{C} ∧ C^{C} ≈ C^{A}.

(d) ∀s^{C}, s^{A} . s^{C} ∼ s^{A} ⇒ ans^{C}(s^{C})==ans^{A}(s^{A});^{4}

3. ∼ ⊆ states^{C} × states^{A} is a weak storage layout relation for M^{C} and M^{A} iff conditions 2b and 2d above hold.

Lemma 16 The sequential extension of ∼, restricted to computations of M^{C} and M^{A} (rather than arbitrary sequences of states), is the least relation ≈ satisfying:

1. If s^{C} and s^{A} are initial states and s^{C} ∼ s^{A}, then ⟨s^{C}⟩ ≈ ⟨s^{A}⟩;

2. If γ^{⌢}⟨s_{0}^{C}⟩ ≈ α^{⌢}⟨s^{A}⟩, s_{0}^{C} can proceed to s_{1}^{C}, and s_{1}^{C} ∼ s^{A}, then γ^{⌢}⟨s_{0}^{C}, s_{1}^{C}⟩ ≈ α^{⌢}⟨s^{A}⟩;

3. If γ^{⌢}⟨s_{0}^{C}⟩ ≈ α^{⌢}⟨s_{0}^{A}⟩, s_{0}^{C} can proceed to s_{1}^{C}, s_{0}^{A} can proceed to s_{1}^{A}, and s_{1}^{C} ∼ s_{1}^{A}, then γ^{⌢}⟨s_{0}^{C}, s_{1}^{C}⟩ ≈ α^{⌢}⟨s_{0}^{A}, s_{1}^{A}⟩.

Consequently, a relation ∼ satisfying 2a and 2d is a storage layout relation if for all accessible states s_{0}^{C}, s_{1}^{C}, and s_{0}^{A}, if s_{0}^{C} ∼ s_{0}^{A} and s_{0}^{C} can proceed to s_{1}^{C}, then either

1. s_{1}^{C} ∼ s_{0}^{A}, or

2. there exists an s_{1}^{A} such that s_{1}^{C} ∼ s_{1}^{A}.

These latter conditions amount to saying, for every pair of similar accessible states, that any transition of the concrete machine corresponds either to a no-op or to a transition of the abstract machine.

Storage layout relations provide a way of proving refinement, as we can easily show with the help of a lemma; it requires only a routine induction on the relation ≈:

Lemma 17 Suppose γ ≈ α.

1. ∀i < #α . ∃j . i ≤ j ∧ γ(j) ∼ α(i).

2. ∀j < #γ . ∃i . i ≤ j ∧ γ(j) ∼ α(i).

4We write s==t to mean that s and t are equal if either of them is well defined:

(s ↓ ∨t ↓) ⇒ s = t. In particular, ans^{C}(s^{C})==ans^{A}(s^{A}) entails that either both s^{C} and s^{A} are halt states, or else neither of them is.

Draft of September 29, 1993

3. γ(0) ∼ α(0).

Theorem 18 (Storage layout relations guarantee refinement) Suppose that M^{A} and M^{C} are state machines sharing the same inputs, outputs, null-in, and null-out.

1. If ∼ is a weak storage layout relation for M^{C} and M^{A}, then M^{C} weakly refines M^{A} via ∼_{0} = ∼ ∩ inits^{C} × inits^{A}.

2. If ∼ is a storage layout relation ∼ for M^{C} and M^{A}, then M^{C} strongly refines M^{A} via ∼_{0} = ∼ ∩ inits^{C} × inits^{A}.

Proof: We prove in turn that each of the three clauses in Definition 7 holds. Note that in proving clause 2 we use only clauses 2b and 2d of Definition 8.

1. If s^{A} ∈ inits, then ⟨s^{A}⟩ is a computation, and by clause 2c, there is a C^{C} with C^{C} ≈ ⟨s^{A}⟩. By the definition of ≈, C^{C}(0) ∼ ⟨s^{A}⟩(0) = s^{A}.

2. Suppose that s^{C} ∼_{0} s^{A}; that C^{C}(0) = s^{C}; and that ans(C^{C}) = a. Then by clause 2b, there is a C^{A} with C^{A}(0) = s^{A} and C^{C} ≈ C^{A}. By Lemma 17, there is an i such that C^{A}(i) ∼ C^{C}(#C^{C} − 1). By clause 2d, ans(C^{A}(i)) = a; moreover, as C^{A} is a computation and C^{A}(i) ∈ halts, #C^{A} = i+1, so ans(C^{A}) = ans(C^{A}(i)).

3. Suppose that s^{C} ∼_{0} s^{A}; that C^{A}(0) = s^{A}; and that ans(C^{A}) = a. Then by clause 2b, there is a C^{C} with C^{C}(0) = s^{C} and C^{C} ≈ C^{A}. By the other half of Lemma 17, there is a j such that C^{C}(j) ∼ C^{A}(#C^{A} −1). As before, ans(C^{C}) = ans(C^{C}(j)) = a.

4. The Flattener

The flattener [10] transforms byte coded procedures in the tbc into a linear rather than a tree-structured form. Conditionals are represented in a familiar way using jump and jump-if-false instructions that involve a numeric offset to the target code. Similarly, the target code to which a procedure should return is indicated by a numeric offset from the instruction. We call the output language of the flattener the flattened byte code (fbc).

Draft of September 29, 1993

4.1. The Tabular Byte Code in More Detail

In order to describe the operational semantics of conditionals in the tbcsm, we will need to refer to the open-adjoin of an open instruction list y and any instruction list w, written y^{⌣}w and defined as follows:

Definition 9 (Open-adjoin)

⟨z⟩^{⌣}w = z:: w;

(z:: y)^{⌣}w = z:: (y^{⌣}w);

(⟨make-cont y n⟩:: b)^{⌣}w = ⟨make-cont y^{⌣}w n⟩:: b; and

(⟨make-cont ⟨⟩ n⟩:: b)^{⌣}w = ⟨make-cont w n⟩:: b.

It may help to note, first, that in the grammar presented in Table 12, a closed tbc instruction list can contain (at top level) no instruction of the form ⟨make-cont y n⟩ or ⟨make-cont ⟨⟩ n⟩, and, hence, that an open instruction list is either a list of neutral instructions or contains exactly one instruction of this form. Open-adjoin proceeds recursively inwards from its first argument through the code lists of such instructions until it reaches one which is just a (possibly empty) list of neutral instructions and then it concatenates w to the “open” end of that list.

Lemma 19 Properties of open-adjoin. For all y, w, y_{1}, and b,

1. y^{⌣}w is well-defined by the above recursion and is an instruction list;

2. y^{⌣}y_{1} is open, and y^{⌣}b is closed; and

3. y^{⌣}(y_{1}^{⌣}w) = (y^{⌣}y_{1})^{⌣}w (associativity).

The rules for conditionals in open instruction lists use ^{⌣}:

Rule 5: Open Branch/True Domain conditions:

   b = ⟨unless-false y_{1} y_{2}⟩:: b_{1}

v ≠ false

Changes:

b′ = y_{1}^{⌣}b_{1} Rule 6: Open Branch/False Domain conditions:

                               b = ⟨unless-false y_{1} y_{2}⟩:: b_{1}

v = false Changes: b′ = y_{2}^{⌣}b_{1}

In the remainder of this section, we will to present the fbc and give it an operational semantics in a style very similar to the presentation of

Draft of September 29, 1993

   t ::= ⟨template w e⟩

e ::= o*

   o ::= ⟨constant c⟩ | ⟨global-variable i⟩ | t

w ::= ⟨⟩ | m^{⌢}w

  m ::= ⟨call n⟩ | ⟨return⟩ | ⟨make-cont n_{0} n_{1} n_{2}⟩ | ⟨literal n⟩
       | ⟨closure n⟩ | ⟨global n⟩ | ⟨local n_{0} n_{1}⟩ | ⟨set-global! n⟩
       | ⟨set-local! n_{0} n_{1}⟩ | ⟨push⟩ | ⟨make-env n⟩
       | ⟨make-rest-list n⟩ | ⟨unspecified⟩ | ⟨jump n_{0} n_{1}⟩
       | ⟨jumpf n_{0} n_{1}⟩ | ⟨checkargs= n⟩ | ⟨checkargs>= n⟩ | ⟨i⟩

Table 17: Flattened Byte Code: Syntax

the tbc semantics in Section 3.2.2. We will then briefly describe the flattener algorithm. To prove the correctness of this algorithm, we develop a correspondence relation between flattened and unflattened code, and prove that the flattener produces code bearing this relation to its input. Finally, we extend the code correspondence relation to a storage layout relation between states of the newly introduced flattened byte code state machine (fbcsm) and the tbcsm. This establishes that the fbcsm is a refinement of the tbcsm.

4.2. Flattened Byte Code Syntax

The Flattened Byte Code (fbc) is a modification of the Tabular Byte Code that uses exclusively unnested linear sequences of tokens for the code part of its templates. Instead of the tbc conditional instruction unless-false, fbc has jumpf and jump, both of which take a pair of numeric operands that together indicate an offset to another location in the instruction sequence. The syntax of make-cont has been altered so that it too can use numeric offsets. The bnf definitions of these classes appears as Table 17.

Note that, here in fbc, every member of w is a sequence, of which each element is either a token representing the name of a byte code operation or a number. In the vlisp implementation, these numbers are all small enough unsigned integers to be stored in a single byte (i.e., less than 256).

Draft of September 29, 1993

4.3. Flattened Byte Code Operational Semantics

fbc states differ from tbc states in that they contain a template belonging to the fbc language rather than the tbc language. In addition, instead of having a “code register” they have a numerical “program counter.” It is interpreted as an offset into the code sequence of the template.

Officially, the states of an fbc state machine are the sequences of the form

⟨t, n, v, a, u, k, s⟩.

We will use the variable w to refer to the code sequence (or just the code) of a state, i.e., w = t(1). With our conventions, w(n) is the first element of w † n, if 0 ≤ n < #w. The halts are the states such that n = #w (so w†n = ⟨⟩). The answer function, normal states, and initial states are defined as before.

The presentation of the pure rules for the fbc will use the same conventions as were used for the tbc, except that here n stands for the offset of the ingoing state, n′ for the offset of the state produced, and w for t(1), the code sequence of the template of the ingoing state. The operator ⊕ takes two integers and returns an integer representing an offset they are together coding; it is defined:

n_{0} ⊕ n_{1} = (256 ∗ n_{0}) + n_{1}.

Rule 1: Call

Domain conditions: w†n = ⟨call #a⟩^{⌢}w_{1} v = ⟨closure t_{1} u_{1} l_{1}⟩ Changes: t′ = t_{1} n′ = 0 u′ = u_{1}

Rule 2: Jumpf/False Domain conditions: w†n = ⟨jumpf n_{1} n_{2}⟩^{⌢}w_{1} v = false Changes: n′ = n + 3 + (n_{1} ⊕ n_{2})

Rule 3: Make Continuation Domain conditions: w†n =

⟨make-cont n_{1} n_{2} #a⟩^{⌢}w_{1} Changes: n′ = n + 4 a′ = ⟨⟩ k′ =

⟨cont t (n + 4 + (n_{1} ⊕ n_{2})) a u k⟩

Rule 4: Jumpf/True Domain conditions: w†n = ⟨jumpf n_{1} n_{2}⟩^{⌢}w_{1} v ≠ false Changes: n′ = n + 3 4.4. The Flattener

Draft of September 29, 1993

The flattener is implemented by a purely applicative Scheme program; it is a straightforward recursive descent. It is however sensitive to the syntactic category of the code that it is flattening, whether it is a closed tbc instruction list b or an open tbc instruction list y.

An obvious induction shows that the algorithm terminates, and produces a syntactically well-formed fbc template from any tbc template.

We will use F (w) to abbreviate the result of applying flatten-code to w and closed, if w is of the form b, and for the result of applying flatten-code to w and open, if w is of the form y. Similarly, we will use F (e) as an abbreviation for the result of applying flatten-table to e, and we will use F (t) to mean the result of applying flatten-template to t. Observe from the code that F (⟨template b e⟩) = ⟨template F (b) F (e)⟩.

4.5. Code Correspondence

We will define the storage layout relation between states justifying this refinement in terms of a preliminary “code correspondence” relation ≃. This is really a four-place relation on a tbc instruction list, a tbc table, a fbc code sequence, and a fbc table. We think of it as a binary correspondence between the pair of its first two arguments and the pair of its last two arguments, meaning that the former pair represents or implements the latter, and we will write, for instance, (w_{F} , e_{F}) ≃ (w, e). It is defined as the least relation satisfying the conditions summarized in Table 19. One fine point in the definition concerns expressions of the form w†n: when we make an atomic assertion about w†n, we are implicitly asserting that it is well defined, so that n ≤ #w. We will repeatedly use a fact about sequences:

Lemma 20 drop/adjoin. When n ≤ #w_{0}, (w_{0}†n)^{⌢}w_{1} = (w_{0}^{⌢}w_{1})†n.

For closed instruction lists, adding code to the end of a flattened version does not destroy the ≃ relation. Since the proofs in this section are all similar, we present only the first in detail.

Lemma 21 ≃/adjoin. If (w_{0}, e^{F}) ≃ (b_{0}, e), then for any w_{1}:

(w_{0}^{⌢}w_{1}, e^{F}) ≃ (b_{0}, e).

Proof: We will assume that w_{0} is not of the form ⟨jump n_{0} n_{1}⟩^{⌢}w_{2},
and thus that (w_{0}^{⌢}w_{1}, e^{F}) ≃ (b_{0}, e) is not true in virtue of clause 6.
For otherwise, (w_{2}†(n_{0} ⊕ n_{1}), e^{F}) ≃ (b_{0}, e), and we may apply the

Draft of September 29, 1993

(define (flatten-template tem)
  `(template ,(raw-code (flatten-code (cadr tem) 'closed))
             ,(flatten-table (caddr tem))))
(define (flatten-table table)
  (map (lambda (entry) (if (tbc-template? entry)
                           (flatten-template entry)
                           entry))
       table))
(define (flatten-code code category)
  (if (null? code) empty-code-sequence
      (let ((instr (car code)) (after-code (cdr code)))
        (case (operator instr)
          ((make-cont)
           (flatten-make-cont (rand1 instr) (rand2 instr)
                              after-code category))
          ((unless-false) ...)
          (else
           (flatten-default instr after-code category))))))
(define (flatten-make-cont saved nargs after category)
  (let ((after-code (flatten-code after 'closed))
        (saved-code (flatten-code saved category)))
    (add-offset+byte-instruction
     'make-cont (code-length after-code) nargs
     (adjoin-code-sequences after-code saved-code))))
(define (flatten-default instr after category)
  (let ((after-code (flatten-code after category)))
    (prepend-instruction instr after-code)))

Table 18: Flattener Algorithm 1. For m = ⟨return⟩ or ⟨call n⟩, (m^{⌢}w_{F} , e_{F}) ≃ (⟨m⟩, e).

Draft of September 29, 1993

2. For atomic z, (z^{⌢}w_{F} , e_{F}) ≃ (z:: m*, e) if, first, either m* = w_{F} = ⟨⟩ or (w_{F} , e_{F}) ≃ (m*, e), and second, depending on the form of z:

(a) if z = ⟨literal n⟩, ⟨global n⟩, or ⟨set-global! n⟩, then e(n) = e_{F} (n);

(b) if z = ⟨closure n⟩, then:

i. e(n) is of the form ⟨template b_{1} e_{1}⟩, and ii. e_{F} (n) is of the form ⟨template w_{2} e_{2}⟩, where iii. (w_{2}, e_{2}) ≃ (b_{1}, e_{1}).

3. (⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} , e_{F}) ≃ (⟨make-cont w n⟩:: b, e) if:

(a) (w_{F} , e_{F}) ≃ (b, e); and

(b) (w_{F} †(n_{0} ⊕ n_{1}), e_{F}) ≃ (w, e).

3′. (⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} , e_{F}) ≃ (⟨make-cont ⟨⟩ n⟩:: b, e) if:

(a) (w_{F} , e_{F}) ≃ (b, e); and

(b) #w_{F} = n_{0} ⊕ n_{1}.

4. (⟨jumpf n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) ≃ (⟨⟨unless-false b_{1} b_{2}⟩⟩, e) if:

(a) (w_{F} , e_{F}) ≃ (b_{1}, e); and

(b) (w_{F} †(n_{0} ⊕ n_{1}), e_{F}) ≃ (b_{2}, e).

5. (⟨jumpf n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) ≃ (⟨unless-false y_{1} y_{2}⟩:: w, e) if:

(a) (w_{F} , e_{F}) ≃ (y_{1}^{⌣}w, e);

(b) (w_{F} †(n_{0} ⊕ n_{1}), e_{F}) ≃ (y_{2}^{⌣}w, e).

6. (⟨jump n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) ≃ (w, e) if (w_{F} †(n_{0} ⊕ n_{1}), e_{F}) ≃ (w, e).

Table 19: Recursive Conditions for ≃.

Draft of September 29, 1993

lemma^{5} to infer that

(w_{2}†(n_{0} ⊕ n_{1})^{⌢}w_{1}, e^{F}) ≃ (b_{0}, e).

Since w_{2}†(n_{0} ⊕ n_{1})^{⌢}w_{1} = w_{2}^{⌢}w_{1}†(n_{0} ⊕ n_{1}), we may apply clause 6 to infer:

(⟨jump n_{0} n_{1}⟩^{⌢}(w_{2}^{⌢}w_{1}), e^{F}) ≃ (b_{0}, e).

By the associativity of ^{⌢}, the desired conclusion holds. The proof is by induction mirroring the inductive definition of ≃.

1. Suppose b_{0} = ⟨m⟩ = ⟨⟨return⟩⟩ or ⟨⟨call n⟩⟩, and w_{0} = ⟨m⟩^{⌢}w. By the associativity of^{⌢}, (⟨m⟩^{⌢}w)^{⌢}w_{1} = ⟨m⟩^{⌢}(w^{⌢}w_{1}), which is also an instance of clause 1.

2. Suppose that b_{0} = z:: b, w_{0} = z^{⌢}w. (The syntax ensures that m* really is of the form b.) Since, inductively, (w^{⌢}w_{1}, e_{F}) ≃ (b, e), we simply apply clause 2 to w^{⌢}w_{1}. The subclauses dealing with e and e_{F} are unaffected.

3. If b_{0} = ⟨make-cont b_{1} n⟩:: b, and w_{0} = ⟨make-cont n_{0} n_{1} n_{2}⟩^{⌢}w: Assume inductively:

(w^{⌢}w_{1}, e_{F}) ≃ (b, e)

and

(w†(n_{0} ⊕ n_{1})^{⌢}w_{1}, e_{F}) ≃ (b_{1}, e).

By the drop/adjoin lemma, we may apply clause 3 with w^{⌢}w_{1} in place of w.

3′. A closed instruction sequence b_{0} is not of this form. 4, 5, 6. Similar to 3.

On the other hand, for open instruction lists, adding code to the end of a flattened version corresponds to ^{⌣}:

Lemma 22 ≃/open-adjoin. If (w_{0}, e^{F}) ≃ (y, e) and (w_{1}, e^{F}) ≃ (w, e), then (w_{0}^{⌢}w_{1}, e^{F}) ≃ (y^{⌣}w, e).

Lemma 23 No initial jumps. F (w) is not of the form ⟨jump n_{0} n_{1}⟩^{⌢}w_{1}.

Theorem 24 Flattener establishes ≃. Suppose that w respects the template table e.

A. (F (w), F (e)) ≃ (w, e);

B. If n occurs in w and e(n) is of the form ⟨template b_{1} e_{1}⟩, then

(F (w_{1}), F (e_{1})) ≃ (b_{1}, e_{1}).

5Naturally, w_{2}†(n_{0} ⊕ n_{1}) might begin with a jump, but this may be repeated only a finite number of times.

Draft of September 29, 1993

4.6. State Correspondence

Based on the underlying “code correspondence” relation ≃, we will define a binary “miscellaneous correspondence” relation ∼ between various kinds of syntactic objects of afbc on the left and ones of abc on the right, building up to a notion of correspondence between fbc states and tbc states that is preserved by state transitions. The main result of this section is that the state correspondence is a storage layout relation; hence by Theorem 18 the fbcsm is a faithful refinement of the tbcsm.

We take advantage of the inessential fact that the two languages share some syntactic objects to simplify the definition. Thus some of the syntactic objects that are shared by the two languages are to be called self corresponding, namely, the halt continuation; all environments; undefined; unspecified; all constants; and all values beginning with mutable-pair, string, or vector.

The relation ∼ is then defined recursively, as the least set of pairs whose right element is a member of one of the abc classes t, v, a, u, k or s, or is an abc state, and which satisfies the closure conditions given in Table 20. Note especially clauses 6 and 7, which reflect differences in how, and even in which registers, the two machines store “active” code. Also, clause 4 applies to both argument stacks and stores.

From this definition and Theorem 24, it immediately follows that for any initial tbc state ⟨t, t(1), unspecified, ⟨⟩, empty-env, halt, s⟩, that the fbc initial state ⟨F (t), 0, unspecified, ⟨⟩, empty-env, halt, s⟩ corresponds to it. Thus condition 2a in Definition 8 (storage layout relations) is satisfied. Moreover, condition 2d follows immediately from clause 8 for ∼.

Corollary 25 ∼ satisfies the initial condition (2a) and the halt condition (2d) for being a storage layout relation.

The following easy lemma shortens the proof of the preservation theorem somewhat and justifies a looser way of thinking about computations of tbc and fbc state machines. One can talk about what they do (or would do under given circumstances), not just about what they might do.

Lemma 26 (Determinacy of Pure Transitions) If M is either a tbc machine or an fbc machine, and M is in state S, then there is at most one state S′ such that M can proceed by one rule transition from S to S′.

Proof: The domain conditions for the different rules (of the same machine) are pairwise mutually incompatible, as can be seen by looking just at the required form of the code register, except for a few

Draft of September 29, 1993

1. x ∼ x, if x is self corresponding

2. ⟨closure t_{1} u l⟩ ∼ ⟨closure t_{2} u l⟩, if t_{1} ∼ t_{2}

3. ⟨escape k_{1} l⟩ ∼ ⟨escape k_{2} l⟩, if k_{1} ∼ k_{2}

4. v_{1}^{∗} ∼ v_{2}^{∗}, if #v_{1}^{∗} = #v_{2}^{∗} and, for every n < #v_{1}^{∗}, v_{1}^{∗}(n) ∼ v_{2}^{∗}(n)

5. ⟨template w e_{2}⟩ ∼ ⟨template b e_{1}⟩, if (w, e_{2}) ≃ (b, e_{1})

6. ⟨cont t_{2} n a_{2} u k_{2}⟩ ∼ ⟨cont t_{1} b a_{1} u k_{1}⟩, if (a) (t_{2}(1) † n, t_{2}(2)) ≃ (b, t_{1}(2)), and

(b) a_{2} ∼ a_{1} and k_{2} ∼ k_{1}

7. ⟨t_{2}, n, v_{2}, a_{2}, u, k_{2}, s_{2}⟩ ∼ ⟨t_{1}, b, v_{1}, a_{1}, u, k_{1}, s_{1}⟩, if (a) (t_{2}(1) † n, t_{2}(2)) ≃ (b, t_{1}(2)), and

(b) v_{2} ∼ v_{1}, a_{2} ∼ a_{1}, k_{2} ∼ k_{1}, and s_{2} ∼ s_{1}

8. ⟨t_{2}, n, v_{2}, a_{2}, u, k_{2}, s_{2}⟩ ∼ ⟨t_{1}, b, v_{1}, a_{1}, u, k_{1}, s_{1}⟩, if each is a halt state and v_{1} = v_{2}.

Table 20: Closure Conditions for ∼.

Draft of September 29, 1993

cases when one must also consider the value register or the argument register. Given a particular pure rule and a state, there is always at most one way of binding the variables of the domain equations so that they are satisfied. The next state is clearly determined by the rule, the ingoing state, and these bindings.

Clearly the tbc rules are closely paralleled by the fbc rules – let us say that a tbc rule A corresponds to an fbc rule B if A and B have the same name, also that Closed Branch/True and Open Branch/True both correspond to Jumpf/True, and finally that Closed Branch/False and Open Branch/False both correspond to Jumpf/False. No tbc rule corresponds to Jump. A branch rule means one whose name ends in /True or /False – four for tbc and two for fbc.

Theorem 27 (Preservation of State Correspondence) Let M be a tbc machine and M_{F} be a fbc machine with the same globals as M. Let S be the state of M and S_{F} the state of M_{F}, and assume that S_{F} ∼ S. Then

1. if M_{F} proceeds by the Jump rule to state S′_{F}, then S′_{F} ∼ S, and

2. if M_{F} cannot proceed by the Jump rule, then, if either machine proceeds, then the other machine proceeds by a corresponding rule, and the resulting states correspond.

The proof consists of a careful analysis of the rules of the two machines. Using Lemma 16 and Theorem 18, we have:

Corollary 28 ∼ is a storage layout relation for the fbcsm and the tbcsm. The fbcsm refines the tbcsm.

5. State Observers and Mutators

Microcode functions are classified into two categories.

State Observers These are functions that return an atomic piece of information about the state. They may be composed when the return type of one state observer matches the type of a parameter to another observer; we will call a (well-formed) expression built from variables, constants, and names for state observers an “observer expression.”

State Modifiers These are operations, possibly taking parameters, that modify an atomic component of a state. A “state modifier expression” consists of a state modifier name applied to observer expressions.

Draft of September 29, 1993

We use “modifier” and “mutator” interchangeably. mspm observers are specified in Table 21 and mspm mutators are specified in Table 22.

The stores in mspm accessible states^{6} satisfy a representation invariant, namely they contain a collection of stored objects. A stored object consists of a header and a tuple of values. The header contains a type tag for the stored object and the length of the tuple of values. The header and the values are stored in consecutive locations in the store. The address at which the first value is stored is called the address of the stored object.

An important property of mspm-accessible states is that if an accessible state contains a term of the form ⟨ptr ℓ⟩, then ℓ is the address of a stored object in the store. The representation invariant and this property are established in the correctness proof of the mspm.

Definition 10 (Stored Objects) s contains a stored object at ℓ if:

1. s(ℓ − 1) = ⟨header h p m⟩, for some h, p, and m;

2. s(j) is a well-defined non-header value for each j for ℓ ≤ j < ℓ + m.

A state Σ is composed of stored objects if, whenever ⟨ptr ℓ⟩ occurs in any (transitive) component of Σ, then the store of Σ contains a stored object at location ℓ.

Action Rules. mspm action rules are specified as programs composed from state modifier expressions and observer expressions using the constructs while, if-then-else, and sequential composition. Tests are equations between observer expressions or boolean combinations of equations. The atomic statements are the modifier expressions. The rules are exceedingly simple programs, so there need be no procedure call mechanism. In fact, only the rule to make a rest-argument list—when calling a Scheme procedure with a dotted argument list—requires the while construct; the others could be expressed using only a primitive recursive for-loop. The majority of rules require no iteration whatever.

For our purposes it suffices to regard this language as having a simple Floyd-style [8] operational semantics. To describe the execution of a program, we regard that program as a flow graph. The execution state consists of an mspm state together with a “program counter” selecting a node in the flow graph, representing the phrase of the program currently being executed. Evaluating a test expression selects between two next nodes; executing a modifier expression alters the mspm state and advances the current node.

6An accessible state is a state in a computation from an initial state.

Draft of September 29, 1993

VLISP SCHEME 55

Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be an mspm state. Then, Register Observers

template-ref Σ  = t
offset-ref Σ  = n
value-ref Σ  = v
env-ref Σ  = u
cont-ref Σ  = k
spare-ref Σ  = r

Stack Observers

stack-top Σ  = a(0)  if #a > 0

stack-empty? Σ  = (#a = 0)
stack-length Σ  = #a

Stored Object Observers Let d = ⟨ptr l⟩ and s(l − 1) = ⟨header h p m⟩. Then,

stob-ref d i Σ  = s(l + i)

stob-tag d Σ  = h
stob-mutable? d Σ  = p
stob-size d Σ  = m

Table 21: mspm State Observers.

Draft of September 29, 1993

56 GUTTMAN, SWARUP, RAMSDELL

Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be an mspm state. Then, Register Mutators

template-set vd Σ = Σ[t′ = vd]
offset-set i Σ  = Σ[n′ = i]

value-set vd Σ  = Σ[v′ = vd]
env-set vd Σ  = Σ[u′ = vd]
cont-set vd Σ  = Σ[k′ = vd]
spare-set vd Σ  = Σ[r′ = vd]

Stack Mutators

stack-push vd Σ = Σ[a′ = vd ::a]
stack-pop Σ  = Σ[a′ = a † 1]  if #a > 0

stack-clear Σ  = Σ[a′ = ⟨⟩]

Miscellaneous Mutators

assert p Σ  = if p then Σ else abort

Stored Object Mutators

make-stob h p m Σ  =

Σ[s′ = s^{⌢} ⟨header h p m⟩^{⌢} v_{1} ^{⌢} …^{⌢} v_{m}] [r′ = ⟨ptr #s + 1⟩] where v_{1} = … = v_{m} = ⟨imm undefined⟩

stob-set ⟨ptr l⟩ i vd Σ = Σ[s′ = s[(l + i) ↦ vd]]
if s(l − 1) = ⟨header h p m⟩
and 0 ≤ i < m

Table 22: mspm State Mutators.

Draft of September 29, 1993

We will refer to the programs in this language as “rule programs.” The states in the operational semantics for a rule program P we will call “Pstates,” so each P-state is a pair consisting of a node in the flow graph for P together with an mspm state. We will refer to these as the “control node” of the state and the “underlying mspm state.” An initial P-state is a pair whose control node is at the start of P, and whose underlying state may be any mspm state, while a halt state is one whose control node has reached the end of the program. A computation of the state machine corresponding to P will be a “P-computation.” Since rule programs are deterministic, we can freely refer to the maximal computation starting from any initial P-state.

Theorem 29 The implementation of the action rules of the mspm is correct with respect to the specification of the spm action rules.

The proof is simple, but highly tedious. A detailed examination of the correctness of all the action rules was carried out.

As with the fbcsm (Lemma 26), the mspm is determinate: for every state of the mspm, there is at most one rule that can be applied in that state, and there is at most one next state that the rule may produce.

6. Garbage Collection

In this section we will prove that a garbage collected state machine gcsm is a faithful refinement of the mspm. The two machines share the same set of states, the same initial states, halt states, and answer function. The only difference between the gcsm and the mspm is that the gcsm may perform a garbage collection before executing the “microcode” mutator make-stob, which allocates a new stored object.^{7}

We will define a relation ≅ of similarity between gcsm states and mspm states. The initial states of the gcsm are the same as the initial states of the mspm. Thus, because identity suffices for similarity, the initial state condition 2a for a storage layout relation (Definition 8) is trivial. Moreover, the definition of the answer function on halt states ensures that similar halt states yield identical answers (condition 2d). Thus the proof reduces to showing that execution of the two machines preserves the similarity relation, i.e., that each “microcode” operation, including garbage collection in the gcsm, preserves ≅.

7In the form of the proof given here, we will not use the fact that garbage collection occurs only immediately before make-stob; we shall regard it simply as a new state transition. However, the fact that garbage collection does occur only before this one mutator can be used to justify an optimization to make-stob, so that it need not initialize the newly allocated memory to a distinctive value empty [20].

Draft of September 29, 1993

The proof is partitioned into two parts. First, we partially specify gcsm, stipulating that garbage collection is some function g from states to states with the property that g(Σ) ≅ Σ (for all accessible states Σ). That the remaining rules preserve ≅ establishes that garbage collection is a legitimate implementation strategy, independent of the selection of any particular garbage collection algorithm. Naturally, there are many choices of rules for which this is false, for instance most kinds of pointer arithmetic.

We then complete the specification of gcsm by defining a specific garbage collection algorithm gc. We prove that it satisfies its correctness requirement, which is to say that gc(Σ) ≅ Σ for accessible states Σ.

We define the state similarity relation using a variant of the storagelayout relations notation. The treatment in [22] assumes that terms are tree-structured, and storage layout relations are defined by structural induction over such terms. However, states can effectively contain cycles, since a Scheme program, during execution, can use operations with sideeffects to construct circular data structures. A garbage collector must faithfully relocate these data structures also. Thus the storage-layout relations cannot be defined by structural induction over the states regarded as terms. Instead, we use an existential quantifier. Two states^{8} s and s^{M} are similar if there exists some correlation between locations in their respective stores, such that corresponding values can be found in correlated locations, as well as in registers. Because we formalize the correlation as a binary predicate relating concrete and abstract store locations, this is a second-order existential quantifier.

Our experience is that this technique is intuitively understand and that it leads to straightforward proof obligations. By contrast, although the technique of taking greatest fixed points is sometimes suggested for building up a representation relation suited to circular structures, it seems not to be easily applicable to this problem. It is intuitively important that the representation relation between concrete and abstract locations should be one-one on the active parts of the stores, so that an assignment to a concrete location can matched an assignment to the corresponding abstract location. There is, however, generally no single greatest relation ∼ between concrete and abstract store locations which is one-one on the active locations. For instance, if different locations in the abstract store contain the same values, then there are arbitrary but incompatible choices about which concrete locations should correspond to each. Moreover, a theory of maximal fixed points among one-one relations would be theoretically unfamiliar, and by no means guaranteed to work.

8We will typically indicate objects from the more abstract mspm by variables with a superscript M, leaving variables representing gcsm objects unadorned. Since the mspm and gcsm agree in their sets of states, however, as well as in their other components apart from acts, the objects involved are generally drawn from the same sets. Rather, the superscript connects the object with the machine we regard it as arising in.

Draft of September 29, 1993

6.1. State Similarity

We formalize locations as natural numbers, but use ℓ-like variables when we are regarding the numbers as store locations.

Definition 11 (Store Correspondence) When ∼ is a binary relation on natural numbers (regarded as representing concrete and abstract store locations), we say that ∼ is a store correspondence between concrete store s and abstract store s^{M} if the following two conditions are met:

1. ℓ ∼ ℓ_{0}^{M} and ℓ ∼ ℓ_{1}^{M} implies ℓ_{0}^{M} = ℓ_{1}^{M};

2. if ℓ ∼ ℓ^{M} then ℓ and ℓ^{M} are in the domain of s and s^{M} respectively.

An explicit condition extends a store correspondence to a correspondence between values of all kinds:

Definition 12 (Term Correspondence) Let ∼ be a store correspondence between stores s and s^{M}.

The term correspondence generated by ∼ is a relation ≃ between values cell and cell^{M}, defined by taking cases on cell^{M}. cell ≃ cell^{M} holds just in case one of the following holds:

1. ⟨ptr l^{M}⟩ = cell^{M} and

(a) ⟨ptr l⟩ = cell;

(b) s^{M}(l^{M} − 1) = s(l − 1) = ⟨header h p m⟩, for some header type h, mutability bit p and stored object length m; and

(c) for all 0 ≤ i < m, (l + i) ∼ (l^{M} + i).

2. ⟨fixnum m⟩ = cell^{M} = cell, for some number m.

3. imm = cell^{M} = cell, for some immediate value imm.

4. b^{∗} = cell^{M} = cell, for some sequence of bytes b^{∗}.

If x and x^{M} are not cells, then for convenience we will say that x ≃ x^{M} just in case x = x^{M}.

Finally, we define the state correspondence to hold if there exists a suitable store correspondence:

Draft of September 29, 1993

Definition 13 (State Similarity) Let ∼ be a store correspondence between concrete gcsm store s and abstract mspm store s^{M}, with generated term correspondence ≃. Σ, of the form ⟨t, n, v, a, u, k, s, r⟩, and Σ^{M}, of the form ⟨t^{M}, n^{M}, v^{M}, a^{M}, u^{M}, k^{M}, s^{M}, r^{M}⟩, are similar with respect to ∼, written Σ ≈ Σ^{M}, just in case:

1. #a^{M} = #a and ∀0 ≤ i < #a . a(i) ≃ a^{M}(i);

2. for all locations l^{M} and l, l ∼ l^{M} ⇒ s(l) ≃ s^{M}(l^{M});

3. x ≃ x^{M}, where x and x^{M} are any of the pairs of state components ⟨t, t^{M}⟩, ⟨n, n^{M}⟩, ⟨v, v^{M}⟩, ⟨u, u^{M}⟩, ⟨k, k^{M}⟩, and ⟨r, r^{M}⟩.

Σ and Σ^{M} are similar, written Σ ≅ Σ^{M}, just in case there exists a store correspondence ∼ such that Σ and Σ^{M} are similar with respect to ∼.

We will slightly abuse notation by sometimes not showing ∼ when using ≃ and ≈. When both ≃ and ≈ are used in the same assertion, then ≃ is the term correspondence generated by the omitted ∼. By inspecting the structure of states we can verify:

Lemma 30 (Properties of ≅)

1. Σ ≅ Σ;

2. Σ ≅ Σ^{M} ⇒ Σ ∈ halts iff Σ^{M} ∈ halts;

3. Σ ≅ Σ^{M} ⇒ ans(Σ)==ans(Σ^{M}).

Thus, by Lemma 16 and Theorem 18, to show that gcsm refines mspm it suffices to show that for every pair of similar accessible states, any transition of gcsm corresponds to either a transition of mspm or a no-op. The garbage collections will correspond to no-ops. The proof itself must show how to extend a given ∼ for any transition of the abstract state machine that allocates new memory. And it must also show that the similarity is preserved for transitions that do not allocate new storage. In our proof, the similarity holds with respect to the same ∼ in all non-allocating transitions.

6.2. Legitimacy of Garbage Collection

We now partially specify the gcsm to be a state machine differing from the mspm only in the tuple component acts. We will use g as a function symbol of type states → states, subject to the (axiomatic) assumptions:

1. Σ ≅ Σ^{M} ⇒ g(Σ) ≅ Σ^{M};

Draft of September 29, 1993

2. If Σ consists of stored objects, then so does g(Σ).

We now define acts to be

acts^{M} ∪ {⟨Σ, g(Σ)⟩ | Σ ∈ states},

so that the transitions of gcsm are those of mspm together with garbage collection steps. We will “instantiate” g in the next section with a particular function gc; to do so we will need to establish that axioms 1 and 2 hold of gc. This may be regarded as a form of theory interpretation [7].

To prove that ≅ is a storage layout relation, we will want to show that every modifier expression preserves it. To do so, we will segregate observers and modifiers into the following lemmas, each of which is proved [20] by perfectly straightforward (but lengthy) applications of the definitions:

Lemma 31 (Observers preserve ≈) Let e(s, x⃗) be any of the state observers listed in Table 21, taking state parameter s and possibly other parameters x⃗. Suppose:

1. Σ ≈ Σ^{M}; and

2. the respective components of a⃗ and a^{M} satisfy ≃.

Then e(Σ, a⃗) ≃ e(Σ^{M}, a^{M}).

Lemma 32 (State modifiers preserve ≅) Let e(s, x⃗) be any of the state modifiers listed in Table 22, taking state parameter s and possibly other parameters x⃗. Suppose:

1. Σ ≈ Σ^{M}; and

2. the respective components of a⃗ and a^{M} satisfy ≃.

Then e(Σ, a⃗) ≅ e(Σ^{M}, a^{M}).

In the proof of Lemma 32, the underlying store correspondence ∼ is used unaltered for every mutator except make-stob, and in this case the new correspondence ∼′ is the extension of ∼′ which associates the newly allocated locations.

The following lemma ensures that test expressions in rule programs are invariant with respect to similar states:

Lemma 33 Suppose:

Draft of September 29, 1993

1. e(s, x⃗) and e′(s, y⃗) are observer expressions;

2. Σ ≈ Σ^{M}; and

3. the respective components of a⃗ and a^{M} satisfy ≃;

4. the respective components of b⃗ and b⃗^{M} satisfy ≃;

Then e(Σ, a⃗) = e′(Σ, b⃗) iff e(Σ^{M}, a^{M}) = e′(Σ^{M}, b⃗^{M}).

Proof. By structural induction on observer expressions, using Lemma 31 and the definition of ≈. QED.

Lemma 34 (Rule programs ≅-invariant) Suppose that P is a rule program, and that Σ_{0} ≅ Σ_{0}^{M}.

1. Suppose P terminates in a state Σ_{1}, when started from Σ_{0}. Then there exists a state Σ_{1}^{M} such that P terminates in Σ_{1}^{M} when started from Σ_{0}^{M} and Σ_{1} ≅ Σ_{1}^{M}.

2. Conversely, suppose P terminates in a state Σ_{1}^{M}, when started from Σ_{0}^{M}. Then there exists a state Σ_{1} such that P terminates in Σ_{1} when started from Σ_{0} and Σ_{1} ≅ Σ_{1}^{M}.

Proof: Consider C and C^{M}, the maximal computations starting with underlying mspm states Σ_{0} and Σ_{0}^{M} respectively. We show by induction on i that the control nodes of C(i) and C^{M}(i) are equal, and that the underlying mspm states are in ≅. The base case is immediate. If the control node of C(i) is a choice point (i.e. an if or while test), then we apply Lemma 33 to show that the next pair of control nodes are equal; there is no change in the underlying mspm states. Otherwise, we apply Lemma 32 to show that the next pair of underlying mspm states remain in ≅; there is no choice about the next control node. So if C(j) is a halt state, then, as only the control node matters, so is C^{M}(j), and conversely. Moreover, we may take Σ_{1}^{M} (for assertion 1) and Σ_{1} (for assertion 2) to be the underlying states of C^{M}(j) and C(j) respectively.

Lemma 35 Suppose:

1. R is any mspm rule with auxiliary variables x⃗;

2. The domain condition for R is satisfied in Σ using the witnessing values a⃗ in place of x⃗; 3. Σ ≈ Σ^{M};

Draft of September 29, 1993

4. Σ consists of stored objects.

Then there is a unique a^{M} such that:

1. #a⃗ = #a^{M};

2. a⃗(i) ≃ a^{M}(i), for each i where 0 ≤ i < #a⃗;

3. The domain condition for R is satisfied in Σ^{M} using the witnessing values a^{M} in place of x⃗.

Proof: Let a^{M}(i) be a⃗(i) if the latter is not of the form ⟨ptr ℓ⟩. Otherwise, let a^{M}(i) be ⟨ptr ℓ^{M}⟩ where ℓ^{M} is the unique ℓ′ such that ℓ ∼ ℓ′. If this a^{M} is well-defined, then it is clear that conditions 1 and 2 are satisfied, and condition 3 follows from Lemma 33, given that the domain conditions are always equations between observer expressions. Moreover, for non-pointer a⃗(i), ≃ requires equality, so there is no alternative candidate. When a⃗(i) is a pointer, the definedness of the definite description operator entails that there is no alternative candidate. Thus, it suffices to show that there is a unique ℓ′ such that ℓ ∼ ℓ′, whenever ⟨ptr ℓ⟩ is a witnessing value for a domain condition auxiliary variable. By Definition 11 clause 1, there is at most one such ℓ′. Inspecting the domain conditions of the rules, we find three cases:

1. The value of some state register r_{0} is ⟨ptr ℓ⟩;

2. The value of some state register r_{0} is ⟨ptr ℓ_{0}⟩, and ⟨ptr ℓ⟩ is a component of the object stored at ℓ_{0};

3. The value of some state register r_{0} is ⟨ptr ℓ_{0}⟩; ⟨ptr ℓ_{1}⟩ is a component of the object stored at ℓ_{0}; and ⟨ptr ℓ⟩ is a component of the object stored at ℓ_{1}.

The third case occurs in the rules to reference or set the value of a global variable, as the store location for the variable is determined from the current template table. In the first case, we use Definition 13 clause 3 to infer that, if v is the value of r_{0} in Σ^{M}, then ⟨ptr ℓ⟩ ≃ v. By Definition 12, v is of the form ⟨ptr ℓ^{M}⟩, and by clause 1c, ℓ ∼ ℓ^{M}. The remaining cases are similar, except that Definitions 13 and 12 must be used repeatedly.

Theorem 36 (Transition preserves ≅) Suppose that Σ_{0} ≅ Σ_{0}^{M} and that gcsm can proceed from Σ_{0} to Σ_{1}. Then either:

Draft of September 29, 1993

1. Σ_{1} ≅ Σ_{0}^{M} or

2. there exists a Σ_{1}^{M} such that mspm can proceed from Σ_{0}^{M} to Σ_{1}^{M} and Σ_{1} ≅ Σ_{1}^{M}.

Proof: If Σ_{1} ≅ Σ_{0}^{M}, then we’re done, so assume otherwise. Since this is not a g-transition, there is an mspm rule R such that ⟨Σ_{0}, Σ_{1}⟩ ∈ R, and by the determinacy of mspm, there is just one such R. Since R is applicable in Σ_{0}, there is a sequence a⃗ of witnesses for its auxiliary variables. By Lemma 35, R is also applicable in Σ_{0}^{M}. Thus, we may apply Lemma 34 clause 1 to the rule program P implementing R, which completes the proof.

6.3. The Correctness of a Copying Garbage Collector

In the remainder of this section, we present a specific garbage collection algorithm gc and we prove that it satisfies the above property specified of g. The algorithm uses a simple semi-space garbage collection technique where two stores are maintained, one active and one inactive. During garbage collection, “live” data from the active store is copied to the inactive store and then the roles of the two stores are swapped. Live data refers to data that can be accessed either directly or indirectly (via pointers) from the registers (or stack) of the state. The garbage collection algorithm is presented in Figure 2. In this presentation, the new (not-yet-active) store is regarded as the set of locations beyond the end of the old (previously active) store. Thus, if s is the old store, and #s ≤ ℓ, then ⟨ptr ℓ⟩ points at the location ℓ − #s words beyond the beginning of new space. To model the change of active store, we use the auxiliary function shift, a partial function from states and integers to states.

Definition 14 (Shift store, Shift) If s is a store, then

shift store(s, j)(i)== \{ \begin{matrix}⟨ptr ℓ − j⟩ & if s(j + i) = ⟨ptr ℓ⟩ \\ s(j + i) & otherwise \end{matrix}

If Σ is a state, then shift(Σ, j) is the result of replacing the store s of Σ by shift store(s, j), and replacing every component ⟨ptr ℓ⟩ of Σ with ⟨ptr ℓ − j⟩.

Then shift(Σ, j) is a well-formed state if, whenever ⟨ptr ℓ⟩ is a component of Σ, or occurs at a location ℓ_{0} in its store, then j ≤ ℓ_{0} implies j ≤ ℓ. This condition ensures that a pointer always has a nonnegative argument.

The function gc-convert takes a pointer to a stored object in the active store as argument. If the object has not yet been copied from the old store

Draft of September 29, 1993

VLISP SCHEME 65

Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be a gcsm state. Then, gc-convert(⟨ptr l⟩, s) =

⟨⟨ptr l′⟩ s⟩ if s(l − 1) = ⟨ptr l′⟩ (Object already relocated)

⟨⟨ptr l′⟩ s′′⟩ if s(l − 1) = ⟨header h p m⟩ and l′ = #s + 1 and s′ = s^{⌢} s(l − 1)^{⌢} s(l)^{⌢} …^{⌢} s(l + m − 1) and s′′ = s′[l − 1 ↦ ⟨ptr l′⟩]

gc-trace(d, s) =

gc-convert(d, s) if d is a pointer
⟨d s⟩  otherwise

gc-trace-stack(a, s) = ⟨a′ s_{m}⟩ where gc-trace(a(0), s) = ⟨a′_{0} s_{1}⟩ and gc-trace(a(1), s_{1}) = ⟨a′_{1} s_{2}⟩ and gc-trace(a(m − 1), s_{m−1}) = ⟨a′_{m−1} s_{m}⟩ and m = #a and a′ = ⟨a′_{0} a′_{1} … a′_{m−1}⟩

gc-scan-heap(s, m) =

s  if m = #s

gc-scan-heap(s′[m ↦ d], m + 1),

where ⟨d, s′⟩ = gc-trace(s(m), s) otherwise

gc_{0}(Σ, n) = ⟨t′, n, v′, a′, u′, k′, s_{7}, r⟩ where gc-trace(t, s) = ⟨t′ s_{1}⟩ and gc-trace(v, s_{1}) = ⟨v′ s_{2}⟩ and gc-trace(u, s_{2}) = ⟨u′ s_{3}⟩ and gc-trace(k, s_{3}) = ⟨k′ s_{4}⟩ and gc-trace-stack(a, s_{4}) = ⟨a′ s_{5}⟩ and gc-trace(r, s_{5}) = ⟨r′ s_{6}⟩ and gc-scan-heap(s_{6}, n) = s_{7}

gc(Σ) = shift(gc_{0}(Σ, #s))

Figure 2: Garbage Collection Algorithm to the new store, it copies the stored object and returns a pointer to the newly allocated stored object. It also replaces the header of the old stored object with a “broken heart” pointing to the new object; all other pointers to the old stored object can be modified to point to the new object. If the object has already been copied to the new store, gc-convert uses the broken heart. The result of this function is always a pointer to an object in the new store.

Draft of September 29, 1993

The function gc-trace takes an arbitrary value d as argument. If the value d is not a pointer, it returns the argument value d. Otherwise it invokes gc-convert on the pointer d and returns the result.

The function gc-trace-stack successively calls gc-trace on each element of the argument stack a. It accumulates the result values into a new argument stack a′.

The function gc-scan-heap successively calls gc-trace on each value in the new store. Note that each call to gc-trace may potentially extend the new store by copying a stored object to it.

Finally, the function gc invokes gc-trace on all registers, on all components of the stack and on the store. All resulting pointers reference the new store, so we may apply shift to discard the old store.

Since garbage collection is a non-trivial algorithm that transforms the state through a succession of intermediate states, the proof requires the use of a relation similar to ≅ to express an invariant maintained by the algorithm. That is, this technique is used to prove that each intermediate gcsm state encountered during garbage collection is similar (by a state correspondence relation ≅^{gc} still to be specified) to the gcsm state prior to garbage collection. Since ≅^{gc} will be defined to coincide with ≅ when a store contains no broken hearts, it will follow that garbage collection preserves ≅.

Definition 15 (GC Term Correspondence, GC State Similarity) Let ∼ be a store correspondence between s and abstract mspm store s′. The GC term correspondence generated by ∼ is a relation ≃^{gc} between

values cell and cell′, defined by taking cases on cell′. cell ≃ cell′ holds just in case one of the following holds:

1. ⟨ptr l′⟩ = cell′ and, letting a′ = b′ if s′(l′ − 1) = ⟨ptr b′⟩ and letting a′ = l′ otherwise,

(a) ⟨ptr l⟩ = cell, and let a = b if s(l − 1) = ⟨ptr b⟩ and a = l otherwise;

(b) s′(a′ − 1) = s(a − 1) = ⟨header h p m⟩, for some header type h, mutability bit p and stored object length m; and

Draft of September 29, 1993

(c) for all 0 ≤ i < m, (a + i) ∼ (a′ + i).

2. ⟨fixnum m⟩ = cell′ = cell, for some number m.

3. imm = cell′ = cell, for some immediate value imm.

4. b^{∗} = cell′ = cell, for some sequence of bytes b^{∗}.

Σ and Σ′, of the forms ⟨t, n, v, a, u, k, s, r⟩ and ⟨t′, n′, v′, a′, u′, k′, s′, r′⟩, respectively, are GC-similar with respect to ∼, written Σ ≈^{gc} Σ′, just in case:

1. #a′ = #a and ∀0 ≤ i < #a . a(i) ≃^{gc} a′(i);

2. for all locations l′ and l, l ∼ l′ ⇒ s(l) ≃^{gc} s′(l′);

3. x ≃^{gc} x′, where x and x′ are any of the pairs of state components ⟨t, t′⟩, ⟨n, n′⟩, ⟨v, v′⟩, ⟨u, u′⟩, ⟨k, k′⟩, and ⟨r, r′⟩.

Σ and Σ′ are GC-similar, written Σ ≅^{gc} Σ′, just in case there exists a store correspondence ∼ such that Σ and Σ′ are GC-similar with respect to ∼.

The proof of the following lemma simply composes the witness store correspondences.

Lemma 37 ≅^{gc} is a transitive relation. That is,

Σ_{2} ≅^{gc} Σ_{1} and Σ_{3} ≅^{gc} Σ_{2} ⇒ Σ_{3} ≅^{gc} Σ_{1}

GC stored objects are like stored objects, except that we may dereference a broken heart for free:

Definition 16 (GC Stored Objects) Let a = b if s(ℓ − 1) = ⟨ptr b⟩ and let a = ℓ otherwise. Then s contains a GC stored object at ℓ if:

1. s(a − 1) = ⟨header h p m⟩, for some h, p, and m;

2. s(j) is a well-defined non-header value for each j for a ≤ j < a + m.

A state Σ is composed of GC stored objects if, whenever ⟨ptr ℓ⟩ occurs in any (transitive) component of Σ, then the store of Σ contains a GC stored object at location ℓ.

Lemma 38 Suppose that Σ = ⟨t, n, v, a, u, k, s, r⟩ be a state encountered during garbage collection; then Σ is composed of GC stored objects.

Draft of September 29, 1993

Proof: This holds of every accessible gcsm state prior to garbage collection. During garbage collection, all mutations of the state are made via the function gc-trace which preserves this property.

We may now discharge the instance of axiom 2 on g (page 61), as instantiated for our garbage collector.

Theorem 39 (GC preserves stored objects) If Σ consists of stored objects and Σ′ = gc(Σ), then Σ′ consists of stored objects.

Proof: Since Σ consists of stored objects, it consists (a fortiori) of GC stored objects. Using Lemma 38 inductively, the same is true of gc_{0}(Σ). The property of consisting of GC stored objects is preserved by shift, so Σ′ = shift(gc_{0}(Σ), #s) consists of GC stored objects. Finally, Σ′ contains no broken hearts, so it also consists of stored objects.

The following key lemma asserts that the function gc-trace respects similarity, i.e., it maps values and states to similar values and states.

Lemma 40 Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be accessible in garbage collection; let gc-trace(d, s) = ⟨d′ s′⟩ for some d′, s′. If d is not a pointer, or if d = ⟨ptr l⟩ and s contains a GC stored object at l, then there exists a store correspondence ∼ with generated GC term correspondence ≃^{gc} such that

1. d′ ≃^{gc} d

2. Σ ≅^{gc} ⟨t, n, v, a, u, k, s′, r⟩ with ∼ as the witness store correspondence.

Proof: The proof is by cases. We show the crucial case in which d is a pointer ⟨ptr l⟩ and s(l − 1) is a header, rather than a broken heart, so that the object must be copied. Case: d = ⟨ptr l⟩ and s(l − 1) = ⟨header h p m⟩, so, by definition of gc-trace, d′ = ⟨ptr a⟩, a = #s + 1, and

s′ = s\begin{matrix}[a − 1 ↦ s(l − 1)][a ↦ s(l)] … [a + m − 1 ↦ s(l + m − 1)] \\ [l − 1 ↦ ⟨ptr a⟩] \end{matrix}

Define ∼ as follows:

a + i ∼ l + i for 0 ≤ i < m
x ∼ x  for all x ∈ dom(s) such that s(x) is not a header
and x ≠ l + i for 0 ≤ i < m.

Draft of September 29, 1993

1. s(l − 1) = ⟨header h p m⟩ by case condition. s′(a − 1) = s(l−1) = ⟨header h p m⟩ by definition of s′. For all 0 ≤ i < m, a + i ∼ l + i holds by definition of ∼. Thus, by definition of a term correspondence,

⟨ptr a⟩ ≃^{gc} ⟨ptr l⟩.

2. We show that if vd is a value in one of the registers, or a component of the stack, then vd ≃^{gc} vd. If vd is not a pointer, vd ≃^{gc} vd holds by definition of ≃^{gc}. If vd = ⟨ptr x⟩ where x ≠ l, then s(x − 1) = s′(x − 1) = ⟨header h′ p′ m′⟩ for some h′, p′, m′. Further, x + i ∼ x + i for all 0 ≤ i < m′. Thus ⟨ptr x⟩ ≃^{gc} ⟨ptr x⟩ holds by definition of ≃^{gc}. If vd = ⟨ptr l⟩, then we know that s(l − 1) = ⟨header h p m⟩ by case condition. Further, s′(l − 1) = ⟨ptr a⟩ and s′(a − 1) = ⟨header h p m⟩ by definition of s′. Finally, for all 0 ≤ i < m, a + i ∼ l + i holds by definition of ∼. Thus, ⟨ptr l⟩ ≃^{gc} ⟨ptr l⟩ holds by definition of ≃^{gc}.

3. If vd is a component of the store other than a header, then the condition to verify is:

for all x, x′, x′ ∼ x ⇒ s′(x′) ≃^{gc} s(x)

So assume x′ ∼ x. If x ≠ l + i for 0 ≤ i < m, then x = x′ by definition of ∼. Since x is in the domain of ∼, s(x) is not a header (by definition of ∼). Thus x ≠ l − 1, and so s′(x′) = s′(x) = s(x). The result then follows since vd ≃^{gc} vd was shown above for any component of the state. Otherwise, x = l + i for some 0 ≤ i < m. Then, x′ = a + i by definition of ∼. Now s′(x′) = s′(a + i) = s(l + i) = s(x) by definition of s′. The result then follows since vd ≃^{gc} vd was shown above for any component of the state.

Lemma 41 Let Σ = ⟨t, n, v, a, u, k, s, r⟩, where s consists of stored objects, and let gc-trace(s(l), s) = ⟨d′ s′⟩. Then ⟨t, n, v, a, u, k, s′[l ↦ d′], r⟩ ≅^{gc} Σ.

Hence, inductively, gc-scan-heap(s, l) ≅^{gc} Σ.

Proof: By Lemma 40, ⟨t, n, v, a, u, k, s′, r⟩ ≅^{gc} Σ with ∼ as the witness store correspondence (where ϵ = ⟨s, s′⟩). Let ∼ extend to the term correspondence ≃^{gc} where α = ⟨∼, s, s′⟩. Then, by the same lemma, d′ ≃^{gc} s(l). If s(l) is not a pointer, then by definition of gc-trace, s(l) = s′(l) = d′. Thus, s′[l ↦ d′] = s′ and so ⟨t, n, v, a, u, k, s′[l ↦ d′], r⟩ ≅^{gc} Σ.

Draft of September 29, 1993

If s(l) = ⟨ptr a⟩ for some a, then by definition of gc-trace, s(l) = s′(l) = ⟨ptr a⟩ since gc-trace only modifies s(a − 1) which is a header (by lemma 38) and hence a − 1 ≠ l. Thus, we have that d′ ≃^{gc} s′(l) = ⟨ptr a⟩. We show that

⟨t, n, v, a, u, k, s′[l ↦ d′], r⟩ ≅^{gc} ⟨t, n, v, a, u, k, s′, r⟩

since the result will then follow by transitivity of ≅^{gc} (lemma 37). Let ∼ be the identity function on all defined locations of s′ that are not headers of stored objects, and generate term correspondence ≃^{gc}. We prove that ∼ is the witness store correspondence to the above state correspondence. For all terms vd that are components of the state, vd ≃^{gc} vd holds. This is immediate for non-pointer values, while for pointer values ⟨ptr b⟩ it depends on s′(b − 1) and s′[l ↦ d′](b − 1) being the same header value. This holds since we know that s′(l) is not a header and hence l ≠ b − 1. Moreover, s′[l ↦ d′](l) ≃^{gc} s′(l), because, as we showed above, d′ ≃^{gc} s′(l) = ⟨ptr a⟩. Finally, we must show that gc-scan-heap terminates. We assume that the original store s consists of stored objects, and that s_{1} has the property that if i < #s and s(i) is not a header, then s_{1}(i) = s(i). Let ⟨d, s′⟩ = gc-trace(s_{1}(m), s_{1}), let s′′ = s′[m ↦ d], and let #s ≤ m. We have:

1. s_{1}, s′, and s′′ all contain the same total number of headers;

2. Assuming

∀n ≥ m, ∀l′ . s(n) = ⟨ptr l′⟩ ⇒ l′ < #s,

then we may infer

∀n ≥ m + 1, ∀l′ . s′′(n) = ⟨ptr l′⟩ ⇒ l′ < #s,

using the assumptions that s consists of stored objects and agrees with s_{1} on non-headers.

3. If s′′ ≠ s_{1}, then s′′ has one fewer header below #s than did s_{1}.

The correctness of gc_{0} now follows from Lemmas 37, 40, and 41.

Lemma 42 Let Σ = ⟨t, n, v, a, u, k, s, r⟩ and Σ′ = gc_{0}(Σ, #s). Then Σ′ ≅^{gc} Σ.

We now justify the application of shift:

Draft of September 29, 1993

Lemma 43 Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be a gcsm state. If, for some b, ⟨ptr b⟩ is a component of gc(Σ) = ⟨t_{1}, n_{1}, v_{1}, a_{1}, u_{1}, k_{1}, s_{1}, r_{1}⟩ (i.e., if one of t_{1}, v_{1}, u_{1}, k_{1}, a_{1}(i), or s_{1}(i) is the value ⟨ptr b⟩) then

1. b ≥ #s;

2. s_{1}(b − 1) = ⟨header h p m⟩ for some h, p, m.

Proof: By definition of gc, the state components t, v, u, k, a(i), and s(i) are replaced by the values of gc-trace applied to the components. Let Σ′ = ⟨t′, n′, v′, a′, u′, k′, s′, r′⟩ be a state such that if s′ contains a header of the form ⟨ptr b⟩, then b > #s and s′(b − 1) = ⟨header h p m⟩ for some h, p, m. If d′ is the value of one of the above mentioned state components of Σ′, gc-trace(d′, s′) = (d′′, s′′), and Σ′′ is the state obtained by modifying Σ′ with the values d” and s”, then we prove that Σ′′ also satisfies the above property. First, we prove that if s′′ contains a header of the form ⟨ptr b⟩, then b > #s and s′(b − 1) = ⟨header h p m⟩ for some h, p, m. If s′ also contains the same header ⟨ptr b⟩, this follows by induction hypothesis. Otherwise, by definition of gc-trace,

s′ = (s^{⌢} s(l − 1)^{⌢} s(l)^{⌢} …^{⌢} s(l + m − 1))[l − 1 ↦ ⟨ptr #s + 1⟩]

where s(l − 1) = ⟨ptr #s + 1⟩ is the above mentioned header. The result follows since #s + 1 > #s and s′′(#s) = s(l − 1) = ⟨header h p m⟩ for some h, p, m (by definition of gc-trace). Next we show that if d′′ = ⟨ptr b⟩ for some b, then b > #s and s′(b − 1) = ⟨header h p m⟩ for some h, p, m. If ⟨ptr b⟩ is a header in s′, this follows by induction hypothesis. Otherwise, by definition of gc-trace, b = #s + 1 and s′′(#s) = ⟨header h p m⟩ for some h, p, m. Since s′′ and d′′ are the only values that differ between Σ′′ and Σ′, it follows that Σ′′ satisfies the desired property. By induction, we have that all intermediate states during garbage collection satisfy the property. But it follows from the definition of gc-trace that in such states, if gc-trace returns a pointer ⟨ptr b⟩, then b ≥ #s and s_{1}(b − 1) = ⟨header h p m⟩ for some h, p, m.

Finally, combining Theorem 39 with Lemmas 42 and 43, we have:

Theorem 44 (Garbage Collection preserves ≅^{gc}, ≅) If Σ consists of stored objects, then

gc(Σ) ≅^{gc} Σ

and

Σ ≅ gc(Σ).

Draft of September 29, 1993

7. The Finite Stored Program Machine

A finite stored program machine (with any fixed word size) is of course not correct in the strongest sense. It cannot simulate the computation histories of the garbage collected machine, because there will always be computations that require more pointers than can be stored in words of the given size.

The finite stored byte code (fsbc) language is defined to be a strict subset of gsbc. The operational semantics of fsbc is given by a state machine similar to the gcsm. Each microcode transition of the fgcsm is defined to be a restriction of the corresponding microcode transition of the gcsm. That is, if a fgcsm transition is defined on a state, then its value at that state is the same as the corresponding gcsm transition.

The finite machine is only partially correct. That is, any computation history of the finite machine simulates a computation history of the garbage collected machine. Thus, if the finite machine returns a computational answer, then the garbage collected machine computes the same computational answer. The finite machine is easily shown to be correct in this weaker sense.

8. The VLISP Scheme Implementation

vlisp is a comprehensive implementation of Scheme, as is illustrated by the fact that a full bootstrap could be carried out. Moreover, the system has quite acceptable performance. Finally, the verification covers the implementation quite comprehensively.

8.1. The VLISP Bootstrap Process

vlisp is certainly the only verified programming language implementation there is that can be used to bootstrap itself. The possibility of a bootstrap underlines the power of the Scheme source language, as well as the comprehensive character of the vlisp implementation.

There are five source files and two binary files in a vlisp distribution. One binary file is an executable version of the vlisp vm and the other is an image which results from compiling the Scheme to Byte Code compiler. The source files are listed in Table 23. One cycle in the bootstrap process involves using these files to produce a new version of the binary files.

The first action of the vm is to read an image which encodes the initial state of the machine. A new version of the Scheme to Byte Code image is produced using the old image to compile its own source. This new image is used to compile the other Scheme programs, vps.scm and pps.scm. A new vm is produced by first translating the source for the vm into Pure

Draft of September 29, 1993

vscm.scm Scheme to Byte Code compiler
vvm.scm The vlisp vm in vlisp PreScheme
vps.scm The vlisp PreScheme Front End
pps.scm The Pure PreScheme compiler
prims.c I/O primitives for Pure PreScheme

Table 23: vlisp Source Files

Image  Input  Output  Sun4 Run Time (min.)

   old vscm.image  vscm.scm  vscm.image  49
   vscm.image     vps.scm   vps.image  64
   vscm.image     pps.scm   pps.image  2664 (44 hrs.)
   vps.image      vvm.scm   vvm.pps  36
   pps.image      vvm.pps   vvm.s  24

Table 24: Sun4 Bootstrap Run Times

PreScheme using the image produced from vps.scm, and then into assembly language using the image produced from pps.scm. An executable is produced by linking the assembly language with Pure PreScheme’s I/O primitives from prims.c. Since I/O primitives simply call the operating system, and since we are not in a position to prove anything about the effect of a call to the operating system, we did not consider it worth the trouble to code the I/O primitives directly in assembly language. Apart from compiling these C-coded primitives, the only task of the gcc C compiler is to combine the result with the assembly language output vvm.s, and to call the assembler.

One cycle in the bootstrap processes is diagrammed in Figure 3. The small circles in the diagram indicate that the virtual machine given by its right arrow is executed. The image used to initialize the machine is indicated by the top arrow. The input is taken from the file named on the left arrow, and the output is written to the file named on the bottom arrow.

Results of the Bootstrap

Table 24 presents the time required for each step when run on a Sun4 ipx, a 25 specmark sparc-based computer.

After the first bootstrap cycle, the assembly source for the vm is unchanged by any succeeding bootstrap cycle; because of a peculiarity in the

Draft of September 29, 1993

          [figure: vscm.image; vscm.scm; vscm.image; vps.scm; vps.image; pps.scm; vvm.scm; vvm.pps; pps.image; vvm.s; prims.c; gcc -O -o vvm vvm.s prims.c; vvm; . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .]

Figure 3: vlisp Bootstrap Process

way symbols are generated, the image of the Scheme to Byte Code compiler is unchanged by a pair of two bootstrap cycles.

Two initial versions for the vm were constructed. The Scheme sources for the front end and the Pure PreScheme compiler were compiled using Scheme->C [1]. These programs were used to compile the vlisp vm. A second initial vm was constructed by directly implementing the vm algorithms in C.

Two initial images of the Scheme to Byte Code compiler were also constructed. In one, the executable used to compile the source was built by compiling the Scheme to Byte Code compiler using Scheme->C, and this executable was used to compile the source. The image was also constructed using Scheme48 [13]. The bootstrap process was insensitive to the initial image or vm.

8.2. VLISP Virtual Machine Performance

In order to estimate the efficiency of our interpreter program, as compiled by the vlisp PreScheme Front End and the Pure PreScheme compiler, we have also compared it with cvm, the C implementation of the algorithms.

Draft of September 29, 1993

cvm was carefully optimized to ensure that it achieved the maximum performance possible with the type of interpreter we implemented. For instance, we scrutinized the Sun 4 assembly code produced by the gcc C compiler to ensure that registers were effectively used, and that memory references into arrays were optimal.

Differences in performance are due to two main sources. First, we structured the virtual machine program to facilitate our verification. In particular, we used abstractions to encapsulate successive refinement layers in the machine. We also have many run-time checks in the code. They ensure that the conditions for application of the formally specified rules are in fact met as the interpreter executes. Second, gcc has sophisticated optimizations, for which there is nothing comparable in the Pure PreScheme compiler.

Nevertheless, the ratio of the speed of cvm to the speed of the vlisp virtual machine, when run on a Sun 3, is only 3.9. On the Sun 4, it is 6.3. The ratio is higher on the Sun 4 partly because gcc makes very good use of the large Sun 4 register set. Also, gcc does instruction scheduling to keep the Sun 4 instruction pipeline full when possible. Finally, some optimizations to primitives in the PreScheme compiler have been implemented in the Sun 3 version, but not yet in the newer Sun 4 version.

We consider these numbers reasonably good, particularly because there are many additional optimizations that could be verified and implemented for the PreScheme compiler.

8.3. Unverified Aspects of VLISP

Although the vlisp verification is quite comprehensive, and covers the great majority of the detailed implementation, we do not call it a complete verification:

• The verification covers algorithms and data structures used, rather than the concrete code. In most cases the relationship is straightforward, and indeed particular coding approaches were often adopted so that the relationship would be transparent. However, sometimes there is an “interesting” gap between the form of the specification and that of the code.

• The vlisp implementation provides all the standard procedures stipulated in the Scheme language definition. However, because no formal specification has been provided for these user-level procedures, we have not had anything to verify these procedures against. To mitigate this objection, we provide all source code to the user. The majority of the standard procedures are coded in Scheme itself, and can be replaced with any variants the user considers more trustworthy.

Draft of September 29, 1993

• The Scheme language stipulates that some derived syntactic forms should be provided. However, there is no formal account of the expansion process. A user suspicious of these expansions can write programs directly in the primitive Scheme syntax. This is still a high level programming language by any standard.

• In some cases, such as the vlisp Pre-Scheme Front End [16, Section 3], and the compiler proof (Section 2.5), only cases that appeared to us to be “representative” or “interesting” were selected for detailed proof.

• Proofs have not been checked using a mechanical theorem prover.

Although we think it is important to make the limits of our work clear, we still think that it compares very favorably with other research in terms of rigor, clarity, and scope.

8.4. Conclusion.

We believe that the vlisp effort has shown that the rigorous algorithmic verification of substantial programs such as a language implementation is feasible. We have used a relatively small number of techniques which we consider now to be well-defined and broadly reusable.

We consider our decision to carry out the verification at the algorithmic level to have been one key to our success. We also consider the compact and tractable official Scheme semantics to have been another precondition. The third crucial ingredient was using an operational semantics and a state machine refinement approach to the lower levels of the verification. This enabled us to subdivide the complexities of the proof into a succession of intuitively understandable assertions.

These points are developed in more detail in the companion article [11], which also discusses the appropriateness of the different semantic approaches to different parts of the verification.

Acknowledgments. We are deeply indebted to the other participants in the vlisp effort on which this paper is based. They include William Farmer and Leonard Monk of mitre, as well as Dino Oliva and Mitchell Wand of Northeastern University. Leonard Monk suggested many improvements to this paper.

We are also grateful to Northrup Fowler iii of Rome Laboratory as well as to Ronald Haggarty and Edward Lafferty of mitre, for their commitment to enabling us to carry out this work.

Draft of September 29, 1993

References

1. J. F. Bartlett. Scheme–>C: A portable Scheme-to-C compiler. WRL 89/1, Digital Equipment Corporation Western Research Laboratory, January 1989.

2. Will Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, New York, August 1984. The Association for Computing Machinery, Inc.

3. W. Clingers and J. A. Rees (eds.). Revised^{4} report on the algorithmic language Scheme. Technical Report CIS-TR-90-02, University of Oregon, 1990.

4. Paul Curzon. A verified compiler for a structured assembly language. In M. Archer, J. J. Joyce, K. N. Levitt, and P. J. Windley, editors, Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, pages 253–262. IEEE Computer Society Press, 1991.

5. W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell, and V. Swarup. The faithfulness of the VLISP operational semantics. M 92B093, The MITRE Corporation, September 1992.

6. W. M. Farmer, J. D. Guttman, L. G. Monk, J. D. Ramsdell, and V. Swarup. The VLISP linker. M 92B095, The MITRE Corporation, September 1992.

7. W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. Technical report, The MITRE Corporation, 1992. Submitted to CADE-11.

8. R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19–32. American Mathematical Society, 1967.

9. J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The VLISP byte-code compiler. M 92B092, The MITRE Corporation, September 1992.

10. J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The VLISP flattener. M 92B094, The MITRE Corporation, 1992.

Draft of September 29, 1993

11. J. D. Guttman, J. D. Ramsdell, V. Swarup, D. Oliva, and M. Wand. Results and conclusions of the VLISP verification. Submitted to LASC.

12. IEEE Std 1178-1990. IEEE Standard for the Scheme Programming Language. Institute of Electrical and Electronic Engineers, Inc., New York, NY, 1991.

13. Richard Kelsey and Jonathan Rees. Scheme48 progress report. Submitted to LASC, 1993.

14. R. E. Milne and C. Strachey. A Theory of Programming Language Semantics. Chapman and Hall, 1976.

15. J S Moore. Piton: A verified assembly-level language. Technical Report 22, Computational Logic, Inc., Austin, Texas, 1988.

16. D. P Oliva, J. D. Ramsdell, and M. Wand. A verified compiler for VLISP PreScheme. Submitted to LASC.

17. W. Polak. Compiler Specification and Verification, volume 124 of Lecture Notes in Computer Science. Springer-Verlag, 1981.

18. J. D. Ramsdell, W. M. Farmer, J. D. Guttman, L. G. Monk, and V. Swarup. The VLISP PreScheme front end. M 92B098, The MITRE Corporation, September 1992.

19. Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.

20. V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk, and J. D. Ramsdell. The VLISP byte-code interpreter. M 92B097, The MITRE Corporation, September 1992.

21. V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk, and J. D. Ramsdell. The VLISP image builder. M 92B096, The MITRE Corporation, September 1992.

22. M. Wand and D. P. Oliva. Proving the correctness of storage representations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 151–160, New York, 1992. ACM Press.

Draft of September 29, 1993