, , 1–78 ()

\begin{matrix}c \\ ◯ \end{matrix} Kluwer Academic Publishers, Boston. Manufactured in The Netherlands.

The VLISP Verified Scheme System^{*}

JOSHUA GUTTMAN guttman@mitre.org VIPIN SWARUP swarup@mitre.org JOHN RAMSDELL ramsdell@mitre.org The MITRE Corporation 202 Burlington Road Bedford, MA 01730-1420

Abstract. The vlisp project 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 primary 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.

Keywords: Scheme, verified, compiler, interpreter, denotational semantics, operational semantics, refinement, garbage collection

Table of Contents

1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.1 Structure of the VLISP Implementation . . . . . . . . . . . . . . . . . . . . 3 1.2 Structure of the Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 How to Read This Paper . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2 The Byte-Code Compiler . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1 The Scheme Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 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 Faithfulness of an Operational Semantics . . . . . . . . . . . . . . . . . . . . . . 31 3.1 Operational Semantics of the Basic Byte Code . . . . . . . . . . . . . . . . 31 3.2 Faithfulness: Form of the Proof . . . . . . . . . . . . . . . . . . . . . . . . . 34

4 State Machine Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.1 State Machines . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 4.2 Refinement and Storage Layout Relations . . . . . . . . . . . . . . . . . . . 39

5 The Flattener . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43

* The work reported here was carried out as part of The MITRE Corporation’s Technology Program, under funding from Rome Laboratory, Electronic Systems Command, United States Air Force, through contract F19628-89-C-0001. Preparation of this paper was generously supported by The MITRE Corporation.

5.1 The Basic Byte Code in More Detail . . . . . . . . . . . . . . . . . . . . . . 44 5.2 Flattened Byte Code Syntax and Operational Semantics . . . . . . . . . . . 45 5.3 The Flattener . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 5.4 Code Correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 5.5 State Correspondence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50

6 The Virtual Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 6.1 Stored Byte Code and its State Machine . . . . . . . . . . . . . . . . . . . . 54 6.2 The Instantiated SBCM Description . . . . . . . . . . . . . . . . . . . . . . 57 6.3 The Garbage-Collected Stored Byte Code Machine (GSBCM) . . . . . . . . 59 6.4 The Instantiated GSBCM Description . . . . . . . . . . . . . . . . . . . . . 65 6.5 The Finite Stored Byte Code Machine (FSBCM) . . . . . . . . . . . . . . . 73 6.6 Concrete Virtual Machine . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73

7 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75

1. Introduction

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

An implementation for a programming language 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 [10], is of this mixed type. It consists of:

• 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 Pre-Scheme [10]) to execute the resulting byte code programs;

• A second compiler to translate the PreScheme code of the interpreter into assembly language code for a commercial workstation.

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 [12]. An introductory paper [7] discusses the goals and methods of the effort as a whole. The present paper is intended to serve 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, not about concrete program text. We have carefully constructed the actual program text so that it will be a transparently faithful embodiment of the algorithm. Reasoning directly about the concrete program text (under its formal semantics) is considerably more cumbersome. The mass of detail involved in verifying concrete programs frequently obscures the essential reasons why the program is correct.

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. Formal derivations, possibly assisted by mechanical proof tools, might well provide less real insight than mathematical proofs, unless the derivations were accompanied by carefully written, humanly understandable mathematical proofs. We discuss this point further in [7].

1.1. Structure of the VLISP Implementation

The vlisp Scheme implementation derives from Scheme48 [10], and is thus a bytecoded 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.1.1. The Compiler Stages

The compiler stages act on source programs in the Scheme language, taking as its input abstract syntax trees in a format only slightly different from the format used in the Scheme Standard [9]. The ultimate output is in a linearized, binary format byte code suitable for execution in the vm. We will refer to the composite of the compiler stages as the “extended compiler.”

The extended compiler consists of a sequence of procedures which rewrite the original source program in a succession of intermediate languages. Of these, we will discuss two in this paper:

• The byte code compiler [5] rewrites the Scheme source code into a treestructured byte code based on Clinger’s target language [1]. 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 flattener [6] uses branch instructions to linearize conditional code and code to be executed after a procedure call returns. We call the output language of the linearizer the flattened byte code (fbc).

The other layers omitted from this description do not raise significant new verification issues. Their purpose is to apply other transformations needed to produce a binary image format that we call Stored Byte Code or sbc [16]. This is the form that is loaded and executed by the vlisp Virtual Machine.

1.1.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 implementation steps.

These 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.

The 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 are three implementation steps. They involve the following three 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.

• The stored byte code machine, or sbcm, which executes the byte code images produced by the compiler stages;

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

• The finite stored byte code state machine, or fsbcm, which has heaps of bounded size and has a bound on the width of an integer or pointer.

The first step defines the state transitions of the sbcm in terms of programs that manipulate the atomic components of its state. The second step demonstrates that the gcsm is a faithful refinement of the sbcm. The third step justifies the use of a finite state machine. The fsbcm cannot 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. This is a sort of partial correctness.

Table 1. vlisp Verification Steps

Proof Step  Languages  Machines  Section
Byte Code Compiler  Scheme, bbc  —  2
Faithfulness  bbc  bbcm  3
Flattener  bbc, fbc  bbcm, fbcm 5
Procedural Instantiation  sbc  sbcm  6.2
Garbage Collector  ”  sbcm, gcsm 6.3
Finiteness  ”  gcsm, fsbcm 6.5

1.2. Structure of the Verification

The full vlisp Scheme verification is a succession of nine subverifications. Five of these justify successive compiler stages. Three justify the implementation steps embedded in the vm. The remaining subverification justifies the switch from the denotational style of semantics to an operational style. It thus provides a link between, on the one hand, the proofs of the first two compiler stages and, on the other hand, the proofs of the remaining compiler stages and all of the vm proofs.

1.2.1. Main Techniques

In this paper we will describe in detail instances of three of the four main techniques sketched in the introductory paper [7]. They include a Wand-Clinger style denotational compiler proof (Section 2); a proof that an operational semantics is faithful to a denotational semantics (Section 3); and two proofs of state machine refinement using storage layout relations (Sections 5 and 6). Of these, the first uses a simple, inductive form of definition to define the storage layout relation. The second, the garbage collection proof, must contend with cyclic structures, and therefore uses a second-order form of definition. The vlisp Scheme implementation does not use transformational compilation, which is discussed in [12].

Not all the steps in the vlisp Scheme verification are discussed in this paper. In particular, the compiler stages include a tabulator, a linker, and an image builder that do not require new techniques.

We have ordered the material to reflect a top-down view of the implementation. Within the vm, the focus will be on the garbage collection proof.

The next five subsections describe the remainder of this paper, with Subsection 1.2.n devoted to Section n of the paper. Table 1 summarizes the main vlisp verification steps discussed in this paper.

1.2.2. The Byte Code Compiler

Section 2 describes the byte code compiler, the first of the compiler stages mentioned in Section 1.1.1. It presents a proof that the byte code compiler preserves the semantics of the Scheme source code. The proof itself is adapted from Clinger’s compiler proof [1], which in turn elaborates an approach derived from Wand [17]. In this approach, the source and target languages are both given denotational definitions using the same domains; thus, one can stipulate that the compiler is correct if the denotation of its output code is the same as the denotation of its input.

The denotational semantics for Scheme and for the byte code target language occupy Sections 2.1 and 2.2. We then turn to the main impediment to adapting Clinger’s proof. The problem is that the official Scheme semantics makes theoretical provision for procedures that may return multiple values. However, ieee standard Scheme offers no way of constructing such procedures, and an implementation need not support them, as vlisp does not. This contrast between the official semantics and the expressive resources of the language in its current state required us to develop (in Sections 2.3–2.4) a denotational theory interrelating procedure objects and the single-valued procedures that approximate them.

The section, thus, provides an illustration of “real-life” formal methods, in which the specification to be established may not reach the verifier in a convenient form. We encountered a mismatch between the given specification and the intended implementation and proof technique.

With the alternative semantics in hand, we carry out a Clinger-style proof in 2.5.

1.2.3. Faithfulness of an Operational Semantics

Later portions of the implementation were justified using an operational semantics based on state machines. Section 3 is devoted to justifying the transition from the denotational semantics of Section 2.2 to a corresponding state machine semantics. We show that the state machine semantics is faithful to the denotational semantics. By this we mean that when the state machine, starting with a program p, computes a final answer, then that is the answer predicted by the denotational semantics for p. To prove this, we use the denotational semantics to attach an answer to each state, and we prove that the transitions of the state machine leave the answer unchanged. Thus, faithfulness reduces to observing that initial states faithfully embed the semantics of the program to be executed, and that final states deliver their answers correctly.

The approach is conceptually simple and eminently suited to mechanization. However, it does not establish the converse: namely, when the denotational semantics predicts that p will evaluate to a particular answer, then the state machine actually delivers it. The method of [12, Section 5] can be used to establish this.

1.2.4. State Machine Refinement

The remainder of the paper consists of a sequence of state machine implementation steps. These steps are of two kinds, which we call refinement steps and instantiation steps. Section 4 sets up a general framework for the refinement steps.

A more concrete machine refines a more abstract machine when the former can compute the same final answers as the latter, when started in corresponding initial states. This idea is formalized in Definition 9. In order to prove that this relation holds, it is convenient to have a relation between states of the two machines. As the machines compute, the relation should be preserved, and if they reach final states, the relation should entail that the answers achieved are equal. Following [18], we call such a relation a storage layout relation. We formalize this notion in Definition 11; we prove in Theorem 6 that a storage layout relation guarantees that refinement holds. The theorem justifies a general method that in [18] is presented only by means of an example.

In some cases we use state machine refinement to justify a translation between two different programming languages. In these cases, we exhibit a storage layout relation ∼ between the two state machines that give semantics for the languages. We also show that the translation function F establishes the relation ∼. Typically, one state component contains the program to be executed, so that establishing the relation ∼ means showing that Σ′ ∼ Σ, where Σ′ is the concrete state that results from Σ by replacing its program p by F (p).

An instantiation step replaces a declarative specification of a transition relation by a procedural specification of it. Thus, the state space of the machine is unchanged in an instantiation step. In fact, the transition relation may also be left unchanged in an instantiation step, or alternatively the degree of non-determinism in the transition relation may be reduced. What changes is the form of description of the transition relation. In place of a declarative description of the transition relation, we substitute a procedural description instead. To justify an instantiation step, we must show that whenever a state Σ is in the domain of the original transition relation Tr, then the procedure being introduced, when started in state Σ, terminates in some state Σ′, and moreover Tr(Σ, Σ′).

We have not emphasized instantiation as a separate major technique. As we use it, either the justification requires only simple Hoare-style reasoning, as in Section 6.2; or else the justification centers on a relation much like a storage layout relation, as in Section 6.4.

1.2.5. The Flattener

The primary purpose of this section is to illustrate storage layout relations as a way to justify a language translation F. The translation F is the vlisp algorithm for linearizing code.

After some syntactic preliminaries (Section 5.1) we present the operational semantics of the target language in Section 5.2. The flattener algorithm itself is described in Section 5.3. The main content of the assertion that the flattener F establishes ∼ is presented in Section 5.4, Theorem 7. In Section 5.5 we then show that ∼ really is a storage layout relation.

1.2.6. The Virtual Machine

In Section 6, we describe the implementation steps used within the virtual machine. In this section there are no further changes in the programming language being executed; this is in all cases the binary stored byte code sbc. By contrast, the notion of execution is successively refined.

Section 6.2 shows how to instantiate the sbcm state machine using very simple operations. These operations are divided into state observers and state modifiers. The state observers are functions that return the value of one ultimate (atomic) constituent of the state; for instance, the value stored at a particular location in the store. State modifiers return an altered state by changing the contents of one atomic ultimate constituent of the state. To implement the declaratively defined “macrolevel” instructions of the sbcm, we give a short program that executes observers and modifiers. Very few of these programs require iteration, so the simplest Hoare-style program verification suffices for ensuring them correct.

Section 6.3, on garbage collection, makes up the bulk of the discussion of the vm. There are two main facts to be established. The first, which is the subject of Section 6.3.2, is that garbage collection is a legitimate implementation strategy for the sbcm. There are many state machines for which this would not be the case; for instance, machines that allow pointer arithmetic. To establish the legitimacy of garbage collection for the sbcm, we specify the state machine gcsm, but without defining a specific garbage collection algorithm. We then exhibit a storage layout relation to establish state machine refinement.

The primary interest in this portion lies in how the storage layout relation is defined. The possibility of circular data structures means that the inductive form of definition used in the flattener proof is not available. We use instead a second order existential quantifier to assert the existence of a function correlating store locations within the gcsm and sbcm states.

The second main fact to be established is that a particular copying garbage collection algorithm does indeed respect the storage layout relation, and this instantiation step is the content of Section 6.4.

The brief Section 6.5 justifies the transition to the state machine fsbcm. This state machine has as its states a subset of those of the gcsm, in which state components are of bounded size. Its transition relation is the restriction of the transition relation of gcsm to the smaller set of states. Therefore it is clearly correct as an implementation of the gcsm, at least in the sense that when it computes an answer a, then the gcsm could also compute the same answer.

Table 2. Scheme Abstract Syntax

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 ::= 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 ::= identifiers (variables)
Γ ::= e  (commands)

1.3. How to Read This Paper

Many portions of this paper can be read independently. Section 2 can be read on its own; it describes the denotational methods we used in vlisp. Section 3 relies on Sections 2.1–2.2, but not on the remainder of Section 2. Sections 5 and 6 both depend on Section 4, which justifies the storage layout method in general terms. However, their dependence on earlier material—and on each other—is limited to the bnf presentations of syntax.

We have gathered presentations of syntax, declarations of semantic functions and representative semantic clauses, and similar material into tables. For ease of reference, a list of tables appears on page 77 at the end of the paper.

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 [1] and Kelsey and Rees [10]. 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 two-dimensional ⟨over, down⟩ lexical addresses for lexical variables, which it distinguishes from global variables.

The compiler algorithm itself is a syntax-directed recursive descent, based on the abstract syntax shown in Table 2. 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:

   ⟨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.

In this and subsequent bnf presentations, we regard the label on the left hand side, such as e and c, both as a typical variable ranging over the syntax class being defined, and also as symbol naming the class, in this case the Scheme expressions and constants, respectively. Thus, we will write the type of a function f taking arguments from e and yielding values in a class C in the form f : e → C.

The compiler’s target language is the Basic Byte Code language (bbc). Expressions of bbc are nested sequences constructed ultimately 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 templates, representing procedures, which consist of the keyword lap followed by a constant, which annotates the name of the procedure, and the code of the procedure;

b for closed instruction lists or blocks, in which execution eventually encoun-

ters a call or return instruction; y for open instruction lists, in which execution eventually runs off the end; z for neutral instructions that may occur in either closed or open instruction

lists; and w for (general) instruction lists, the union of the open and closed lists.

This syntax as defined in Table 3 is 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, and this pattern is crucial to the correctness of the flattener (Section 5). When a conditional expression is the last Scheme expression in the block being compiled, the compiler can emit a closed instruction list in which the code of each branch will contain a call or return instruction. 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 emits an open instruction list in which neither branch is terminated by a call or return. Thus, execution “drops into” the following code when the selected branch is completed. The flattener algorithm uses this distinction between open and closed instruction lists systematically. Its semantic significance is summarized in Lemmas 15 and 16.

After taking cases based on the abstract syntax class of the expression being compiled, the compiler algorithm combines the code produced by its recursive calls with some additional instructions. The main dispatch and one typical case, which

Table 3. Grammar for the Basic Byte Code

t ::= ⟨lap c b⟩
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⟩

         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⟩
w ::= b | y

compiles an application, are shown in slightly simplified form in Figure 1. The remaining cases are not presented here. 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,” a bbc instruction list. It is the result of a recursive call to the main dispatch to compile the portion of the procedure after the expression currently being compiled. It will be attached at the end of the code generated from the current expression.

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 on its expression argument, so that it is guaranteed to terminate.

Syntactic correctness. If e is a Scheme expression, then C(e, ρ_{C}, 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 ρ_{C} and w, which are the empty compile-time environment and code consisting of a bare return respectively.

Theorem 1 (Compiler syntactic correctness)

For any Scheme expression e, compile-time environemnt ρ_{C}, bbc closed instruction sequence b_{0}, and bbc open instruction sequence y_{0},

(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.

1. C(e) is a bbc template;

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

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

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

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 for semantic correctness. In order to carry out this idea, we will need to describe the formal semantics of the Scheme and of the byte code.

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. See [15] for a description of the underlying approach, and [5] for additional details; we have summarized some notation in Table 4. Apart from a few cosmetic changes of notation, our version differs from the standard in three ways.

• The domains have been made somewhat more concrete. In particular, the domian of locations L has been identified with rthe natural numbers N, and consequently S, the domain of stores, has been identified with E*. This formalizes our decision to regard memory as unbounded, at this level of the verification.

• 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 have been added. It was needed to prove that an operational semantics for the bbc is faithful to its denotational semantics.

Perhaps the main cosmetic change is that we regard sequences as partial functions from natural numbers to values. To project the ith element from a sequence s, we write the function application s i. We treat pairs similarly.

Table 4. Some Notation

⟨ … ⟩  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
a:: s  prepend (cons) a before s
p 0, p 1  left and right components (resp)

of a pair p of type D_{0} × D_{1}

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 5. Domains for the Semantics of Scheme

ν ^{∈} N  natural numbers
α ^{∈} L = N  locations
ρ ^{∈} U = i → L  environments
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

Table 6. Scheme Semantic Functions

K : c → E
E : e → U → K → C
E* : e* → U → K → C
C : Γ* → U → C → C

The domains used in the denotational semantics of Scheme are presented in Table 5. Exactly one “domain equation” is actually not an equation. It implicitly introduces an isomorphism ψE between E and a disjoint sum domain, E_{Σ} = Q + H + R + … 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, but not involving E.

The semantic domains are given in Table 6. They are not disjoint from the syntactic domains of the abstract syntax of Scheme as given in Table 2, because a Scheme constant c may be a number, boolean, …, or else a list, dotted list, or vector of other constants. These are members of the domains R, T, …, or else E_{p} or E_{v}. In this second group of cases, the Scheme definition stipulates that the pair or vector be immutable, in contrast to the objects produced by calling cons or make-vector, which may be side-effected.

Semantics of Constants. The semantics of constants, given by a function K, is “intentionally undefined” in [9]. Although we will not define a particular choice of K, we will need to give some constraints that it must satisfy. In essence, we consider its actual value to be a parameter to the semantics of Scheme. We do, however, 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 in E

K[[nil]] = null in E; K[[#f]] = false in E; and K[[#t]] = true in E

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

1. 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. From this it follows that types are correct: if c is a string, vector, or pair, then K[[c]] : D where D is E_{s}, E_{v}, or E_{p}, respectively.

2. Lengths are correct:

(A) Suppose c is a vector of length n, and K[[c]] is a non-bottom value ϵ; then the length of its left component is n, i.e. #((ϵ | E_{v}) 0) = n.

Table 7. Scheme Semantics: Some Semantic Clauses

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”

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

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

The syntax of constants, together with the type correctness condition 1, ensures 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 pairs and vectors.

Semantics of Expressions. In Table 7, we give the clauses—almost unchanged from [9]—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 [5].

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

Table 8. Byte Code Semantics: Additional Domains

ψ ^{∈} 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 9. Byte Code Semantic Functions

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 ∪ {⟨⟩}.)

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 the contents of 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 8. Semantic functions appear in Table 9, and representative semantic clauses stated in terms of these semantic functions are presented in Table 10. Together with similar clauses, they specify a semantics for the bbc.

The B[[⟨⟩]] 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 11) follow the Wand-Clinger style of byte code specification. In each case, the auxiliary function takes as arguments:

• the denotations of the operands of the instruction (if necessary);

• the denotation of the code following the current instruction;

• 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

Table 10. Some Byte Code Semantic Clauses

T [[⟨lap c b⟩]] = B[[b]]

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[[⟨push⟩]] = λρ . push

Table 11. Some Byte Code Auxiliary Functions

make cont : P → N → P → P

make cont =

λπ′νπ . λϵϵ*ρ_{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}ψ

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 ψϵ will β-reduce 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-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 [12, Theorem 9], 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 [14] 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, 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 following association of values, the semantics predicts that the correct computational answer from the program is 3:

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

When the program (F) is executed, the procedure value stored in location ℓ_{1} is retrieved, and its second component, ϕ_{1} is invoked with no arguments. It in turn applies the continuation κ_{0} to the sequence ⟨1, 2, 3⟩, which should then return the computational answer 3. However, if an implementation makes no provision for multiple-value returners, and if κ_{0} is implemented at all, then it always results in the wrong answer 1.

Table 12. Pure Procedure Objects

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

In the next section, we will formalize the reasoning that justifies an implementation in assuming it need implement only “single-valued” objects, and need make no provision for multiple value returners.

In essence our approach is to introduce a new semantics for Scheme. In this semantics, it is clear that there is no mechanism for multiple return values. Since this alternate semantics uses “single valued approximations” to the values used in the standard semantics, we will introduce an operator called sva that will transform the standard semantics E into an alternate semantic function (sva E). With the alternate semantics 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:

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

at least in the intended case in which the initial values κ and σ—the halt continuation and the initial store respectively—are unproblematic, single-valued objects in a sense to be defined (Theorem 2, clause 2).

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

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

yield the same answer when applied to suitable initial values (Theorem 4).

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 12). 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. trunc : E* → E* is the non-strict function which takes its argument ϵ* to ⟨zeroth ϵ*⟩. Hence

trunc ϵ* = \{ \begin{matrix}⟨⊥E*⟩ & if ϵ* = ⊥E* or ϵ* = ⟨⟩ \\ ⟨ϵ* 0⟩ & otherwise. \end{matrix}

and #(trunc ϵ*) = 1, even for ϵ* = ⊥E*.

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

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

The auxiliaries one arg and multiple coerce from K to K_{1} and back. Expanding the definitions, we have:

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

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

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_{Σ}.

Definition 2 (D, Ω, E-free)

D is the smallest set of domains containing:

1. The primitive Scheme semantic domains N, T, T_{L}, Q, H, R, M, E, and A;

2. The Scheme syntactic classes e, c_{pr}, i, and Γ, regarded as flat domains to which a ⊥ has been added;

3. The byte code syntactic classes t, b, y, z, and w, also regarded as flat domains to which a ⊥ has been added;

and closed under the operations:

1. →, producing function domains (containing continuous functions);

2. +, producing disjoint union domains;

3. ^{∗}, producing sequence domains; and

4. ×, producing product domains.

We 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; in this case we will refer to the operator of the domain and the arguments of the domain. A domain not produced by one of these operators will be called an indecomposable domain.

Ω is the disjoint union of D (in some order).

If D ∈ D, we call D E-free if D is not E, and every argument of D is E-free.

We assume E to be indecomposable, as opposed to E_{Σ}, which has + as its operator. We next define 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}. This function ϕ′_{p} calls ϕ_{p} with a singlevalued approximation to the same expressed value arguments and with the same store. The continuation argument is truncated to ensure that the modified continuation can access only one expressed value, and only a single-valued approximation to that. Crudely put, ϕ′_{p} cannot pass anything infected with multiple values 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 operator of the domain. Thus, the only interesting case is the one for procedure objects ϕ_{p}.

Definition 3 (Respecting types, f^{D}, Single-valued approximation)

Given f : Ω → Ω, f respects types if f is strict, and for every D in D and every x in Ω such that x : D, we have fx : D.

For each D in D, let f^{D} ∈ D → D be defined, for d ∈ D, to be

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

sva : Ω → Ω is the least fixed point of the operator α ∈ (Ω → Ω) → (Ω → Ω), which is defined as follows. Let f ∈ Ω → Ω and ω ∈ Ω be arbitrary. Then:

1. if ω = ⊥_{Ω}, then αfω = ω;

2. if ω : D for an indecomposable D other than E, then αfω = ω;

3. if ω : E, then

αfω = (ψE^{−1}(f(ψE(ω | E)in Ω) | E_{Σ}))in Ω;

4. if ω : F_{p}, then

(λϵ*κ . (ω | F_{p}) (fE* ϵ*) (λϵ* . (fC(κ (trunc (map fE ϵ*))))))in Ω,

where (map fE ϵ*) is taken to be ⊥E* for ϵ* = ⊥E*;

5. 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}, and lift these to g : D → D; αfω = g(ω | D)in Ω. More explicitly:

(A) If ω : D_{0} → D_{1}, then αfω = (λy . (f^{D_{1}} ((ω | (D_{0} → D_{1})) (f^{D_{0}} y))))in Ω;

(B) If ω : (D_{0} +…+D_{n}), and comes from the ith argument D_{i} in the sense that (ω | (D_{0} + … + D_{n})) : D_{i}, then αfω = (f^{D_{i}}((ω | (D_{0} + … + D_{n})) | D_{i}))in Ω;

(C) If ω : D* and ω | D* = ⟨x, …, y⟩, then αfω = ⟨f^{D} x, …, f^{D} y⟩in Ω;

(D) If ω : D_{0} × D_{1} and ω | D_{0} × D_{1} = ⟨x, y⟩, then αfω = ⟨f^{D_{0}} x, f^{D_{1}} y⟩in Ω.

All of the real work of α is done by the truncation in the case 4.

If ω : D, then αfω : D; because in addition αf is strict, for all f : Ω → Ω, αf respects types.

As a consequence of the definition, we may infer computational rules for manipulating expressions of the form sva t, depending on the type of t.

Lemma 2 (Rules for sva)

1. If D ∈ D is indecomposable and different from E, then sva^{D} is the identity on D.

2. If D ∈ D is of the form D_{0} → D_{1} and different from F_{p}, and f ∈ D, then

(sva f) = λy . sva(f(sva(y))).

3. If D ∈ D is of the form D_{0}^{∗}, and x = ⟨x_{0}, …, x_{n}⟩ ∈ D , then

sva x = ⟨sva x_{0}, …, sva x_{n}⟩,

and similarly for product types.

4. If D ∈ D is of the form D_{0} + … + D_{n}, and x : D_{i}, then

sva x = (sva(x | D_{i}))in D.

Hence, if D is E-free, then sva^{D} is the identity on D.

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

Lemma 3 sva is idempotent.

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 the 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 clause 4. Let ω : F_{p}; we must show that (α f)(α f ω) = (α f ω). By clause 4, the former (projected into F_{p} for convenience) equals:

λϵ*κ . (λϵ*κ . (ω | F_{p})(fE*ϵ*)(λϵ_{0}* . fC(κ(trunc(map fE ϵ_{0}*)))))
(fE*ϵ*)(λϵ_{1}* . fC(κ(trunc(map fE ϵ_{1}*))))
= λϵ*κ . (ω | F_{p})(fE*(fE*ϵ*))
(λϵ_{0}* . fC(fC(κ(trunc(map fE (trunc(map fE ϵ_{0}*)))))))
= λϵ*κ . (ω | F_{p})(fE*ϵ*)
(λϵ_{0}* . fC(κ(trunc(map fE (trunc(map 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(map fE (trunc(map fE ϵ_{0}*))) = trunc(map fE ϵ_{0}*),

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

By this lemma, x is of the form sva y if and only if x = sva x. We will call an object single-valued if it is fixed under sva.

Since D contains the syntactic classes as well as the semantic domains, it follows that sva may be applied to the semantic functions K, E, E*, and C.

In particular, sva c = c; since, moreover, Scheme has no constants denoting procedure objects, the type of K[[c]] is always E-free. Thus,

(sva K)[[c]] = sva (K[[sva c]]) = K[[c]],

so (sva K) = K. However, the remaining semantic functions are not unchanged under sva, and the alternative semantics consists in replacing them with their single-valued approximations (sva E), (sva E*), and (sva C).

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 byte code is justified against the denotational semantics using the initial continuation:

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

which is single-valued.

Theorem 2 (Faithfulness of Alternative Semantics)

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

stores σ,

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

2. Suppose κ = sva κ and σ = sva σ. Then E[[e]]ρ κ σ = (sva E)[[e]]ρ κ σ.

Proof: The second assertion follows immediately from the first.

1. We first use Lemma 2, clause 2 repeatedly:

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

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

However, since the domain of Scheme expressions and the domain of environments are E-free, sva e = e and sva ρ = ρ. Finally, since the domain of answers is E-free,

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

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 3 (Truncate Continuations, Eliminate “Single”)

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

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

Proof: The (very similar) proofs are by induction on e; we will show the details for clause 1.

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 ϵ*)))). 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 ϵ*))))

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 that (sva E)[[e]] and (sva B)[[b]] deliver the same values when applied to suitable initial values. Suitable initial values for e include any environment ρ and expression continuation κ. Since the type of (sva B)[[b]] is U → E → E* → U_{R} → K_{1} → C, we use the same environment ρ as the first argument and one arg κ for the last. As for the other arguments, we choose:

1. unspecified as the initial value in the “value register;”

2. ⟨⟩ as the initial “argument stack;” and 3. λν_{1}ν_{2} . ⊥ as the initial “run-time environment.”

Definition 4 (Environment Composition, mt_{C}, mt_{R}) 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 define mt_{C} to be λi . not lexical, and mt_{R} to be λi . ⊥.

We will refer to objects ρ_{C} and ρ_{R} as “compile-time environments” and “run-time environment” respectively. Expanding definitions and applying extensionality, we have:

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

We return now to proving the correctness of our compiler function, namely C(e, ρ_{C}, w), which, for the top-level call C(e, mt_{C}, ⟨⟨return⟩⟩), we abbreviate C(e). We prove first that code generated by compiling a full Scheme expression (as opposed to code fragments) does not depend on the argument given for the value register. In effect, it ignores the original value in the register, and sets it before any reference to it. We use Cargs to refer to the function implemented by comp-args in Table 1 on page 12.

Lemma 5 (Compiled expressions ignore the value register)

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

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

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

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}, b) = b. Otherwise, it is of the form:

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

so that the result follows by Clause 1.

We give next a portion of the proof of the main lemma, which is due to Will Clinger [1], for the case of the vlisp compiler.

Lemma 6 (Clinger’s Lemma) Consider any Scheme expression e, bbc closed instruction list b, bbc open instruction list y, segment π, environment ρ, compiletime environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, initial values ϵ, ϵ_{1}, and one-argument expression continuation ψ.

1. Let π_{1} = (sva B)[[b]]ρ and π_{2} = (sva B)[[C(e, ρ_{C}, b)]]ρ. Then

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

2. Let π_{1} = (sva Y)[[y]]ρπ and π_{2} = (sva Y)[[C(e, ρ_{C}, y)]]ρπ. Then

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

3. Let π_{1} = (svaB)[[b]]ρ and π_{2} = (svaB)[[Cargs(e*, ρ_{C}, b)]]ρ. Suppose that the after code π_{1} ignores the value register, in the sense that, for all values ϵ′, π_{1}ϵ = π_{1}ϵ′. Then

(sva E*)[[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, 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. In proving 2, we make the same assumption and also assume that 1 holds for e itself. 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 [1].

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

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

(sva E*)[[⟨⟩]](ρ◁_{ρ_{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}, 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*. Abbreviating λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ by κ, we may apply the semantic clause for E* to put the left hand side of our goal in 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} = (sva B)[[Cargs(e*, ρ_{C}, b)]]ρ,

we may infer:

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

Plugging this in, followed by Lemma 5, 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} .
(sva B)[[⟨push⟩:: Cargs(e*, ρ_{C}, b)]]ρ
ϵ_{0} ϵ* ρ_{R} ψ))

We will apply Clause 1 with

b = ⟨push⟩:: Cargs(e*, ρ_{C}, b),

and thus with

π_{2} = (sva B)[[C(e, ρ_{C}, ⟨push⟩:: Cargs(e*, ρ_{C}, b))]]ρ.

Hence,

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})
(multiple(λϵ_{0} . (sva B)[[⟨push⟩:: Cargs(e*, ρ_{C}, b)]]ρ
ϵ_{0} ϵ* ρ_{R} ψ))
= π_{2} ϵ ϵ* ρ_{R} ψ

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

(sva B)[[Cargs(e:: e*, ρ_{C}, b)]],

as the latter is the code:

C(e, ρ_{C}, ⟨push⟩:: Cargs(e*, ρ_{C}, b)).

Finally, we define the appropriate notion of computational equivalence, and prove the main theorem using Clinger’s lemma.

Definition 5 (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]]ρκ = (sva B)[[b]]ρ unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

“Equivalence” is a slight abuse of language, as this is not formally an equivalence relation (its domain and codomain are disjoint). Using the rules for sva in Lemma 2 and also Theorem 2, we infer that the definition of ≡ could equally have been stated only for single-valued κ:

Lemma 7 1. sva (one arg κ) = one arg (sva κ);

2. e ≡ b iff for every ρ and κ such that κ = (sva κ),

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

Theorem 4 (Compiler semantic correctness)

For any Scheme expression e, e ≡ C(e).

Proof: The theorem is a direct consequence of Clinger’s lemma, Clause 1. Let ρ be arbitrary, and let κ be single-valued. Since

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

we instantiate Clause 1 by putting (svaB)[[C(e)]]ρ = π_{2}, and (svaB)[[⟨⟨return⟩⟩]]ρ = sva return = π_{1}; we also let ψ = one arg κ and ρ_{R} = mt_{R}. Substituting the other initial values in the right hand side, we infer:

(sva E)[[e]] (ρ◁\begin{matrix}mt & R \\ mt & C \end{matrix}) (multiple λϵ . (sva return) ϵ⟨⟩mt_{R}(one arg κ))  (1)
= π_{2} unspecified ⟨⟩ mt_{R} (one arg κ).

The right hand side is already in the form we want; we need to reduce the left hand side to (sva E)[[e]] ρ κ. Since return = λϵϵ*ρ_{R}ψ . ψϵ, we may use Lemma 2, followed by Lemma 7 and the assumption that κ = (sva κ), to compute:

λϵ . (sva return) ϵ⟨⟩mt_{R}(one arg κ)
= λϵ . (sva (one arg κ))(sva ϵ) = λϵ . sva ((one arg κ)(sva (sva ϵ)))
= λϵ . sva ((one arg κ)(sva ϵ)) = λϵ . (sva (one arg κ))ϵ
= λϵ . (one arg (sva κ))ϵ = (one arg κ).

Hence we may rewrite Equation 1 as:

(sva E)[[e]] (ρ◁\begin{matrix}mt & R \\ mt & C \end{matrix}) (multiple (one arg κ))
= π_{2} unspecified ⟨⟩ mt_{R} (one arg κ).

By Lemmas 1 and 4, the left hand side equals:

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

But by Theorem 3, the latter equals (sva E)[[e]] ρ κ.

3. Faithfulness of an Operational Semantics

With this compiler correctness result, we have completed the denotational portion of the paper. We are ready to introduce a state machine semantics for the Basic Byte Code, and to prove that the state machine semantics is faithful to the denotational one that we have been using up to now.

3.1. Operational Semantics of the Basic Byte Code

The operational semantics of the bbc is determined by a state machine. That state machine uses bbc code as well as other objects as the components of its states. We introduce an expanded syntax called the augmented byte code or abc; it is a language which includes the bbc and also expressions belonging to other grammar classes. The objects from these other classes are used as state components together with code to build up the states of the machine.

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 locations) and the constructors appearing in small capitals in Table 13. The new abc syntactic categories, which will be defined by bnf, are

v for values,

a for argument stacks u for environments, k for continuations, s for stores, and Σ for abc states.

Syntactic categories from the bbc such as templates t and closed instruction lists b retain the same meaning. The additional productions do not feed back into the recursive construction of the old categories, so the productions for the old categories generate the same set of tree-like objects as they did in the bbc. The new productions are given in Table 13; the old productions, which were given in Table 3, will not be repeated here. The components of a state Σ are called, in order, its template, code, value, argument stack, environment, continuation, and

Table 13. abc Syntactic Definition

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^{∗}
Σ ::= ⟨t, b, v, a, u, k, s⟩ | ⟨t, ⟨⟩, v, a, u, k, s⟩

store, and we may informally speak of them as being held in registers. Strictly speaking, the template is hardly needed. It contains the name of the procedure, which is useful for debugging; moreover, its presence makes it easier to compare abc states with the states in lower level machines, in which the template does contain crucial information. The halt states in this machine are the states such the code is ⟨⟩. The answer function ans is defined for halt states Σ by

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

Form of the Rules. We present the machine transition relation, which we will call acts, as the union of subfunctions called (action) rules. The action rules are functions from disjoint subsets of states into states. Because their domains are disjoint, the union is in fact a function, and the resulting machine is deterministic.

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.

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 (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}).

Table 14. Some Operational Rules for the Basic Byte Code

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} = ⟨lap c b_{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⟩

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 Basic Byte Code Machine. In Table 14, we present the rules connected with make-cont, call, and return. This form of presentation is more compact and convenient than the explicit form, which would write (for instance) the rule for return in the form:

⟨t, ⟨⟨return⟩⟩, v, a, u, ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩, s⟩
⟹ ⟨t_{1}, b_{1}, v, a, u_{1}, k_{1}, s⟩

We will refer to all the rules R given in [6] 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 function acts.

The full set of rules is not exhaustive, in the sense of there being a next state whenever a state s is not a halt state. On the contrary, when a state represents a program that has encountered a run-time error, the operational semantics simply provides no next state.

Table 15. Semantic Functions for the Faithfulness Proof

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

3.2. Faithfulness: Form of the Proof

The main idea of the faithfulness proof, which is presented in full in [3], is to associate a denotation in the domain A with each state. If Σ is an initial state with template t = ⟨lap c b⟩, then the denotation of Σ 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 Σ, the denotation is equal to its computational answer ans(Σ), which has been defined to yield the same value as κ_{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. The definitions of the functions take an additional primitive, namely a function ρ_{G} : Ide → L. It associates the names of global variables with the locations in which their values are stored. It is not defined, but only constrained below in the definition of normal states. The semantic functions are defined by the equations shown in Table 16.

Definition 6 (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]]ρ_{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];

Table 16. Semantic Clauses for the Faithfulness Proof

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}[[unspecified]] = unspecified in E.

D_{v}[[undefined]] = empty in E.

D_{a} = rev ∘ (map 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 ⟨lap c b_{0}⟩ b a u k⟩]] = λϵ.B[[b]]ρ_{G}ϵD_{a}[[a]]D_{u}[[u]]D_{k}[[k]].

D_{s} = (map D_{v}).

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 Σ = ⟨⟨lap c b_{0}⟩, b, v, a, u, k, s⟩ be an abc state. The functions L_{glo}, L_{env}, L_{mp}, and L_{ip} map abc states to finite sets of locations. The formal definitions ([3]) will not be repeated here; the functions represent respectively the sets of locations in use in Σ for global variables, local variables, mutable pairs, and immutable pairs. For instance, L_{glo} is the range of the function ρ_{G}.

Definition 7 (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 immutable pair p = '(c_{1} . c_{2}) occurring in Σ, there are l_{1}, l_{2} ∈ L such that s(l_{1}) = c_{1} and s(l_{2}) = c_{2}; and similarly for immutable vectors and strings.

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 bbc template t = ⟨lap c b⟩ is any normal abc state of the form

⟨t, b, unspecified, ⟨⟩, empty-env, halt, s⟩

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. The following lemmas are needed in the proof of faithfulness.

Lemma 8 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 9 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 10 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 10, 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 Σ = ⟨⟨lap c b⟩, ⟨⟨return⟩⟩, v, a, u, k, s⟩, where k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ and t_{1} = ⟨lap c′ b′⟩.

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

D[[Σ]] = B[[⟨⟨return⟩⟩]]ρ_{G}(D_{v}[[v]])(D_{a}[[a]])(D_{u}[[u]])(D_{k}[[k]])(D_{s}[[s]])
= (λρ.return)ρ_{G}(D_{v}[[v]])(D_{a}[[a]])(D_{u}[[u]])(D_{k}[[k]])(D_{s}[[s]])
= return(D_{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}]]ρ_{G}ϵ(D_{a}[[a_{1}]])(D_{u}[[u_{1}]])(D_{k}[[k_{1}]]))(D_{v}[[v]])(D_{s}[[s]])
= B[[b_{1}]]ρ_{G}(D_{v}[[v]])(D_{a}[[a_{1}]])(D_{u}[[u_{1}]])(D_{k}[[k_{1}]])(D_{s}[[s]])
= D[[Σ′]]

Although not all of the cases are as straightforward as this (see [3] 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.

Theorem 5 (Faithfulness) The operational semantics for bbc is faithful: for all bbc 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[[Σ]], using Lemmas 8–10.

In fact the actual vlisp faithfulness proof as described in [3] differs from this description in several ways. First, the proof is not carried out at the level of the bbc, but rather at the level of the Tabular Byte Code introduced in [5]. This version of the byte code uses a template table to store embedded templates (representing locally introduced procedures), constants, and global variables. These are referenced by their numeric index within the table. Conceptually this makes no difference to any of the issues described here, so we have opted to avoid introducing another grammar.

Moreover, the actual proof is somewhat more complex. The operational semantics and the denotational semantics differ in the order in which they copy values from 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 [3] splits the faithfulness proof into two parts. The first part has exactly the form described in this section, but uses a state machine with an appropriate version of the rule to make an environment rib. The second part shows that the machine with the actual, implemented rule refines the one used in the first part, in the sense to be developed in the next section.

Theorem 5 is a conditional: it asserts only that if the machine computes an answer, then that is the correct answer. This property also holds of less useful machines than the bbcm, for instance a machine whose transition relation is empty. However, we conjecture that the technique of [12, Theorem 9] would allow us to prove the converse, which would establish the adequacy of the operational semantics. It would assert that the machine succeeds in computing an answer when the denotational semantics predicts a non-⊥, non-erroneous answer. The work described in this section was carried out before we became aware of that technique.

4. State Machine Refinement

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) that we already know would be acceptable.

We consider non-deterministic machines but not i/o here. Non-deterministic machines arose naturally when we introduced garbage collection. By contrast, we avoided treating i/o. On the one hand, the official Scheme semantics does not treat i/o. On the other hand, i/o can be added, either within the denotational or the operational style, without any very serious theoretical problem, but with more notational burden.

In this section we will define a notion of state machine refinement, and we will justify a particular technique for showing that one state machine refines another. We call this technique “storage layout relations,” following Wand and Oliva [18], although the underlying idea appears to be much older [8]. Wand and Oliva introduce the method by means of an example. Because vlisp used the method repeatedly, we will use this section to provide a formal definition, and to justify the method relative to a precise notion of refinement. We begin with some notation for state machines.

4.1. State Machines

There are many ways of pinning down details for state machines. Since we consider non-deterministic machines but not i/o, the following is convenient.

Definition 8 (State Machines)

State transition machines are 5-tuples

⟨states, inits, halts, acts, ans⟩

such that

(a) inits ⊆ states, and halts ⊆ states;

(b) acts ⊆ states × states;

(c) Σ ∈ halts implies that Σ is not in the domain of acts; and

(d) ans : halts → A.

If ⟨Σ, Σ′⟩ ∈ acts, we will say that Σ can proceed to Σ′. A state Σ is called a halt state if Σ ∈ halts, which is equivalent to ans(Σ) being well defined. If acts is actually a function, then the machine is deterministic.

If T is a finite or infinite sequence of states, then it is a computation (or a trace) if and only if T (0) ∈ inits and, for every i such that T (i+1) is defined, ⟨T (i), T (i+1)⟩ ∈ acts.

A computation is maximal if it is infinite or its last state is not in the domain of acts. A finite, maximal computation is successful if its last state is a halt state; any other finite, maximal computation is erroneous.

A state is accessible if it is T (i) for some computation T and integer i.

When T is a successful computation, that is, a finite computation terminating with a halt state Σ, we will write ans(T) to mean ans(Σ). Otherwise, ans(T) is undefined. We will say that M can compute a from Σ if there exists a T such that T (0) = Σ and ans(T) = a.

4.2. Refinement and Storage Layout Relations

In this section we will define a notion of refinement suitable for state machines without i/o. We will then introduce the notion of a storage layout relation, which we will show guarantees refinement.

In this section we will let M^{A} and M^{C} be state machines, which we regard as abstract and concrete respectively, and we will let decorated symbols refer to objects in these state machines. So for instance inits^{A} is the set of initial states of M^{A}; the variable T^{C} ranges over the traces of M^{C}; and the variable Σ^{C} ranges over the states of M^{C}.

The reader may want to pronounce the relations ∼_{0}, ∼, and ≈ in this section using terms such as “refines” or “implements.” This motivates the order of the arguments, with the more concrete argument always appearing on the left.

Definition 9 (Refinement) Consider a relation ∼_{0} ⊆ inits^{C} × inits^{A}.

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

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

1. Every abstract initial state corresponds to some concrete initial state:

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

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

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

Strong refinement in the sense given here is a very natural notion when state machines return information only through eventually computing an answer. As for weak refinement, it is an informative relation between state machines—it explains what behavior to expect from the concrete machine M^{C}—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, the computations that can be simulated are those in which all the values that arise can be stored in a machine word of fixed width, such as 32 bits.

Our standard approach [18] for proving that one state machine refines another is to prove that there is a storage layout relation between them. The definition makes use of a similarity relation on traces, induced from a similarity relation on states.

Definition 10 (Sequential extension ≈) Consider a relation

∼ ⊆ states^{C} × states^{A}.

Then ≈, the sequential extension of ∼, is the relation between traces of M^{C} and traces of M^{A} such that T^{C} ≈ T^{A} iff there exists a monotonic function f from the domain of T^{C} onto the domain of T^{A}, such that for all i in the domain of T^{C},

T^{C}(i) ∼ T^{A}(f(i)).

Thus, f(i) tells us “where we are” in the abstract trace, when we have reached position i in the concrete trace. In some cases, however, more than one function f will meet the condition.

The following lemma is intended to bring out the operational significance of ≈. It holds between two traces when their successive states are related by ∼. Either the concrete machine can proceed by a “stuttering” transition, which corresponds to no transition in the abstract machine, or else the two machines may each perform a transition. In either case, the resulting states must still be related by ∼. The stuttering transition is expressed below in Clause 3, while the lockstep transition is expressed in Clause 4.

Lemma 11 Suppose that ∼⊆ states^{C} ×states^{A}. Let ≃ be the least relation between traces of M^{C} and traces of M^{A} such that:

1. ⟨⟩ ≃ ⟨⟩;

2. If Σ^{C} and Σ^{A} are initial states and Σ^{C} ∼ Σ^{A}, then ⟨Σ^{C}⟩ ≃ ⟨Σ^{A}⟩;

3. If Σ_{0}^{C} can proceed to Σ_{1}^{C}, and Σ_{1}^{C} ∼ Σ^{A}, then

T^{C}^{⌢}⟨Σ_{0}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ^{A}⟩ implies T^{C}^{⌢}⟨Σ_{0}^{C}, Σ_{1}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ^{A}⟩;

4. If Σ_{0}^{C} can proceed to Σ_{1}^{C}, Σ_{0}^{A} can proceed to Σ_{1}^{A}, and Σ_{1}^{C} ∼ Σ_{1}^{A}, then

T^{C}^{⌢}⟨Σ_{0}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ_{0}^{A}⟩ implies T^{C}^{⌢}⟨Σ_{0}^{C}, Σ_{1}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ_{0}^{A}, Σ_{1}^{A}⟩.

Then if T^{C} and T^{A} are finite, T^{C} ≃ T^{A} iff T^{C} ≈ T^{A}.

Proof: We first make a general observation. Suppose that i is in the domain of T^{C}, and x = {j | 0 ≤ j ≤ i}. Then, since f is monotonic and onto the domain of T^{A}, the image of x under f is

{j | 0 ≤ j ≤ f(i)}.

Letting i = 0, we may infer that f(0) = 0 unless the trace T^{C} is ⟨⟩. Similarly, we must have either f(i + 1) = f(i) or f(i + 1) = f(i) + 1, whenever i + 1 is in the domain of T^{C}.

⇒: If T^{C} ≃ T^{A} by Clause 1 or 2, then the function f is the empty function or the function mapping 0 to 0 respectively.

Suppose that T^{C}^{⌢}⟨Σ_{0}^{C}, Σ_{1}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ^{A}⟩ holds by Clause 3, that the index of the last occurrence of Σ_{1}^{C} is i + 1, and the index of the last occurrence of Σ^{A} is j. Then inductively there is an acceptable f_{0} mapping {k | 0 ≤ k ≤ i} onto {k | 0 ≤ k ≤ j}. Then extending f_{0} to f by stipulating i+1 ↦ j, f is monotone and onto {k | 0 ≤ k ≤ j}. Moreover, by the hypothesis to Clause 3, T^{C}(i + 1) ∼ T^{A}(j).

Suppose that T^{C}^{⌢}⟨Σ_{0}^{C}, Σ_{1}^{C}⟩ ≃ T^{A}^{⌢}⟨Σ_{0}^{A}, Σ_{1}^{A}⟩ holds by Clause 4, where the last occurrences of Σ_{1}^{C} and Σ_{1}^{A} have indices i+1 and j+1 respectively. Then inductively there is an acceptable f_{0} mapping {k | 0 ≤ k ≤ i} onto {k | 0 ≤ k ≤ j}, which we may extend to the needed f by stipulating i + 1 ↦ j + 1.

⇐: By induction on T^{C}. Let f be an acceptable function from the domain of T^{C} to the domain of T^{A}. The cases for ⟨⟩ and ⟨Σ^{C}⟩ are immediate from Clauses 1 and 2. Otherwise, T^{C} is of the form T_{0}^{C}^{⌢}⟨Σ_{0}^{C}, Σ_{1}^{C}⟩, where the last occurrence of Σ_{1}^{C} has index i + 1. If f(i + 1) = f(i), then apply Clause 3; if f(i + 1) = f(i) + 1, apply Clause 4.

In the following definition, we use the notion of quasi-equality [2, 4], written s == t, meaning that s and t are equal if either of them is well defined. If ↓ means “is defined,” then s == t is in effect an abbreviation of (s ↓ ∨ t ↓) ⇒ s = t. In particular, ans^{C}(Σ^{C}) == ans^{A}(Σ^{A}) implies that either both Σ^{C} and Σ^{A} are halt states, or else neither of them is.

Definition 11 (Storage layout relation) A relation ∼ ⊆ states^{C} × states^{A} is a storage layout relation for M^{C} and M^{A} iff:

1. Every abstract initial state corresponds to some concrete initial state:

∀Σ^{A} : inits^{A} . ∃Σ^{C} : inits^{C} . Σ^{C} ∼ Σ^{A};

2. For every concrete trace, and abstract initial state Σ^{A} corresponding to its first member, some corresponding abstract trace starts from Σ^{A}:

∀T^{C}, Σ^{A} : inits^{A} . T^{C}(0) ∼ Σ^{A} ⇒ ∃T^{A} . T^{A}(0) = Σ^{A} ∧ T^{C} ≈ T^{A};

3. For every abstract trace, and concrete initial state Σ^{C} corresponding to its first member, some corresponding concrete trace starts from Σ^{C}:

∀T^{A}, Σ^{C} : inits^{C} . Σ^{C} ∼ T^{A}(0) ⇒ ∃T^{C} . T^{C}(0) = Σ^{C} ∧ T^{C} ≈ T^{A};

4. Of two corresponding states, if both are halt states, then they deliver the same answer, and otherwise neither is a halt state:

∀Σ^{C}, Σ^{A} . Σ^{C} ∼ Σ^{A} ⇒ ans^{C}(Σ^{C}) == ans^{A}(Σ^{A}).

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

Theorem 6 (Storage layout relations guarantee refinement) If ∼ is a weak storage layout relation for M^{C} and M^{A}, then M^{C} weakly refines M^{A} via the relation ∼_{0} defined to be ∼ ∩ inits^{C} × inits^{A}.

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: Clause 1 of Definition 9 is immediate from Clause 1 of Definition 11. We next argue that Clause 4 of Definition 11 implies that, when T^{C} ≈ T^{A},

ans^{C}(T^{C}) == ans^{A}(T^{A}). (†)

On the one hand, if ans^{C}(T^{C}) is well-defined, then T^{C} terminates in a halt state at its last index i. Moreover, T^{C}(i) ∼ T^{A}(f(i)), so by Clause 4, answer^{C}(T^{C}(i)) = answer^{A}(T^{A}(f(i))). Finally, since T^{A} is a trace, f(i) must be its last index, and ans^{A}(T^{A}) = answer^{A}(T^{A}(f(i))). On the other hand, if ans^{A}(T^{A}) is well-defined, similar reasoning applies, using the fact that f is onto.

To prove Clause 2 of Definition 9, suppose that T^{C} computes the answer a from Σ^{C}. By Clause 2 of Definition 11, there is a T^{A} with T^{A}(0) = Σ^{A} and T^{C} ≈ T^{A}. By †, ans^{A}(T^{A}) = a.

For Clause 3, we use Clause 3 of Definition 11 similarly.

Clause 2 in Definition 11 is, in essence, a safety condition on the concrete machine, while Clause 3 is a liveness condition on it, as the following lemma suggests. In this lemma, we will use γ as a variable over sequences of states of M^{C}.

Lemma 12 (Safety and liveness conditions) Consider a relation ∼⊆ states^{C} × states^{A}.

1. (Safety) Suppose that whenever Σ_{0}^{C} ∼ Σ_{0}^{A} and Σ_{0}^{C} can proceed to Σ_{1}^{C}, then

(A) either Σ_{1}^{C} ∼ Σ_{0}^{A} (a stuttering step);

(B) or else there exists a Σ_{1}^{A} such that Σ_{0}^{A} can proceed to Σ_{1}^{A} and Σ_{1}^{C} ∼ Σ_{1}^{A}.

Then Clause 2 of Definition 11 holds.

2. (Liveness) Suppose that whenever Σ_{0}^{C} ∼ Σ_{0}^{A} and Σ_{0}^{A} can proceed to Σ_{1}^{A}, then there exists a γ such that:

(A) ∀i . i < #γ − 1 ⇒ γ(i) ∼ Σ_{0}^{A};

(B) γ(#γ − 1) ∼ Σ_{1}^{A}; and

(C) γ is tracelike, in the sense that

∀i < #γ − 1 . ⟨γ(i), γ(i + 1)⟩ ∈ acts^{C}.

With this definition, γ is a trace T^{C} if it is tracelike and γ(0) is an initial state.

Then Clause 3 of Definition 11 holds.

Proof: 1. By induction on T^{C}. 2. By induction on T^{A}.

This lemma shows that the notion of storage layout relation is akin to the notion of a weak bisimulation (see [11, Chapter 5, Definition 5], for example). However, in our formulation, the relation is one-sided in that all the silent τ-transitions are taken by the concrete machine.

In many cases, such as the linearizer algorithm presented in Section 5, we use a storage layout relation to prove not just that one state machine refines another, but that a particular language translation F is correct. To see why that makes sense, let M^{A} be the state machine that gives the operational semantics for the source language, and let M^{C} give the operational semantics for the target language. Also, suppose that the states of M^{A} have the form of pairs ⟨p, Σ_{0}⟩, where p is a program in the source language of F and Σ_{0} contains the remaining state components, while the states of M^{C} have the form ⟨p′, Σ′_{0}⟩, where p′ is a program in the target language of F. Suppose further that at least for initial states, the non-code portion of a state may be shared between an abstract state and a concrete state. That is,

⟨p, Σ_{0}⟩ ∈ inits^{A} ⇒ ⟨F (p), Σ_{0}⟩ ∈ inits^{C}.

This was the point of the restriction to codeless stores in Definition 7.

Then we may say that F exhibits M^{C} as a refinement of M^{A} if M^{C} refines M^{A} via a relation built from projection, F, and pairing. In particular, the relation is to hold between a concrete initial state ⟨p′, Σ′_{0}⟩ and an abstract initial state ⟨p, Σ_{0}⟩ if p′ = F (p) and Σ′_{0} = Σ_{0}. If this relation is a refinement, then M^{C} computes the same answers when started in state ⟨F (Σ^{A}(0)), Σ^{A}(1)⟩ that M^{A} computes when started in state Σ^{A}.

How can we use the storage layout relation method to prove that F refines M^{C} to M^{A}? We must exhibit a storage layout relation ∼ such that F establishes ∼, in the sense that ⟨F (p), Σ_{0}⟩ ∼ ⟨p, Σ_{0}⟩, whenever the latter is an initial state of M^{A}.

We illustrate this method in the next section, by proving that the vlisp flattener (or code linearizer) is correct. Section 5.4 proves that the flattener establishes a relation ∼, which is the real content of Theorem 7. Then Theorem 8 in Section 5.5 shows that ∼ is in fact a storage layout relation.

5. The Flattener

The flattener [6] transforms byte coded procedures in the bbc into a linear rather than a tree-structured form. Conditionals are represented in a familiar way using branch and branch-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).

However, before we introduce the new language, we will provide a bit more detail about the bbc and its operational semantics (Section 5.1). We will then present the fbc and give it an operational semantics (Section 5.2) in a style very similar to the presentation of the bbc semantics in Section 3.1. We will briefly describe the flattener algorithm(Section 5.3). 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 (Section 5.4). Finally, we extend the code correspondence relation to a storage layout relation between states of the newly introduced flattened byte code state machine (fbcm) and the bbcm (Section 5.5). This establishes that the fbcm is a refinement of the bbcm.

5.1. The Basic Byte Code in More Detail

In order to describe the operational semantics of conditionals in the bbcm, 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 12 (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 3, a closed bbc 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 13 (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 ^{⌣}, as shown in Table 17.

Table 17. bbcm Open Branch Rules

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}

Table 18. Flattened Byte Code: Syntax

        t ::= ⟨template c w⟩

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

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

5.2. Flattened Byte Code Syntax and Operational Semantics

The Flattened Byte Code (fbc) is a modification of the Basic Byte Code that uses unnested linear sequences of tokens for the code part of its templates. Instead of the bbc conditional instruction unless-false, fbc has branchf and branch, 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 appear as Table 18. In this version of the syntax, the code sequences are not exclusively unnested, since the instructions ⟨closure t⟩ and ⟨constant c⟩ may have nested subexpressions. However, in the full vlisp development, this is not the case; a “tabularizer” stage had previously moved the nested values into a template table, in which they were referenced by a natural number index (cf. page 37).

fbc states—characterized in Table 19—differ from bbc states in that their templates and code belong to the fbc language rather than the bbc language. In addition, instead of having a “code register” they have a numerical “program counter,” to which we will refer conventionally as n. It is interpreted as an offset into the code sequence of the template. We will use the variable w to refer to the code sequence (or just the code) of a state, i.e., w = t(2). With our conventions, w(n) is

Table 19. Flattened Byte Code State Machine: State Component Syntax

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^{∗}
Σ ::= ⟨t, n, v, a, u, k, s⟩

the first element of w † n, if 0 ≤ n < #w. The states in halts are those such that n = #w (so w † n = ⟨⟩). The answer function, normal states, and initial states are defined as before.

The presentation of the rules for the fbc (Table 20) will use the same conventions as were used for the bbc, except that here n stands for the offset of the ingoing state, n′ for the offset of the state produced, and w for t(2), 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 by the condition n_{0} ⊕n_{1} = (256∗n_{0})+n_{1}. In the fsbcm implementation, the values of n_{0} and n_{1} are always stored in a single byte. The operator ⊕ is needed so that we can represent offsets that are larger than 255. Although large numbers may be represented in more than one way in the form n_{0} ⊕ n_{1} (if n_{1} may be large), this does not affect our proof.

5.3. The Flattener

The flattener is implemented by a purely applicative Scheme program, part of which is shown in Figure 2; 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 bbc instruction list b or an open bbc instruction list y.

An obvious induction shows that the algorithm terminates, and produces a syntactically well-formed fbc template from any bbc 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.

In the next two subsections, we will exhibit a relation between bbcm states and fbcm. The task of the first section is to show that the flattener establishes this relation; the task of the second section is to show that the relation is in fact a storage

Table 20. Typical fbcm Rules

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: 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 3: Branchf/False Domain conditions: w † n = ⟨branchf n_{1} n_{2}⟩^{⌢}w_{1}; v = false Changes: n′ = n + 3 + (n_{1} ⊕ n_{2})

Rule 4: Branchf/True Domain conditions: w † n = ⟨branchf n_{1} n_{2}⟩^{⌢}w_{1}; v ≠ false Changes: n′ = n + 3

(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)))

Figure 2. Flattener Algorithm Table 21. Recursive Conditions for ≃.

1. For m = ⟨return⟩ or ⟨call n⟩, m^{⌢}w_{F} ≃ ⟨m⟩.

2. ⟨closure t_{F} ⟩^{⌢}w_{F} ≃ ⟨closure t⟩:: m* if, first, either m* = w_{F} = ⟨⟩ or w_{F} ≃ m*, and, second, the code correspondence holds between the code embedded within t_{F} and t respectively:

t_{F} (2) ≃ t(2).

3. For atomic z other than closure, z^{⌢}w_{F} ≃ z:: m* if either m* = w_{F} = ⟨⟩ or w_{F} ≃ m*.

4. ⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} ≃ ⟨make-cont w n⟩:: b if

w_{F} ≃ b and w_{F} † (n_{0} ⊕ n_{1}) ≃ w.

4′. ⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} ≃ ⟨make-cont ⟨⟩ n⟩:: b if

w_{F} ≃ b and w_{F} † (n_{0} ⊕ n_{1}) = ⟨⟩.

5. ⟨branchf n_{0} n_{1}⟩^{⌢}w_{F} ≃ ⟨⟨unless-false b_{1} b_{2}⟩⟩ if

w_{F} ≃ b_{1} and w_{F} † (n_{0} ⊕ n_{1}) ≃ b_{2}.

6. ⟨branchf n_{0} n_{1}⟩^{⌢}w_{F} ≃ ⟨unless-false y_{1} y_{2}⟩:: w if

w_{F} ≃ y_{1}^{⌣}w and w_{F} † (n_{0} ⊕ n_{1}) ≃ y_{2}^{⌣}w.

7. ⟨branch n_{0} n_{1}⟩^{⌢}w_{F} ≃ w if w_{F} † (n_{0} ⊕ n_{1}) ≃ w.

layout relation. Thus, the two subsections together establish that flattening code leaves its computational results unchanged.

5.4. Code Correspondence

We will define the storage layout relation between states justifying this refinement in terms of a preliminary “code correspondence” relation ≃ holding between flattened and unflattened code. We will write w_{F} ≃ w; the main theorem of this section asserts that the flattener establishes this relation: F (w) ≃ w. The correspondence relation is defined as the least relation satisfying the conditions given in Table 21. 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 14 (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 15 (≃/adjoin) If w_{0} ≃ b_{0}, then for any w_{1}, w_{0}^{⌢}w_{1} ≃ b_{0}.

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

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

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

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

⟨branch n_{0} n_{1}⟩^{⌢}(w_{2}^{⌢}w_{1}) ≃ b_{0}.

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} = ⟨closure t⟩:: b and w_{0} = ⟨closure t_{1}⟩^{⌢}w. Since w_{0} ≃ b_{0}, we may infer from the definition of ≃ that w ≃ b and t_{1}(2) ≃ t(2). Hence we may apply the induction hypothesis to infer that w^{⌢}w_{1} ≃ b, and we may then apply Clause 2 to infer that w_{0}^{⌢}w_{1} ≃ b_{0}.

3. Suppose that b_{0} = z:: b, w_{0} = z^{⌢}w, where z is not a closure instruction. (The syntax ensures that m* really is of the form b.) Since, inductively, w^{⌢}w_{1} ≃ b, we simply apply clause 3 to w^{⌢}w_{1}.

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

ductively:

w^{⌢}w_{1} ≃ b and w † (n_{0} ⊕ n_{1})^{⌢}w_{1} ≃ b_{1}.

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

4′. A closed instruction sequence b_{0} is not of this form.

5, 6, 7. Similar to 4.

In contrast to closed instruction lists, for open instruction lists, adding code to the end of a flattened version corresponds to ^{⌣}:

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

The main theorem of this section asserts that the output produced by the flattener bears the code correspondence relation ≃ to its input. Its proof is similar in structure to the proof of Lemma 15.

Theorem 7 (Flattener establishes ≃) F (w) ≃ w.

Table 22. Closure Conditions for ∼.

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 c w⟩ ∼ ⟨template c b⟩, if w ≃ b

6. ⟨cont t_{2} n a_{2} u k_{2}⟩ ∼ ⟨cont t_{1} b a_{1} u k_{1}⟩, if

(A) t_{2}(2) † n ≃ b, 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}(2) † n ≃ b, 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}.

5.5. State Correspondence

Based on the underlying “code correspondence” relation ≃, we will define a binary “miscellaneous correspondence” relation ∼ between various kinds of syntactic objects of the fbcm on the left and the bbcm on the right, building up to a notion of correspondence between fbc states and bbc 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 6 the fbcm is a faithful refinement of the bbcm.

Because the two languages share some syntactic objects, we can simplify the definition. Some of the objects that are shared by the two languages are 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 22. 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.

By this definition and Definition 7, which ensures that the stores of initial states are codeless, we may infer that if an initial bbc and an initial fbc state share the same store, then they correspond if their code corresponds. That is, suppose t_{F} = ⟨template c w⟩; t = ⟨template c′ b⟩; and w ≃ b. Then

⟨t_{F} , 0, unspecified, ⟨⟩, empty-env, halt, s⟩

corresponds to

⟨t, t(2), unspecified, ⟨⟩, empty-env, halt, s⟩.

By Theorem 7, we can always take w to be F (b), so condition 1 in Definition 11 (storage layout relations) is satisfied. Moreover, condition 4 follows immediately from clause 8 for ∼; hence:

Lemma 17 ∼ satisfies the initial condition (1) and the halt condition (4) 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 bbc 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 18 (Determinacy of Transitions) If M is either the bbcm or the fbcm, and M is in state Σ, then there is at most one state Σ′ such that M can proceed by one rule transition from Σ to Σ′.

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 cases when one must also consider the value register or the argument register. Given a particular 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.

For instance, the rules for primitives allocating new storage stipulate that the new locations selected lie immediately after the previously active portion of the store.

Clearly the bbc rules are closely paralleled by the fbc rules: let us say that a bbc 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 Branchf/True, and finally that Closed Branch/False and Open Branch/False both correspond to Branchf/False. No bbc rule corresponds to Branch. A branch rule means one whose name ends in /True or /False—four for bbc and two for fbc.

Theorem 8 (Preservation of State Correspondence) Let Σ be the state of the bbcm and Σ_{F} the state of the fbcm, and assume that Σ_{F} ∼ Σ. Then

1. if the fbcm proceeds by the Branch rule to state Σ′_{F}, then Σ′_{F} ∼ Σ and the fbcm cannot proceed from Σ′_{F} by the Branch rule;

2. if the fbcm cannot proceed by the Branch 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 17, Lemma 12, and Theorem 6, we can infer:

Theorem 9 ∼ is a storage layout relation for the fbcm and the bbcm. Hence, the fbcm refines the bbcm.

The vlisp Scheme compiler is structured as the composition of five stages: the byte code compiler, tabulator, flattener, linker, and image builder. We have now completed our presentation of the algorithms and correctness proofs of the byte code compiler and the flattener. We have ignored the tabulator and the linker since they do not raise significant new verification issues. The image builder, which produces the final sbc program as a binary image (i.e., a flat sequence of bits), uses a storage layout relation defined in a different way. However, since this same technique is used in the more interesting proof of the garbage collector (see Section 6.3), we will not describe the image builder in this paper.

6. The Virtual Machine

The vlisp Scheme compiler translates any Scheme program p to a program sbc in a language called Stored Byte Code (sbc), while the vlisp Virtual Machine (vm) evaluates sbc programs to answers. Together, these evaluate Scheme programs to answers.

The semantics of sbc is given in terms of a state machine called the Stored Byte Code Machine (sbcm); the meaning of sbc is given by the answer computed by the sbcm when started in an initial state Σ_{0} constructed from sbc. The correctness of the compiler as a whole asserts that if the sbcm computes an answer a when started in Σ_{0}, then a is the result of applying the denotation of p to suitable initial parameters x⃗.

The correctness of the vlisp Virtual Machine (vm) requires that when the vm evaluates sbc to an answer a, then the sbcm should compute a when started in an initial state constructed from sbc. In this section, we present the algorithms and correctness proofs of parts of the vlisp Virtual Machine relative to the sbcm.

There are three main reasons why the sbcm must be refined before being embodied in concrete program code. First, the size of the active store in the sbcm is unbounded in size, whereas any concrete implementation will have a limited address space. As a consequence, a garbage collector must be introduced. Second, other values are also bounded by the finite resources available to a concrete implementation. Third, the declarative specifications of some of the rules are not trivial to embody in concrete, procedural code. For this last reason, we will instantiate these rules using programs that manipulate a set of primitive operations that can be directly and reliably coded. We thus refine and instantiate the state machine description until we obtain a concrete implementation of the vm. Refinement is a binary relation between state machines; as formalized in Section 4, these state machines may have completely different state spaces.

Instantiation is a binary relation between machines sharing the same state space. Instantiation may reduce the non-determinism of a machine; however, it is useful even if the two state machines are identical, as is the case in Section 6.2. The reason is that the description of the state machine has changed; in place of the declarative rules, we have substituted algorithms calling simple primitive operations, and have thus moved closer to a concrete program.

We use refinement and instantiation in contrasting ways. We use refinement to alter the states and action rules of state machines. We use instantiation to specify algorithms that implement the action rules. In both cases, the minimal correctness criterion is that we should refine the observable behavior of the state machines, in the sense that every observable behavior of the more concrete machine should also be an observable behavior of the more abstract machine.

We will briefly describe the state machine sbcm. We proceed by alternately instantiating and refining the state machine as follows:

1. We define a collection of primitive state operations that observe and modify states. We instantiate the sbcm action rule descriptions by coding them in terms of these state operations. The state machine remains the same, while its description is altered (made more “concrete”). The correctness proof shows that the implementation of each action rule meets its specification; this is long and tedious.

2. We justify garbage collection in two main steps:

(A) We refine the sbcm to the Garbage-Collected Stored Byte Code Machine (gcsm). This machine is similar to the sbcm except that it includes a new primitive state-modifying operation (gc). The refinement proof uses the storage layout relation technique to show that the gcsm refines the sbcm. The main difference between this proof and the proof of the flattener in Section 5 is in the definition of the storage layout relation.

(B) We instantiate the gc primitive by presenting a concrete implementation that is defined in terms of the primitive state operations. The instantiation proof shows that the garbage collector meets the specification of the action rule.

3. We weakly refine the gcsm to a Finite, Garbage-Collected Stored Byte Code Machine (fgcsm). The fgcsm state set is a subset of the gcsm state set, namely the set of all states with components of bounded size. The length of stacks, the length of stores, and the values of registers, stack cells, and store cells receive upper bounds. The fgcsm initial states, halt states, action rules, and answer function are restrictions of the corresponding gcsm components. The proof of weak refinement is trivial.

4. We directly encode the fgcsm description in PreScheme; this is the concrete implementation of the vlisp Virtual Machine.

Our implementation also incorporates several optimizations, mentioned in Section 6.6; we have not justified these optimizations in this paper since they add complexity to the proofs but do not involve any new techniques.

6.1. Stored Byte Code and its State Machine

Stored Byte Code (sbc) language represents the image builder’s output. Its operational semantics is given in terms of a deterministic state machine called the Stored Byte Code Machine (sbcm).

The abstract syntax of sbc is presented in Table 23. An sbc program is an sbc store together with an index into the store. A store is a sequence of cells, with each cell being one of:

1. A header ⟨header h p m⟩ where h (the header tag) is a tag that describes the object occupying the storage that follows; p (the mutability flag) is a boolean value that describes whether the object is mutable; and m (the header size) is the number of cells in the stored object;

2. A pointer ⟨ptr l⟩ where l is an index into the store;

3. A number ⟨fixnum n⟩ where n is an integer;

4. An immediate value ⟨imm imm⟩ where imm is a simple (unstructured) value such as a character, boolean, etc.

5. A byte b where b is a number that represents either a character or an instruction opcode.

A term of the form 2, 3, or 4 above is called a value descriptor. For each byte that represents an instruction opcode, we define a named constant and refer to the byte by this name, e.g., call, return, etc.

We will write a typical state of the sbcm in the form

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

where n is a number, t, v, u, k, and r are value descriptors, a is a stack of value descriptors and s is a store. The components of the state are called, in order, its template, offset, value, argument stack, environment, continuation, store, and spare.

The stores in accessible states of the sbcm, where again by an accessible state we mean a state that occurs in some trace of the machine, 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 l at which the first value is stored is called the address of the stored object, and the term ⟨ptr ℓ⟩ is called a pointer to the stored object. We name the stored object by its header tag; thus we call a stored object with header tag template a “template” stored object.

Table 23. Abstract Syntax of Stored Byte Code (sbc).

program ::= ⟨s v⟩
s ::= cell^{∗}
cell ::= desc | byte
desc ::= ⟨header htag bool n⟩ | v
v ::= ⟨ptr n⟩ | ⟨fixnum n⟩ | ⟨imm imm⟩
imm ::= false | true | ⟨char n⟩ | null | undefined

unspecified | empty-env | halt | eof

htag ::= bhtag | dhtag
bhtag ::= string | codevector
dhtag ::= pair | symbol | vector | location | template |

closure | port | continuation | environment

byte ::= n
a ::= v^{∗}
Σ ::= ⟨v_{0} n v_{1} a v_{2} v_{3} s v_{4}⟩

Definition 13 (Stored Objects) s contains a stored object at ℓ (or alternatively, ℓ is a pointer to an object in s) 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 ℓ.

If s contains a stored object at ℓ with s(ℓ − 1) = ⟨header h p m⟩ for some h, p, and m, then S(⟨ptr l⟩, s) extracts the stored object in s at l:

S(⟨ptr l⟩, s) = ⟨h p ⟨s(l) … s(l + m − 1)⟩⟩

H(⟨ptr l⟩, s) gives its header type h = (S(⟨ptr l⟩, s))(0).

Definition 14 (Current Instruction, Parameters)

Let Σ = ⟨t, n, v, a, u, k, s, r⟩ and let

S(t, s) = ⟨template false c::v^{∗}⟩
S(c, s) = ⟨codevector false b^{∗}⟩

for some sequences v^{∗}, b^{∗}. Then,

Table 24. Action Rule for the call Instruction.

Rule 0: call m Domain conditions:

current inst(n, t, s) = call

current inst param(n, 1, t, s) = m S(v, s) = ⟨closure false ⟨t_{1} u_{1} d_{1}⟩⟩

Changes:

\begin{matrix}t′ = t_{1} \\ n′ = 0 \\ u′ = u_{1} \end{matrix}

current inst(n, t, s) = b^{∗}(n)

current inst param(n, i, t, s) = b^{∗}(n + i)

current inst(n, t, s) is the current instruction, while current inst param(n, i, t, s) is the ith parameter to the current instruction.

An sbcm state is initial if it is of the form

⟨t, 0, ⟨imm unspecified⟩, ⟨⟩, ⟨imm empty-env⟩, ⟨imm halt⟩, s, r⟩

and satisfies the two state invariants in Lemma 19 below. A state ⟨t, n, v, a, u, k, s, r⟩ is a halt state if:

• current inst(n, t, s) = return

• k = ⟨imm halt⟩

As before, acts is the union of subfunctions called (action) rules. Table 24 presents the call rule as an example. As with the flattened byte code machine fbcm (Lemma 18), the sbcm is deterministic: for every state of the sbcm, 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. Two basic invariants hold for sbcm-accessible states.

Lemma 19 (SBCM Invariants) If an accessible state Σ with store s contains a term of the form ⟨ptr ℓ⟩, then ℓ points to an object in s.

If Σ = ⟨t, n, v, a, u, k, s, r⟩ is accessible, then

1. H(t) = template;

2. n < #(S(c, s)(2)), where c = S(t, s)(2)(1) is the code component of the template;

3. either u = ⟨imm empty-env⟩ or H(u) = environment; and

4. either k = ⟨imm halt⟩ or H(k) = continuation.

Table 25. sbcm State Observers for Σ = ⟨t, n, v, a, u, k, s, r⟩.

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

6.2. The Instantiated SBCM Description

The action rules of the sbcm are instantiated in terms of some primitive operations on states.

We define a set of primitive operations on the state, and we instantiate each action rule of the sbcm in terms of these operations. The state operations are presented in Tables 25 and 26. These operations 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 procedures that modify a component of a state. A “state modifier expression” consists of a state modifier name applied to observer expressions.

Each sbcm action rule is instantiated as a program composed from state observer and modifier 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. We will

Table 26. sbcm State Modifiers for Σ = ⟨t, n, v, a, u, k, s, r⟩.

Register Modifiers

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 Modifiers

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

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

Miscellaneous Modifiers

assert p Σ  = if p then Σ else abort

Stored Object Modifiers

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]]

    (assert (closure-stob? (value-ref))
             "op/call: value register does not contain a closure")
    (template-set
     (stob-ref (value-ref) 0))    ;; Closure's template
    (env-set
     (stob-ref (value-ref) 1))    ;; Closure's env
    (offset-set 0)

Figure 3. Instantiation of the call Action Rule.

call such a program a rule program. We will say that a rule program is applicable in a state Σ if the domain conditions of the associated rule are true in Σ.

The instantiations are exceedingly simple programs. In fact, only the rule makerest-list, which makes an argument list—when calling a Scheme procedure with a dotted argument list—requires the while construct; the others can be instantiated using only a primitive recursive for-loop. The majority of rules require no iteration whatever. Thus, the instantiated programs are easily verified using Hoare logic.

Figure 3 presents the instantiation of the call action rule. The proof of its correctness consists of simple Hoare-style reasoning about the effects of this straightline code.

Theorem 10 The instantiation of the sbcm action rules is correct with respect to the specification of the action rules.

The proof is simple, but highly tedious. A detailed examination of the correctness of all the action rules was carried out. This process would have been eased had we had reasonable mechanized proof support, particularly during phases of development when the rule specifications and instantiations changed.

The sbcm is deterministic, so the instantiation is identically the same state machine: it has (extensionally) the same transition relation. Although the state machine remains the same, the instantiation provides a much more informative description of it. The instantiation determines the majority of the code for the vm.

6.3. The Garbage-Collected Stored Byte Code Machine (GSBCM)

In this section we define the Garbage Collected Stored Byte Code Machine (gcsm) and prove that it is a faithful refinement of the sbcm. As a consequence, we justify adding garbage collection to the instantiated form of the gcsm.

The sbcm and gcsm share the same set of states, the same initial states, halt states, and answer function. The only difference between them is that the gcsm includes a new primitive state modifier (called gc). It is not fully specified, so that the gcsm is not a deterministic state machine. We will define gc in terms of a relation ≅ of similarity between gcsm states and sbcm states. We define ≅ in turn using a variant of the storage-layout relations approach. The treatment in [18] assumes that terms are tree-structured, and storage layout relations are defined by structural induction over such terms. However, our 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 Σ and Σ^{A} 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 understandable 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 match 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.

6.3.1. State Similarity

We formalize locations as natural numbers, but use ℓ-like variables when we are regarding the numbers as store locations. We will typically indicate objects from the more abstract sbcm by variables with a superscript A, leaving variables representing gcsm objects unadorned. Since the sbcm 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. The superscript only connects the object with the machine we regard it as arising in.

Definition 15 (Store Correspondence) Suppose ∼ is a binary relation on natural numbers, regarded as representing concrete and abstract store locations. Then ∼ is a store correspondence between concrete store s and abstract store s^{A} if for all values of the location variables, the following three conditions are met:

1. if ℓ_{0} ∼ ℓ^{A} and ℓ_{1} ∼ ℓ^{A}, then ℓ_{0} = ℓ_{1};

2. if ℓ ∼ ℓ_{0}^{A} and ℓ ∼ ℓ_{1}^{A}, then ℓ_{0}^{A} = ℓ_{1}^{A};

3. if ℓ ∼ ℓ^{A}, then ℓ and ℓ^{A} are in the domain of s and s^{A} respectively.

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

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

The term correspondence generated by ∼ is a relation ≃ between cells (i.e., value descriptors or bytes) cell and cell^{A}, defined by taking cases on cell^{A}. cell ≃ cell^{A} holds just in case one of the following holds:

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

(A) ⟨ptr l⟩ = cell;

(B) s^{A}(l^{A} −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^{A} + i).

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

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

4. cell^{A} = b = cell, for some byte b.

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

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

Definition 17 (State Similarity) Let ∼ be a store correspondence between concrete gcsm store s and abstract sbcm store s^{A}, with generated term correspondence ≃.

Σ and Σ^{A}, of the forms

⟨t, n, v, a, u, k, s, r⟩ and ⟨t^{A}, n^{A}, v^{A}, a^{A}, u^{A}, k^{A}, s^{A}, r^{A}⟩,

respectively, are similar with respect to ∼, written Σ ≈ Σ^{A}, just in case the invariants on sbcm states given in Lemma 19 hold and:

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

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

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

Finally, Σ and Σ^{A} are similar, written Σ ≅ Σ^{A}, just in case there exists a store correspondence ∼ such that Σ and Σ^{A} 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 we assume they are generated by the same omitted ∼. If Σ and Σ^{A} are similar with respect to ∼, then we will call it a witness for Σ ≅ Σ^{A}. By inspecting the structure of states we can verify:

Lemma 20 (Properties of ≅)

1. ≅ is an equivalence relation;

2. Σ ≅ Σ^{A} ⇒ ans(Σ)==ans(Σ^{A}), where ans is defined as in Section 3.1, and s==t means that s and t are equal if either of them is well defined (see Section 4.2); hence,

3. Σ ≅ Σ^{A} ⇒ Σ ∈ halts iff Σ^{A} ∈ halts.

6.3.2. Legitimacy of Garbage Collection

We now define the gcsm to be a state machine having the same states, initial states, halt states, and answer function as sbcm. It differs from the sbcm only in the tuple component acts. We regard any transition from Σ to Σ′ where Σ ≅ Σ′ as a potential garbage collection, and allow garbage collection to occur non-deterministically in the course of executing any rule program immediately before executing the storageallocating modifier make-stob.

To formalize this idea, we add one state modifier to the ones that were used in the sbcm, and we also add one keyword to the programming language for building up rule programs. The modifier is gc. Its specification is non-deterministic: gc Σ returns some state Σ′ such that Σ ≅ Σ′. The keyword is maybe; if e is a modifier expression, then so is maybe e. It also introduces non-determinism. If the modifier expression e, executed in state Σ, may return Σ′, then so may maybe e, and moreover maybe e may do nothing and return Σ unchanged.

Because ≅ happens to be a reflexive relation, there is in fact no difference between gc and maybe gc. Nevertheless, we introduce both because the two kinds of nondeterminism get resolved differently. The non-determinism of gc is resolved in Section 6.4, when we select a particular garbage collection algorithm. The nondeterminism introduced by the maybe is resolved when we pass to a finite machine in Section 6.5. At that point the stores are finite, and garbage collection can occur when they are nearly full.

The transition relation of the gcsm is defined implicitly by means of rule programs. If P is one of the rule programs of the sbcm, then P′ is defined to be the result of replacing every occurence of (make-stob h p m) by

   (maybe (gc))
   (make-stob h p m)

If P′ derives from a sbcm rule program P in this way, we will say that P′ corresponds to P. We define acts to be the set of pairs ⟨Σ, Σ′⟩ such that for some sbcm rule program P, P is applicable in Σ, and the corresponding program P′, when started in Σ, may terminate in Σ′. Thus, the domain conditions for the sbcm rules are carried over in the gcsm; the changes of state are the same, except that gc is permitted.

We want to establish that ≅ is a storage layout relation between sbcm and gcsm. Clause 1 of Lemma 20 implies Clause 1 of Definition 11, while Clause 2 of the lemma is the same as Clause 4 of Definition 11. By Lemma 12 and Theorem 6, to show that gcsm refines sbcm it suffices to show the safety and liveness conditions hold.

The safety condition asserts that for every pair of similar states Σ ≅ Σ^{A}, if Σ can proceed to Σ_{1}, then either Σ_{1} ≅ Σ^{A} or else Σ^{A} can proceed to some Σ_{1}^{A} such that Σ_{1} ≅ Σ_{1}^{A}. In fact, the latter always holds, so the liveness condition is also satisfied.

To prove this, we will show

1. If Σ ≅ Σ^{A}, then the domain conditions for a rule either hold in both states or else fail in both states (Theorem 11); and

2. If Σ_{0} ≅ Σ_{0}^{A} and P′ corresponds to P, then either both programs fail to terminate when started in those states (respectively) or else both programs terminate, and the results satisfy ≅ (Theorem 12).

For both these results, the real heart of the matter is that the individual observers and modifiers are invariant under ≅. We will separate observers and modifiers in the following two lemmas, each of which is proved [16] by perfectly straightforward (but lengthy) applications of the definitions:

Lemma 21 (Observers respect ≃) Let ∼ be a store correspondence, with generated term correspondence ≃; let e be any of the state observers listed in Table 25, taking state parameter and possibly other parameters. Suppose:

1. Σ ≈ Σ^{A}; and

2. the respective components of x⃗ and x^{A} satisfy ≃.

Then e(Σ, x⃗) ≃ e(Σ^{A}, x^{A}).

Lemma 22 (State modifiers preserve ≅) Let ∼ be a store correspondence, with generated term correspondence ≃; let e be any of the state modifiers listed in Table 26, taking state parameter and possibly other parameters. Suppose:

1. Σ ≈ Σ^{A}; and

2. the respective components of x⃗ and x^{A} satisfy ≃.

Then e(Σ, x⃗) ≅ e(Σ^{A}, x^{A}).

In the proof of Lemma 22, the underlying store correspondence ∼ is used unaltered for every modifier 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 23 Let ∼ be a store correspondence, with generated term correspondence ≃. Suppose:

1. e and e′ are observer expressions;

2. Σ ≈ Σ^{A}; and

3. the respective components of x⃗ and x^{A} satisfy ≃;

4. the respective components of y⃗ and y^{A} satisfy ≃;

Then e(Σ, x⃗) = e′(Σ, y⃗) iff e(Σ^{A}, x^{A}) = e′(Σ^{A}, y^{A}).

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

Theorem 11 Let ∼ be a store correspondence. Suppose:

1. R is any sbcm rule (with auxiliary variables);

2. The domain condition for R is satisfied in Σ using the witnessing values x⃗ for the auxiliary variables;

3. Σ ≈ Σ^{A};

4. Σ consists of stored objects.

Then there is an x^{A} such that:

1. #x⃗ = #x^{A};

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

3. The domain condition for R is satisfied in Σ^{A} using the witnessing values x^{A}.

Proof: Let x^{A}(i) be x⃗(i) if the latter is not of the form ⟨ptr ℓ⟩. Otherwise, let x^{A}(i) be ⟨ptr ℓ^{A}⟩ where ℓ^{A} is some ℓ′ such that ℓ ∼ ℓ′.

On the assumption there is such an ℓ′, then it follows that conditions 1 and 2 are satisfied. Condition 3 follows from Lemma 23, because the domain conditions are always equations between observer expressions.

Thus, it suffices to show that there is an ℓ′ such that ℓ ∼ ℓ′, whenever ⟨ptr ℓ⟩ is a witnessing value for a domain condition auxiliary variable. By Definition 15 clause 1, there is at most one such ℓ′, so x^{A} is actually unique.

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 17 clause 3 to infer that, if v is the value of r_{0} in Σ^{A}, then ⟨ptr ℓ⟩ ≃ v. By Definition 16, v is of the form ⟨ptr ℓ^{A}⟩, and by clause 1c, ℓ ∼ ℓ^{A}. The remaining cases are similar, except that Definitions 17 and 16 must be used repeatedly.

Theorem 12 (Corresponding programs produce corresponding results) Suppose that Σ_{0} ≅ Σ_{0}^{A}, and that P′ and P are corresponding rule programs. Then, when P′ and P are started in states Σ_{0} and Σ_{0}^{A} respectively, then either

1. both fail to terminate; or else

2. both terminate, and in states Σ_{1} and Σ_{1}^{A}, respectively, such that Σ_{1} ≅ Σ_{1}^{A}.

Proof: By induction on the sequence of states traversed as P′ and P compute, using Lemmas 22 and 23.

From Lemma 20 and Theorems 11 and 12, we may conclude:

Theorem 13 The gcsm refines the sbcm.

6.4. The Instantiated GSBCM Description

We instantiate the gc primitive by a specific garbage collection algorithm gc and we prove that it satisfies the property that gc(Σ) ≅ Σ. 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 Table 4. 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. It in effect translates the store to the left, adjusting all of the pointers to match.

Definition 18 (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⟩.

The result of shift(Σ, j) is a well-formed state if j ≤ ℓ whenever ⟨ptr ℓ⟩ is a component of Σ, and j ≤ ℓ whenever ⟨ptr ℓ⟩ occurs at a location ℓ_{0} in its store such that j ≤ ℓ_{0}. This condition ensures that a pointer always has a nonnegative value after the translation.

The garbage collector, which implements the algorithm given in Figure 4, uses several auxiliary functions. 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 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 pointer to the new object, called a broken heart; all other pointers to the old stored object will eventually be modified to point to the new object. If the object has already been copied to the new store, gc-convert returns the broken heart. The result of this function is always a pointer to an object in the new store.

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. 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.

We regard the garbage collector as an algorithm rather than simply a function. In the course of executing, the garbage collector modifies the store component of the state repeatedly. We say somewhat informally—for instance, in Lemma 25—that a store s occurs in a run of the garbage collection algorithm. By this we mean that gc-trace returns a pair ⟨d s⟩ on some “call” from gc_{0}, gc-trace-stack, or gc-scan-heap.

Garbage collection is indeed a non-trivial algorithm and it transforms the store through a succession of intermediate values. Therefore, the proof requires the use of a relation similar to ≅ to express an invariant maintained by the algorithm. 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 19 (GC Term Correspondence, GC State Similarity) Let ∼ be a store correspondence between gcsm stores s and s′.

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_{#a}⟩

where s_{0} = s and gc-trace(a(i), s_{i}) = ⟨a′_{i} s_{i+1}⟩

for 0 ≤ i < #a and a′ = ⟨a′_{0} a′_{1} … a′_{#a−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_{0}) = ⟨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_{0}) = s_{7}

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

Figure 4. Garbage Collection Algorithm

The GC term correspondence generated by ∼ is a relation ≃^{gc} between cells (i.e., value descriptors or bytes) cell and cell′, defined by taking cases on cell′. cell ≃^{gc} cell′ holds just in case one of the following holds:

1. cell′ = ⟨ptr l′⟩ and cell = ⟨ptr l⟩. Let l_{1} be l unless s(l − 1) is a broken heart ⟨ptr l_{0}⟩, in which case let l_{1} be l_{0}. Let l′_{1} be l′ unless s′(l′ − 1) is a broken heart ⟨ptr l′_{0}⟩, in which case let l′_{1} be l′_{0}. We require further:

(A) s′(l′_{1} − 1) = s(l_{1} − 1) = ⟨header h p m⟩, for some header type h, mutability

bit p and stored object length m; and (B) for all 0 ≤ i < m, (l_{1} + i) ∼ (l′_{1} + i).

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

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

4. cell′ = b = cell, for some byte 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 ∼.

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

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

Proof: Compose the witness store correspondences.

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

Definition 20 (GC Stored Objects) If s(l − 1) is a broken heart ⟨ptr l_{0}⟩, let l_{1} = l_{0}; let l_{1} = l otherwise. Then s contains a GC stored object at l if:

1. s(l_{1} − 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 l_{1} ≤ j < l_{1} + m.

A state Σ consists of GC stored objects if, whenever ⟨ptr l⟩ occurs in any (transitive) component of Σ, then the store of Σ contains a GC stored object at location l. Similarly, a store s consists of GC stored objects if, whenever ⟨ptr l⟩ occurs in a cell of s, then s contains a GC stored object at location l.

Lemma 25 1. Suppose that s is a store encountered (i.e., returned by gc-trace) during garbage collection of a gcsm accessible state; then s consists of GC stored objects.

2. If Σ consists of stored objects and Σ′ = gc(Σ), then Σ′ consists of stored objects.

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

2. Since Σ consists of stored objects, it consists (a fortiori) of GC stored objects. Using part 1 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.

This establishes that gc preserves the first invariant of Lemma 19; the properties given in its second clause are straightforward consequences of the algorithm.

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 26 Let s be a store encountered (i.e., returned by gc-trace) during garbage collection of a gcsm accessible state Σ, and let d be a component of Σ. Let

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

for some d′, s′. Suppose d is not a pointer, or that d = ⟨ptr l⟩ and s contains a GC stored object at l.

Then there exists a store correspondence ∼ between s and s′ with generated GC term correspondence ≃^{gc} such that

1. d′ ≃^{gc} d

2. ⟨t, n, v, a, u, k, s′, r⟩ ≅^{gc} Σ 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 l_{0}⟩, l_{0} = #s + 1, and

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

Define ∼ as follows:

l_{0} + 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.

1. s(l − 1) = ⟨header h p m⟩ by case condition. s′(l_{0} − 1) = s(l − 1) = ⟨header h p m⟩ by definition of s′. For all 0 ≤ i < m, l_{0} + i ∼ l + i holds by definition of ∼. Thus, by definition of ≃^{gc},

⟨ptr l_{0}⟩ ≃^{gc} ⟨ptr l⟩.

2. We first show that if vd is a value in one of the registers, or a component of the stack, then vd ≃^{gc} vd. First, if vd is not a pointer, vd ≃^{gc} vd holds by definition of ≃^{gc}.

Second, suppose vd = ⟨ptr y⟩ where y ≠ l. Let x = l′ if s(y−1) is a broken heart ⟨ptr l′⟩ and let x = y otherwise. Then s(x−1) = s′(x−1) = ⟨header h′ p′ m′⟩ for some h′, p′, m′, and x+i ∼ x+i for all 0 ≤ i < m′. Thus ⟨ptr y⟩ ≃^{gc} ⟨ptr y⟩ holds by definition of ≃^{gc}.

Finally, if vd = ⟨ptr l⟩, then we know that s(l − 1) = ⟨header h p m⟩ by the case condition. Further, s′(l − 1) = ⟨ptr l_{0}⟩ and s′(l_{0} − 1) = ⟨header h p m⟩ by definition of s′. Finally, for all 0 ≤ i < m, l_{0} + i ∼ l + i holds by definition of ∼. Thus, ⟨ptr l⟩ ≃^{gc} ⟨ptr l⟩ holds by definition of ≃^{gc}.

To complete the proof that ⟨t, n, v, a, u, k, s′, r⟩ ≅^{gc} Σ, we need to show that:

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′ = l_{0} + i by definition of ∼. Now s′(x′) = s′(l_{0} + 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 27 Let s_{0} and s consist of stored objects, where s_{0} is a prefix of s and #s_{0} ≤ l. Let Σ = ⟨t, n, v, a, u, k, s, r⟩, and let gc-trace(s(l), s) = ⟨d′ s′⟩. Then ⟨t, n, v, a, u, k, s′[l ↦ d′], r⟩ ≅^{gc} Σ.

Hence, inductively, ⟨t, n, v, a, u, k, gc-scan-heap(s, #s_{0}), r⟩ ≅^{gc} Σ.

Proof: By Lemma 26, ⟨t, n, v, a, u, k, s′, r⟩ ≅^{gc} Σ with ∼ as the witness store correspondence. Let ∼ extend to the term correspondence ≃^{gc}. 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} Σ.

If s(l) = ⟨ptr l_{0}⟩ for some l_{0}, then by definition of gc-trace, s(l) = s′(l) = ⟨ptr l_{0}⟩ since gc-trace only modifies s(l_{0} − 1) if it is a header and hence l_{0} − 1 ≠ l. Thus, we have that d′ ≃^{gc} s′(l) = ⟨ptr l_{0}⟩. 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 24).

Let ∼ be the identity function on all defined locations of s′ that are not headers of stored objects, and generate the 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 l_{0}⟩ it depends on s′(l_{0} − 1) and s′[l ↦ d′](l_{0} − 1) being the same header value. This holds since we know that s′(l) is not a header and hence l ≠ l_{0} − 1.

Moreover, s′[l ↦ d′](l) ≃^{gc} s′(l), because, as we showed above, d′ ≃^{gc} s′(l) = ⟨ptr l_{0}⟩.

Finally, we must show that gc-scan-heap terminates. We assume that the original store s_{0} consists of stored objects, and that s has the property that if i < #s_{0} and s_{0}(i) is not a header, then s(i) = s_{0}(i). Let ⟨d, s′⟩ = gc-trace(s(m), s), let s′′ = s′[m ↦ d], and let #s_{0} ≤ m. We have:

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

2. Assuming

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

then we may infer

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

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

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

The correctness of gc_{0} now follows from Lemmas 24, 26, and 27.

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

We now justify the application of shift:

Lemma 29 Let Σ = ⟨t, n, v, a, u, k, s, r⟩ be a gcsm state and let

gc_{0}(Σ) = ⟨t_{1}, n_{1}, v_{1}, a_{1}, u_{1}, k_{1}, s_{1}, r_{1}⟩.

If, for some l_{0}, one of t_{1}, v_{1}, u_{1}, k_{1}, r_{1}, a_{1}(i) for 0 ≤ i < #a, or s_{1}(i) for #s ≤ i is the value ⟨ptr l_{0}⟩, then 1. l_{0} ≥ #s;

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

Proof: By definition of gc, the state components t, v, u, k, r, a(i), and s(i) are replaced by the values of gc-trace applied to the components.

Let s′ be a store encountered during garbage collection of Σ such that if s′ contains a header of the form ⟨ptr l_{0}⟩, then l_{0} > #s and s′(l_{0} − 1) = ⟨header h p m⟩ for some h, p, m. If d′ is the value of a state component of Σ, and gc-trace(d′, s′) = (d′′, s′′), then we prove that s′′ also satisfies the above property. That is, we prove that if s′′ contains a header of the form ⟨ptr l_{0}⟩, then l_{0} > #s and s′(l_{0} − 1) = ⟨header h p m⟩ for some h, p, m. If s′ also contains the same header ⟨ptr l_{0}⟩, 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).

By induction, we have that all intermediate stores during garbage collection satisfy the property. But it follows from the definition of gc-trace that given such stores, if gc-trace returns a pointer ⟨ptr l_{0}⟩, then l_{0} ≥ #s and s_{1}(l_{0}−1) = ⟨header h p m⟩ for some h, p, m.

Finally, combining Lemmas 25, 28 and 29, we have:

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

gc(Σ) ≅^{gc} Σ

and

gc(Σ) ≅ Σ.

Implementation Note. Our proofs are proofs about algorithms, while of course our implementation consists of code. Thus, we have taken care to ensure that our code reflects the algorithms it implements in as lucid a way as possible. There is, however, one complication in matching the vm program to its specification. It is due to the fact that vlisp PreScheme, in the version used in this work, compiles to a language in which all procedure calls are in tail recursive position. Thus, where a procedure call is not in tail recursive position, the Front End must substitute the code for the called procedure in line. There are several instructions in the sbcm that cause memory to be allocated, and each of them, when coded in the obvious way, contains a non-tail-recursive 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, because the original procedure must 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 only a little lucidity as a consequence of this programming approach. Our PreScheme implementation has since been improved; procedure calls in non-tail-recursive position need no longer be expanded in line [13].

6.5. The Finite Stored Byte Code Machine (FSBCM)

A finite state machine (with any fixed word size, bounded store size, and bounded stack size) cannot simulate all the computation histories of the gcsm, because there will always be computations that require more pointers than can be stored in words, stores, or stacks of the given size. We define a Finite Stored Byte Code Machine (fgcsm) and prove that it is a weak refinement (see Section 4) of the gcsm.

Table 27 contains the abstract syntax for the states of the fgcsm. The definition ensures that they form a proper subset of the states of sbc. The initial (halt) fgcsm states are the fgcsm states that are gcsm initial (halt) states. The fgcsm action rules are the gcsm action rules with domain and range restricted to fgcsm states. Thus, if an fgcsm action rule is defined on an fgcsm state, then its value at that state is the same as that of the corresponding gcsm action rule. The implemented values of max-store-size and of the upper and lower bounds for fixed point numbers reflect a 32-bit word size in which two bits are reserved for tags.

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

Theorem 15 Let ∼ be the identity relation on fgcsm states. Then ∼ is a weak storage layout relation between fgcsm and gcsm, and fgcsm weakly refines gcsm.

6.6. Concrete Virtual Machine

A concrete implementation of the Virtual Machine is obtained by directly encoding the fgcsm as a PreScheme program. The actual vlisp Virtual Machine implementation differs from the implementation described here in several ways:

1. The actual implementation is designed to run on machines with 32-bit physical memory words. Since there are fewer than 256 distinct fsbc bytes, the implementation optimizes the representations of “string” and “codevector” stored

Table 27. Abstract Syntax of Finite Stored Byte Code (fsbc).

program ::= term
term ::= ⟨store vdesc⟩
store ::= cell^{∗}  with #cell^{∗} < max-store-size
stack ::= vdesc^{∗} with #vdesc^{∗} < max-stack-size
cell ::= desc | byte
desc ::= ⟨header htag bool nat_{1}⟩ | vdesc
vdesc ::= ⟨ptr nat_{2}⟩ | ⟨fixnum int⟩ | ⟨imm imm⟩
imm ::= false | true | ⟨char nat_{3}⟩ | null | undefined

unspecified | empty-env | halt | eof

htag ::= bhtag | dhtag
bhtag ::= string | codevector
dhtag ::= pair | symbol | vector | location | template |

closure | port | continuation | environment

byte ::= nat_{4}

nat_{1} ::= 0..max-object-size
nat_{2} ::= 0..max-pointer-size

nat_{3} ::= 0..127
nat_{4} ::= 0..255

 int ::= min-fixnum-size..max-fixnum-size

objects by packing the bytes within them; specifically, four bytes are packed into a single store cell.

2. The actual implementation represents both the argument stack and the store within a single vector (called the heap). The representation is non-trivial and is designed to optimize certain expensive action rules. Specifically, this optimization permits the action rules make-env and make-cont to create environment and continuation stored objects respectively, without copying the contents of the argument stack to the store. This results in a much faster interpreter.

3. The actual implementation contains two heaps, only one of which is in active use. During garbage collection, it copies the reachable contents of the active heap to the inactive heap and switches the roles of the heaps. In this paper, the state machines have a single store, and the garbage collector copies reachable objects to the end of the current store.

4. The correctness proof of the garbage collector requires that all stored objects in the store have active value fields. To meet this condition, the state operation make-stob is specified (see Table 26) to create a new stored object and to initialize the value fields of this object to a distinctive value (⟨imm undefined⟩). Since this is time-consuming, the actual implementation does not initialize objects during allocation, but explicitly writes active values into new objects immediately after allocation. The garbage collector is not invoked until these writes have been performed.

5. The actual implementation represents fsbc cells as 32-bit binary numerals.

The proofs presented here have been extended to accommodate these optimizations.

7. Conclusion

Although the vlisp verification is quite comprehensive, and covers the great majority of the detailed implementation, there are a number of unverified aspects:

• 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.

• 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 PreScheme Front End [12, 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.

To have fully verified these aspects would have greatly increased the scale of the work.

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 [7].

List of Tables

1 vlisp Verification Steps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2 Scheme Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3 Grammar for the Basic Byte Code . . . . . . . . . . . . . . . . . . . . . . . 11 4 Some Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 5 Domains for the Semantics of Scheme . . . . . . . . . . . . . . . . . . . . . 14 6 Scheme Semantic Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 7 Scheme Semantics: Some Semantic Clauses . . . . . . . . . . . . . . . . . . 16 8 Byte Code Semantics: Additional Domains . . . . . . . . . . . . . . . . . . 17 9 Byte Code Semantic Functions . . . . . . . . . . . . . . . . . . . . . . . . . 17 10 Some Byte Code Semantic Clauses . . . . . . . . . . . . . . . . . . . . . . . 18 11 Some Byte Code Auxiliary Functions . . . . . . . . . . . . . . . . . . . . . . 18 12 Pure Procedure Objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 13 abc Syntactic Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 14 Some Operational Rules for the Basic Byte Code . . . . . . . . . . . . . . . 33 15 Semantic Functions for the Faithfulness Proof . . . . . . . . . . . . . . . . . 34 16 Semantic Clauses for the Faithfulness Proof . . . . . . . . . . . . . . . . . . 35 17 bbcm Open Branch Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 18 Flattened Byte Code: Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . 45 19 Flattened Byte Code State Machine: State Component Syntax . . . . . . . 46 20 Typical fbcm Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 21 Recursive Conditions for ≃. . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 22 Closure Conditions for ∼. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 23 Abstract Syntax of Stored Byte Code (sbc). . . . . . . . . . . . . . . . . . . 55 24 Action Rule for the call Instruction. . . . . . . . . . . . . . . . . . . . . . . 56 25 sbcm State Observers for Σ = ⟨t, n, v, a, u, k, s, r⟩. . . . . . . . . . . . . . . . 57 26 sbcm State Modifiers for Σ = ⟨t, n, v, a, u, k, s, r⟩. . . . . . . . . . . . . . . . 58 27 Abstract Syntax of Finite Stored Byte Code (fsbc). . . . . . . . . . . . . . 74

List of Figures

1 Compiler Dispatch Procedure, and case for Procedure Call. . . . . . . . . . 12 2 Flattener Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3 Instantiation of the call Action Rule. . . . . . . . . . . . . . . . . . . . . . 59 4 Garbage Collection Algorithm . . . . . . . . . . . . . . . . . . . . . . . . . . 67

References

1. William 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.

2. William M. Farmer. A partial functions version of Church’s simple theory of types. Journal of Symbolic Logic, 55(3):1269–91, 1990. Also MITRE Corporation technical report M88-52, 1988; revised 1990.

3. William M. Farmer, Joshua D. Guttman, Leonard G. Monk, John D. Ramsdell, and Vipin Swarup. The faithfulness of the VLISP operational semantics. M 92B093, The MITRE Corporation, September 1992.

4. William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. imps: an Interactive Mathematical Proof System. Journal of Automated Reasoning, 11(2):213–248, October 1993.

5. Joshua D. Guttman, Leonard G. Monk, William M. Farmer, John D. Ramsdell, and Vipin Swarup. The VLISP byte-code compiler. M 92B092, The MITRE Corporation, September 1992.

6. Joshua D. Guttman, Leonard G. Monk, William M. Farmer, John D. Ramsdell, and Vipin Swarup. The VLISP flattener. M 92B094, The MITRE Corporation, 1992.

7. Joshua D. Guttman, John D. Ramsdell, and Mitchell Wand. VLISP: A verified implementation of Scheme. Lisp and Symbolic Computation, 8(1/2):???–???, 1995.

8. C. A. R. Hoare. Notes on data structuring. In O.-J. Dahl, editor, Structured Programming. Academic Press, 1972.

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

10. Richard A. Kelsey and Jonathan A. Rees. Scheme48 progress report. Manuscript in preparation, 1992.

11. Robin Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

12. Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified PreScheme compiler. Lisp and Symbolic Computation, 8(1/2):???–???, 1995.

13. John D. Ramsdell. The revised VLISP PreScheme front end. M 93B095, The MITRE Corporation, August 1993.

14. Jonathan A. Rees, Norman I. Adams, and James R. Meehan. The T Manual. Computer Science Department, Yale University, fifth edition edition, 1988.

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

16. Vipin Swarup, William M. Farmer, Joshua D. Guttman, Leonard G. Monk, and John D. Ramsdell. The VLISP byte-code interpreter. M 92B097, The MITRE Corporation, September 1992.

17. Mitchell Wand. Semantics-directed machine architecture. In Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang., pages 234–241, 1982.

18. Mitchell Wand and Dino 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.