VLISP Byte Code Interpreter

Vipin Swarup  William M. Farmer  Joshua D. Guttman
Leonard G. Monk  John D. Ramsdell

The MITRE Corporation^{1} M92B097 September 1992

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. \begin{matrix}c \\ ◯ \end{matrix}1992 The MITRE Corporation. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the MITRE copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of the MITRE Corporation.

Abstract

The Verified Programming Language Implementation project has developed a formally verified implementation of the Scheme programming language. This report documents the byte-code interpreter, which executes a user program presented in the form of a binary image. It specifies several intermediate abstract machines, and proves that they are (successive) faithful implementations of the Vlisp operational semantics. Garbage collection and the finiteness of computer memories are among the issues handled. iv

Contents

1 Introduction 1 1.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2 Microcoded SBC State Machine 4

2.1 SBC Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . 4 2.1.2 Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 2.1.3 Programs . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.2 MSBC State Machines (MSBCM) . . . . . . . . . . . . . . . . 9 2.2.1 Microcoded Stored Byte Code (msbc) . . . . . . . . . 9 2.2.2 Stored Object Predicates . . . . . . . . . . . . . . . . 14 2.2.3 States . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.2.4 Initial and Halt States . . . . . . . . . . . . . . . . . . 16 2.2.5 State Observers and Mutators . . . . . . . . . . . . . . 17 2.2.6 Stored Object Manipulators . . . . . . . . . . . . . . . 17 2.2.7 Miscellaneous Auxiliary Functions . . . . . . . . . . . 40 2.2.8 Action Rules . . . . . . . . . . . . . . . . . . . . . . . 40

2.3 SBC Operational Semantics . . . . . . . . . . . . . . . . . . . 53 2.4 State Correspondence Relation . . . . . . . . . . . . . . . . . 57 2.5 Establishing State Correspondence . . . . . . . . . . . . . . . 58 2.6 Preserving State Correspondence . . . . . . . . . . . . . . . . 60 2.7 Correspondence of Final Answers . . . . . . . . . . . . . . . . 63 2.8 Correspondence of Semantics . . . . . . . . . . . . . . . . . . 64

3 Garbage-collected SBC State Machine 65

3.1 GSBC State Machine (GSBCM) . . . . . . . . . . . . . . . . 65 3.1.1 States . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 3.1.2 Garbage Collection Algorithm . . . . . . . . . . . . . . 66 3.1.3 State Observers and Mutators . . . . . . . . . . . . . . 69 3.1.4 Action Rules . . . . . . . . . . . . . . . . . . . . . . . 69

3.2 SBC Operational Semantics . . . . . . . . . . . . . . . . . . . 69 3.3 State Correspondence Relation . . . . . . . . . . . . . . . . . 70 3.4 Establishing State Correspondence . . . . . . . . . . . . . . . 72 3.5 Preserving State Correspondence . . . . . . . . . . . . . . . . 73

3.5.1 Garbage Collection . . . . . . . . . . . . . . . . . . . . 73 3.5.2 Microcode Functions . . . . . . . . . . . . . . . . . . . 81

3.6 Correspondence of Final Answers . . . . . . . . . . . . . . . . 91

3.7 Correspondence of Semantics . . . . . . . . . . . . . . . . . . 91

4 Finite SBC State Machine 93

4.1 FSBC State Machine (FSBCM) . . . . . . . . . . . . . . . . . 93 4.1.1 Finite Stored Byte Code (FSBC) . . . . . . . . . . . . 93 4.1.2 Stores . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 4.1.3 States . . . . . . . . . . . . . . . . . . . . . . . . . . . 96 4.1.4 Action Rules . . . . . . . . . . . . . . . . . . . . . . . 97 4.1.5 Implementation . . . . . . . . . . . . . . . . . . . . . . 97 4.1.6 SBC Operational Semantics . . . . . . . . . . . . . . . 101

4.2 Correspondence Relation . . . . . . . . . . . . . . . . . . . . . 102 4.3 Establishing State Correspondence . . . . . . . . . . . . . . . 103 4.4 Preserving State Correspondence . . . . . . . . . . . . . . . . 104 4.5 Correspondence of Final Answers . . . . . . . . . . . . . . . . 105 4.6 Correspondence of Semantics . . . . . . . . . . . . . . . . . . 105

A A New Storage Layout 106

References 107

1 Introduction

The vlisp byte code compiler translates Scheme programs into vlisp Stored Byte Code (sbc) programs. This report presents and justifies the translation of sbc programs to vlisp Finite Stored Byte Code (fsbc) programs, and the vlisp implementation of an interpreter for fsbcprograms. fsbc is a “finite” subset of sbc. The syntax of sbc is presented in the vlisp report on the image builder [5]. That report also presents an operational semantics of sbc (and hence of fsbc) in terms of a state machine called the Stored Byte Code Machine (sbcm). We do not reproduce the syntax and sbcm semantics of Stored Byte Code but refer the reader to the vlisp report that describes that language [5].

This report shall address several issues related to the implementation of a practical interpreter:

1. The interpreter has operations that create environments and continuations by copying an argument stack. By changing the representation of stores and stacks, it is possible to eliminate this copying. A minor modification to this representation permits continuations to be created and restored in a stack-like fashion; the result is a much faster interpreter.

2. A physical computer has finite memory, i.e., it has a fixed number of memory cells. Since the vlisp interpreter makes heavy use of memory, its practicality depends on automatic storage reclamation; this is provided via a garbage-collector that reclaims memory cells whose contents do not affect the behavior of the interpreter.

3. Another factor in the finiteness of a physical computer’s memory is that each memory cell can only contain a number within fixed bounds. The vlisp interpreter terminates gracefully (with an error message) if its memory bounds are ever exceeded.

This report presents:

1. an operational semantics of sbc in terms of a state machine called the microcoded stored byte code machine (msbcm). This machine incorporates a storage optimization which permits the implementation to create environments and continuations without copying the argument stack. It also refines the sbcm so that the action rules of the state machine can be expressed as the composition of a small set of primitive functions.

2. a proof that the operational semantics of sbc as given by the msbcm is equivalent to the operational semantics of sbc as given by the sbcm.

3. an operational semantics of sbc in terms of a state machine called the garbage-collected stored byte code machine (gsbcm). This machine incorporates a storage optimization which permits the implementation to reclaim memory via a standard garbage-collection algorithm.

4. a proof that the operational semantics of sbc programs in terms of the gsbcm is equivalent to the operational semantics of sbc programs in terms of the msbcm.

5. the syntax of vlisp Finite Stored Byte Code (fsbc) (defined as a subset of sbc), and a function that checks whether a sbc program is an fsbc program.

6. an operational semantics of fsbc in terms of a state machine called the finite stored byte code machine (fsbcm). This machine has states whose components are either finite numbers (with fixed bounds) or fixed-length sequences of such finite numbers. This permits the implementation to be realized on a physical machine with finite storage capacity.

7. a proof that the operational semantics of fsbc as given by the fsbcm is faithful to the operational semantics of fsbc as given by the gsbcm. That is, if the fsbcm operational semantics assigns a meaning to an fsbc program, then the gsbcm operational semantics assigns the same meaning to the program.

8. a map from fsbc programs to binary images.

1.1 Notation

We will use the notation contained in Table 1. Additional explanation of our notation can be found in the vlisp report [1].

⟨ … ⟩  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
s^{⌢} t  concatenation of sequences s and t
Σ_{i=0}^{n−1}α_{i} concatenation of sequences α_{i} for 0 ≤ i < n
s † k  drop the first k members of sequence s
s ‡ k  the sequence of only the first k members of s
ρ[i ↦ x] the function which is the same as ρ

except that it takes the value x at i Figure 1: Some Notation

2 Microcoded SBC State Machine

The vlisp report [5] defined the syntax and operational semantics of stored byte code (sbc), and justified the vlisp translation from linked byte code to sbc. The operational semantics of sbc was presented in terms of a state machine called the stored byte code machine (sbcm). In this chapter, we describe the operational semantics of sbc in terms of a new state machine called the microcoded stored byte code machine (msbcm), and we show that this semantics is equivalent to the semantics presented in terms of the sbcm. The msbcm refines the sbcm in two ways:

1. The msbcm alters the representation of stores and stacks to permit a more efficient implementation of some of the action rules; in particular, the action rules make-env and make-cont can be implemented without copying the argument stack. It is possible to modify this algorithm to permit continuations to be created and restored in a stack-like fashion. This optimization can be added and verified at this level and, based on preliminary benchmarks, would speed up the interpreter substantially.

2. The msbcm includes four temporary registers in its states; this permits the msbcm action rules to be expressed as the composition of a small set of primitive functions. In subsequent chapters, we shall refine these primitive functions, thus obtaining an implementation of an sbc interpreter. The actual implementation is written in a subset of Scheme called PreScheme and it is compiled by a verified PreScheme compiler [4, 3].

2.1 SBC Syntax

We reproduce the syntax of the sbc from the vlisp Image Builder report [5].

2.1.1 Abstract Syntax

We express the syntax of sbc in Backus-Naur form (bnf). The terminal symbols of sbc are:

primitives: natural numbers (i.e., 0,1,2,…), booleans (i.e., #t and #f), and identifiers (i.e., alphanumeric symbols that begin with an alphabetic letter); constructors: header, ptr, fixnum, imm, false, true, char, null,

undefined, pair, symbol, string, vector, location, template, codevector;

keywords: empty, call, return, make-cont, literal, closure, global,
local, set-global!, set-local!, push, make-env, make-restlist,
unspecified, jump, jump-if-false, check-args=, check-args>=

symbols: “<”, “>”

The nonterminal symbols are as follows:

nat  for natural numbers,
bool  for booleans,
ident  for identifiers,
program for (sbc) programs,
term  for (sbc) terms,
store  for (sbc) stores,
cell  for (sbc) cells,
desc  for (sbc) descriptors,
vdesc  for (sbc) value descriptors,
imm  for (sbc) immediates,
htag  for (sbc) header tags,
bhtag  for (sbc) byte header tags,
dhtag  for (sbc) descriptor header tags,
byte  for (sbc) bytes,
loc  for (sbc) locations, and
obj  for (sbc) stored object data

We use extended bnf with productions having the form N ::= S_{1} | … | S_{n} where N is a nonterminal, and the S_{i}’s are possible forms for phrases in the set denoted by N. We use a variant of the conventional notation for repetition. We write S^{k} (where k is a nonnegative integer) to stand for the sequence ⟨SS … S⟩ containing k occurrences of S. We write S^{∗} to stand for the sequence ⟨SS …⟩ containing a finite number of occurrences of S (including, possibly, no occurrence of S).

We assume bpw to be some constant natural number; in the implementation, bpw will be either 1 or 4 (due to the architecture of the physical machines we shall be working with).

The abstract syntax of Stored Byte Code (sbc) is as follows:

program ::= term
term ::= ⟨store vdesc⟩
store ::= cell^{∗}
cell ::= desc | byte^{bpw}
desc ::= ⟨header htag bool nat⟩ | vdesc
vdesc ::= ⟨ptr loc⟩ | ⟨fixnum nat⟩ | ⟨immediate imm⟩
imm ::= false | true | ⟨char nat⟩ | null | undefined
htag ::= bhtag | dhtag
bhtag ::= string | codevector
dhtag ::= pair | symbol | vector | location | template

byte ::= nat | empty | call | return | make-cont | literal |

closure | global | local | set-global! | set-local! |
push | make-env | make-restlist | unspecified | jump |
jump-if-false | check-args= | check-args>= | ident

loc ::= nat
obj ::= vdesc | byte

We will use i and m-like variables for natural numbers, p-like variables for booleans, and r-like variables for identifiers. Similarly for the other nonterminals, with

P  for (sbc) programs,
T  for (sbc) terms,
s  for (sbc) stores,
c  for (sbc) cells,
d  for (sbc) descriptors,
vd  for (sbc) value descriptors,
imm for (sbc) immediates,
h  for (sbc) header tags,
bh  for (sbc) byte header tags,
dh  for (sbc) descriptor header tags,
b  for (sbc) bytes,
l  for (sbc) locations, and
o  for (sbc) stored object data

We will define an sbc store in such a way that it can be viewed as a succession of stored objects. Each stored object is a sequence of cells, with the first cell being a header and the remaining cells being data. Stored objects are classified into two broad classes: descriptor objects and byte objects.

The data cells of descriptor objects are value descriptors, which are either constants (numbers, booleans, characters, etc.) or pointers to stored objects. A pointer is restricted to index the first data cell of some stored object. A header cell of a descriptor object has the form ⟨header dh p m⟩ where dh (the (descriptor) header tag) is a tag that describes the stored object, p (the mutability flag) is a boolean value that describes whether the object is mutable, and m (the header size) is a multiple of the number of value descriptors in the stored object, the multiple being the constant bpw.

The data cells of byte objects are fixed length sequences of bytes, bytes being numbers, keywords, or (special) identifiers. These sequences of bytes can be concatenated to obtain a single sequence of bytes. Only a prefix of this sequence is considered to be useful, and the bytes in this prefix are called useful bytes. A header cell of a byte object has the form ⟨header bh p m⟩ where bh (the (byte) header tag) is a tag that describes the stored object, p (the mutability flag) is a boolean value that describes whether the object is mutable, and m (the header size) is the number of useful bytes in the stored object.

We shall identify a stored object by the name of its header tag. Thus we call a stored object with header tag template to be a template. Templates, codevectors, and symbols are immutable and hence their immutability flag is always false (#f). Locations are always mutable, while pairs, strings, and vectors may be either mutable or immutable. Likewise, the header size of symbols is always 1 ∗ bpw, the header size of locations and pairs is always 2 ∗ bpw, and the header size of templates, codevectors, strings, and vectors varies.

An sbc term is an sbc store together with a value descriptor. If the value descriptor is a constant, then the store is irrelevant; otherwise, the value descriptor will be a pointer to a stored object in the store. An sbc program is an sbc term that consists of an sbc store and a pointer to a “template object” in the store.

The header of a stored object contains the object size in units of the number of bytes — we call this the size in bytes. The object size in units of cells (i.e., the size in cells) is obtained by means of a function ℧ that converts a size in bytes to a size in cells. Thus if a stored object’s header size is n, then the object consists of ℧(n) data cells. The function Ω converts a size in cells to a size in bytes. These functions use the constant bpw which represents the number of bytes per cell.

Definition 1 Let div be the integer division (i.e., quotient) operation. Then ℧ and Ω are functions (from natural numbers to natural numbers) defined as follows:

℧n =^{def} (n + bpw − 1) div bpw
Ωn =^{def} n ∗ bpw

2.1.2 Stores

A store s is represented as a sequence of cells. Thus #s is the domain of s, and is also the least l such that s(l) is not defined. s[l ↦ v] is the function whose domain is #s ∪ l and which is identical to s at all arguments except possibly l where its value is v. This is a store if and only if l ≤ #s. An sbc store is defined to be a store that satisfies the following invariants:

1. If s(l) = ⟨header h p m⟩ for some l, h, p, m, then for all 1 ≤ x ≤ ℧m,

• If h ∈ bhtag, then s(l + x) = ⟨b_{1} … b_{bpw}⟩ for some b_{1} … b_{bpw},

• If h ∈ dhtag, then s(l + x) = vd for some vd;

2. For all l such that s(l) is defined,

s(l)(1) ≠ header ⇒

(∃l′, h, p, m) \begin{matrix}(s(l′) = ⟨header h p m⟩)∧ \\ (l′ < l ≤ l′ + ℧m) \end{matrix}

3. If s(l) = ⟨ptr l′⟩ for some l, l′, then s(l′ − 1) = ⟨header h p m⟩ for some h, p, m.

These invariants ensure that the store is a succession of stored objects. Thus every header cell in the store is the header of a stored object and should be followed by the appropriate number and kind of data cells (invariant 1), every non-header cell in the store is a data cell of some stored object (invariant 2), and every pointer cell is a pointer to the first data cell of a stored object (invariant 3).

2.1.3 Programs

An sbc program is defined to be a term ⟨s vd⟩ such that

1. s is an sbc store;

2. all location objects have undefined values. That is, if s(l − 1) = ⟨header location #t 2∗bpw⟩, then s(l) = ⟨immediate undefined⟩; and

3. vd is a pointer to a template object in the store s, i.e., vd = ⟨ptr l⟩ and s(l−1) = ⟨header template #f m⟩ for some l, m. vd represents the root template of the program.

2.2 MSBC State Machines (MSBCM)

The operational semantics of stored byte code is defined in terms of a deterministic state machine with concrete states. The state machine is called the Microcoded Stored Byte Code Machine (msbcm). We define the syntax of msbc states by augmenting the syntax of the Stored Byte Code. We then define the states and action rules of a deterministic state machine. We adopt the notation and conventions presented in the vlisp Image Builder report [5].

2.2.1 Microcoded Stored Byte Code (msbc)

The Microcoded Stored Byte Code (msbc) provides the syntactic objects that form the states of the msbcm. It expands the sbc to provide representations of objects such as environments, closures, continuations, etc. These objects are not part of sbc as they do not occur in the code obtained by compiling Scheme programs; they are put in the initial state of the msbcm and are also generated during the course of computation.

The new msbc tokens are as follows:

constructors: unspecified, empty-env, halt, eof, closure, port, continuation, environment

The new msbc syntactic categories are:

t for (msbc) templates,
n for (msbc) offsets,
c for (msbc) codevectors,
v for (msbc) values,
u for (msbc) environments,
k for (msbc) continuations,
a for (msbc) argument stacks

The abstract syntax of Microcoded Stored Byte Code (msbc) is defined below. This grammar redefines several syntactic categories of sbc.

program ::= term
term ::= ⟨store vdesc⟩
store ::= ⟨storeseg storeseg storeseg storeseg⟩
storeseg ::= cell^{∗}
cell ::= desc | byte^{bpw}
desc ::= ⟨header htag bool nat⟩ | vdesc
vdesc ::= ⟨ptr loc⟩ | ⟨fixnum nat⟩ | ⟨immediate imm⟩
imm ::= false | true | ⟨char nat⟩ | 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 | empty | call | return | make-cont | literal |

closure | global | local | set-global! | set-local! |
push | make-env | make-restlist | unspecified | jump |
jump-if-false | check-args= | check-args>= | ident

loc ::= ⟨nat nat⟩
obj ::= vdesc | byte
stack ::= vdesc^{∗}

We extend the naming conventions of sbc for variables. Thus, we will use m-like variables for numbers, p-like variables for booleans, and r-like variables for identifiers. Similarly for the other nonterminals, with

P  for (msbc) programs,
T  for (msbc) terms,
s  for (msbc) stores,
s_{i}  for (msbc) store segments with i < 4,
cell for (msbc) cells,
d  for (msbc) descriptors,
vd  for (msbc) value descriptors,
imm for (msbc) immediates,
h  for (msbc) header tags,
bh  for (msbc) byte header tags,
dh  for (msbc) descriptor header tags,
b  for (msbc) bytes,
l  for (msbc) locations,
o  for (msbc) stored object data, and
a  for (msbc) stacks

In addition, we will use t, c, v, u, k, and r-like variables for (msbc) value descriptors, and i,m,n-like variables for numbers.

Stores A store s is represented as a sequence of four store segments, where each store segment is a sequence of cells. By abuse of notation, we shall write s(⟨i, m⟩) to mean s(i)(m). The first and third store segments are indexed by the nonnegative integers, while the second and fourth are indexed by the nonpositive integers.

Let 0 ≤ i < 4 and let s_{i} = s(i). Then, for i ∈ {0, 2}, #s_{i} is the domain of s_{i}, and is also the least nonnegative m such that s_{i}(m) is not defined. For i ∈ {1, 3}, −#s_{i} is the domain of s_{i}, and is also the greatest nonpositive m such that s_{i}(m) is not defined. s_{i}[m ↦ v] is the function whose domain is #s_{i} ∪ m and which is identical to s_{i} at all arguments except possibly m where its value is v. This is a store if and only if i ∈ {0, 2} and m ≤ #s_{i} or i ∈ {1, 3} and m ≥ −#s_{i}. We shall write s[⟨i, m⟩ ↦ v] to mean s(i)[m ↦ v].

A location l is a pair of numbers ⟨i, m⟩ such that

• m ≥ 0 if i ∈ {0, 2}

• m ≤ 0 if i ∈ {1, 3}

Let l = ⟨i, m⟩ and l′ = ⟨i′, m′⟩. By the above notation, s(l) = s(i)(m) and s(l′) = s(i′)(m′). We shall also use the following notation:

l +_{A} n =^{def} ⟨i, (m + n)⟩
l −_{A} n =^{def} ⟨i, (m − n)⟩
l <_{A} l′ =^{def} (i = i′) ∧ (m < m′)
l ≤_{A} l′ =^{def} (i = i′) ∧ (m ≤ m′)

An msbc store is defined to be a store that satisfies the following invariants:

1. If s(l) = ⟨header h p m⟩ for some l, h, p, m, then for all 1 ≤ x ≤ ℧m,

• If h ∈ bhtag, then s(l +_{A} x) = ⟨b_{1} … b_{bpw}⟩ for some b_{1} … b_{bpw}.

• If h ∈ dhtag, then s(l +_{A} x) = vd for some vd.

2. For all l such that s(l) is defined,

s(l)(1) ≠ header ⇒

(∃l′, h, p, m) \begin{matrix}(s(l′) = ⟨header h p m⟩)∧ \\ (l′ <_{A} l ≤_{A} l′ +_{A} ℧m) \end{matrix}

3. If s(l) = ⟨ptr l′⟩ for some l, l′, then s(l′ −_{A} 1) = ⟨header h p m⟩ for some h, p, m.

These invariants ensure that each store segment is a succession of stored objects. Thus every header cell in the store is the header of a stored object and should be followed by the appropriate number and kind of data cells (invariant 1), every non-header cell in the store is a data cell of some stored object (invariant 2), and every pointer cell is a pointer to the first data cell of a stored object (invariant 3).

Stored Objects An msbc store consists of a succession of stored objects. Each stored object is a sequence of cells, with the first cell being a header and the remaining cells being data. A stored object is always identified by the location of its first data cell. If l is a location such that s(l) is the first data cell of a stored object, then ⟨ptr l⟩ is called a pointer to the stored object in store s.

Let d be a pointer into store s. Then S(d, s) is defined to be a sequence of the contents of the stored object pointed to by d in s. The first element of this sequence is the header tag, the second element is the mutability flag, and the remaining elements are the data elements of the object. Note that the sequences of bytes within a byte object are flattened into a single byte sequence; this resulting sequence may be larger than the object size, so the extra bytes are truncated from the end of the sequence. The result is the sequence of “useful” bytes in the stored object.

Definition 2 For all d, s, h, p, m, o^{∗}, l such that s(l +_{A} (℧m − 1)) is defined,

S(d, s) =^{def} ⟨h p o^{∗}⟩ if

• d = ⟨ptr l⟩

• s(l −_{A} 1) = ⟨header h p m⟩

• if h ∈ dhtag then

o^{∗} = ⟨s(l) … s(l +_{A} (℧m − 1))⟩ else

o^{∗} = (s(l)^{⌢} …^{⌢} s(l +_{A} (℧m − 1))) ‡ m

The following notation provides a concise way of appending stored objects to stores.

Definition 3 Let s = ⟨s_{0} s_{1} s_{2} s_{3}⟩ be an msbc store. If i ∈ {0, 2} then

s +_{i} ⟨h p o^{∗}⟩ =^{def} if h ∈ dhtag then s[i ↦ s_{i} ^{⌢} ⟨⟨header h p (Ω#o^{∗})⟩⟩^{⌢} o^{∗}] else s[i ↦ s_{i} ^{⌢} ⟨⟨header h p #o^{∗}⟩⟩^{⌢} o^{′∗}] where #o^{′∗} = ℧#o^{∗}, and (∀0 ≤ i < #o^{′∗}) #o^{′∗}(i) = bpw and o^{∗} = (Σ_{i=0}^{#o^{′∗}−1}o^{′∗}(i)) ‡ #o^{∗}

If i ∈ {1, 3} then

s +_{i} ⟨h p o^{∗}⟩ =^{def} if h ∈ dhtag then s[i ↦ ⟨⟨header h p (Ω#o^{∗})⟩⟩^{⌢} o^{∗} ^{⌢} s_{i}] else s[i ↦ ⟨⟨header h p #o^{∗}⟩⟩^{⌢} o^{′∗} ^{⌢} s_{i}] where #o^{′∗} = ℧#o^{∗}, and (∀0 ≤ i < #o^{′∗}) #o^{′∗}(i) = bpw and o^{∗} = (Σ_{i=0}^{#o^{′∗}−1}o^{′∗}(i)) ‡ #o^{∗}

The following lemma asserts that appending a stored object to the ith segment of a store s (for i ∈ {0, 2}) results in a new store s′ such that ⟨ptr ⟨i (#s_{i} + 1)⟩⟩ is a pointer to the stored object in the new store s′.

Lemma 4 S(⟨ptr ⟨i (#s_{i} + 1)⟩⟩, s +_{i} ⟨h p o^{∗}⟩) = ⟨h p o^{∗}⟩

Proof: Immediate from definitions.

□

The following lemma asserts that appending a stored object to the ith segment of a store s (for i ∈ {1, 3}) results in a new store s′ such that ⟨ptr ⟨i (−#s_{i} − #o^{∗} + 1)⟩⟩ is a pointer to the stored object in the new store s′.

Lemma 5 S(⟨ptr ⟨i (−#s_{i} − #o^{∗} + 1)⟩⟩, s +_{i} ⟨h p o^{∗}⟩) = ⟨h p o^{∗}⟩

Proof: Immediate from definitions.

□

The following notation provides a concise way of creating a new stored object and appending it to a store. Let i ∈ {0, 2} and let s be an msbc store. Then,

s ⊕_{i} ⟨h p m⟩ = s +_{i} ⟨h p d_{u}^{∗}⟩ if h ∈ dhtag and #d_{u}^{∗} = m
s +_{i} ⟨h p b^{∗}⟩ if h ∈ bhtag and #b^{∗} = m

2.2.2 Stored Object Predicates

We define a family of predicates that characterize the types of stored objects in an msbc store. These relations are defined recursively.

Let d, t, c, v, u, k range over value descriptors. The free variables in each formula are (implicitly) existentially quantified over the entire formula. Thus, for example,

String(d, s) =^{def} S(d, s) = ⟨string p b^{∗}⟩

means

String(d, s) =^{def} (∃p, b^{∗})S(d, s) = ⟨string p b^{∗}⟩.

Pair(d, s)  ⟺ S(d, s) = ⟨pair p ⟨o_{1} o_{2}⟩⟩

and Value(o_{1}, s) and Value(o_{2}, s)

Symbol(d, s)  ⟺ S(d, s) = ⟨symbol #f ⟨o⟩⟩ and String(o, s)
String(d, s)  ⟺ S(d, s) = ⟨string p b^{∗}⟩
Vector(d, s)  ⟺ S(d, s) = ⟨vector p o^{∗}⟩

and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

Location(d, s)  ⟺ S(d, s) = ⟨location #t ⟨o_{1} o_{2}⟩⟩

and Value(o_{1}, s) and Symbol(o_{2}, s)

Template(t, s)  ⟺ S(t, s) = ⟨template #f c::o^{∗}⟩

and Codevector(c, s) and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

Codevector(c, s)  ⟺ S(c, s) = ⟨codevector #f b^{∗}⟩
Offset(n, t, s)  ⟺ Template(t, s)

and S(t, s) = ⟨template #f c::o^{∗}⟩ and S(c, s) = ⟨codevector #f b^{∗}⟩ and 0 ≤ n < #b^{∗}

Closure(d, s)  ⟺ S(d, s) = ⟨closure #f ⟨t u⟩⟩

and Template(t, s) and Environment(u, s)

Continuation(k, s) ⟺ k = ⟨immediate halt⟩ or

S(k, s) = ⟨continuation #f ⟨t n u k⟩^{⌢} vd^{∗}⟩ and Template(t, s) and Offset(n, t, s) and Environment(u, s) and Continuation(k, s) and (∀0 ≤ i < #vd^{∗}) Value(vd^{∗}(i), s)

Environment(u, s) ⟺ u = ⟨immediate empty-env⟩ or

S(u, s) = ⟨environment #t u′::o^{∗}⟩ and Environment(u′, s) and (∀0 ≤ i < #o^{∗}) Value(o^{∗}(i), s)

Value(v, s)  ⟺ v = ⟨fixnum n⟩ or v = ⟨immediate imm⟩

or S(v, s) is defined

2.2.3 States

The states of a microcoded sbc state machine (msbcm) are the sequences of the form

⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ that satisfy the following (msbcm) state invariants:

1. s is an msbc store

2. Template(t, s)

3. Codevector(c, s)

4. S(t, s) = ⟨template #f c::o^{∗}⟩ for some o^{∗}.

5. Offset(n, t, s)

6. Value(v, s)

7. Environment(u, s)

8. Continuation(k, s)

9. (∀0 ≤ i < #a) Value(a(i), s) The components of a state are called, in order, its template, offset, codevector, value, argument stack, environment, continuation, store, spare1, spare2, spare3, and spare4, and we may informally speak of them as being held in registers. The first three state invariants ensure that the store is an msbc store. The remaining invariants restrict the values of the register components of states. For example, the register t is restricted to hold pointers to templates (i.e., stored objects with header tag template).

Note that the msbcm state invariants are the same as the sbcm state invariants. 2.2.4 Initial and Halt States The initial states of the msbcm are the states ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ such that

• n = 0,

• v = ⟨immediate unspecified⟩,

• a = ⟨⟩,

• u = ⟨immediate empty-env⟩,

• k = ⟨immediate halt⟩, and • s(1) = s(2) = s(3) = ⟨⟩.

The halt states of the msbcm are the states ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ such that for some b^{∗},

• S(c, s) = ⟨codevector #f b^{∗}⟩,

• b^{∗}(n) = return, and

• k = ⟨immediate halt⟩.

2.2.5 State Observers and Mutators

We shall implement the action rules of the msbcm as the composition of functions drawn from a small set of functions (called microcode functions). Microcode functions are classified into two categories. Microcode functions that map msbcm states to non-state values are called (msbcm) observers since they only observe the state and do not mutate it. Microcode functions that map msbcm states to msbcm states are called (msbcm) mutators. msbcm observers are specified in Figure 2 and msbcm mutators are specified in Figures 3 and 4.

2.2.6 Stored Object Manipulators

In Figures 2, 3, and 4 we specified a collection of microcode functions. These functions were classified into register, stack, stored object, and miscellaneous functions. In this section, we specify a fairly large collection of auxiliary functions that will be used to manipulate stored objects in an msbcm store. These auxiliary functions (called stored object manipulators) are implemented in terms of the microcode functions; their primary purpose is to abstract away from representation details of how stored objects are represented in the store. The msbcm action rules will be implemented in terms of the register and stack microcode functions, the stored object manipulators, and other miscellaneous auxiliary functions. As with the microcode functions, we distinguish between stored object manipulators on the basis of their being observers or mutators.

For each stored object observer we give names to the function and its arguments, one or more conditions determining when the function is defined (and possibly introducing new locally bound variables for later use), a specification of the value returned by the function, and an “implementation” of the function in terms of microcode observers and other auxiliary functions.

Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be an msbcm state. Then, Register Observers

template-ref Σ  = t
codevector-ref Σ  = c
offset-ref Σ  = n
value-ref Σ  = v
env-ref Σ  = u
cont-ref Σ  = k
spare1-ref Σ  = r_{1}
spare2-ref Σ  = r_{2}
spare3-ref Σ  = r_{3}
spare4-ref Σ  = r_{4}

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 −_{A} 1) = ⟨h p m⟩. Let S(d, s) = ⟨h p o^{∗}⟩. Then

stob-desc-ref d i Σ  = o^{∗}(i)  if h ∈ dhtag
stob-byte-ref d i Σ  = o^{∗}(i)  if h ∈ bhtag

stob-tag d Σ  = h
stob-mutable? d Σ  = p
stob-size-in-bytes d Σ  = m
stob-size-in-cells d Σ  = ℧m

Figure 2: msbcm State Observers.

Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be an msbcm state. Then, Register Mutators

template-set vd Σ = Σ[t′ = vd]  if Template(vd)
codevector-set vd Σ = Σ[c′ = vd]  if Codevector(vd)
offset-set i Σ  = Σ[n′ = i]  if Offset(i, t, s)
offset-inc i Σ  = Σ[n′ = n + i]  if Offset(n + i, t, s)
value-set vd Σ  = Σ[v′ = vd]  if Value(vd)
env-set vd Σ  = Σ[u′ = vd]  if Environment(vd)
cont-set vd Σ  = Σ[k′ = vd]  if Continuation(vd)
spare1-set vd Σ  = Σ[r′_{1} = vd]
spare2-set vd Σ  = Σ[r′_{2} = vd]
spare3-set i Σ  = Σ[r′_{3} = i]
spare4-set d Σ  = Σ[r′_{4} = d]

Stack Mutators

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

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

Miscellaneous Mutators

assert p Σ  = if p then Σ else abort

Figure 3: msbcm State Mutators.

Stored Object Mutators

make-desc-stob h p m Σ = Σ\begin{matrix}[s′ = s ⊕_{0} ⟨h p m⟩] \\ [r′_{1} = ⟨0, #s(0)⟩] \end{matrix}

if h ∈ dhtag

make-desc-stob-from-stack h p Σ

= Σ\begin{matrix}[s′ = s +_{1} ⟨h p a⟩] \\ [a′ = ⟨⟩] \\ [r′_{1} = ⟨1, −#s(1) − #a + 1⟩] \end{matrix}

if h ∈ dhtag

make-byte-stob h p m Σ = Σ\begin{matrix}[s′ = s ⊕_{0} ⟨h p m⟩] \\ [r′_{1} = ⟨0, #s(0)⟩] \end{matrix}

if h ∈ bhtag

Let d = ⟨ptr l⟩ and S(d, s) = ⟨h p o^{∗}⟩. Then

stob-desc-set d i vd Σ = Σ[s′ = s[(l +_{A} i) ↦ vd]]

if h ∈ dhtag and 0 ≤ i < #o^{∗}

stob-byte-set d i b Σ  = Σ[s′ = s[(l +_{A} i′) ↦ b^{∗}]]

if h ∈ bhtag and 0 ≤ i < #o^{∗} and i′ = ℧(i + 1) − 1 and b^{∗} = s(l +_{A} i′)[(i mod bpw) ↦ b]

Figure 4: msbcm State Mutators (continued).

For each stored object mutator we give names to the function and its arguments, one or more conditions determining when the function is defined (and possibly introducing new locally bound variables for later use), a specification of the new values of some registers, and an “implementation” of the function in terms of microcode mutators and other auxiliary functions.

Often the domain of a stored object manipulator is specified by equations giving “the form” of certain registers or values. In all specifications, the original values of the various registers are designated by conventional variables used exactly as in the definition of a state: t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, and r_{4}. Call these the original register variables. In specifications of stored object mutators, the new values of the registers are indicated by the same variables with primes attached: t′, n′, c′, v′, a′, u′, k′, s′, r′_{1}, r′_{2}, r′_{3}, and r′_{4}. Call these the new register variables. New register variables occur only as the left hand sides of equations specifying 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 function arguments, and may introduce new variables (not among the function arguments or 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 + 12 places

(†) R(t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}, x_{1}, …, x_{j}).

The domain condition really is this: the rule can be applied in a given state if there exist x_{1}, …, x_{j} such that (†). Furthermore, in the value and 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.

The “implementation” of the action rules expresses each rule as the composition of stored object manipulators, microcode functions, and other auxiliary functions. The implementation is expressed as a Scheme program. Note that Scheme is a call-by-value language that implicitly threads the global state through function calls; hence the global state does not appear as an explicit parameter.

Function: make-closure-stob! Domain conditions:

Changes:

s′ = s ⊕_{0} ⟨closure #f 2⟩

Implementation:

(make-desc-stob! hdr/closure #f 2)

Function: closure-stob? d Domain conditions: Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨closure #f ⟨d_{0} d_{1}⟩⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/closure))

Function: closure-stob-template d Domain conditions:

S(d, s) = ⟨closure #f ⟨d_{0} d_{1}⟩⟩

Return value:

d_{0}

Implementation:

(stob-desc-ref d 0)

Function: closure-stob-env d Domain conditions:

S(d, s) = ⟨closure #f ⟨d_{0} d_{1}⟩⟩

Return value:

d_{1}

Implementation:

(stob-desc-ref d 1)

Function: closure-stob-template-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨closure #f ⟨d_{0} d_{1}⟩⟩

Changes:

s′ = s[l ↦ val]

Implementation:

(stob-desc-set! d 0 val)

Function: closure-stob-env-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨closure #f ⟨d_{0} d_{1}⟩⟩

Changes:

s′ = s[l +_{A} 1 ↦ val]

Implementation:

(stob-desc-set! d 1 val)

Function: make-codevector-stob! m Domain conditions: Changes:

s′ = s ⊕_{0} ⟨codevector #f m⟩

Implementation:

(make-desc-stob! hdr/codevector #f m)

Function: codevector-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨codevector #f b^{∗}⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/codevector))

Function: codevector-stob-length d Domain conditions:

S(d, s) = ⟨codevector #f b^{∗}⟩

Return value:

#b^{∗}

Implementation:

(stob-size-in-bins d)

Function: codevector-stob-ref d i Domain conditions:

S(d, s) = ⟨codevector #f b^{∗}⟩

0 ≤ i < #b^{∗}

Return value:

b^{∗}(i)

Implementation:

(stob-binarray-ref d i)

Function: codevector-stob-init! d i b Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨codevector #f b^{∗}⟩

0 ≤ i < #b^{∗}
i′ = ℧(i + 1) − 1

b^{′∗} = s(l +_{A} i′)[(i mod bpw) ↦ b]

Changes:

s′ = s[(l +_{A} i′) ↦ b^{′∗}]

Implementation:

(stob-binarray-set! d i b)

Function: make-continuation-stob! Domain conditions:

Changes:

s′ = s +_{1} ⟨continuation #f a⟩

Implementation:

(make-desc-stob-from-stack! hdr/continuation #f)

Function: continuation-stob? d Domain conditions:

Return value:

#t if d = ⟨immediate halt⟩
#t if d = ⟨ptr l⟩

and S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

#f otherwise

Implementation:

(or (= d halt)
    (and (pointer? d) (= (stob-type d) hdr/continuation)))

Function: continuation-stob-template d Domain conditions:

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Return value:

d_{0}

Implementation:

(stob-desc-ref d 0)

Function: continuation-stob-offset d Domain conditions:

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Return value:

d_{1}

Implementation:

(stob-desc-ref d 1)

Function: continuation-stob-env d Domain conditions:

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Return value:

d_{2}

Implementation:

(stob-desc-ref d 2)

Function: continuation-stob-cont d Domain conditions:

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Return value:

d_{3}

Implementation:

(stob-desc-ref d 3)

Function: continuation-stob-template-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Changes:

s′ = s[l ↦ val]

Implementation:

(stob-desc-set! d 0 val)

Function: continuation-stob-offset-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Changes:

s′ = s[l +_{A} 1 ↦ val]

Implementation:

(stob-desc-set! d 1 val)

Function: continuation-stob-env-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Changes:

s′ = s[l +_{A} 2 ↦ val]

Implementation:

(stob-desc-set! d 2 val)

Function: continuation-stob-cont-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨continuation #f ⟨d_{0} d_{1} d_{2} d_{3}⟩^{⌢} d_{4}^{∗}⟩

Changes:

s′ = s[l +_{A} 3 ↦ val]

Implementation:

(stob-desc-set! d 3 val)

Function: make-environment-stob! Domain conditions: Changes:

s′ = s +_{1} ⟨environment #t a⟩

Implementation:

(make-desc-stob-from-stack! hdr/environment #t)

Function: environment-stob? d Domain conditions: Return value:

#t if d = ⟨immediate empty-env⟩
#t if d = ⟨ptr l⟩ and S(d, s) = ⟨environment #t v^{∗}⟩
#f otherwise

Implementation:

(or (= d emptyenv)
    (and (pointer? d) (= (stob-type d) hdr/environment)))

Function: environment-stob-length d Domain conditions:

S(d, s) = ⟨environment #t v^{∗}⟩

Return value:

#v^{∗}

Implementation:

(stob-size-in-cells d)

Function: environment-stob-parent d Domain conditions:

S(d, s) = ⟨environment #t v^{∗}⟩

Return value:

v^{∗}(0)

Implementation:

(stob-desc-ref d 0)

Function: environment-stob-ref d i Domain conditions:

S(d, s) = ⟨environment #t v^{∗}⟩

1 ≤ i < #v^{∗}

Return value:

v^{∗}(i)

Implementation:

(stob-desc-ref d i)

Function: environment-stob-set! d i val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨environment #t v^{∗}⟩

1 ≤ i < #v^{∗}

Changes:

s′ = s[l +_{A} i ↦ val]

Implementation:

(stob-desc-set! d i val)

Function: make-location-stob! Domain conditions:

Changes:

s′ = s ⊕_{0} ⟨location #t 2⟩

Implementation:

(make-desc-stob! hdr/location #t 2)

Function: location-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨location #t ⟨d_{0} d_{1}⟩⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/location))

Function: location-stob-value d Domain conditions:

S(d, s) = ⟨location #t ⟨d_{0} d_{1}⟩⟩

Return value:

d_{0}

Implementation:

(stob-desc-ref d 0)

Function: location-stob-name d Domain conditions:

S(d, s) = ⟨location #t ⟨d_{0} d_{1}⟩⟩

Return value:

d_{1} Implementation:

(stob-desc-ref d 1)

Function: location-stob-value-set! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨location #t ⟨d_{0} d_{1}⟩⟩

Changes:

s′ = s[l ↦ val]

Implementation:

(stob-desc-set! d 0 val)

Function: make-mutable-pair-stob! Domain conditions: Changes:

s′ = s ⊕_{0} ⟨pair #t 2⟩

Implementation:

(make-desc-stob! hdr/pair #t 2)

Function: make-immutable-pair-stob! Domain conditions: Changes:

s′ = s ⊕_{0} ⟨pair #f 2⟩

Implementation:

(make-desc-stob! hdr/pair #f 2)

Function: pair-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨pair p ⟨d_{0} d_{1}⟩⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/pair))

Function: pair-stob-fst d Domain conditions:

S(d, s) = ⟨pair p ⟨d_{0} d_{1}⟩⟩

Return value:

d_{0}

Implementation:

(stob-desc-ref d 0)

Function: pair-stob-snd d Domain conditions:

S(d, s) = ⟨pair p ⟨d_{0} d_{1}⟩⟩

Return value:

d_{1}

Implementation:

(stob-desc-ref d 1)

Function: pair-stob-fst-set! d val Domain conditions:

\begin{matrix}d = ⟨ptr l⟩ \\ S(d, s) = ⟨pair #t ⟨d_{0} d_{1}⟩⟩ \end{matrix}

Changes:

s′ = s[l ↦ val]

Implementation:

(stob-desc-set! d 0 val)

Function: pair-stob-snd-set! d val Domain conditions:

\begin{matrix}d = ⟨ptr l⟩ \\ S(d, s) = ⟨pair #t ⟨d_{0} d_{1}⟩⟩ \end{matrix}

Changes:

s′ = s[l +_{A} 1 ↦ val]

Implementation:

(stob-desc-set! d 1 val)

Function: make-immutable-string-stob! m Domain conditions: Changes:

s′ = s ⊕_{0} ⟨string #f m⟩

Implementation:

(make-desc-stob! hdr/string #f m)

Function: make-mutable-string-stob! m Domain conditions: Changes:

s′ = s ⊕_{0} ⟨string #t m⟩

Implementation:

(make-desc-stob! hdr/string #t m)

Function: string-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨string p b^{∗}⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/string))

Function: string-stob-length d Domain conditions:

S(d, s) = ⟨string p b^{∗}⟩

Return value:

#b^{∗}

Implementation:

(stob-size-in-bins d)

Function: string-stob-ref d i Domain conditions:

\begin{matrix}S(d, s) = ⟨string p b^{∗}⟩ \\ 0 ≤ i < (#b^{∗} − 1) \end{matrix}

Return value:

b^{∗}(i)

Implementation:

(char->immediate (integer->char (stob-binarray-ref d i)))

Function: string-stob-set! d i c Domain conditions: d = ⟨ptr l⟩ S(d, s) = ⟨string #t b^{∗}⟩ 0 ≤ i < (#b^{∗} − 1) c = ⟨immediate ⟨char b⟩⟩ i′ = ℧(i + 1) − 1 b^{′∗} = s(l +_{A} i′)[(i mod bpw) ↦ b]

Changes:

s′ = s[(l +_{A} i′) ↦ b^{′∗}]

Implementation:

(stob-binarray-set! d i (char->integer (immediate->char c)))

Function: make-symbol-stob! Domain conditions:

Changes:

s′ = s ⊕_{0} ⟨symbol #f 1⟩

Implementation:

(make-desc-stob! hdr/symbol #f 1)

Function: symbol-stob-name-init! d val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨symbol #f ⟨v⟩⟩

Changes:

s′ = s[l ↦ val]

Implementation:

(stob-desc-set! d 0 val)

Function: symbol-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨symbol #f ⟨v⟩⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/symbol))

Function: symbol-stob-name d Domain conditions:

S(d, s) = ⟨symbol #f ⟨v⟩⟩

Return value:

v

Implementation:

(stob-desc-ref d 0)

Function: make-template-stob! m Domain conditions: Changes:

s′ = s ⊕_{0} ⟨template #f m⟩

Implementation:

(make-desc-stob! hdr/template #f m)

Function: template-stob? d Domain conditions: Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨template #f v^{∗}⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/template))

Function: template-stob-length d Domain conditions:

S(d, s) = ⟨template #f v^{∗}⟩

Return value:

#v^{∗}

Implementation:

(stob-size-in-cells d)

Function: template-stob-codevector d Domain conditions:

S(d, s) = ⟨template #f v^{∗}⟩

Return value:

v^{∗}(0)

Implementation:

(stob-desc-ref d 0)

Function: template-stob-ref d i Domain conditions:

S(d, s) = ⟨template #f v^{∗}⟩

1 ≤ i < #v^{∗}

Return value:

v^{∗}(i)

Implementation:

(stob-desc-ref d i)

Function: template-stob-init! d i val Domain conditions:

d = ⟨ptr l⟩
S(d, s) = ⟨template #f v^{∗}⟩
0 ≤ i < #v^{∗}

Changes:

s′ = s[l +_{A} i ↦ val]

Implementation:

(stob-desc-set! d i val)

Function: make-mutable-vector-stob! m Domain conditions:

Changes:

s′ = s ⊕_{0} ⟨vector #t m⟩

Implementation:

(make-desc-stob! hdr/vector #t m)

Function: make-immutable-vector-stob! m Domain conditions:

Changes:

s′ = s ⊕_{0} ⟨vector #f m⟩

Implementation:

(make-desc-stob! hdr/vector #f m)

Function: vector-stob? d Domain conditions:

Return value:

#t if d = ⟨ptr l⟩ and S(d, s) = ⟨vector p v^{∗}⟩
#f otherwise

Implementation:

(and (pointer? d) (= (stob-type d) hdr/vector))

Function: vector-stob-length d Domain conditions:

S(d, s) = ⟨vector p v^{∗}⟩

Return value:

#v^{∗}

Implementation:

(stob-size-in-cells d)

Function: vector-stob-ref d i Domain conditions:

\begin{matrix}S(d, s) = ⟨vector p v^{∗}⟩ \\ 0 ≤ i < #v^{∗} \end{matrix}

Return value:

v^{∗}(i)

Implementation:

(stob-desc-ref d i)

Function: vector-stob-set! d i val Domain conditions:

d = ⟨ptr l⟩

S(d, s) = ⟨vector #t v^{∗}⟩

0 ≤ i < #v^{∗}

Changes:

s′ = s[l +_{A} i ↦ val]

Implementation:

(stob-desc-set! d i val)

2.2.7 Miscellaneous Auxiliary Functions

Before presenting the action rules, we present several auxiliary functions.

The function env-frame(u, n, s) returns the environment that is nested n levels deep within the environment pointed to by u in store s.

env-frame(u, 0, s) = u, and
env-frame(u, n + 1, s) = env-frame(u′, n, s) if S(u, s) = ⟨environment #t u′::vd^{∗}⟩

The function stack-to-list(lp, n, a, s) pops the first n values of a stack a and stores them as a linked list in store s. The tail of this linked list is the list pointed to by lp in store s. The function returns a pointer to the new linked list, together with the modified stack and store.

stack-to-list(lp, 0, a, s) = ⟨lp a s⟩, and stack-to-list(lp, n + 1, a, s) =

stack-to-list(⟨ptr ⟨0 #s_{0} + 1⟩⟩, n, a † 1, s +_{0} ⟨pair #f ⟨a(0) lp⟩⟩)

The function list-to-stack(p, a, s) returns the stack a′ ^{⌢} a, where a′ is the stack represented by the linked list pointed to by p in store s.

list-to-stack(⟨immediate null⟩, a, s) = a, and list-to-stack(p, a, s) = list-to-stack(p′, v :: a, s) if S(p, s) = ⟨pair p ⟨v p′⟩⟩

The function compute-offset takes two integers and returns an integer representing an offset they are together encoding. For 0 ≤ n_{0}, n_{1},

compute-offset(n_{0}, n_{1}) = (256 ∗ n_{0}) + n_{1}.

We will usually write n_{0} ⊗ n_{1} for compute-offset(n_{0}, n_{1}).

2.2.8 Action Rules

We present actions as the union of subfunctions called (action) rules. The action rules are functions from pairwise disjoint subsets of states × inputs × outputs into states × inputs × outputs where states is the set of sbcm states, and inputs and outputs are sets of finite sequences of characters. Since the domains of these functions are disjoint, the union of these functions is a partial function from states × inputs × outputs into states × inputs × outputs. We denote this function by R.

Let Σ, i^{∗}, and o^{∗} be a state, input sequence, and output sequence respectively. The value of the function R at ⟨Σ, i^{∗}, o^{∗}⟩ only depends on Σ and possibly on the first element of i^{∗}. Let R(⟨Σ, i^{∗}, o^{∗}⟩) = ⟨Σ′, i^{′∗}, o^{′∗}⟩. Then, one of the following hold:

• The input and output sequences are unchanged, i.e., i^{′∗} = i^{∗} and o^{′∗} = o^{∗}. We call such rules pure rules.

• The rule drops the first element of the argument input sequence, i.e., i^{′∗} = i^{∗} † 1 and o^{′∗} = o^{∗}. We call such rules input port rules.

• The rule appends a sequence of values to the argument output sequence, i.e., i^{′∗} = i^{∗} and o^{′∗} = o^{∗} ^{⌢} o^{′′∗}. We call such rules output port rules.

We define a function R^{∗} as follows:

R^{∗} =^{def} R^{∗}(R(⟨Σ, i^{∗}, o^{∗}⟩)) if R(⟨Σ, i^{∗}, o^{∗}⟩) is defined
⟨Σ, i^{∗}, o^{∗}⟩  otherwise

If, when started in state ⟨Σ, i^{∗}, o^{∗}⟩, the state machine halts, then R^{∗}(⟨Σ, i^{∗}, o^{∗}⟩) is defined and is the state the machine halts in. Otherwise, R^{∗}(⟨Σ, i^{∗}, o^{∗}⟩) is undefined.

We present the definition of the action rules below. We also present an “implementation” of the action rules of the msbcm, with the state transformations of the action rules being specified as the composition of several microcode functions.

We modify the presentation format for pure action rules that is described in the VLISP Flattener report [2]. For each pure 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), a specification of the new values of some registers, and an “implementation” of the rule. 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, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, and r_{4}. Call these the original register variables. The new values of the registers are indicated by the same variables with primes attached: t′, n′, c′, v′, a′, u′, k′, s′, r′_{1}, r′_{2}, r′_{3}, and r′_{4}. Call these the new register variables. New register variables occur only as the left hand sides of equations specifying new register values. Registers for which no new value is given are tacitly asserted to remain unchanged. Input and output must both be null. We use the two auxiliary functions defined below. Let S(c, s) = ⟨codevector #f b^{∗}⟩. Then,

current inst(n, c, s) =^{def} b^{∗}(n)  if 0 ≤ n < #b^{∗}
current inst param(n, i, c, s) =^{def} b^{∗}(n + i) if 0 ≤ n + i < #b^{∗}

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 + 12 places

(†) R(t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}, x_{1}, …, x_{j}).

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

The “implementation” of the action rules expresses each rule as the composition of stored object manipulators, microcode functions, and other auxiliary functions. The implementation is expressed as a Scheme program. Note that Scheme is a call-by-value language that implicitly threads the global state through function calls; hence the global state does not appear as an explicit parameter.

Rule 1: return Domain conditions:

current inst(n, c, s) = return k = halt

Changes:

Halt in final state Σ

Implementation:

(if (= (cont-ref) halt)
    (halt!)
    (begin
      (spare2-set! (cont-ref))
      (template-set! (continuation-stob-template (spare2-ref)))

(codevector-set! (template-stob-codevector (template-ref)))
(offset-set! (fixnum->int
              (continuation-stob-offset (spare2-ref))))
(env-set! (continuation-stob-env (spare2-ref)))
(cont-set! (continuation-stob-cont (spare2-ref)))
(stack-restore! (spare2-ref))
))

Rule 2: return Domain conditions:

current inst(n, c, s) = return

S(k, s) = ⟨continuation #f ⟨t_{1} n_{1} u_{1} k_{1}⟩^{⌢} a_{1}⟩ S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩ n_{1} = ⟨fixnum m⟩

Changes:

t′ = t_{1}

n′ = m

c′ = c_{1}

a′ = a_{1}

u′ = u_{1}

k′ = k_{1}

r′_{2} = k

Implementation:

(if (= (cont-ref) halt)
(halt!)
(begin
(spare2-set! (cont-ref))
(template-set! (continuation-stob-template (spare2-ref)))
(codevector-set! (template-stob-codevector (template-ref)))
(offset-set! (fixnum->int
              (continuation-stob-offset (spare2-ref))))
(env-set! (continuation-stob-env (spare2-ref)))
(cont-set! (continuation-stob-cont (spare2-ref)))
(stack-restore! (spare2-ref))
))

Rule 3: call m Domain conditions: current inst(n, c, s) = call current inst param(n, 1, c, s) = m S(v, s) = ⟨closure #f ⟨t_{1} u_{1} d_{1}⟩⟩ S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩

Changes:

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

Implementation:

(assert! (closure-stob? (value-ref))
 "op/call: value register does not contain a closure")
(template-set! (closure-stob-template (value-ref)))
(env-set! (closure-stob-env (value-ref)))
(codevector-set! (template-stob-codevector (template-ref)))
(offset-set! 0)

Rule 4: jump-if-false m_{1} m_{2} Domain conditions:

current inst(n, c, s) = jump-if-false current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} v ≠ ⟨immediate false⟩

Changes:

n′ = n + 3

Implementation:

(if (= (value-ref) false)
(offset-inc! (+ 3 (compute-offset (current-inst-param 1)
                              (current-inst-param 2))))
(offset-inc! 3))

Rule 5: jump-if-false m_{1} m_{2} Domain conditions: current inst(n, c, s) = jump-if-false current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} v = ⟨immediate false⟩

Changes:

n′ = n + 3 + (m_{1} ⊗ m_{2})

Implementation:

(if (= (value-ref) false)
(offset-inc! (+ 3 (compute-offset (current-inst-param 1)
                              (current-inst-param 2))))
(offset-inc! 3))

Rule 6: jump m_{1} m_{2} Domain conditions:

current inst(n, c, s) = jump current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2}

Changes:

n′ = n + 3 + (m_{1} ⊗ m_{2})

Implementation:

(offset-inc! (+ 3 (compute-offset (current-inst-param 1)
                          (current-inst-param 2))))

Rule 7: make-cont m_{1} m_{2} m_{3} Domain conditions:

current inst(n, c, s) = make-cont current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} current inst param(n, 3, c, s) = m_{3} m = n + 4 + (m_{1} ⊗ m_{2})

Changes:

n′ = n + 4
a′ = ⟨⟩
k′ = ⟨ptr ⟨1 − #s − #a − 3⟩⟩

s′ = s +_{1} ⟨continuation #f ⟨t ⟨fixnum m⟩ u k⟩^{⌢} a⟩

r′_{1} = ⟨ptr ⟨1 − #s − #a − 3⟩⟩

Implementation:

(stack-push! (cont-ref))
(stack-push! (env-ref))
(stack-push! (int->fixnum
              (+ (offset-ref) 4
                 (compute-offset (current-inst-param 1)
                                 (current-inst-param 2)))))
(stack-push! (template-ref))
(make-continuation-stob!)
(cont-set! (spare1-ref))
(offset-inc! 4)

Rule 8: literal m Domain conditions:

current inst(n, c, s) = literal current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m)

Changes:

\begin{matrix}n′ = n + 2 \\ v′ = o_{m} \end{matrix}

Implementation:

(assert! (in-bounds? (current-inst-param 1)
                     1 (template-stob-length (template-ref)))
         "op/literal: index is outside template bounds")
(value-set! (template-stob-ref (template-ref)
                               (current-inst-param 1)))
(offset-inc! 2)

Rule 9: closure m Domain conditions: current inst(n, c, s) = closure current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) S(o_{m}, s) = ⟨template #f c_{1}::o_{1}^{∗}⟩

Changes:

n′ = n + 2 v′ = ⟨ptr ⟨0 (#s_{0} + 1)⟩⟩ s′ = s +_{0} ⟨closure #f ⟨o_{m} u ⟨immediate unspecified⟩⟩⟩ r′_{1} = ⟨ptr ⟨0 (#s_{0} + 1)⟩⟩ r′_{2} = o_{m}

Implementation:

(assert! (in-bounds? (current-inst-param 1)
             1 (template-stob-length (template-ref)))
 "op/closure: index is outside template bounds")
(make-closure-stob!)
(spare2-set! (template-stob-ref (template-ref)
                        (current-inst-param 1)))
(assert! (template-stob? (spare2-ref))
 "op/closure: indexed datum is not a template stob")
(closure-stob-template-init! (spare1-ref) (spare2-ref))
(closure-stob-env-init! (spare1-ref) (env-ref))
(value-set! (spare1-ref))
(offset-inc! 2)

Rule 10: global m Domain conditions:

current inst(n, c, s) = global current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) S(o_{m}, s) = ⟨location #t ⟨v_{1} x⟩⟩ v_{1} ≠ ⟨immediate undefined⟩

Changes:

\begin{matrix}n′ = n + 2 \\ v′ = v_{1} \\ r′_{2} = o_{m} \end{matrix}

Implementation:

(assert! (in-bounds? (current-inst-param 1)
                     1 (template-stob-length (template-ref)))
 "op/global: index is outside template bounds")
(spare2-set! (template-stob-ref (template-ref)
                                (current-inst-param 1)))
(assert! (location-stob? (spare2-ref))
         "op/global: indexed datum is not a location stob")
(value-set! (location-stob-value (spare2-ref)))
(assert! (not (immediate-undefined? (value-ref)))
         "op/global: location's value is undefined")
(offset-inc! 2)

Rule 11: set-global! m Domain conditions:

current inst(n, c, s) = set-global! current inst param(n, 1, c, s) = m S(t, s) = ⟨template #f c::o^{∗}⟩ 1 ≤ m < (#o^{∗} + 1) o_{m} = (c::o^{∗})(m) = ⟨ptr l⟩ S(o_{m}, s) = ⟨location #t ⟨v_{1} x⟩⟩

Changes:

n′ = n + 2 s′ = s[l ↦ v] v′ = ⟨immediate unspecified⟩ r′_{2} = o_{m}

Implementation:

(assert! (in-bounds? (current-inst-param 1)
                     1 (template-stob-length (template-ref)))
         "op/set-global!: index is outside template bounds")
(spare2-set! (template-stob-ref (template-ref)
                                (current-inst-param 1)))
(assert! (location-stob? (spare2-ref))
         "op/set-global!: indexed datum is not a location stob")
(location-stob-value-set! (spare2-ref) (value-ref))

(value-set! unspecified)
(offset-inc! 2)

Rule 12: local m_{1} m_{2} Domain conditions:

current inst(n, c, s) = local current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} u_{1} = env-frame(u, m_{1}, s) S(u_{1}, s) = ⟨environment #t u_{2}::vd^{∗}⟩ v_{1} = (u_{2}::vd^{∗})(m_{2}) v_{1} ≠ ⟨immediate undefined⟩

Changes:

\begin{matrix}n′ = n + 3 \\ v′ = v_{1} \end{matrix}

Implementation:

(value-set! (environment-stob-ref
     (env-frame! (env-ref) (current-inst-param 1))
     (current-inst-param 2)))
(assert! (not (immediate-undefined? (value-ref)))
 "op/local: indexed local variable has undefined value")
(offset-inc! 3)

Rule 13: set-local! m_{1} m_{2} Domain conditions:

current inst(n, c, s) = set-local! current inst param(n, 1, c, s) = m_{1} current inst param(n, 2, c, s) = m_{2} u_{1} = env-frame(u, m_{1}, s) = ⟨ptr l_{1}⟩ S(u_{1}, s) = ⟨environment #t u_{2}::vd^{∗}⟩ l = l_{1} + m_{2}

Changes:

n′ = n + 3 v′ = ⟨immediate unspecified⟩ s′ = s[l ↦ v]

Implementation:

(environment-stob-set!
 (env-frame! (env-ref) (current-inst-param 1))
 (current-inst-param 2)
 (value-ref))
(value-set! unspecified)
(offset-inc! 3)

Rule 14: push Domain conditions:

current inst(n, c, s) = push

Changes:

\begin{matrix}n′ = n + 1 \\ a′ = v::a \end{matrix}

Implementation:

(stack-push! (value-ref))
(offset-inc! 1)

Rule 15: make-env m Domain conditions:

current inst(n, c, s) = make-env current inst param(n, 1, c, s) = m m = #a

Changes:

n′ = n + 2
a′ = ⟨⟩

u′ = ⟨ptr ⟨1 − #s − #a⟩⟩

s′ = s +_{1} ⟨environment #t u::a⟩r′_{1} = ⟨ptr ⟨1 − #s − #a⟩⟩

Implementation:

(stack-push! (env-ref))
(make-environment-stob)
(offset-inc! 2)
(env-set! (spare1-ref))

Rule 16: make-rest-list m Domain conditions: current inst(n, c, s) = make-rest-list current inst param(n, 1, c, s) = m #a ≥ m ⟨v_{1} a_{1} s_{1}⟩ = stack-to-list(⟨immediate null⟩, (#a − m), a, s)

Changes:

n′ = n + 2 v′ = v_{1} a′ = a_{1} s′ = s_{1} r′_{1} = if (#a − m) = 0 then r_{1} else v_{1} r′_{2} = v_{1} r′_{3} = 0

Implementation:

(let ((m (current-inst-param 1)))
(assert! (>= (stack-length) m)
"op/make-rest-list: argument is larger than stack size")
(spare3-set! (- (stack-length) m))
(spare2-set! null)
(let loop ()
(if (= (spare3-ref) 0)
(begin
(value-set! (spare2-ref))
(offset-inc! 2))
(begin
(make-mutable-pair-stob!)
(pair-stob-fst-set! (spare1-ref) (stack-top))
(stack-pop!)
(pair-stob-snd-set! (spare1-ref) (spare2-ref))
(spare2-set! (spare1-ref))
(spare3-set! (- (spare3-ref) 1))
(loop))
)))

Rule 17: unspecified Domain conditions:

current inst(n, c, s) = unspecified

Changes:

n′ = n + 1 v′ = ⟨immediate unspecified⟩ Implementation:

(value-set! unspecified)
(offset-inc! 1)

Rule 18: check-args= m Domain conditions:

current inst(n, c, s) = check-args= current inst param(n, 1, c, s) = m #a = m

Changes:

n′ = n + 2

Implementation:

(assert! (= (stack-length) (current-inst-param 1))
         "op/check-args=: Incorrect number of arguments.")
(offset-inc! 2)

Rule 19: check-args>= m Domain conditions:

current inst(n, c, s) = check-args>= current inst param(n, 1, c, s) = m #a ≥ m

Changes:

n′ = n + 2

Implementation:

(assert! (>= (stack-length) (current-inst-param 1))
         "op/check-args>=: Incorrect number of arguments.")
(offset-inc! 2)

Rule 20: primitive-throw Domain conditions: current inst(n, c, s) = primitive-throw S(v, s) = ⟨continuation #f ⟨t_{1} n_{1} u_{1} k_{1}⟩^{⌢} a_{1}⟩

Changes:

\begin{matrix}n′ = n + 1 \\ k′ = v \end{matrix}

Implementation:

(assert! (continuation-stob? (value-ref))
         "op/primitive-throw: value is not a continuation")
(cont-set! (value-ref))
(offset-inc! 1)

2.3 SBC Operational Semantics

We first define a function load that maps sbc stores to msbc stores. An sbc store is represented as the first store segment within an msbc store, and all sbc pointers within the sbc store are mapped to corresponding msbc pointers. Let s^{sbc} be an sbc store. Then

relocate(cell) =^{def} ⟨ptr ⟨0 m⟩⟩ if cell = ⟨ptr m⟩ cell otherwise

load(s^{sbc}) =^{def} ⟨s_{0} ⟨⟩ ⟨⟩ ⟨⟩⟩ \begin{matrix}where #s_{0} = #s^{sbc} \\ and for all 0 ≤ m < #s_{0} \\ s_{0}(m) = relocate(s^{sbc}(m)) \end{matrix}

The msbcm Loader L_{msbcm} is defined to be a function that maps sbc programs to msbcm initial states such that:

L_{msbcm}(⟨s^{sbc} t^{sbc}⟩) =^{def} ⟨t, 0, c, d_{u}, ⟨⟩, ⟨immediate empty-env⟩,
⟨immediate halt⟩, s, d_{u}, d_{u}, 0, d_{u}⟩

if s = load(s^{sbc}) and t = relocate(t^{sbc}) and S(t, s) = ⟨template #f c::o^{∗}⟩ and d_{u} = ⟨immediate unspecified⟩.

Note that sbcm initial states are msbc terms, and hence the loader involves coercing sbc terms to msbc terms. We can easily show that the loader maps sbc programs to msbcm initial states:

Lemma 6 If P^{sbc} = ⟨s^{sbc} t^{sbc}⟩ is an sbc program, then L_{msbcm}(P^{sbc}) is an initial msbcm state.

Proof: Let L_{msbcm}(⟨s^{sbc} t^{sbc}⟩) be defined as above. All conditions for it to be an initial msbcm state are trivial except for the conditions that s be an msbc store and t be a pointer to a template object in s.

By definition of s, if s(l) is defined for some l, then l has the form ⟨0, m⟩ for some 0 ≤ m < #s^{sbc}, and further s(l) = relocate(s^{sbc}(l)). Since P^{sbc} is an sbc program, we have by definition that s^{sbc} is an sbc store. Using these facts, it is trivial to show that s is an msbc store.

Since P^{sbc} is an sbc program, we have by definition that t^{sbc} is a pointer to a template object in s^{sbc}. Then it is trivial to show that t = relocate(t^{sbc}) is a pointer to a template object in s.

□

The msbcm Answer A_{msbcm} is defined to be a partial function that maps msbcm halt states to integers such that:

A_{msbcm}(⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩) =^{def} m  if v = ⟨fixnum m⟩

Definition 7 Let P be an sbc program. Then L_{msbcm}(P) is an initial state of the msbcm. If R_{msbcm}^{∗}(L_{msbcm}(P)) is defined, then the meaning of program P as given by the sbc operational semantics is

O_{msbcm}[[P]] =^{def} A_{msbcm}(R_{msbcm}^{∗}(L_{msbcm}(P)))

Otherwise O_{msbcm}[[P]] is undefined.

Theorem 8 If p is an sbc program, then its operational semantics as given by the sbcm yields the same answer as its operational semantics as given by the msbcm. That is,

O_{sbcm}[[p]] = O_{msbcm}[[p]]

Proof: The loader function L_{msbcm} is an extension of the function L_{sbcm} and differs only in the values it assigns the temporary registers r_{1}, r_{2}, r_{3}, and r_{4}. The action rules of the msbcm are defined as extensions of the action rules of the sbcm, and differ only in the values of the temporary registers r_{1}, r_{2}, r_{3}, and r_{4}. The answer functions A_{sbcm} and A_{msbcm} do not depend on the values of the temporary registers. Since the operational semantics is defined as the composition of these three functions, it follows that the two semantics are equivalent.

□

Theorem 9 The implementation of the action rules of the msbcm is correct with respect to the specification of the action rules.

Proof: This follows immediately from the definitions of the action rules, stored object manipulators, microcode functions, and auxiliary functions. In this report, we only present the proof for an example action rule. The proof is very simple, and suggests that the interested reader can verify the correctness of the other rules by perusal. A detailed examination of the correctness of the other action rules has been carried out. A manuscript presenting detailed proofs for (earlier versions) of the action rules is available.

Rule 21: call m Domain conditions:

current inst(n, c, s) = call

current inst param(n, 1, c, s) = m S(v, s) = ⟨closure #f ⟨t_{1} u_{1} d_{1}⟩⟩ S(t_{1}, s) = ⟨template #f c_{1}::o^{∗}⟩

Changes:

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

Implementation:

(assert! (closure-stob? (value-ref))
         "op/call: value register does not contain a closure")
(template-set! (closure-stob-template (value-ref)))
(env-set! (closure-stob-env (value-ref)))
(codevector-set! (template-stob-codevector (template-ref)))
(offset-set! 0)

Let Σ be an msbcm state such that the above domain conditions hold. We rewrite the implementation to make the global state explicit, and simultaneously verify the implementation.

Σ_{1} = (assert!  (closure-stob?  (value-ref Σ) Σ)

         "op/call:  value register does not contain a closure")

Σ_{2} = (template-set!

           (closure-stob-template (value-ref Σ_{1}) Σ_{1}) Σ_{1})

Σ_{3} = (env-set!  (closure-stob-env (value-ref Σ_{2}) Σ_{2}) Σ_{2})
Σ_{4} = (codevector-set!

           (template-stob-codevector (template-ref Σ_{3}) Σ_{3}) Σ_{3})

Σ_{5} = (offset-set!  0 Σ_{4})

From the definitions of the above functions, we have that:

Σ_{1} = Σ
Σ_{2} = Σ_{1}[t′ = t_{1}]
Σ_{3} = Σ_{2}[u′ = u_{1}]
Σ_{4} = Σ_{3}[c′ = c_{1}]
Σ_{5} = Σ_{4}[n′ = 0]

Thus, Σ_{5} = Σ[t′ = t_{1}][u′ = u_{1}][c′ = c_{1}][n′ = 0] as desired. The other rules are verified similarly.

□

2.4 State Correspondence Relation

If ≃ is a four-place relation, we write (s^{S}, s ⊢ x^{S} ≃ x) to mean that (s^{S}, x^{S}, s, x) is in the relation ≃.

Let s^{S} be a sbcm store. Then

ldom(s^{S}) =^{def} dom(s^{S})

is the set of sbcm locations l^{S} such that s^{S}(l^{S}) is defined.

Let s be an msbcm store. Then

ldom(s) =^{def} {⟨i m⟩ | 0 ≤ i < 4 ∧ m ∈ dom(s(i))}

is the set of msbcm locations l such that s(l) is defined.

Definition 10 A location correspondence ≃_{0} ⊆ (s^{S} × l^{S}) × (s × l) is defined to be a relation such that for all s^{S}, s, the set {(l^{S}, l) | (s^{S}, s ⊢ l^{S} ≃_{0} l)} is a 1-to-1 map from a subset of ldom(s^{S}) to a subset of ldom(s). Further, if (s^{S}, s ⊢ l^{S} ≃_{0} l) then s^{S}(l^{S}) and s(l) are not headers.

Definition 11 Let ≃_{0} ⊆ (s^{S} ×l^{S})×(s×l) be a location correspondence. A term correspondence ≃ ⊆ (s^{S} × cell^{S}) × (s × cell) induced by ≃_{0} is defined as follows:

(s^{S}, s ⊢ cell^{S} ≃ cell) holds if one of the following hold:

• 1. cell^{S} = ⟨ptr l^{S}⟩

2. cell = ⟨ptr l⟩

3. s^{S}(l^{S} − 1) = ⟨header h^{S} p^{S} m^{S}⟩

4. s(l −_{A} 1) = ⟨header h p m⟩

5. h^{S} = h

6. p^{S} = p

7. m^{S} = m

8. for all 0 ≤ i < ℧m, (s^{S}, s ⊢ (l^{S} + i) ≃_{0} (l +_{A} i))

• cell^{S} = ⟨fixnum m⟩ = cell

• cell^{S} = imm = cell

• cell^{S} = b^{∗} = cell Definition 12 Let Σ_{sbcm} = ⟨t^{S}, n^{S}, c^{S}, v^{S}, a^{S}, u^{S}, k^{S}, s^{S}⟩ be an sbcm state and let Σ_{msbcm} = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be an msbcm state. The state correspondence relation ≅ ⊂ state^{S} × state is defined as follows:

Σ_{sbcm} ≅ Σ_{msbcm}

if there exists a location correspondence ≃_{0} and a term correspondence ≃ induced by ≃_{0} such that

• for all l^{S} ∈ ldom(s^{S}) and l ∈ ldom(s),

(s^{S}, s ⊢ l^{S} ≃_{0} l) ⇒ (s^{S}, s ⊢ s^{S}(l^{S}) ≃ s(l))

• (s^{S}, s ⊢ t^{S} ≃ t)

• n^{S} = n

• (s^{S}, s ⊢ v^{S} ≃ v)

• #a^{S} = #a and (∀0 ≤ i < #a)(s^{S}, s ⊢ a^{S}(i) ≃ a(i))

• (s^{S}, s ⊢ u^{S} ≃ u)

• (s^{S}, s ⊢ k^{S} ≃ k)

2.5 Establishing State Correspondence

Let d_{u} =^{def} ⟨immediate unspecified⟩. The sbcm Loader, L_{sbcm}, is a function that maps sbc programs to sbcm initial states and is defined as follows:

L_{sbcm}(⟨s^{sbc} t^{sbc}⟩) =^{def} ⟨t^{sbc}, 0, c^{S}, d_{u}, ⟨⟩, ⟨immediate empty-env⟩,
⟨immediate halt⟩, s^{sbc}⟩
if S(t^{sbc}, s^{sbc}) = ⟨template #f c^{S}::o^{∗}⟩.

The msbcm Loader, L_{msbcm}, is a function that maps sbc programs to msbcm initial states and is defined as follows:

L_{msbcm}(⟨s^{sbc} t^{sbc}⟩) =^{def} ⟨t, 0, c, d_{u}, ⟨⟩, ⟨immediate empty-env⟩,
⟨immediate halt⟩, s, d_{u}, d_{u}, 0, d_{u}⟩
if s = load(s^{sbc}) and t = relocate(t^{sbc})
and S(t, s) = ⟨template #f c::o^{∗}⟩.

where load and relocate are as defined in Section 2.3.

Lemma 13 The sbcm Loader and the msbcm Loader map sbc programs to initial states that are related by the state correspondence relation. That is, if P is an sbc program, then

L_{sbcm}(P) ≅ L_{msbcm}(P)

Proof: Let

\begin{matrix}L_{sbcm}(P) = ⟨t^{S}, n^{S}, c^{S}, v^{S}, a^{S}, u^{S}, k^{S}, s^{S}⟩ \\ L_{msbcm}(P) = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ \end{matrix}

Let the location correspondence ≃_{0} be defined as follows:

(s^{S}, s ⊢ m ≃_{0} ⟨0, m⟩) if 0 ≤ m < #s^{S} and s^{S}(m)(0) ≠ header

Let ≃ be the term correspondence induced by ≃_{0}.

Now, by definition of a term correspondence (Definition 11), we have that for all m, imm, and b^{∗},

(s^{S}, s ⊢ ⟨fixnum m⟩ ≃ ⟨fixnum m⟩),
(s^{S}, s ⊢ imm ≃ imm), and
(s^{S}, s ⊢ b^{∗} ≃ b^{∗})

Let l^{S} < #s^{S} be such that s^{S}(l^{S} − 1) = ⟨header h^{S} p^{S} m^{S}⟩ for some h^{S}, p^{S}, m^{S}. Since s^{S} is an sbcm store, s^{S}(l^{S} + i) is not a header for all 0 ≤ i < ℧m^{S}. Let l = ⟨0, l^{S}⟩. By definition of the msbcm loader, s(l−_{A}1) = ⟨header h^{S} p^{S} m^{S}⟩. Also, by definition of ≃_{0} above, we have that for all 0 ≤ i < ℧m, (s^{S}, s ⊢ (l^{S} + i) ≃_{0} (l +_{A} i)). Then, by definition of a term correspondence (Definition 11), we have that

(s^{S}, s ⊢ ⟨ptr l^{S}⟩ ≃ ⟨ptr l⟩)

It is now straightforward to show from the definition of state correspondence (Definition 12) that ≃_{0} and ≃ are witness to the state correspondence:

L_{sbcm}(P) ≅ L_{msbcm}(P)

□

2.6 Preserving State Correspondence

We prove that each action rule preserves state correspondence. That is, if Σ^{S} and Σ are corresponding sbcm and msbcm states, then an sbcm action rule maps Σ^{S} to a state Σ^{′S} if and only if an msbcm action rule maps Σ to a state Σ′; furthermore, the states Σ^{′S} and Σ′ correspond.

The following lemma will be used extensively in the proof. The lemma states that if corresponding values are stored in corresponding (or new) locations of stores in corresponding states, then the resulting states also correspond.

Lemma 14 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let Σ^{S} = ⟨t^{S}, n^{S}, v^{S}, a^{S}, u^{S}, k^{S}, s^{S}⟩ and Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be corresponding states of the sbcm and msbcm respectively, i.e., Σ^{S} ≅ Σ with witnesses ≃_{0} and ≃.

Let e^{S}, e be corresponding terms, i.e., (s^{S}, s ⊢ e^{S} ≃ e). Let l^{S}, l either be corresponding locations or new locations, i.e., either (s^{S}, s ⊢ l^{S} ≃_{0} l) or else l^{S} = #s^{S} and l = #s. Let s^{′S} = s^{S}[l^{S} ↦ e^{S}] and s′ = s[l ↦ e].

Let ≃′_{0} be a location correspondence such that for all l_{1}^{S}, l_{1}, (s^{′S}, s′ ⊢ l_{1}^{S} ≃′_{0} l_{1}) holds if and only if either (s^{S}, s ⊢ l_{1}^{S} ≃_{0} l_{1}) holds or else l_{1}^{S} = l^{S} and l_{1} = l. Let ≃′ be the term correspondence induced by ≃′_{0}.

Then,

1. for all cell^{S}, cell,

(s^{S}, s ⊢ cell^{S} ≃ cell) ⇒ (s^{′S}, s′ ⊢ cell^{S} ≃′ cell)

2. for all l^{S} ∈ ldom(s^{′S}) and l ∈ ldom(s′)

(s^{′S}, s′ ⊢ l^{S} ≃′_{0} l) ⇒ (s^{′S}, s′ ⊢ s^{′S}(l^{S}) ≃′ s′(l))

3. ⟨t^{S}, n^{S}, v^{S}, a^{S}, u^{S}, k^{S}, s^{′S}⟩ ≅ ⟨t, n, c, v, a, u, k, s′, r_{1}, r_{2}, r_{3}, r_{4}⟩ with witnesses ≃′_{0} and ≃′.

Proof:

1. If (s^{S}, s ⊢ l^{S} ≃_{0} l), we have from definition 10 that s^{S}(l^{S}) and s(l) are not headers. By inspection, we see that the definition of a term correspondence relation does not depend on the contents of such locations. Thus modifying the contents of the locations l^{S} and l does not affect the term correspondence relation ≃, hence the result.

Otherwise, l^{S} and l are new locations. Now, ≃ and ≃′ are induced (from the same set of monotonic closure rules) by ≃_{0} and ≃′_{0} respectively. But, by definition of ≃′_{0}, for all l_{1}^{S}, l_{1}, (s^{S}, s ⊢ l_{1}^{S} ≃_{0} l_{1}) implies (s^{′S}, s′ ⊢ l_{1}^{S} ≃′_{0} l_{1}). The result thus follows.

2. Let l_{1}^{S} ∈ ldom(s^{′S}), l_{1} ∈ ldom(s′), and (s^{′S}, s′ ⊢ l_{1}^{S} ≃′_{0} l_{1}). The proof is by cases:

Case (l_{1}^{S} ≠ l^{S}) and (l_{1} ≠ l):

(s^{′S}, s′ ⊢ l_{1}^{S} ≃′_{0} l_{1})  by assumption
⇒ (s^{S}, s ⊢ l_{1}^{S} ≃_{0} l_{1})  by definition of ≃′_{0}

and case condition

⇒ (s^{S}, s ⊢ s^{S}(l_{1}^{S}) ≃ s(l_{1}))  since Σ^{S} ≅ Σ
⇒ (s^{′S}, s′ ⊢ s^{S}(l_{1}^{S}) ≃′ s(l_{1})) by part 1 of this lemma
⇒ (s^{′S}, s′ ⊢ s^{′S}(l_{1}^{S}) ≃′ s′(l_{1})) by case condition and

definitions of s^{′S} and s′

Case (l_{1}^{S} = l^{S}) and (l_{1} = l):

(s^{S}, s ⊢ e^{S} ≃ e)  by assumption
⇒ (s^{′S}, s′ ⊢ e^{S} ≃′ e)  by part 1 of this lemma
⇒ (s^{′S}, s′ ⊢ s^{′S}(l^{S}) ≃′ s′(l)) by definition of s^{′S} and s′
⇒ (s^{′S}, s′ ⊢ s^{′S}(l_{1}^{S}) ≃′ s′(l_{1})) by case condition

There are no other cases by definition of ≃′_{0} (since ≃_{0} and ≃′_{0} are injective on locations and (s^{S}, s ⊢ l^{S} ≃_{0} l)).

3. Follows trivially from Definition 12 and parts (1) and (2) of this lemma.

□

Lemma 15 Let Σ^{S} and Σ be corresponding sbcm and msbcm states. Then an sbcm action rule maps Σ^{S} to a state Σ^{′S} if and only if an msbcm action rule maps Σ to a state Σ′; furthermore, the states Σ^{′S} and Σ′ correspond.

Proof: We prove this in the following subsections by considering each action rule in turn. The following rules have identical definition forms as in the sbcm(except for changes made to the spare registers r_{1}, r_{2}, r_{3}, and

r_{4}): return, call, jump-if-false, jump, literal, global, set-global!,

local, set-local!, push, unspecified, check-args=, check-args>=, and

primitive-throw. Their proof is trivial and is omitted from this report.

The proofs for the remaining four rules (make-cont, make-closure, make-env, and make-rest-list) are similar. We present the proof for make-cont as a representative proof.

Rule: make-cont m_{1} m_{2} m_{3}

Changes:

Σ^{′S} = Σ^{S}[a^{′S} = ⟨⟩] [k^{′S} = ⟨ptr #s^{S} + 1⟩] [s^{′S} = s^{S} > ⟨continuation ⟨t^{S} ⟨fixnum m^{S}⟩ u^{S} k^{S}⟩^{⌢} a^{S}⟩] [n^{′S} = n^{S} + 4] [r_{1}^{′S} = ⟨ptr #s^{S} + 1⟩]

where m^{S} = n^{S} + 4 + (m_{1} ⊗ m_{2})
Σ′ = Σ[a′ = ⟨⟩] [k′ = ⟨ptr ⟨1 − #s(1) − #a − 3⟩⟩] [s′ = s +_{1} ⟨continuation #f ⟨t ⟨fixnum m⟩ u k⟩^{⌢} a⟩] [n′ = n + 4] [r′_{1} = ⟨ptr ⟨1 − #s(1) − #a − 3⟩⟩]

where m = n + 4 + (m_{1} ⊗ m_{2})

Proof Obligations: Let ≃_{0} and ≃ be the location and term correspondences that are witnesses to the state correspondence Σ^{S} ≅ Σ. Let ≃′_{0} be a new location correspondence such that for all locations l_{1}^{S}, l_{1}, (s^{′S}, s′ ⊢ l_{1}^{S} ≃′_{0} l_{1}) holds if either (s^{S}, s ⊢ l_{1}^{S} ≃_{0} l_{1}) holds, or if l_{1}^{S} = #s^{S} + i and l_{1} = ⟨1, −#s(1) − #a − 4) +_{A} i⟩ for some 1 ≤ i < #a^{S} + 5. Let ≃′ be the term correspondence induced by ≃_{0} (by Definition 11). We show that ≃′_{0} and ≃′ are witness to the state correspondence Σ^{′S} ≅ Σ′.

Since Σ^{S} ≅ Σ, we have that

(s^{S}, s ⊢ t^{S} ≃ t)
m^{S} = m
(s^{S}, s ⊢ u^{S} ≃ u)
(s^{S}, s ⊢ k^{S} ≃ k)
(s^{S}, s ⊢ a^{S}(i) ≃ a(i)) for all 0 ≤ i < #a

Now, since

s^{′S} = s^{S} > ⟨continuation #f ⟨t^{S} ⟨fixnum m^{S}⟩ u^{S} k^{S}⟩^{⌢} a^{S}⟩
s′ = s +_{1} ⟨continuation #f ⟨t ⟨fixnum m⟩ u k⟩^{⌢} a⟩

we can use Lemma 14 in proving the obligations.

1. for all l_{1}^{S} ∈ ldom(s^{′S}) and l_{1} ∈ ldom(s′),

(s^{′S}, s′ ⊢ l_{1}^{L} ≃′ l_{1}) ⇒ (s^{′S}, s′ ⊢ s^{′L}(l_{1}^{S}) ≃′ s′(l_{1})) This follows from Lemma 14.

2. (s^{′S}, s′ ⊢ t^{L} ≃′ t) which follows from Lemma 14.

3. n^{′S} = n′ where n^{′S} = n^{S} + 4 and n′ = n + 4; this holds since n^{S} = n by the assumption that Σ^{S} ≅ Σ.

4. (s^{′S}, s′ ⊢ v^{L} ≃′ v) which follows from Lemma 14.

5. #a^{′S} = #a′ and (∀0 ≤ i < #a′)(s^{′S}, s′ ⊢ a^{′L}(i) ≃′ a′(i)) which holds trivially since a^{′S} = a′ = ⟨⟩.

6. (s^{′S}, s′ ⊢ u^{L} ≃′ u) which follows from Lemma 14.

7. (s^{′S}, s′ ⊢ k^{′L} ≃′ k′) where k^{′S} = ⟨ptr #s^{S} + 1⟩ and k′ = ⟨ptr ⟨1 − #s(1) − #a − 3⟩⟩. Now S(k^{′S}, s^{′S}) = ⟨continuation #f ⟨t^{S} ⟨fixnum m^{S}⟩ u^{S} k^{S}⟩^{⌢} a^{S}⟩ and S(k′, s′) = ⟨continuation #f ⟨t ⟨fixnum m⟩ u k⟩ ^{⌢} a⟩ by Lemma 5. The result then follows from Lemma 14 since Σ′ ≅ Σ.

□

2.7 Correspondence of Final Answers

The following lemma asserts that the sbcm and msbcm answer functions map corresponding states to equal natural numbers. Lemma 16 Let Σ_{f}^{S} and Σ_{f} be sbcm and msbcm halt states respectively. If Σ_{f}^{S} ≅ Σ_{f}, then A_{sbcm}(Σ_{f}^{S}) = A_{msbcm}(Σ_{f}).

Proof: Let v^{S} and v be the value registers of Σ_{f}^{S} and Σ_{f} respectively. Since Σ_{f}^{S} ≅ Σ_{f}, we have by definition of state correspondence that v^{S} and v are related (i.e. (s^{S}, s ⊢ v^{S} ≃ v)). By definition of term correspondence, if v^{S} = ⟨fixnum m⟩ then v = ⟨fixnum m⟩ and so A_{sbcm}(Σ_{f}^{S}) = A_{msbcm}(Σ_{f}) = m. If v^{S} is not of the form ⟨fixnum m⟩ then neither is v, and so A_{sbcm}(Σ_{f}^{S}) and A_{msbcm}(Σ_{f}) are both undefined.

□

2.8 Correspondence of Semantics

We can now prove the main theorem of this chapter.

Theorem 17 If P is an sbc program, then its operational semantics as given by the sbcm yields the same answer as its operational semantics as given by the msbcm. That is,

O_{sbcm}^{sbc}[[P]] = O_{msbcm}^{sbc}[[P]]

Proof: Follows immediately from Lemmas 13, 15, and 16.

□

3 Garbage-collected SBC State Machine

In this chapter, we give Stored Byte Code (sbc) programs an (operational) semantics in terms of a deterministic state machine with concrete states. The state machine is called the Garbage-collected Stored Byte Code Machine (gsbcm). We show that this operational semantics is equivalent to the operational semantics in terms of the msbcm.

This chapter presents:

1. an operational semantics of sbc programs in terms of a state machine called the Garbage-collected Stored Byte Code Machine (gsbcm).

2. a correspondence relation that relates msbcm states and gsbcm states;

3. a proof that the msbcm loader and the gsbcm loader map sbc programs to initial states that are related by the above correspondence relation.

4. a proof that the msbcm and gsbcm action rules preserve state correspondence. That is, if an msbcm state is related to a gsbcm state, then either the msbcm and gsbcm action rules are both undefined on the respective states, or else they map the respective related states to states that are also related.

A crucial ingredient of this proof is a proof that if an msbcm state is related to a gsbcm state, then the function garbage-collect maps the gsbcm state to a state that is also related to the msbcm state.

5. a proof that the msbcm and gsbcm answer functions map related states to equal numbers.

6. a proof that the operational semantics of sbc as given by the msbcm is extensionally equal to the operational semantics of sbc as given by the gsbcm.

3.1 GSBC State Machine (GSBCM)

3.1.1 States

The states of the gsbcm are those of the msbcm. The initial and halt states of the gsbcm are also those of the msbcm.

3.1.2 Garbage Collection Algorithm

(define (pointer-to-old-space? p)
(and (pointer? p)
     (let ((a (pointer->addr p)))
       (and (not (addr< a *old-low-heap-base*))
            (addr< a *old-high-heap-limit*)
            ))))
(define (gc-convert! ret p)
(let ((h (stob-header p)))
  (cond ((pointer? h) (ret h))
        ((header? h)
         (nh-alloc! h (addr+ *hp* (+ (header-size-in-cells h)
                                     1)))
         (heap-set! (pointer->addr p) -1 (spare1-ref))
         (do ((src (pointer->addr p) (addr+ src 1))
              (dst (pointer->addr (spare1-ref)) (addr+ dst 1))
              (ret ret)
              )
             ((addr= dst *hp*) (ret (spare1-ref)))
           (heap-set! dst 0 (heap-ref src 0))))
        (else (error!
               "gc-trace: invalid heap structure during gc"))
        )))
(define (gc-trace! ret p)
(if (pointer? p)
    (gc-convert! ret p)
    (ret p)
    ))
(define *stack-scan* *old-stack-base*)
(define (gc-trace-stack!)
(set! *stack-scan* (addr+ *old-stack-base* -1))
(do-gc-trace-stack!))
(define (do-gc-trace-stack!)
(if (addr< *stack-scan* *old-sp*)
    (ret8)
    (gc-trace! ret-gc-trace-stack! (stack-ref *stack-scan*))
    ))
(define (ret-gc-trace-stack! val)
(stack-push! val)
(set! *stack-scan* (addr+ *stack-scan* -1))
(do-gc-trace-stack!))

(define *scan* heap-low)
(define (gc-scan-heap!)
(if (addr< *scan* *hp*)
    (let ((desc (heap-ref *scan* 0)))
      (cond ((pointer-to-old-space? desc)
              (gc-convert! ret-gc-scan-heap! desc))
            ((and (header? desc)
                  (binarray-header-tag? (header-tag desc)))
             (set! *scan*
                   (addr+ *scan* (+ (header-size-in-cells desc)
                                    1)))
             (gc-scan-heap!))
            (else
             (set! *scan* (addr+ *scan* 1))
             (gc-scan-heap!))))
    (ret9)))
(define (ret-gc-scan-heap! val)
(heap-set! *scan* 0 val)
(set! *scan* (addr+ *scan* 1))
(gc-scan-heap!))
(define *gc-ret-address* (lambda () 0))
(define (garbage-collect! ret)
(set! *gc-ret-address* ret)
(if noisy-vm
    (begin
      (write "[Garbage Collecting ..." (current-output-port))
      (force-output (current-output-port))))

;;; Flip

(set! *old-low-heap-base* *low-heap-base*)
(set! *old-hp* *hp*)
(set! *old-sp* *sp*)
(set! *old-stack-base* *stack-base*)
(set! *old-low-heap-limit* *low-heap-limit*)
(set! *old-high-heap-limit* *high-heap-limit*)
(if (addr= *low-heap-base* heap-low)
    (begin
      (set! *low-heap-base* heap-mid)
      (set! *stack-base* heap-high)
      (set! *high-heap-limit* heap-high))
    (begin
      (set! *low-heap-base* heap-low)

      (set! *stack-base* heap-mid)
      (set! *high-heap-limit* heap-mid)))
(set! *hp* *low-heap-base*)
(set! *sp* *stack-base*)
(set! *low-heap-limit*
      (addr+ *stack-base* (- stack-size-in-words)))
(set! *scan* *hp*)
(gc-trace! ret1 (template-ref))  )
(define (ret1 val)
(template-set! val)
(gc-trace! ret2 (value-ref)) )
(define (ret2 val)
(value-set! val)
(gc-trace! ret3 (env-ref)) )
(define (ret3 val)
(env-set! val)
(gc-trace! ret4 (cont-ref)) )
(define (ret4 val)
(cont-set! val)
(gc-trace! ret6 (spare2-ref)) )
(define (ret6 val)
(spare2-set! val)
(gc-trace! ret7 (symbol-table-ref)) )
(define (ret7 val)
(symbol-table-set! val)
(gc-trace-stack!))
(define (ret8)
(gc-scan-heap!))
(define (ret9)
(codevector-set! (template-stob-codevector (template-ref)))
(let ((free (quotient (* (addr- *sp* *hp*) 100)
                      heap-space-size-in-words)))
  (if noisy-vm
      (begin
        (write " done; " (current-output-port))
        (write-int free (current-output-port))
        (write "% free]" (current-output-port))
        (newline (current-output-port))))
  (assert! (> free 10)
           "Only 10% free after garbage collection."))
(*gc-ret-address*))

3.1.3 State Observers and Mutators

The gsbcm state observer and mutator functions are defined as the corresponding msbcm state observer and mutator functions, except for three mutator functions which are defined as follows:

Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let

Σ′ = if C then Σ else garbage-collect(Σ)

where C is some unspecified boolean condition and the function garbagecollect is a partial function from gsbcm states to gsbcm states and is defined in Section 3.1.2. Then,

make-desc-stob h p m Σ = Σ′\begin{matrix}[s′ = s ⊕_{0} ⟨h p m⟩] \\ [r′_{1} = ⟨0, #s(0)⟩] \end{matrix}
if h ∈ dhtag

     make-desc-stob-from-stack h p Σ

= Σ′\begin{matrix}[s′ = s +_{1} ⟨h p a⟩] \\ [a′ = ⟨⟩] \\ [r′_{1} = ⟨1, −#s(1) − #a + 1⟩] \end{matrix}

if h ∈ dhtag
make-byte-stob h p m Σ = Σ′\begin{matrix}[s′ = s ⊕_{0} ⟨h p m⟩] \\ [r′_{1} = ⟨0, #s(0)⟩] \end{matrix}
if h ∈ bhtag

3.1.4 Action Rules

In Section 2.2.8, we specified the action rules of the msbcm as the composition of stored object manipulators, microcode functions, and other auxiliary functions. The action rules of the gsbcm are given identical definition forms. Note, however, that since two gsbcm mutator functions differ from the corresponding msbcm functions, the extensions of the gsbcm action rules are not the same as the extensions of the corresponding msbcm action rules.

3.2 SBC Operational Semantics

The gsbcm Loader L_{gsbcm} is defined to be a function that maps sbc programs to gsbcm initial states such that:

L_{gsbcm}(⟨s^{sbc} t^{sbc}⟩) =^{def} L_{msbcm}(⟨s^{sbc} t^{sbc}⟩)

The gsbcm Answer A_{gsbcm} is defined to be a partial function that maps gsbcm halt states Σ_{gsbcm}^{f} to natural numbers such that

A_{gsbcm}(Σ_{gsbcm}^{f}) =^{def} A_{msbcm}(Σ_{gsbcm}^{f})

Definition 18 Let P be an sbc program. Then L_{gsbcm}(P) is an initial state of the gsbcm. If R_{gsbcm}^{∗}(L_{gsbcm}(P)) is defined, then the meaning of program P as given by the sbc operational semantics is

O_{gsbcm}[[P]] =^{def} A_{gsbcm}(R_{gsbcm}^{∗}(L_{gsbcm}(P)))

Otherwise O_{gsbcm}[[P]] is undefined.

3.3 State Correspondence Relation

We express the relation between msbcm and gsbcm states via a state correspondence relation. Our approach is inspired by Wand and Oliva’s storage relations [6].

If ≃ is a four-place relation, we write (s^{M}, s ⊢ x^{M} ≃ x) to mean that (s^{M}, x^{M}, s, x) is in the relation ≃.

Let s be an msbcm (or gsbcm) store. Then

ldom(s) =^{def} {⟨i, m⟩ | 0 ≤ i < 4 ∧ m ∈ dom(s(i))}

is the set of all locations l such that s(l) is defined.

Definition 19 A location correspondence ≃_{0} ⊆ (s^{M} ×l^{M})×(s×l) is defined to be a relation such that for all s^{M}, s, the set {(l^{M}, l) | (s^{M}, s ⊢ l^{M} ≃_{0} l)} is a 1-to-1 map from a subset of ldom(s^{M}) to a subset of ldom(s). Further, if (s^{M}, s ⊢ l^{M} ≃_{0} l) holds, then s^{M}(l^{M}) and s(l) are not headers.

Definition 20 Let ≃_{0} ⊆ (s^{M} × l^{M}) × (s × l) be a location correspondence. A term correspondence ≃ ⊆ (s^{M} ×cell^{M})×(s×cell) induced by ≃_{0} is defined as follows:

(s^{M}, s ⊢ cell^{M} ≃ cell) holds if one of the following hold:

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

3. s^{M}(l^{M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩

4. s(l −_{A} 1) = ⟨header h p m⟩ 5. h^{M} = h

6. p^{M} = p

7. m^{M} = m

8. for all 0 ≤ i < ℧m, (s^{M}, s ⊢ (l^{M} +_{A} i) ≃_{0} (l +_{A} i))

• cell^{M} = ⟨fixnum m⟩ = cell

• cell^{M} = imm = cell

• cell^{M} = b^{∗} = cell Definition 21 Let

\begin{matrix}Σ_{msbcm} = ⟨t^{M}, n^{M}, c^{M}, v^{M}, a^{M}, u^{M}, k^{M}, s^{M}, r_{1}^{M}, r_{2}^{M}, r_{3}^{M}, r_{4}^{M}⟩, and \\ Σ_{gsbcm} = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ \end{matrix}

be msbcm and gsbcm states respectively. The state correspondence relation ≅ ⊂ state^{M} × state is defined as follows:

Σ_{msbcm} ≅ Σ_{gsbcm}

if there exists a location correspondence ≃_{0} and a term correspondence ≃ induced by ≃_{0} such that

• for all l^{M} ∈ ldom(s^{M}) and l ∈ ldom(s),

(s^{M}, s ⊢ l^{M} ≃_{0} l) ⇒ (s^{M}, s ⊢ s^{M}(l^{M}) ≃ s(l))

• (s^{M}, s ⊢ t^{M} ≃ t)

• n^{M} = n

• (s^{M}, s ⊢ v^{M} ≃ v)

• #a^{M} = #a and (∀0 ≤ i < #a)(s^{M}, s ⊢ a^{M}(i) ≃ a(i))

• (s^{M}, s ⊢ u^{M} ≃ u)

• (s^{M}, s ⊢ k^{M} ≃ k)

• (s^{M}, s ⊢ r_{2}^{M} ≃ r_{2})

• r_{3}^{M} = r_{3}

• r_{4}^{M} = r_{4} Lemma 22 ≅ is a transitive relation, i.e., if Σ ≅ Σ′ and Σ′ ≅ Σ′′ then Σ ≅ Σ′′.

Proof: Follows trivially, since the location and term correspondence relations ≃_{0} and ≃ are easily seen to be transitive.

□

3.4 Establishing State Correspondence

Let d_{u} =^{def} ⟨immediate unspecified⟩. Then, the msbcm and gsbcm loaders, L_{msbcm} and L_{gsbcm}, are partial functions defined as follows:

L_{msbcm}(⟨s^{sbc} t^{sbc}⟩) = L_{gsbcm}(⟨s^{sbc} t^{sbc}⟩)
=^{def} ⟨t, 0, c, d_{u}, ⟨⟩, ⟨immediate empty-env⟩,
⟨immediate halt⟩, s, d_{u}, d_{u}, 0, d_{u}⟩
if s = load(s^{sbc}) and t = relocate(t^{sbc})
and S(t, s) = ⟨template #f c::o^{∗}⟩.

Lemma 23 The msbcm Loader and the gsbcm Loader map sbc programs to initial states that are related by the state correspondence relation. That is, if P is an sbc program, then

L_{msbcm}(P) ≅ L_{gsbcm}(P)

Proof: Let L_{msbcm}(P) = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ = L_{gsbcm}(P) (since the two loaders are equal by definition). Let the location correspondence ≃_{0} be defined as follows:

(s, s ⊢ ⟨0, m⟩ ≃_{0} ⟨0, m⟩) if 0 ≤ m < #s(0) and s(⟨0, m⟩) is not a header

Let ≃ be the term correspondence induced by ≃_{0}.

Now, by definition of a term correspondence (Definition 20), we have that for all m, imm, and b^{∗},

(s, s ⊢ ⟨fixnum m⟩ ≃ ⟨fixnum m⟩),
(s, s ⊢ imm ≃ imm), and
(s, s ⊢ b^{∗} ≃ b^{∗})

Let l ∈ ldom(s) be such that S(⟨ptr l⟩, s) is defined. Then, s(l −_{A} 1) = ⟨header h p m⟩ for some h, p, m. Since s is an msbcm store, s(l +_{A} i) is not a header for all 0 ≤ i < ℧m. Thus, by definition of ≃_{0} above, we have that for all 0 ≤ i < ℧m, (s^{M}, s ⊢ (l +_{A} i) ≃_{0} (l +_{A} i)). Then, by definition of a term correspondence (Definition 20), we have that

(s, s ⊢ ⟨ptr l⟩ ≃ ⟨ptr l⟩)

It then follows immediately from the definition of state correspondence (Definition 21) that ≃_{0} and ≃ are witness to the state correspondence:

L_{msbcm}(P) ≅ L_{gsbcm}(P)

□

3.5 Preserving State Correspondence

3.5.1 Garbage Collection

We define a binary predicate on gsbcm states and show that gsbcm states Σ and garbage-collect(Σ) are related. We use this to show that if an msbcm state Σ^{M} is related to a gsbcm state Σ by the state correspondence relation, then Σ^{M} is also related to garbage-collect(Σ).

Let gc-header-size-in-cells be a function defined as follows:

gc-header-size-in-cells(d, s) = ℧m if d = ⟨header h p m⟩

or d = ⟨ptr l⟩ and s(l −_{A} 1) = ⟨header h p m⟩

Let gc-header be a predicate defined as follows:

• For i ∈ {0, 2}, if s(⟨i, 0⟩) is defined then gc-header(⟨i, 0⟩, s) holds;

• For i ∈ {1, 3}, if s(⟨i, −#s_{i} + 1⟩) is defined then gc-header(⟨i, −#s_{i} + 1⟩, s) holds;

• For all l, if

gc-header(l, s),

gc-header-size-in-cells(s(l), s), and

s(l +_{A} (gc-header-size-in-cells(s(l), s) + 1))

are defined, then

gc-header(l +_{A} (gc-header-size-in-cells(s(l), s) +_{A} 1), s)

holds.

Definition 24 A gc store is a store that satisfies the following conditions:

1. If gc-header(l, s) then either (a) s(l) is a header, or

(b) s(l) = ⟨ptr l′⟩, s(l′ −_{A} 1) is a header, and l has the form ⟨0, m⟩

or ⟨1, m⟩ while l′ has the form ⟨2, n⟩.

2. If gc-header(l, s) then for all 1 ≤ x < ℧m • If h ∈ bhtag, then s(l +_{A} x) = b^{bpw} for some b^{bpw}.

• If h ∈ bhtag, then s(l +_{A} x) = vd for some vd. where either s(l) = ⟨header h p m⟩ or s(l) = ⟨ptr l′⟩ and s(l′) = ⟨header h p m⟩.

3. For all l, l′, if s(l) = ⟨ptr l′⟩ then gc-header(l′ −_{A} 1, s) holds. Definition 25 A gc state is a sequence of the form

⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩

that satisfies the following state invariants:

1. s is a gc store

2. Template(t, s)

3. Offset(n, t, s)

4. Value(v, s)

5. Environment(u, s)

6. Continuation(k, s)

7. (∀0 ≤ i < #a) Value(a(i), s) Lemma 26 Every gsbcm store is a gc store, and every gsbcm state is a gc state. Proof: Follows trivially from the definitions, since the invariants satisfied by gc stores are weaker than those satisfied by gsbcm stores.

□

Definition 27 A gc location correspondence ≃_{0} ⊆ (s×l)×(s×l) is defined to be a relation such that for all s, s′, the set {(l, l′) | (s^{M}, s ⊢ l ≃_{0} l′)} is a 1-to-1 map from a subset of ldom(s) to a subset of ldom(s′). Further, if (s^{M}, s ⊢ l ≃_{0} l′) holds, then s(l) and s′(l′) are not headers.

Definition 28 Let ≃_{0}^{gc} ⊆ (s × l) × (s × l) be a gc location correspondence. A gc term correspondence ≃^{gc} ⊆ (s × cell) × (s × cell) induced by ≃_{0} is defined as follows:

(s, s′ ⊢ cell_{1} ≃^{gc} cell_{2}) holds if one of the following hold:

• 1. cell_{1} = ⟨ptr l_{1}⟩ 2. cell_{2} = ⟨ptr l_{2}⟩

3. (l_{1} = l′)∧(s(l′−_{A}1) = ⟨header h p m⟩) or s(l_{1}−_{A}1) = ⟨ptr l′⟩∧ (s(l′ −_{A} 1) = ⟨header h p m⟩)

4. (l_{2} = l′)∧(s(l′−_{A}1) = ⟨header h p m⟩) or s(l_{2}−_{A}1) = ⟨ptr l′⟩∧ (s(l′ −_{A} 1) = ⟨header h p m⟩)

5. h = h

6. p = p

7. m = m

8. for all 0 ≤ i < ℧m, (s, s′ ⊢ (l′ +_{A} i) ≃_{0}^{gc} (l′ +_{A} i))

• cell_{1} = ⟨fixnum m⟩ = cell_{2}

• cell_{1} = imm = cell_{2}

• cell_{1} = b^{∗} = cell_{2}

Definition 29 Let

\begin{matrix}Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩, and \\ Σ′ = ⟨t′, n′, c′, v′, a′, u′, k′, s′, r′_{1}, r′_{2}, r′_{3}, r′_{4}⟩ \end{matrix}

be gsbcm states. The gc state correspondence relation ≅ ⊂ state × state is defined as follows:

Σ ≅^{gc} Σ′

if there exists a gc location correspondence ≃_{0}^{gc} and a gc term correspondence ≃^{gc} induced by ≃_{0}^{gc} such that • for all l ∈ ldom(s) and l′ ∈ ldom(s′),

(s, s′ ⊢ l ≃_{0}^{gc} l′) ⇒ (s, s′ ⊢ s(l) ≃^{gc} s′(l′))

• (s, s′ ⊢ t ≃^{gc} t′)

• n = n′

• (s, s′ ⊢ v ≃^{gc} v′)

• #a = #a′ and (∀0 ≤ i < #a)(s, s′ ⊢ a(i) ≃^{gc} a′(i))

• (s, s′ ⊢ u ≃^{gc} u′)

• (s, s′ ⊢ k ≃^{gc} k′)

• (s, s′ ⊢ r_{2} ≃^{gc} r′_{2})

• r_{3} = r′_{3}

• r_{4} = r′_{4} Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let ⟨ptr l⟩

be such that gc-header(l −_{A} 1, s) holds. Then,

gc-convert(⟨ptr l⟩, Σ) =

⟨⟨ptr l′⟩ s r_{1}⟩ if s(l −_{A} 1) = ⟨ptr l′⟩
⟨⟨ptr l′⟩ s′′ r′_{1}⟩ if s(l −_{A} 1) = ⟨header h p m⟩

where l′ = ⟨2, #s(2) + 1⟩ and s′ = s +_{2} S(⟨ptr l⟩, s) and s′′ = s′[l −_{A} 1 ↦ ⟨ptr l′⟩] and r′_{1} = ⟨ptr l′⟩

gc-trace(d, Σ) =

gc-convert(d, Σ) if d is a pointer
d  otherwise

Lemma 30 Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let gc-trace(d, Σ) = ⟨d′ s′ r′_{1}⟩. Then there exists a gc location correspondence ≃_{0}^{gc} such that, if ≃^{gc} is the gc term correspondence induced by ≃_{0}^{gc}, then

1. s′ is a gc store.

2. (s′, s ⊢ d′ ≃^{gc} d)

3. Σ ≅^{gc} ⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ with ≃_{0}^{gc} and ≃^{gc} as witnesses.

4. If d′ = ⟨ptr l′⟩ then l′ = ⟨2, m′⟩ and s′(l′ −_{A} 1) = ⟨header h p m⟩ for some h, p, m.

Proof: The proof is by cases. Case s(l −_{A} 1) = ⟨ptr l′⟩ Let ≃_{0}^{gc} be defined such that for all l ∈ ldoms, (s, s ⊢ l ≃_{0}^{gc} l) if ¬gc-header(l, s). Let ≃^{gc} be the term correspondence induced by ≃_{0}.

1. s is a gc store by assumption.

2. s(l′ −_{A} 1) = ⟨header h p m⟩ since gc-header(l −_{A} 1, s) and s(l −_{A} 1) = ⟨ptr l′⟩. s(l −_{A} 1) = ⟨ptr l′⟩ by case condition, and s(l′ −_{A} 1) = ⟨header h p m⟩ (as above). Thus, by definition of term correspondence,

(s, s ⊢ ⟨ptr l⟩ ≃^{gc} ⟨ptr l′⟩).

3. Σ ≅^{gc} Σ holds trivially.

4. s(l′ −_{A} 1) = ⟨header h p m⟩ as in (2), and l′ = ⟨2, m′⟩ since s is a gc store.

Case s(l −_{A} 1) = ⟨header h p m⟩ Let ≃_{0}^{gc} be defined such that

• for all l′′ ∈ ldom(s), if l′′ ≠ l+_{A}i for 0 ≤ i < ℧m and if ¬gc-header(l′′, s), then (s, s′ ⊢ l′′ ≃_{0}^{gc} l′′).

• (s, s′ ⊢ l +_{A} i ≃_{0}^{gc} l′ +_{A} i) for all 0 ≤ i < ℧m.

This is a one-to-one map since l′ = ⟨2, #s(2) + 1⟩ by definition, and hence l′ +_{A} i ∉ ldom(s) for 0 ≤ i < ℧m. Let ≃^{gc} be the gc term correspondence induced by ≃_{0}^{gc}.

1. Since s is a gc store, so is s +_{2} S(⟨ptr l⟩, s), and hence so is s′′ = (s +_{2} S(⟨ptr l⟩, s))[l −_{A} 1 ↦ ⟨ptr l′⟩].

2. s(l −_{A} 1) = ⟨header h p m⟩ by case condition. s′(l′ −_{A} 1) = ⟨header h p m⟩ by definitions of s′ and l′. For all 0 ≤ i < ℧m, (s, s′ ⊢ l +_{A} i ≃_{0}^{gc} l′ +_{A} i) holds by definition of ≃_{0}^{gc}. Thus, by definition of a term correspondence,

(s, s ⊢ ⟨ptr l⟩ ≃^{gc} ⟨ptr l′⟩).

3. The registers of the state are unchanged except for r_{1}, but the definition of gc state correspondence does not depend on the value of r_{1}. Hence the only condition to verify is:

for all l_{1} ∈ ldom(s) and l_{2} ∈ ldom(s′),
(s, s′ ⊢ l_{1} ≃_{0}^{gc} l_{2}) ⇒ (s, s′ ⊢ s(l_{1}) ≃^{gc} s′(l_{2}))

Let (s, s′ ⊢ l_{1} ≃_{0}^{gc} l_{2}). If l_{1} ≠ l +_{A} i for 0 ≤ i < ℧m, then l_{1} = l_{2} by definition of ≃_{0}^{gc}. Further, ¬gc-header(l_{1}, s) and so l_{1} ≠ l −_{A} 1. Thus, s′(l_{2}) = s′(l_{1}) = s(l_{1}). The result then follows since (s, s′ ⊢ s(l_{1}) ≃^{gc} s(l_{1})) holds.

Otherwise, l_{1} = l +_{A} i for some 0 ≤ i < ℧m. Then, l_{2} = l′ +_{A} i by definition of ≃_{0}^{gc}. Now s′(l_{2}) = s′(l′ +_{A} i) = s(l +_{A} i) by definition of s′. The result then follows since (s, s′ ⊢ s(l +_{A} i) ≃^{gc} s(l +_{A} i)) holds.

4. s′(l′ −_{A} 1) is a header by definition of s′ and l′ = ⟨2, m⟩ by definition.

□

Lemma 31 Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let gc-trace(t, Σ) = ⟨t′ s′ r′_{1}⟩. Let S(t′, s′) = ⟨template #f c′:: o^{∗}⟩. Then Σ ≅ ⟨t′, n, c′, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩.

Proof: By Lemma 30, Σ ≅ ⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ and (s′, s ⊢ t′ ≃ t). Thus, by definition of state correspondence,

⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ ≅ ⟨t′, n, c′, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩

The result then holds by transitivity of state correspondence (Lemma 22).

□

Results analogous to Lemma 31 can be proved for v,u,k, and r_{2}.

Lemma 32 Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let gc-trace(a(i), Σ) = ⟨d′ s′ r′_{1}⟩. Let a′ = a[i ↦ d′]. Then

Σ ≅ ⟨t, n, c, v, a′, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩.

Proof: By Lemma 30, Σ ≅ ⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ and (s, s′ ⊢ a(i) ≃^{gc} d′). Thus, for all 0 ≤ i < #a, (s, s′ ⊢ a(i) ≃^{gc} a′(i)) Thus, by definition of state correspondence,

⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ ≅ ⟨t, n, c, v, a′, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩.

The result then holds by transitivity of state correspondence (Lemma 22).

□

Lemma 33 Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state. Let gc-trace(s(⟨2, m⟩), Σ) = ⟨d′ s′ r′_{1}⟩. Then Σ ≅ ⟨t, n, c, v, a, u, k, s′[⟨2, m⟩ ↦ d′], r′_{1}, r_{2}, r_{3}, r_{4}⟩.

Proof: By Lemma 30, Σ ≅ ⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ and (s′, s ⊢ d′ ≃ s(⟨2, m⟩)). Since s(⟨2, m⟩) = s′(⟨2, m⟩), we have that (s′, s ⊢ d′ ≃ s′(⟨2, m⟩)).

Let ≃_{0} be defined as follows:

(s′, s′[⟨2, m⟩ ↦ d′] ⊢ l ≃_{0} l) if l ∈ ldom(s′) and ¬gc-header(l, s′)

Let ≃ be the term correspondence induced by ≃_{0}. Then it follows from the definition of a state correspondence that ≃_{0} and ≃ are witnesses to the state correspondence

⟨t, n, c, v, a, u, k, s′, r′_{1}, r_{2}, r_{3}, r_{4}⟩ ≅ ⟨t, n, c, v, a, u, k, s′[⟨2, m⟩ ↦ d′], r′_{1}, r_{2}, r_{3}, r_{4}⟩

The result then holds by transitivity of state correspondence (Lemma 22).

□

Lemma 34 Let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be an gsbcm state. Let Σ′ = if C then Σ else garbage-collect(Σ). Then Σ ≅ Σ′.

Proof: Let Σ be a gsbcm state. Then Σ is also a gc state. Let

gc-trace(t, Σ) = ⟨t′ s^{1} r_{1}^{1}⟩ Σ^{1} = ⟨t′, n, c, v, a, u, k, s^{1}, r_{1}^{1}, r_{2}, r_{3}, r_{4}⟩

gc-trace(v, Σ^{1}) = ⟨v′ s^{2} r_{1}^{2}⟩ Σ^{2} = ⟨t′, n, c, v′, a, u, k, s^{2}, r_{1}^{2}, r_{2}, r_{3}, r_{4}⟩

gc-trace(u, Σ^{2}) = ⟨u′ s^{3} r_{1}^{3}⟩ Σ^{3} = ⟨t′, n, c, v′, a, u′, k, s^{3}, r_{1}^{3}, r_{2}, r_{3}, r_{4}⟩

gc-trace(k, Σ^{3}) = ⟨k′ s^{4} r_{1}^{4}⟩ Σ^{4} = ⟨t′, n, c, v′, a, u′, k′, s^{4}, r_{1}^{4}, r_{2}, r_{3}, r_{4}⟩

gc-trace(r_{2}, Σ^{4}) = ⟨r′_{2} s^{5} r_{1}^{5}⟩ Σ^{5} = ⟨t′, n, c, v′, a, u′, k′, s^{5}, r_{1}^{5}, r′_{2}, r_{3}, r_{4}⟩

gc-trace-stack(a, Σ^{5}) = ⟨a′ s^{6} r_{1}^{6}⟩ Σ^{6} = ⟨t′, n, c, v′, a′, u′, k′, s^{6}, r_{1}^{6}, r′_{2}, r_{3}, r_{4}⟩

gc-scan-heap(Σ^{6}) = ⟨s^{7} r_{1}^{7}⟩ Σ^{7} = ⟨t′, n, c, v′, a′, u′, k′, s^{7}, r_{1}^{7}, r′_{2}, r_{3}, r_{4}⟩

By Lemmas 31 (and analogous results for other registers), 32, 33, and the transitivity of ≅^{gc}, we have that

Σ ≅^{gc} Σ^{7}

Further, by Lemma 30(4), we have that none of the registers, stack, or cells in s^{7}(2) contain pointers of the form ⟨ptr ⟨i, m⟩⟩ for i ∈ {0, 1, 3}. Thus, if s^{8} = ⟨⟨⟩ ⟨⟩ s^{7}(2) ⟨⟩⟩ and Σ^{8} = Σ^{7}[s′ = s^{8}], then

Σ ≅^{gc} Σ^{8}

Let Σ^{9} = flip(Σ^{8}). Then,

Σ ≅^{gc} Σ^{9}

Let Σ^{10} = (codevector-set! (template-stob-codevector (template-ref Σ^{9}) Σ^{9}) Σ^{9}) .

That is, Σ^{10} = Σ^{9}[c′ = c_{1}] where S(t^{9}, s^{9}) = ⟨template #f c_{1}::o^{∗}⟩ for some o^{∗}. Since s^{10} is a gc store and all locations l in Σ^{10} have the form ⟨0, m⟩, it follows that s^{10} is a gsbcm store. Thus, Σ^{10} is a gsbcm state.

Now garbage-collect(Σ) = Σ^{10} by definition. Thus, since Σ ≅^{gc} Σ and Σ ≅^{gc} Σ^{10}, we have that

Σ ≅^{gc} if C then Σ else garbage-collect(Σ)

□

Lemma 35 Let Σ_{msbcm} be a msbcmstate, and let Σ_{gsbcm} and Σ′_{gsbcm} be gsbcmstates. If Σ_{msbcm} ≅ Σ_{gsbcm} and Σ_{gsbcm} ≅^{gc} Σ′_{gsbcm}, then Σ_{msbcm} ≅ Σ′_{gsbcm}

Proof: Let ≃_{0} and ≃ be witnesses to the state correspondence Σ_{msbcm} ≅ Σ_{gsbcm}. Let ≃_{0}^{gc} and ≃^{gc} be witnesses to the gc state correspondence Σ_{gsbcm} ≅^{gc} Σ′_{gsbcm}.

Let (s, s′ ⊢ cell ≃^{gc} cell′) where cell = ⟨ptr l⟩ and cell′ = ⟨ptr l′⟩. Then, since Σ_{gsbcm} and Σ′_{gsbcm} are gsbcmstates, it follows from the definition of gsbcm states that s(l −_{A} 1) and s′(l′ −_{A} 1) are headers. Thus the gc term correspondence ≃^{gc} is a term correspondence ≃. Similary, the gc state correspondence Σ_{gsbcm} ≅^{gc} Σ′_{gsbcm} is also a state state correspondence Σ_{gsbcm} ≅ Σ′_{gsbcm}. The result then follows by transitivity of ≅.

□

3.5.2 Microcode Functions

Lemma 36 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let

\begin{matrix}Σ^{M} = ⟨t^{M}, n^{M}, c^{M}, v^{M}, a^{M}, u^{M}, k^{M}, s^{M}, r_{1}^{M}, r_{2}^{M}, r_{3}^{M}, r_{4}^{M}⟩, and \\ Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ \end{matrix}

be such that Σ^{M} ≅ Σ with witnesses ≃_{0} and ≃. Let d^{M} = ⟨ptr l^{M}⟩, d = ⟨ptr l⟩, and (s^{M}, s ⊢ d^{M} ≃ d). Then,

  1. (s^{M}, s ⊢ template-ref(Σ^{M}) ≃ template-ref(Σ))
  2. (s^{M}, s ⊢ codevector-ref(Σ^{M}) ≃ codevector-ref(Σ))
  3. offset-ref(Σ^{M}) = offset-ref(Σ)

  4. (s^{M}, s ⊢ value-ref(Σ^{M}) ≃ value-ref(Σ))

5. (s^{M}, s ⊢ env-ref(Σ^{M}) ≃ env-ref(Σ))

6. (s^{M}, s ⊢ cont-ref(Σ^{M}) ≃ cont-ref(Σ))

  7. (s^{M}, s ⊢ spare2-ref(Σ^{M}) ≃ spare2-ref(Σ))
  8. (s^{M}, s ⊢ spare3-ref(Σ^{M}) ≃ spare3-ref(Σ))
  9. (s^{M}, s ⊢ stack-top(Σ^{M}) ≃ stack-top(Σ))
 10. stack-empty?(Σ^{M}) = stack-empty?(Σ)
 11. stack-length(Σ^{M}) = stack-length(Σ)

12. (s^{M}, s ⊢ stob-desc-ref(d^{M}, i, Σ^{M}) ≃ stob-desc-ref(d, i, Σ))

13. (s^{M}, s ⊢ stob-byte-ref(d^{M}, i, Σ^{M}) ≃ stob-byte-ref(d, i, Σ))

 14. stob-tag(d^{M}, Σ^{M}) = stob-tag(d, Σ)
 15. stob-mutable?(d^{M}, Σ^{M}) = stob-mutable?(d, Σ)
 16. stob-size-in-bytes(d^{M}, Σ^{M}) = stob-size-in-bytes(d, Σ)
 17. stob-size-in-cells(d^{M}, Σ^{M}) = stob-size-in-cells(d, Σ)

Proof: Cases 1–8: By definition, template-ref(Σ^{M}) = t^{M} and template-ref(Σ) = t. Since Σ^{M} ≅ Σ, we have by definition that (s^{M}, s ⊢ t^{M} ≃ t) as desired. Cases 2–8 are proved similarly. Cases 9–11: Since Σ^{M} ≅ Σ, we have by definition that #a^{M} = #a and (s^{M}, s ⊢ a^{M}(i) ≃ a(i)) for all 0 ≤ i < #a. Now, stack-top(Σ^{M}) = a^{M}(0) and stack-top(Σ) = a(0). Hence,

   (s^{M}, s ⊢ stack-top(Σ^{M}) ≃ stack-top(Σ))
   stack-empty?(Σ^{M}) = (#a^{M} = 0) = (#a = 0) = stack-empty?(Σ)
   stack-length(Σ^{M}) = #a^{M} = #a = stack-length(Σ)

Cases 12–16: By assumption, d^{M} = ⟨ptr l^{M}⟩ and d = ⟨ptr l⟩. Let s^{M}(l^{M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩ and s(l −_{A} 1) = ⟨header h p m⟩. Since Σ^{M} ≅ Σ and (s^{M}, s ⊢ d^{M} ≃ d), we have by definition that h^{M} = h, p^{M} = p, m^{M} = m, and (s^{M}, s ⊢ (l^{M} +_{A} i) ≃_{0} (l +_{A} i)) for all 0 ≤ i < ℧m. Hence, by definition of state correspondence, (s^{M}, s ⊢ s^{M}(l^{M} +_{A} i) ≃ s(l +_{A} i)) for all 0 ≤ i < ℧m.

Since

stob-desc-ref(d^{M}, i, Σ^{M}) = s^{M}(l^{M} +_{A} i), and
stob-desc-ref(d, i, Σ) = s(l +_{A} i)

we have that

     (s^{M}, s ⊢ stob-desc-ref(d^{M}, i, Σ^{M}) ≃ stob-desc-ref(d, i, Σ)).

Similarly, (s^{M}, s ⊢ stob-byte-ref(d^{M}, i, Σ^{M}) ≃ stob-byte-ref(d, i, Σ)). Finally,

stob-tag(d^{M}, Σ^{M}) = h^{M} = h = stob-tag(d, Σ)

 stob-mutable?(d^{M}, Σ^{M}) = p^{M} = p = stob-mutable?(d, Σ)
 stob-size-in-bytes(d^{M}, Σ^{M}) = m^{M} = m = stob-size-in-bytes(d, Σ)
 stob-size-in-cells(d^{M}, Σ^{M}) = ℧m^{M} = ℧m
     = stob-size-in-cells(d, Σ)

□

Lemma 37 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let l^{M} ∈ ldom(s^{M}), l ∈ ldom(s), (s^{M}, s ⊢ l^{M} ≃_{0} l), and (s^{M}, s ⊢ cell^{M} ≃ cell) for some l^{M}, l, cell^{M}, cell such that s^{M}(l^{M}) and s(l) are not headers. Let s^{′M} = s^{M}[l^{M} ↦ cell^{M}] and s′ = s[l ↦ cell].

Let ≃′_{0} be a location correspondence such that (s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) holds if and only if (s^{M}, s ⊢ l^{M} ≃_{0} l) holds. Note that this is a valid definition since ldom(s^{′M}) = ldom(s^{M}) and ldom(s′) = ldom(s). Let ≃′ be the term correspondence induced by ≃′_{0}.

Then,

(∀cell^{M}, cell)(s^{M}, s ⊢ cell^{M} ≃ cell) ⇒ (s^{′M}, s′ ⊢ cell^{M} ≃′ cell)

Proof: Let (s^{M}, s ⊢ cell^{M} ≃ cell). We proceed by cases:

Case cell^{M} = ⟨ptr l^{′M}⟩ and cell = ⟨ptr l′⟩:

By definition of term correspondence, the following hold:

1. s^{M}(l^{′M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩ 2. s(l′ −_{A} 1) = ⟨header h p m⟩

3. h^{M} = h

4. p^{M} = p

5. m^{M} = m

6. for all 0 ≤ i < ℧m, (s^{M}, s ⊢ (l^{′M} +_{A} i) ≃_{0} (l′ +_{A} i)) Now s^{M}(l^{′M} −_{A} 1) is a header while s^{M}(l^{M}) is not (by assumption) and hence l^{′M} −_{A} 1 ≠ l^{M}. Similarly, l′ −_{A} 1 ≠ l. Thus,

1. s^{′M}(l^{′M} −_{A} 1) = s^{M}(l^{′M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩

2. s′(l′ −_{A} 1) = s(l′ −_{A} 1) = ⟨header h p m⟩

3. h^{M} = h

4. p^{M} = p

5. m^{M} = m

6. By definition of ≃′_{0}, for all l^{M}, l, (s^{M}, s ⊢ l^{M} ≃_{0} l) holds if and only if (s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) holds. We thus have that for all 0 ≤ i < ℧m, (s^{′M}, s′ ⊢ (l^{′M} +_{A} i) ≃′_{0} (l′ +_{A} i)).

Thus, by definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds.

Case cell^{M} = ⟨fixnum m⟩ and cell = ⟨fixnum m⟩:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds. Case cell^{M} = imm and cell = imm:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds. Case cell^{M} = b^{∗} and cell = b^{∗}:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds.

□

Lemma 38 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let l^{M} ∉ ldom(s^{M}), l ∉ ldom(s), and (s^{M}, s ⊢ cell^{M} ≃ cell) for some cell^{M}, cell. Let s^{′M} = s^{M}[l^{M} ↦ cell^{M}] and s′ = s[l ↦ cell].

Let ≃′_{0} be a location correspondence such that, for all l_{1}^{M}, l_{1}, (s^{′M}, s′ ⊢ l_{1}^{M} ≃′_{0} l_{1}) holds if and only if either (s^{M}, s ⊢ l_{1}^{M} ≃_{0} l_{1}) holds or l_{1}^{M} = l^{M} and l_{1} = l. Note that this is a valid definition since ldom(s^{′M}) = ldom(s^{M})∪{l^{M}} and ldom(s′) = ldom(s) ∪ {l}. Let ≃′ be the term correspondence induced by ≃′_{0}.

Then,

(∀cell^{M}, cell)(s^{M}, s ⊢ cell^{M} ≃ cell) ⇒ (s^{′M}, s′ ⊢ cell^{M} ≃′ cell)

Proof: Let (s^{M}, s ⊢ cell^{M} ≃ cell). We proceed by cases: Case cell^{M} = ⟨ptr l^{′M}⟩ and cell = ⟨ptr l′⟩:

By definition of term correspondence, the following hold:

1. s^{M}(l^{′M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩

2. s(l′ −_{A} 1) = ⟨header h p m⟩

3. h^{M} = h

4. p^{M} = p

5. m^{M} = m

6. for all 0 ≤ i < ℧m, (s^{M}, s ⊢ (l^{′M} +_{A} i) ≃_{0} (l′ +_{A} i)) Now s^{M}(l^{′M} −_{A} 1) is defined while s^{M}(l^{M}) is not (by assumption) and hence l^{′M} −_{A} 1 ≠ l^{M}. Similarly, l′ −_{A} 1 ≠ l. Thus,

1. s^{′M}(l^{′M} −_{A} 1) = s^{M}(l^{′M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩

2. s′(l′ −_{A} 1) = s(l′ −_{A} 1) = ⟨header h p m⟩

3. h^{M} = h

4. p^{M} = p

5. m^{M} = m

6. By definition of ≃′_{0}, for all l_{1}^{M}, l_{1}, (s^{M}, s ⊢ l_{1}^{M} ≃_{0} l_{1}) holds if and only if either (s^{′M}, s′ ⊢ l_{1}^{M} ≃′_{0} l_{1}) holds or l_{1}^{M} = l^{M} and l_{1} = l. We thus have that for all 0 ≤ i < ℧m, (s^{′M}, s′ ⊢ (l^{′M} +_{A} i) ≃′_{0} (l′ +_{A} i)).

Thus, by definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds.

Case cell^{M} = ⟨fixnum m⟩ and cell = ⟨fixnum m⟩:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds. Case cell^{M} = imm and cell = imm:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds.

Case cell^{M} = b^{∗} and cell = b^{∗}:

By definition of term correspondence, (s^{′M}, s′ ⊢ cell^{M} ≃′ cell) holds. □

Lemma 39 Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}. Let

\begin{matrix}Σ^{M} = ⟨t^{M}, n^{M}, c^{M}, v^{M}, a^{M}, u^{M}, k^{M}, s^{M}, r_{1}^{M}, r_{2}^{M}, r_{3}^{M}, r_{4}^{M}⟩, and \\ Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ \end{matrix}

be such that Σ^{M} ≅ Σ with witnesses ≃_{0} and ≃. Let d^{M} = ⟨ptr l^{M}⟩, d = ⟨ptr l⟩, (s^{M}, s ⊢ d^{M} ≃ d), and (s^{M}, s ⊢ vd^{M} ≃ vd) for some l^{M}, l, vd^{M}, vd. Then,

1. template-set(d^{M}, Σ^{M}) ≅ template-set(d, Σ)
2. codevector-set(d^{M}, Σ^{M}) ≅ codevector-set(d, Σ)
3. offset-set(i, Σ^{M}) ≅ offset-set(i, Σ)
4. offset-inc(i, Σ^{M}) ≅ offset-inc(i, Σ)
5. value-set(d^{M}, Σ^{M}) ≅ value-set(d, Σ)

6. env-set(d^{M}, Σ^{M}) ≅ env-set(d, Σ)

7. cont-set(d^{M}, Σ^{M}) ≅ cont-set(d, Σ)
8. spare1-set(d^{M}, Σ^{M}) ≅ spare1-set(d, Σ)
9. spare2-set(d^{M}, Σ^{M}) ≅ spare2-set(d, Σ)
10. spare3-set(i, Σ^{M}) ≅ spare3-set(i, Σ)
11. stack-push(d^{M}, Σ^{M}) ≅ stack-push(d, Σ)
12. stack-pop(Σ^{M}) ≅ stack-pop(Σ)
13. stack-clear(Σ^{M}) ≅ stack-clear(Σ)

14. stob-desc-set(d^{M}, i, vd^{M}, Σ^{M}) ≅ stob-desc-set(d, i, vd, Σ)

15. stob-byte-set(d^{M}, i, b^{M}, Σ^{M}) ≅ stob-byte-set(d, i, b, Σ)

 16. make-desc-stob^{M}(h, p, m, Σ^{M}) ≅ make-desc-stob(h, p, m, Σ)

17.

      make-desc-stob-from-stack^{M}(h, p, Σ^{M}) ≅

         make-desc-stob-from-stack(h, p, Σ)
 18. make-byte-stob^{M}(h, p, m, Σ^{M}) ≅ make-byte-stob(h, p, m, Σ)

Proof: Cases 1–10: By definition, template-set(d^{M}, Σ^{M}) = Σ^{M}[t^{′M} = d^{M}] and template-set(d, Σ) = Σ[t′ = d]. Since Σ^{M} ≅ Σ and (s^{M}, s ⊢ d^{M} ≃ d), we have by definition that Σ^{M}[t^{′M} = d^{M}] ≅ Σ[t′ = d] as desired. Cases 2–10 are proved similarly.

Cases 11–13: Since Σ^{M} ≅ Σ, we have by definition that #a^{M} = #a and (s^{M}, s ⊢ a^{M}(i) ≃ a(i)) for all 0 ≤ i < #a. Now, stack-push(d^{M}, Σ^{M}) = Σ[a^{′M} = d^{M}::a^{M}] and stack-push(d, Σ) = Σ[a′ = d::a]. Since (s^{M}, s ⊢ d^{M} ≃ d), we have that #a^{′M} = #a′ and (s^{M}, s ⊢ a^{′M}(i) ≃ a′(i)) for all 0 ≤ i < #a′. Thus Σ[a^{′M} = d^{M}::a^{M}] ≅ Σ[a′ = d::a]. Cases 12 and 13 are proved similarly.

Cases 14–15: By assumption, d^{M} = ⟨ptr l^{M}⟩ and d = ⟨ptr l⟩. Let s^{M}(l^{M} −_{A} 1) = ⟨header h^{M} p^{M} m^{M}⟩ and s(l −_{A} 1) = ⟨header h p m⟩. Now, Σ^{′M} = stob-desc-set(d^{M}, i, vd^{M}, Σ^{M}) = Σ[s^{′M} = s^{M}[(l^{M} +_{A} i) ↦ vd^{M}]] and Σ′ = stob-desc-set(d, i, vd, Σ) = Σ[s′ = s[(l +_{A} i) ↦ vd]].

Let ≃′_{0} be a location correspondence such that (s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) holds if and only if (s^{M}, s ⊢ l^{M} ≃_{0} l) holds. Note that this is a valid definition since ldom(s^{′M}) = ldom(s^{M}) and ldom(s′) = ldom(s). Let ≃′ be the term correspondence induced by ≃′_{0}. We show that Σ^{′M} ≅ Σ′ by choosing ≃′_{0} and ≃′ as the witness location and term correspondences, and showing that:

• for all l^{M} ∈ ldom(s^{M}) and l ∈ ldom(s),

(s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) ⇒ (s^{′M}, s′ ⊢ s^{′M}(l^{M}) ≃′ s′(l))

Let (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}).

Case \overline{l^{M}} = l^{M} +_{A} i:

Since (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}) we have by definition of ≃′_{0} that \overline{l} = l +_{A} i. By definition, s^{′M}(l^{M} +_{A} i) = vd^{M} and s′(l +_{A} i) = vd. Since (s^{M}, s ⊢ vd^{M} ≃ vd) by assumption, the result follows by Lemma 37. Case \overline{l^{M}} ≠ l^{M} +_{A} i:

Since (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}), we have by definition of ≃′_{0} that \overline{l} ≠ l+_{A}i and (s^{M}, s ⊢ \overline{l^{M}} ≃_{0} \overline{l}). Since Σ^{M} ≅ Σ, we have that (s^{M}, s ⊢ s^{M}(\overline{l^{M}}) ≃ s(\overline{l})). Hence, by Lemma 37, (s^{′M}, s′ ⊢ s^{M}(\overline{l^{M}}) ≃′ s(\overline{l})). Now s^{M}(\overline{l^{M}}) = s^{′M}(\overline{l^{M}}) since \overline{l^{M}} ≠ l^{M} +_{A} i, and s(\overline{l}) = s′(\overline{l}) since

\overline{l} ≠ l +_{A} i. Thus, (s^{′M}, s′ ⊢ s^{′M}(\overline{l^{M}}) ≃′ s′(\overline{l})) as desired.

Otherwise:

There are no other cases since ≃′_{0} is a 1-to-1 map and (s^{M}, s ⊢ l^{M} +_{A} i ≃_{0} l +_{A} i) by assumption.

• (s^{′M}, s′ ⊢ t^{M} ≃′ t)

Since Σ^{M} ≅ Σ, we have that (s^{M}, s ⊢ t^{M} ≃ t). The result then follows by Lemma 37.

• n^{M} = n Follows from Σ^{M} ≅ Σ.

• (s^{′M}, s′ ⊢ v^{M} ≃′ v)

Follows from Σ^{M} ≅ Σ and Lemma 37.

• #a^{M} = #a and (∀0 ≤ i < #a)(s^{′M}, s′ ⊢ a^{M}(i) ≃′ a(i)) Follows from Σ^{M} ≅ Σ and Lemma 37.

• (s^{′M}, s′ ⊢ u^{M} ≃′ u)

Follows from Σ^{M} ≅ Σ and Lemma 37.

• (s^{′M}, s′ ⊢ k^{M} ≃′ k)

Follows from Σ^{M} ≅ Σ and Lemma 37.

• (s^{′M}, s′ ⊢ r_{2}^{M} ≃′ r_{2})

Follows from Σ^{M} ≅ Σ and Lemma 37.

• r_{3}^{M} = r_{3} Follows from Σ^{M} ≅ Σ.

• r_{4}^{M} = r_{4} Follows from Σ^{M} ≅ Σ.

Case 15 is proved similarly.

Cases 16–18: Now, Σ^{′M} = make-desc-stob^{M}(h, p, m, Σ) = Σ^{M}[s^{′M} = s^{M} ⊕_{0} ⟨h p m⟩][r_{1}^{′M} = ⟨0, #s^{M}(0)⟩] and Σ′ = make-desc-stob(h, p, m, Σ) = Σ[s′ = s ⊕_{0} ⟨h p m⟩][r′_{1} = ⟨0, #s(0)⟩].

Let ≃_{0} be a location correspondence and ≃ be the term correspondence induced by ≃_{0}

Let ≃′_{0} be a location correspondence such that, for all l^{M}, l, (s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) holds if and only if either (s^{M}, s ⊢ l^{M} ≃_{0} l) holds or l^{M} = ⟨0, #s^{M} + i⟩ and l = ⟨0, #s + i⟩ hold for some 1 ≤ i < m + 1. Let ≃′ be the term correspondence induced by ≃′_{0}. We show that Σ^{′M} ≅ Σ′ by choosing ≃′_{0} and ≃′ as the witness location and term correspondences, and showing that:

• for all l^{M} ∈ ldom(s^{M}) and l ∈ ldom(s),

(s^{′M}, s′ ⊢ l^{M} ≃′_{0} l) ⇒ (s^{′M}, s′ ⊢ s^{′M}(l^{M}) ≃′ s′(l))

Let (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}).

Case \overline{l^{M}} = ⟨0, #s^{M}(0) + i⟩ for some 0 ≤ i < m + 1:

Since (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}), we have by definition of ≃′_{0} that i > 0 and \overline{l} = ⟨0, #s(0) + i⟩. By definition, s^{′M}(\overline{l^{M}}) = d_{u}^{M} and s′(\overline{l}) = d_{u}. The result follows since (s^{′M}, s′ ⊢ d_{u}^{M} ≃′ d_{u}) by definition.

Case \overline{l^{M}} <_{A} ⟨0, #s^{M}(0)⟩:

Since (s^{′M}, s′ ⊢ \overline{l^{M}} ≃′_{0} \overline{l}), we have by definition of ≃′_{0} that \overline{l} <_{A} ⟨0, #s(0)⟩ and (s^{M}, s ⊢ \overline{l^{M}} ≃_{0} \overline{l}). Since Σ^{M} ≅ Σ, we have that (s^{M}, s ⊢ s^{M}(\overline{l^{M}}) ≃ s(\overline{l})). Hence, by Lemma 38, (s^{′M}, s′ ⊢ s^{M}(\overline{l^{M}}) ≃′ s(\overline{l})). Now s^{M}(\overline{l^{M}}) = s^{′M}(\overline{l^{M}}) and s(\overline{l}) = s′(\overline{l}). Thus (s^{′M}, s′ ⊢ s^{′M}(\overline{l^{M}}) ≃′ s′(\overline{l})) as desired.

• (s^{′M}, s′ ⊢ t^{M} ≃′ t)

Since Σ^{M} ≅ Σ, we have that (s^{M}, s ⊢ t^{M} ≃ t). The result then follows by Lemma 38.

• n^{M} = n Follows from Σ^{M} ≅ Σ.

• (s^{′M}, s′ ⊢ v^{M} ≃′ v)

Follows from Σ^{M} ≅ Σ and Lemma 38.

• #a^{M} = #a and (∀0 ≤ i < #a)(s^{′M}, s′ ⊢ a^{M}(i) ≃′ a(i)) Follows from Σ^{M} ≅ Σ and Lemma 38.

• (s^{′M}, s′ ⊢ u^{M} ≃′ u)

Follows from Σ^{M} ≅ Σ and Lemma 38.

• (s^{′M}, s′ ⊢ k^{M} ≃′ k)

Follows from Σ^{M} ≅ Σ and Lemma 38.

• (s^{′M}, s′ ⊢ r_{2}^{M} ≃′ r_{2})

Follows from Σ^{M} ≅ Σ and Lemma 38.

• r_{3}^{M} = r_{3} Follows from Σ^{M} ≅ Σ.

• r_{4}^{M} = r_{4}

Follows from Σ^{M} ≅ Σ. Case 17 and 18 are proved similarly. □

Lemma 40 Let Σ^{M} and Σ be msbcm and gsbcm states respectively. If Σ^{M} ≅ Σ, then Σ^{M} is a halt state of the msbcm if and only if Σ is a halt state of the gsbcm. Proof: Let Σ^{M} = ⟨t^{M}, n^{M}, c^{M}, v^{M}, a^{M}, u^{M}, k^{M}, s^{M}, r_{1}^{M}, r_{2}^{M}, r_{3}^{M}, r_{4}^{M}⟩ be an msbcm halt state, let Σ = ⟨t, n, c, v, a, u, k, s, r_{1}, r_{2}, r_{3}, r_{4}⟩ be a gsbcm state, and let Σ^{M} ≅ Σ. We show that Σ is a gsbcm halt state.

Since Σ^{M} is a msbcm halt state, we have that

• S(c^{M}, s^{M}) = ⟨codevector #f b^{∗M}⟩,

• b^{∗M}(n^{M}) = return, and

• k^{M} = ⟨immediate halt⟩. Since Σ^{M} ≅ Σ, we have that (s^{M}, s ⊢ c^{M} ≃ c) and (s^{M}, s ⊢ k^{M} ≃ k). Hence, we have by definition of a term correspondence that

• S(c, s) = ⟨codevector #f b^{∗}⟩,

• b^{∗}(n) = return, and

• k = ⟨immediate halt⟩. and so Σ is a gsbcm halt state.

The converse holds similarly. □ Lemma 41 Let Σ_{i}^{M} and Σ_{i} be msbcm and gsbcm initial states respectively. If Σ_{i}^{M} ≅ Σ_{i}, then

1. R_{msbcm}^{∗}Σ_{i}^{M} is defined if and only if R_{gsbcm}^{∗}Σ_{i} is defined,

2. If R_{msbcm}^{∗}Σ_{i}^{M} and R_{gsbcm}^{∗}Σ_{i} are defined, then R_{msbcm}^{∗}Σ_{i}^{M} ≅ R_{gsbcm}^{∗}Σ_{i}.

Proof: Each action rule of the msbcm and gsbcm is expressed as the composition of the microcode functions and auxiliary functions. Each of these functions preserve term and state correspondence and hence so do their composition. Thus each action rule preserves state correspondence and hence so does the union and transitive closure of the action rules.

□

3.6 Correspondence of Final Answers

The following lemma asserts that the msbcm and gsbcm answer functions map corresponding states to equal natural numbers.

Lemma 42 Let Σ_{f}^{M} and Σ_{f} be msbcm and gsbcm halt states respectively. If Σ_{f}^{M} ≅ Σ_{f}, then A_{msbcm}(Σ_{f}^{M}) = A_{gsbcm}(Σ_{f}).

Proof: Let v^{M} and v be the value registers of Σ_{f}^{M} and Σ_{f} respectively. Since Σ_{f}^{M} ≅ Σ_{f}, we have by definition of state correspondence that v^{M} and v are related (i.e. (s^{M}, s ⊢ v^{M} ≃ v)). By definition of term correspondence, if v^{M} = ⟨fixnum m⟩ then v = ⟨fixnum m⟩ and so A_{msbcm}(Σ_{f}^{M}) = A_{gsbcm}(Σ_{f}) = m. If v^{M} is not of the form ⟨fixnum m⟩ then neither is v, and so A_{msbcm}(Σ_{f}^{M}) and A_{gsbcm}(Σ_{f}) are both undefined.

□

3.7 Correspondence of Semantics

We can now prove the main theorem of this chapter.

Theorem 43 If P is an sbc program, then its operational semantics as given by the msbcm yields the same answer as its operational semantics as given by the gsbcm. That is,

O_{msbcm}^{sbc}[[P]] = O_{gsbcm}^{sbc}[[P]]

Proof: Follows immediately from Lemmas 23, 41, and 42. □

4 Finite SBC State Machine

In this chapter, we give Stored Byte Code (sbc) programs an (operational) semantics in terms of a deterministic state machine with “finite” concrete states. The state machine is called the Finite Stored Byte Code Machine (fsbcm). We show that this operational semantics is equivalent to the operational semantics in terms of the gsbcm. This chapter concludes the implementation and verification of the VLISP byte code interpreter.

This chapter presents:

1. an operational semantics of sbc programs in terms of a state machine called the Finite Stored Byte Code Machine (fsbcm).

2. a correspondence relation that relates gsbcm states and fsbcm states;

3. a proof that the operational semantics of sbc as given by the fsbcm is faithful to the operational semantics of sbc as given by the gsbcm. That is, if the fsbcm operational semantics assigns a meaning to an sbc program, then the gsbcm operational semantics assigns the same meaning to the program.

4.1 FSBC State Machine (FSBCM)

4.1.1 Finite Stored Byte Code (FSBC)

The Finite Stored Byte Code (fsbc) provides the syntactic objects that form the states of the fsbcm. All syntactic objects of fsbc have a finite structure. They are either finite numbers or finite sequences, with bounds specified by the syntax.

The abstract syntax of Finite Stored Byte Code (fsbc) is defined below.

Let z = 2 ∗ heap-size-in-words.

program ::= term
term ::= ⟨store nat⟩
store ::= nat^{z}
loc ::= nat

We will use i,m,n, t, c, v, u, k, and r-like variables for numbers, and s-like variables for (fsbc) stores.

We define a family of partial functions from msbc terms to fsbcm terms (i.e., natural numbers). Since all sbc terms are msbc terms, these functions will also map sbc terms to natural numbers.

F^{byte}(call)  = 0
F^{byte}(return)  = 1

F^{byte}(make-cont)  = 2

F^{byte}(literal)  = 3
F^{byte}(closure)  = 4
F^{byte}(global)  = 5
F^{byte}(local)  = 6

F^{byte}(set-global!)  = 7
F^{byte}(set-local!)  = 8

F^{byte}(push)  = 9
F^{byte}(make-env)  = 10

F^{byte}(make-rest-list) = 11
F^{byte}(unspecified)  = 12

F^{byte}(jump)  = 13

F^{byte}(jump-if-false) = 14
F^{byte}(check-args=)  = 15
F^{byte}(check-args>=) = 16

F^{byte}(empty)  = 18
F^{byte}(r)  = m  for 19 ≤ m < MAXBYTEVAL
F^{byte}(m)  = m  if 0 ≤ m < MAXBYTEVAL
F^{byteseq}(⟨⟩)  = 0
F^{byteseq}(b^{∗} ^{⌢} ⟨b⟩)  = MAXBYTEVAL ∗ F^{byteseq}(b^{∗}) + F^{byte}(b)

F^{loc}(⟨0, m⟩) = low-heap-base + m

             if (low-heap-base + m) < low-heap-limit

F^{loc}(⟨1, m⟩) = high-heap-limit + m − 1

             if stack-base ≤ (high-heap-limit + m − 1)

F^{loc}(⟨2, m⟩) = old-low-heap-base + m

             if (old-low-heap-base + m) < old-low-heap-limit

F^{bool}(#f)  = 0
F^{bool}(#t)  = 1
F^{imm}(false)  = 64 ∗ 0 + 0
F^{imm}(true)  = 64 ∗ 0 + 1
F^{imm}(char(m)) = 64 ∗ m + 2 if 0 ≤ m < MAXBYTEVAL
F^{imm}(unspecified)  = 64 ∗ 0 + 3
F^{imm}(undefined)  = 64 ∗ 0 + 4
F^{imm}(null)  = 64 ∗ 0 + 5
F^{imm}(halt)  = 64 ∗ 0 + 6
F^{imm}(empty-env)  = 64 ∗ 0 + 7
F^{imm}(eof)  = 64 ∗ 0 + 8

F^{fixnum}(m)  = m  if MINFIXNUM ≤ m < MAXFIXNUM

F^{htag}(pair)  = 0
F^{htag}(symbol)  = 1
F^{htag}(vector)  = 2
F^{htag}(closure)  = 3
F^{htag}(location)  = 4
F^{htag}(port)  = 5
F^{htag}(continuation)  = 6
F^{htag}(template)  = 7
F^{htag}(environment)  = 8
F^{htag}(string)  = 10
F^{htag}(codevector)  = 11
F^{desc}(⟨fixnum m⟩)  = 4 ∗ F^{fixnum}(m) + 0
F^{desc}(⟨immediate imm⟩) = 4 ∗ F^{imm}(imm) + 1
F^{desc}(⟨header h p m⟩) = 256 ∗ m + 128 ∗ F^{bool}(p) + 4 ∗ F^{htag}(h) + 2
F^{desc}(⟨ptr l⟩)  = 4 ∗ F^{loc}(l) + 3
F^{cell}(desc)  = F^{desc}(desc)
F^{cell}(b^{∗})  = F^{byteseq}(b^{∗})

4.1.2 Stores

A store s is represented as a fixed-length sequence of natural numbers. Segments of the store are represented as triples of locations ⟨l_{1}, l_{2}, l_{3}⟩ where l_{1} ≤ l_{2} ≤ l_{3} ≤ #s. This denotes the map from the locations l_{1}, l_{1} + 1, …, l_{3} − 1 to the cells s(l_{1}), s(l_{1} + 1), …, s(l_{3} − 1). We call a subset of the domain of a segment to be the active portion of the segment; we will only be interested in the value of a segment at locations within this subset. We distinguish between positive segments and negative segments. The active portion of a positive segment consists of the locations l_{1}, l_{1} + 1, …, l_{2} − 1, while the active portion of a negative segment consists of the locations l_{2}, l_{2} + 1, …, l_{3} − 1.

4.1.3 States

The states of the fsbcm are the sequences of the form

⟨t, n, c, v, g_{a}, g_{a′}, u, k, s, g_{0}, g_{1}, g_{2}, g_{3}, r_{1}, r_{2}, r_{3}, r_{4}⟩

where g_{a}, g_{a′}, g_{0}, g_{1}, g_{2}, g_{3} are six segments of the store s such that:

  1. g_{0} = ⟨low-heap-base, hp, low-heap-limit⟩
  2. g_{a} = ⟨low-heap-limit, sp, stack-base⟩
  3. g_{1} = ⟨stack-base, stack-base, high-heap-limit⟩
  4. g_{2} = ⟨old-low-heap-base, old-hp, old-low-heap-limit⟩
  5. g_{a′} = ⟨old-low-heap-limit, old-sp, old-stack-base⟩
  6. g_{3} = ⟨old-stack-base, old-stack-base, old-high-heap-limit⟩
  7. Either old-high-heap-limit = low-heap-base or high-heap-limit =
     old-low-heap-base.

The components of a state are called, in order, its template, offset, codevector, value, argument stack, old argument stack, environment, continuation, store, segment0, segment1, segment2, segment3, spare1, spare2, spare3, and spare4, and we may informally speak of them as being held in registers. Note that the definition implies that the six segments are disjoint, i.e., if a location l is in the domain of a segment, then it is not in the domain of any other segment.

4.1.4 Action Rules

In Section 2.2.8, we specified the action rules of the msbcm as the composition of stored object manipulators, microcode functions, and other auxiliary functions. Stored object manipulators were in turn specified in terms of the microcode functions and auxiliary functions. In Section 3.1.4, the action rules of the gsbcm were given the same definition forms as in the msbcm. Similarly, the action rules of the fsbcm are given those same definition forms. We denote the transitive closure of the union of all fsbcm action rules by R_{fsbcm}^{∗}.

Now, the extensions of the gsbcm action rules are not the same as the extensions of the corresponding msbcm action rules since three gsbcm mutator functions differ from the corresponding msbcm functions. Similarly, the definitions of the fsbcm microcode functions and auxiliary functions differ from those in the gsbcm; hence, the extensions of the action rules differ from the extensions of the corresponding gsbcm action rules. We present the implementation of the fsbcm global state, microcode functions, and auxiliary functions in the next section.

4.1.5 Implementation

Global State The following functions define the global state of the FSBCM.

(define *template* unspecified)  ; t
(define *codevector* *hp*)  ; c
(define *offset* 0)  ; n
(define *value* unspecified)  ; v
(define *env* unspecified)  ; u
(define *cont* unspecified)  ; k
(define *spare1* unspecified)  ; r_{1}
(define *spare2* unspecified)  ; r_{2}
(define *spare3* 0)  ; r_{3}
(define *gc-spare* unspecified)  ; r_{4}
(define *symbol-table* unspecified)  ; symbol table
(define *low-heap-base* heap-low)  ; g_{0}(0)
(define *hp* heap-low)  ; g_{0}(1)
(define *low-heap-limit* heap-mid)  ; g_{0}(2) = g_{a}(0)
(define *sp* heap-mid)  ; g_{a}(1)
(define *stack-base* heap-mid)  ; g_{a}(2) = g_{1}(0) = g_{1}(1)
(define *high-heap-limit* heap-mid)  ; g_{1}(2)

(define *old-low-heap-base* heap-mid)  ; g_{2}(0)
(define *old-hp* heap-mid)  ; g_{2}(1)
(define *old-low-heap-limit* heap-mid) ; g_{2}(2) = g′_{a}(0)
(define *old-sp* heap-high)  ; g′_{a}(1)
(define *old-stack-base* heap-high)  ; g′_{a}(2) = g_{3}(0) = g_{3}(1)
(define *old-high-heap-limit* heap-high) ; g_{3}(2)

Microcode Functions

Observers

(define (template-ref) *template*)
(define (codevector-ref) *codevector*)
(define (offset-ref) *offset*)
(define (value-ref) *value*)
(define (env-ref) *env*)
(define (cont-ref) *cont*)
(define (spare1-ref) *spare1*)
(define (spare2-ref) *spare2*)
(define (spare3-ref) *spare3*)
(define (gc-spare-ref) *gc-spare*)
(define (symbol-table-ref) *symbol-table*)
(define (stack-top) (stack-ref *sp*))
(define (stack-nth n) (stack-ref (addr+ *sp* n)))
(define (stack-empty?) (addr= *stack-base* *sp*))
(define (stack-length) (addr- *stack-base* *sp*))
(define (stob-desc-ref a i)
  (heap-ref (heap-pointer->addr a) i))
(define (stob-binarray-ref a i)
  (heap-byte-ref (heap-pointer->addr a) i))
(define (stob-header a) (heap-ref (heap-pointer->addr a) -1))
(define (desc-stob? a) (desc-header-tag? (stob-type a)))
(define (binarray-stob? a) (binarray-header-tag? (stob-type a)))
(define (stob-type a) (header-tag (stob-header a)))
(define (stob-mutable? a hdr-tag)
  (= (header-tags-bin (stob-header a))
     (make-header-tags-bin hdr-tag \#t)))
(define (stob-size-in-bins a)
  (header-size-in-bins (stob-header a)))
(define (stob-size-in-cells a)
  (header-size-in-cells (stob-header a)))

Mutators

(define (template-set! v) (set! *template* v))
(define (codevector-set! v)
  (set! *codevector* (heap-pointer->addr v)))
(define (offset-set! v) (set! *offset* v))
(define (offset-inc! n) (set! *offset* (+ *offset* n)))
(define (value-set! v) (set! *value* v))
(define (env-set! v) (set! *env* v))
(define (cont-set! v) (set! *cont* v))
(define (spare1-set! v) (set! *spare1* v))
(define (spare2-set! v) (set! *spare2* v))
(define (spare3-set! v) (set! *spare3* v))
(define (gc-spare-set! v) (set! *gc-spare* v))
(define (symbol-table-set! v) (set! *symbol-table* v))
(define (stack-push! v)
  (assert! (addr< *low-heap-limit* *sp*)
           "stack-push!: argument stack overflow")
  (set! *sp* (addr+ *sp* -1))
  (stack-set! *sp* v))
(define (stack-pop!) (set! *sp* (addr+ *sp* 1)))
(define (stack-clear!) (set! *sp* *stack-base*))
(define (stack-restore! ret)
  (lambda (ptr)
    (stack-clear!)
    (let ((a (addr+ (heap-pointer->addr ptr) 4)))
      (do ((src (addr+ a (- (stob-size-in-cells ptr) 5))
                (addr+ src -1))
           (a a))
          ((addr< src a) (ret))
        (stack-push! (heap-ref src 0))
        ))))
(define (stob-desc-set! a i v)
  (heap-set! (heap-pointer->addr a) i v))
(define (stob-binarray-set! a i v)
  (heap-byte-set! (heap-pointer->addr a) i v))
(define (make-desc-stob! ret s m)
  (lambda (w) ((alloc! ret) ((make-desc-header s m) w) w)))
(define (make-binarray-stob! ret s m)
  (lambda (w)
    ((alloc! ret) ((make-binarray-header s m) w) (bins->cells w))))

(define (alloc-object-from-stack hdr)
(spare1-set! (addr->pointer *sp*))
(stack-push! hdr)
(set! *stack-base* *sp*)
(set! *low-heap-limit* (addr+ *stack-base* (- stack-size-in-words)))
)
(define *ret-make-desc-stob-from-stack!* (lambda () 0))
(define (make-desc-stob-from-stack! ret s m)
(lambda ()
  (let ((new-low-heap-limit
         (addr+ *sp* (- -1 stack-size-in-words)))
        (hdr ((make-desc-header s m) (stack-length)))
        )
    (if (addr< *hp* new-low-heap-limit)
        (begin
          (alloc-object-from-stack hdr)
          (ret))
        (begin
          (set! *ret-make-desc-stob-from-stack!* ret)
          (gc-spare-set! hdr)
          (garbage-collect! ret-make-desc-stob-from-stack!))
        ))))
(define (ret-make-desc-stob-from-stack!)
(alloc-object-from-stack (gc-spare-ref))
(*ret-make-desc-stob-from-stack!*))
(define (nh-alloc! hdr newhp)
(heap-set! *hp* 0 hdr)
(spare1-set! (addr->pointer (addr+ *hp* 1)))
(set! *hp* newhp))
(define *alloc-ret* (lambda () 0))
(define (alloc! ret)
(lambda (hdr size)
  (let ((newhp (addr+ *hp* (+ size 1))))
    (if (addr< newhp *low-heap-limit*)
        (begin
          (nh-alloc! hdr newhp)
          (ret))
        (begin
          (gc-spare-set! hdr)
          (set! *alloc-ret* ret)
          (garbage-collect! after-garbage-collect!)
          )))))

(define (after-garbage-collect!)
(let ((newhp
(addr+ *hp* (+ (header-size-in-cells (gc-spare-ref)) 1))))
(assert! (addr< newhp *low-heap-limit*)
   "Garbage collector could not reclaim enough space.")
(nh-alloc! (gc-spare-ref) newhp)
(*alloc-ret*)))

4.1.6 SBC Operational Semantics

We first define a function load that maps sbc stores to fsbcm stores. An sbc store is represented as the first store segment within an fsbcm store, and all sbc pointers within the sbc store are mapped to corresponding fsbc pointers. Let s^{sbc} be an sbc store. Then Let s^{sbc} be an sbc store. Then

relocate(cell, base) =^{def} ⟨ptr base + m⟩ if cell = ⟨ptr m⟩ cell otherwise

load(s^{sbc}, base) =^{def} s where s(base + i) = relocate(s^{sbc}(i), base) for all 0 ≤ i < #s^{sbc}

The fsbcm Loader L_{fsbcm} is defined to be a function that maps sbc programs to fsbcm initial states such that:

L_{fsbcm}(⟨s^{sbc} t^{sbc}⟩) =^{def}

⟨t, 0, c, d_{u}, g_{a}, g_{a′}, F^{desc}(⟨immediate empty-env⟩),

F^{desc}(⟨immediate halt⟩), s, g_{0}, g_{1}, g_{2}, g_{3}, d_{u}, d_{u}, 0, d_{u}⟩ if d_{u} = F^{desc}(⟨immediate unspecified⟩)

and size^{s} = heap-size-in-words
and size^{a} = stack-size-in-words

and g_{0} = ⟨0, #s^{sbc}, (size^{s} − size^{a})⟩ and g_{a} = ⟨(size^{s} − size^{a}), size^{s}, size^{s}⟩ and g_{1} = ⟨size^{s}, size^{s}, size^{s}⟩ and g_{2} = ⟨size^{s}, size^{s}, (2 ∗ size^{s} − size^{a})⟩ and g′_{a} = ⟨(2 ∗ size^{s} − size^{a}), 2 ∗ size^{s}, 2 ∗ size^{s}⟩ and g_{3} = ⟨2 ∗ size^{s}, 2 ∗ size^{s}, 2 ∗ size^{s}⟩ and s = load(s^{sbc}, g_{0}(0)) and t = relocate(t^{sbc}, g_{0}(0)) and S(t, s) = ⟨template #f c::o^{∗}⟩ The fsbcm Answer A_{fsbcm} is defined to be a partial function that maps fsbcm halt states Σ_{fsbcm}^{f} to natural numbers such that

A_{fsbcm}(⟨t, n, c, v, g_{a}, g_{a′}, u, k, s, g_{0}, g_{1}, g_{2}, g_{3}, r_{1}, r_{2}, r_{3}, r_{4}⟩) =^{def} m

if v = ⟨fixnum m⟩

Definition 44 Let P be an sbc program. Then L_{fsbcm}(P) is an initial state of the fsbcm. If R_{fsbcm}^{∗}(L_{fsbcm}(P)) is defined, then the meaning of program P as given by the sbc operational semantics is

O_{fsbcm}[[P]] =^{def} A_{fsbcm}(R_{fsbcm}^{∗}(L_{fsbcm}(P)))

Otherwise O_{fsbcm}[[P]] is undefined.

4.2 Correspondence Relation

Definition 45 We define a fsbcm state correspondence relation

≅⊂ gsbcmstate × fsbcmstate

as follows:

Let

\begin{matrix}Σ_{gsbcm} = ⟨t^{G}, n^{G}, c^{G}, v^{G}, a^{G}, u^{G}, k^{G}, s^{G}, r_{1}^{G}, r_{2}^{G}, r_{3}^{G}, r_{4}^{G}⟩, and \\ Σ = ⟨t, n, c, v, g_{a}, g_{a′}, u, k, s, g_{0}, g_{1}, g_{2}, g_{3}, r_{1}, r_{2}, r_{3}, r_{4}⟩ \end{matrix}

be a gsbcm state and fsbcm state respectively.

Then, Σ_{gsbcm} ≅ Σ holds if

• F^{desc}(t^{G}) = t

• F^{offset}(n^{G}) = n

• F^{desc}(c^{G}) = c

• F^{desc}(v^{G}) = v

• (g_{a}(1) + i) < g_{a}(2) for all 0 ≤ i < #a^{G}

• F^{desc}(a^{G}(i)) = s(g_{a}(1) + i) for all 0 ≤ i < #a^{G}

• F^{desc}(u^{G}) = u

• F^{desc}(k^{G}) = k • For all ⟨i, m⟩ ∈ ldom(s^{G}),

\begin{matrix}(g_{i}(0) + m) < g_{i}(1) & if i ∈ \{0, 2\} \\ g_{i}(1) ≤ (g_{i}(2) + m) & if i ∈ \{1, 3\} \end{matrix}

• For all ⟨i, m⟩ ∈ ldom(s^{G}),

F^{cell}(s^{G}(⟨i, m⟩)) = \begin{matrix}s(g_{i}(0) + m) & if i ∈ \{0, 2\} \\ s(g_{i}(2) + m) & if i ∈ \{1, 3\} \end{matrix}

• F^{desc}(r_{1}^{G}) = r_{1}

• F^{desc}(r_{2}^{G}) = r_{2}

• F^{desc}(r_{3}^{G}) = r_{3}

• F^{desc}(r_{4}^{G}) = r_{4}

4.3 Establishing State Correspondence

Lemma 46 The gsbcm Loader and the fsbcm Loader map sbc programs to initial states that are related by the state correspondence relation. That is, if P = ⟨s^{sbc} t^{sbc}⟩ is an sbc program, then

L_{gsbcm}(P) ≅ L_{fsbcm}(P)

Proof: All cases are immediate from the definitions of the loaders and state correspondence except for the following:

1. For all ⟨i, m⟩ ∈ ldom(s^{G}),

\begin{matrix}(g_{i}(0) + m) < g_{i}(1) & if i ∈ \{0, 2\} \\ g_{i}(1) ≤ (g_{i}(2) + m) & if i ∈ \{1, 3\} \end{matrix}

By definition of L_{gsbcm}, if ⟨i, m⟩ ∈ ldom(s^{G}) then i = 0 and 0 ≤ m < #s^{sbc}. But by definition of L_{fsbcm}, g_{0}(1) = g_{0}(0) + #s^{sbc}, and so the condition holds.

2. For all ⟨i, m⟩ ∈ ldom(s^{G}),

F^{cell}(s^{G}(⟨i, m⟩)) = \begin{matrix}s(g_{i}(0) + m) & if i ∈ \{0, 2\} \\ s(g_{i}(2) + m) & if i ∈ \{1, 3\} \end{matrix}

By definition of L_{gsbcm}, if ⟨i, m⟩ ∈ ldom(s^{G}) then i = 0 and 0 ≤ m < #s^{sbc}. If s^{sbc}(m) = ⟨ptr l⟩ then

s^{G}(⟨0, m⟩) = relocate^{G}(⟨ptr l⟩) = ⟨ptr ⟨0, l⟩⟩
s(g_{0}(0) + m) = relocate(⟨ptr l⟩, g_{0}(0)) = ⟨ptr g_{0}(0) + l⟩

But F^{cell}(⟨ptr ⟨0, l⟩⟩) = ⟨ptr g_{0}(0) + l⟩ by definition.

If s^{sbc}(m) ≠ ⟨ptr l⟩ then

s^{G}(⟨0, m⟩) = relocate^{G}(s^{sbc}(m)) = s^{sbc}(m)
s(g_{0}(0) + m) = relocate(s^{sbc}(m), g_{0}(0)) = F^{cell}(s^{sbc}(m))

The result thus holds trivially.

□

4.4 Preserving State Correspondence

Lemma 47 Let Σ_{i}^{G} and Σ_{i} be gsbcm and fsbcm initial states respectively. If Σ_{i}^{G} ≅ Σ_{i}, then

1. If R_{fsbcm}^{∗}Σ_{i} is defined, then so is R_{gsbcm}^{∗}Σ_{i}^{G}.

2. If R_{gsbcm}^{∗}Σ_{i}^{G} and R_{fsbcm}^{∗}Σ_{i} are both defined, then R_{gsbcm}^{∗}Σ_{i}^{G} ≅ R_{fsbcm}^{∗}Σ_{i}.

Proof: Each action rule of the gsbcm and fsbcm is expressed as the composition of the microcode functions and auxiliary functions. Each of these fsbcm functions is less defined than the corresponding gsbcm function. Thus each action rule is less defined than the corresponding gsbcm action rule and hence so is the union and transitive closure of the action rules.

By definition, if an fsbcm microcode or auxiliary function is defined on an argument, it returns the same value as the corresponding gsbcm function. Thus each action rule has this property, and hence so does the union and transitive closure of the action rules.

□

4.5 Correspondence of Final Answers

The following lemma asserts that the gsbcm and fsbcm answer functions map corresponding states to equal natural numbers.

Lemma 48 Let Σ_{f}^{G} and Σ_{f} be gsbcm and fsbcm halt states respectively. If Σ_{f}^{G} ≅ Σ_{f}, then A_{gsbcm}(Σ_{f}^{M}) = A_{fsbcm}(Σ_{f}).

Proof: Let v^{G} and v be the value registers of Σ_{f}^{G} and Σ_{f} respectively. Since Σ_{f}^{G} ≅ Σ_{f}, we have by definition of state correspondence that v^{G} and v are related (i.e. F^{desc}(v^{G}) = v). By definition of F^{desc}, if v^{G} = ⟨fixnum m⟩ then v = ⟨fixnum m⟩ and so A_{gsbcm}(Σ_{f}^{M}) = A_{fsbcm}(Σ_{f}) = m. If v^{G} is not of the form ⟨fixnum m⟩ then neither is v, and so A_{gsbcm}(Σ_{f}^{M}) and A_{fsbcm}(Σ_{f}) are both undefined.

□

4.6 Correspondence of Semantics

We can now prove the main theorem of this chapter.

Theorem 49 If the fsbcm operational semantics assigns a meaning to an sbc program, then the gsbcm operational semantics assigns the same meaning to the program. That is, if

O_{fsbcm}^{sbc}[[P]]

is defined, then

O_{fsbcm}^{sbc}[[P]] = O_{gsbcm}^{sbc}[[P]]

Proof: Follows immediately from Lemmas 46, 47, and 48.

□

[figure: low heap; free space; arg stack; cont stack; upper heap; stack limit; stack base; heap pointer; stack pointer]

Figure 5: Memory Layout

A A New Storage Layout

The Vlisp VM currently uses two areas for heap allocation and a separate area for the argument stack. All stored objects are heap allocated. We think can verify a new organization for storage which greatly reduces the number of garbage collections.

The layout (Figure 5) uses just two equal sized areas, one of which is active at any time (except during garbage collection). All stack and heap allocation performed in the same area. All stored objects other than continuations are allocated in the low heap which grows upward. The stack grows downward and garbage collection in invoked when the stack and the low heap meet.

The new version of the MAKE-CONT instruction pushes registers on the stack, pushes a continuation header on the stack, adjusts the stack base and stack pointer to be at the newly allocated continuation, and finally updates the continuation register. The argument stack is not copied although we found this savings to be small.

The new version of RETURN does the old actions if the continuation is not in the continuation stack. Otherwise, the continuation stack is popped. This is where the real saving comes because we garbage collect many fewer continuations. When our compiler compiles itself, it now uses 90 GC’s instead of 250.

Call-with-current-continuation is implemented by moving the stack limit to the current stack base. All the continuations on the stack now behave as if the were heap allocated.

The garbage collector copies the argument stack to the top of the new area, and traces the stack and the registers. After a GC, all continuations are in the low heap. One could try to preserve the continuation stack during GC, but it is too complicated for too little savings.

References

[1] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp byte-code compiler. M 92B092, The MITRE Corporation, 1992.

[2] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp flattener. M 92B094, The MITRE Corporation, 1992.

[3] Dino P. Oliva and Mitchell Wand. A verified compiler for pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February 1992.

[4] J. D. Ramsdell, W. M. Farmer, J. D. Guttman, L. G. Monk, and V. Swarup. The vlisp PreScheme front end. M 92B098, The MITRE Corporation, 1992.

[5] V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk, and J. D. Ramsdell. The vlisp image builder. M 92B096, The MITRE Corporation, 1992.

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