Correctness of Procedure Representations in Higher-Order Assembly Language

Mitchell Wand^{∗}

College of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA wand@{corwin,flora}.ccs.northeastern.edu

Abstract

Higher-order assembly language (HOAL) generalizes combinator-based target languages by allowing free variables in terms to play the role of registers. We introduce a machine model for which HOAL is the assembly language, and prove the correctness of a compiler from a tiny language into HOAL. We introduce the notion of a λ-representation, which is an abstract binding operation, show how some common representations of procedures and continuations can be expressed as λ-representations. Last, we prove the correctness of a typical procedure-calling convention in this framework.

1 Introduction

The concept of higher-order assembly language (HOAL) was introduced by [1, 7], who used λ-terms in continuation-passing style as an abstract assembly language. They showed how this technique could be used to build sophisticated compilers. In this paper we make two contributions to this model:

First, we introduce a formal machine model to provide an operational semantics for HOAL code. We show how the action of this machine can be derived from the reduction sequence of the HOAL code, and how its action mimics the behavior of typical target machines. This provides a formal basis to replace what had been only a heuristic connection between HOAL code and real assembly code.

Second, we introduce the concept of λ-representations as a technique for showing the correctness of various procedure-representation tactics. Such tactics are a crucial part of CPS compiling techniques. We show that λ-representations are powerful enough to model typical representations, such as closures, and typical procedure call instructions, such as jsr and rts. We then prove a conservative extension theorem which guarantees that the results of our computations are independent of the choice of representation.

∗Work supported by the National Science Foundation and DARPA under grant numbers CCR-8801591, CCR-9002253, and CCR-9014603.

2 Higher-Order Assembly Language and its Machine

In this section, we show, following [1, 7], how the idea of higher-order abstract syntax can be adapted to assembly language. We call the resulting language, or class of languages, higher-order abstract assembly language, or HOAL. We then introduce an abstract machine that uses this higher-order abstract assembly language as its machine language, and we show how the behavior of this machine can be deduced from the reduction behavior of HOAL terms.

A higher-order abstract syntax [11], also sometimes called a Church encoding [4], is a representation of the abstract syntax of a phrase as a λ-term in which the binding relationships in the source phrase are represented using the binding relationships in the λ-term. For example, a quantified formula ∀x.A in first-order logic might be represented as ∀(λx.A). This shows how x is bound in A.

To adapt this idea to assembly language, consider a simple addition instruction add r_{1}, r_{2}, r_{3} , which puts the sum of the contents of registers r_{1} and r_{2} in register r_{3}, and goes on to the next instruction. Since we must take control flow into account we consider instead the instruction stream add r_{1}, r_{2}, r_{3}; C beginning with our addition instruction. It is clear that r_{1} and r_{2} are “free” in this sequence, because the meaning of the sequence depends on their values. The register r_{3}, however, is not free, since it is set rather than referenced. In fact, the addition instruction binds r_{3} for the remainder of the sequence C. Therefore we define the abstract syntax of add r_{1}, r_{2}, r_{3}; C to be

add r_{1} r_{2} (λr_{3}.C)

for some combinator add. Furthermore, given this syntax, it is reasonably clear that the semantics of add ought to be

add = λxyκ.κ(x + y)

Similarly, the abstract syntax for a move instruction, whose concrete syntax is move r_{1}, r_{2}; C, should be move r_{1}(λr_{2}.C), and its semantics should be move = λxκ.κx. Last, a halt instruction has abstract syntax halt r and its semantics is halt = λx.x. This gives us a higher-order abstract assembly language given by the grammar

C ::= halt r | move r_{1}(λr_{2}.C) | add r_{1}r_{2}(λr_{3}.C)

where r, r_{1}, etc., range over register names (λ-variables). We call this the language of HOAL terms.

If this set of λ-terms is an assembly language, what is the machine which executes it? We next show how to derive such a machine from the abstract syntax and the definitions of the combinators.

The state of the machine will be a pair, written ⟨C, ρ⟩, consisting of an HOAL term C and a substitution ρ mapping λ-variables (including the free variables of C) to constants or closed abstractions (what [12] calls closed values). The substitution represents the contents of the target machine’s registers.

The state ⟨C, ρ⟩ is a representation of the term Cρ obtained by actually performing the substitution ρ on C. The machine operates by simulating the reduction of Cρ. By using the semantics of the combinators, we can work out the reduction rules for the machine for each possible state ⟨C, ρ⟩. In this way, we define the action of the machine as a rewriting relation ⇒ on machine states such that if ⟨C, ρ⟩ ⇒ ⟨C′, ρ′⟩, then Cρ reduces to C′ρ′. Thus, given a denotational semantics for our machine instructions, we derive an operational semantics by inheriting the operational semantics of the λ-calculus.

Let us first fix some notation. We write substitution from left to right: Mρ_{1}ρ_{2} represents (Mρ_{1})ρ_{2}, and we write xρ for the value of ρ on the variable x. We write ρ_{−x} for the substitution ρ with x deleted from its domain.

The key observation, due to [3], is that the “structure-sharing” representation ⟨C, ρ⟩ allows us to simulate substitution without ever actually performing it. This is expressed as follows:

Lemma 1 Let V be a closed value and ρ be a closed substitution. Then

((λx.M)V)ρ = M(ρ[x := V])

Proof: We calculate:

((λx.M)V)ρ ≡ ((λx.M)ρ)V  (definition of substitution)
≡ ((λx.(Mρ_{−x}))V) (definition of substitution)
→ (Mρ_{−x})[x := V]  (β-reduction)
≡ M(ρ[x := V])  (definition of substitution)

Here ≡ denotes syntactic equivalence, obtained by working out the definition of substitution, and → denotes reduction. Note that we do not need to worry about variable capture since the range of ρ contains only closed terms. QED

Thus we can simulate substitution and β-reduction by merely manipulating substitutions.

For example, let us consider reducing the state ⟨add r_{1}r_{2}(λr_{3}.C), ρ⟩

⟨add r_{1}r_{2}(λr_{3}.C), ρ⟩ ≡ add(r_{1}ρ)(r_{2}ρ)((λr_{3}.C)ρ)
→ ((λr_{3}.C)ρ)((r_{1}ρ) + (r_{2}ρ)) (definition of add)
→ C(ρ[r_{3} := ((r_{1}ρ) + (r_{2}ρ))])  (by Lemma 1)

Therefore we define the action of the machine on the add instruction as

⟨add r_{1}r_{2}(λr_{3}.C), ρ⟩ ⇒ ⟨C, ρ[r_{3} := ((r_{1}ρ) + (r_{2}ρ))]⟩

which simulates the reduction of the term, as desired. Note that the reduction sequence for this closure does just what an addition instruction normally does: it goes on to execute the code sequence C in a substitution where r_{3} is bound to the sum of the contents of r_{1} and r_{2}. Here ρ is single-threaded [13], so that we can model this operation by a destructively-updated register file.

The halt and move instructions similarly turn out to do the expected things. By using the semantics for the halt and move combinators, we calculate as follows:

(halt r)ρ → rρ
(move r_{1}(λr_{2}.C))ρ → ((λr_{2}.C)ρ)(r_{1}ρ)
→ C(ρ[r_{2} := ρr_{1}])

Thus the machine action for these instructions should be:

⟨halt r, ρ⟩  ⇒ rρ
⟨move r_{1}(λr_{2}.C), ρ⟩ ⇒ ⟨C, ρ[r_{2} := ρr_{1}]⟩

The halt instruction halts, returning the value in the specified register, and the move instruction copies the value in register r_{1} to register r_{2}.

3 Defining New Machine Instructions

In general, an instruction that applies f to the contents of registers r_{1}, r_{2}, and r_{3}, and puts the result in register r_{4} will have the abstract syntax

op r_{1}r_{2}r_{3}(λr_{4}.C)

and its semantics should be

op = λv_{1}v_{2}v_{3}κ.κ(fv_{1}v_{2}v_{3}))

This easily generalizes to multiple continuations (for branching instructions, or even 0 continuations, as in halt), setting multiple registers, or dependence on certain fixed registers. For example, consider an instruction br that branches if the contents of r_{1} is non-negative and leaves some information (fr_{1}) in the fixed register cc. This could be expressed by using the abstract syntax

br r_{1}(λcc.C_{1})(λcc.C_{2})

with semantics

br = λvκ_{1}κ_{2}.(v ≥ 0) → κ_{1}(fv), κ_{2}(fv)

By using continuation semantics, we need not postulate an additional stack mechanism in the machine architecture, beyond what is explicitly manipulated in the instructions.

This recipe for specifying both semantics and the format of an instruction makes it easy to incorporate new machine instructions into this technique. We next define some instructions that will be useful for our development.

movem r (λr_{1} … r_{n}.C) decomposes the record contained in register r and places the results in registers r_{1}, …, r_{n}. This is inspired by the movem instruction on the MC 68000 series. It can be tediously defined as a family of combinators movem_{n} using recorddecomposition primitives; for our purposes, however, its properties are summarized by the identity

movem[u_{1}, …, u_{n}](λu_{1} … u_{n}.C) = C

where [−, …, −] denotes a record-formation operation. We can similarly define recordextraction operations move .i r (λr′.C) that extract the i-th field from a record.

push r_{1}r_{2}(λr_{2}.C) is defined by push = λvsκ.κ(v :: s), where the :: represents a stack push operation. push pushes the value in register r_{1} onto the stack contained in register r_{2}. The fact that this instruction both uses and sets r_{2} is reflected in the two occurrences of r_{2} in the abstract syntax.

pop r_{1}(λr_{2}r_{1}.C) is defined by pop = λsκ.κ(first s)(rest s); it pops a stack contained in register r_{1}, copying the top element into register r_{2}. We assume that a register can contain a stack; considerations of pointer manipulation are left to another layer, as in [6].

Similarly, we can move multiple registers on and off the stack with push- and popmultiple instructions, with abstract syntax

pushm r_{1} … r_{n}r(λr.C)

and

popm r(λr_{1} … r_{n}r.C)

The semantics of pushm is given by

pushm r_{1} … r_{n}rκ = κ(r_{n} :: …:: r_{1} :: r)

and popm satisfies the identity

popm(r_{n} :: …:: r_{1} :: r)(λr_{1} … r_{n}r.C) = C

by analogy with movem.

4 Compiling Addition Expressions

The goal of a compiler is to produce an HOAL term which is equal (using the definitions of the combinators and λ-conversion) to the semantics of the source program. This is a generalization of the principle stated for a target language of combinators in [17, 19]; here the free variables in HOAL terms play the role of machine registers.

To illustrate this idea, we write a tiny compiler with HOAL as its target. Our source language will be addition expressions, given by the grammar

⟨pgm⟩ ::= ⟨exp⟩
⟨exp⟩ ::= ⟨var⟩
::= (⟨exp⟩ + ⟨exp⟩)

We model both the semantics and the compiler as syntax-directed transducers, taking phrases of the source language as input and producing untyped λ-terms in continuationpassing style as output. As we did for assembly language, we use a Church coding instead of a Frege-style environment coding [21], translating variables in the source language into free variables in the λ-terms. The resulting semantics looks very much like Plotkin’s algorithm for conversion to continuation-passing style [12].

\begin{aligned}E_{pgm}[[e]] & ≡ E[[e]](λv.v) \\ E[[I]] & ≡ λκ.κr_{I} \\ E[[(M + N)]] & ≡ λκ.E[[M]](λm.E[[N]](λn.κ(m + n))) \end{aligned}

Here r_{I} is a λ-variable associated with source identifier I, and κ, m, and n are fresh variables.

Following [5], our compiler will take two arguments M and K, where M is the source term to be compiled and K is the sequel, the target code to be executed following the code for M, represented as a λ-term of the form λv.C, where C is an HOAL term. The output C[[M]]K will be a λ-term that must meet the following two requirements for correctness:

C[[−]]− is correct iff

1. C[[M]]K = E[[M]]K, where equality means interconvertibility under the rules of the λ-calculus, and

2. if C is an HOAL term, then C[[M]](λv.C) is also an HOAL term.

Note that C[[−]]− is a binary (mixfix) operator, and not an application; so the lefthand side of property (1) is the result of applying transformation C[[−]]− to M and K, while the right-hand side is a λ-calculus application, whose operator is the term E[[M]] and whose operand is the term K.

The compiler is very simple:

C_{pgm}[[e]]  ≡ C[[e]](λv. halt v)
C[[I]]K  ≡ move r_{I}K
C[[(M + N)]]K ≡ C[[M]](λm.C[[N]](λn. add mnK))

where m and n are fresh.

Theorem 1 This compiler is correct.

Proof: This is an easy structural induction. We prove only the case of addition expressions.

C[[(M + N)]]K ≡ C[[M]](λm.C[[N]](λn. add mnK))
= E[[M]](λm.C[[N]](λn. add mnK)) (IH(M))
= E[[M]](λm.E[[N]](λn. add mnK)) (IH(N))
= E[[M]](λm.E[[N]](λn.K(m + n))) (definition of add)
= E[[(M + N)]]K

The other cases, and the proof of condition (2), is similar. QED The program (I + J) + K is compiled as follows:

C[[(I + J) + K]](λv. halt v)
≡ C[[(I + J)]](λu.C[[K]](λw. add uw(λv. halt v)))
≡ C[[(I + J)]](λu. move r_{K}(λw. add uw(λv. halt v)))
≡ C[[I]](λa.C[[J]](λb. add ab(λu. move r_{K}(λw. add uw(λv. halt v)))))
≡ move r_{I}(λa.move r_{J}
(λb. add ab(λu. move r_{K}(λw. add uw(λv. halt v)))))

We can see the correspondence to concrete syntax by writing this term as follows:

move r_{I}λa. ; move r_{J}λb. ; add abλu. ; move r_{K}λw. ; add uwλv. ; halt v

This corresponds to the concrete syntax

                        move rI, ra
                        move rJ, rb
                        add  ra, rb, ru
                        move rK, rw
                        add  ru, rw, rv
                        halt rv

Note that, unlike the situation in [17, 18, 19], there was no need to use associative rules or to rotate trees; the code was generated directly.

Our specifications for a correct compiler enable the compiler writer to use whatever cleverness he or she wishes, so long as the resulting abstract syntax is interconvertible with the code above. For example, by reducing the move instructions, we can generate

add r_{I}r_{J}(λu. add ur_{K}(λv. halt v))

corresponding to

                        add rI, rJ, ru
                        add ru, rK, rv
                        halt rv

Our goal is not to dictate a compiler strategy (e.g., whether this optimized code is generated immediately or by transformations), but rather to give a method for proving the correctness of the chosen strategy. We now consider some strategies for a particular problem: the representation of procedures.

5 λ-Representations

The semantics given in the previous section suggests the following semantics for procedures:

\begin{aligned}E[[(proc I.M)]] & ≡ λκ.κ(λr_{I}κ.E[[M]]κ) \\ E[[(MN)]] & ≡ λk.E[[M]](λm.E[[N]](λn.mnκ)) \end{aligned}

Here any occurrence of I in M generates an occurrence of r_{I} in E[[M]], which is bound by the λr_{I}. However, we want the compiled code for this procedure to return a closure record, not a λ-abstraction. To solve this problem, we introduce abstract binding operations, which enable us to abstract any desired binding operator, much as combinators abstract any desired combination.

We define a λ-representation to be a syntactic abstraction of a λ-expression. More precisely,

A λ-representation consists of a syntactic operation abs (taking a variable and a λ-term and producing a λ-term) and a combinator Ap, satisfying the following properties:

1. x is not free in abs x.M.

2. Ap (abs x.M) = λx.M (where = means λ-convertibility).

It is easy to give some examples of λ-representations:

1. The ordinary representation, with abs x.M ≡ λx.M, and Ap ≡ λf.f.

2. The combinator representation, with abs x.M ≡ λ^{∗}x.M (where λ^{∗}x.M denotes some simulation of λ-abstraction e.g. [2, Def. 7.1.5] or [16]), and Ap ≡ λf.f again.

3. A closure representation, in which a λ-abstraction is represented as a record consisting of a closed λ-term and a record of the free variables. This might be expressed as something like

\begin{aligned}abs x.M & ≡ [λ[u_{1}, …, u_{n}]x.M, [u_{1}, …, u_{n}]] \\ Ap & ≡ λf.(f.1)(f.2) \end{aligned}

where the free variables of M are u_{1}, …, u_{n}, x, and we have slightly extended our lambda-calculus to include [− …, −] as either a record-forming or pattern-matching operation, and (−.1) and (−.2) as selectors.

To apply this idea to a typical language with procedures, we observe that we do not really care whether procedures are represented as λ-abstractions or not; all that matters is that their representations can be made to behave like λ-abstractions. The same fact holds for continuations that are passed to procedures. Therefore we use two λ-representations: one for procedures (denoted abs, Ap_{p}), and one for continuations (denoted cont, Ap_{c}).

In each case, we know exactly where this behavior is required: for procedures, it is required at procedure call time, and for continuations, it is required at procedure return time. This leads to the following generalization of Plotkin’s algorithm [12]:

E[[(proc I.M)]] = λκ.κ(abs r_{I}.λκ.E[[M]](λv. Ap_{c} κv))
E[[(MN)]] = λκ.E[[M]](λm.E[[N]](λn. Ap_{p} mn(cont v.κv)))

(It turns out that it suffices to have a single abs for r_{I}, and it is not necessary to replace the λκ by abs κ.)

Part of the compiler design is choosing a representation for abs and and cont. We can use different versions of abs freely in the same compiler, so long as they share the same Ap. This is an important idea, but we will not explore it further here. We will show two designs: one using the ordinary representation for abs and cont, and one using a “continuation-passing, closure-passing style” [1].

6 A Simple Procedure Design

For example, the conventional version of Plotkin’s algorithm is recaptured by using the ordinary representation for abs and cont.

To compile these constructs, we must introduce suitable combinators so that the right-hand sides match the general form of the compiler, in which every application is performed by a combinator, and in which every recursive call to the compiler (or semantics) has an abstraction as its second argument. We can do this by introducing the combinators

close = λxκ.κx
apply = λfaκ.faκ
return = λr_{1}r_{2}.r_{1}r_{2}

With these combinators, we can compile procedure creations and applications as follows:

C[[(proc I M)]]K ≡ close(λr_{I}κ.C[[M]](λv. return κv))K
C[[(MN)]]K  ≡ C[[M]](λf.C[[N]](λa. apply faK))

where all the indicated variables are fresh. It is now easy to confirm, by structural induction, that this compiler is still correct.

The formats for our three additional instructions are

C ::= close(λr_{1}r_{2}.C)(λr_{3}.C′)
| apply r_{1}r_{2}(λr_{3}.C)
| return r_{1}r_{2}

By examining the definitions of the combinators, we can now work out the behavior of the machine on these instructions. The close instruction creates a closure of two arguments which represents a procedure and stores the closure in the target register.

\begin{aligned}(close(λr_{1}r_{2}.C)(λr_{3}.C′)ρ) & → ((λr_{3}.C′)ρ)((λr_{1}r_{2}.C)ρ) \\ & → C′(ρ[r_{3} := ((λr_{1}r_{2}.C)ρ)]) \end{aligned}

Here we assume that we do not actually carry out the substitution (λr_{1}r_{2}.C)ρ. Instead, we assume that the machine copies the contents of the current register set into some data structure (a closure). This leaves the variable ρ single-threaded so we may continue to update it destructively.

The apply instruction invokes such a procedure object. It creates a closure to serve as the continuation, and applies the procedure object to the argument and the continuation. In the following, assume that r_{1}ρ = (λxκ.C′)ρ′. Then we reduce as follows:

(apply r_{1}r_{2}(λr_{3}.C))ρ → (r_{1}ρ)(r_{2}ρ)((λr_{3}.C)ρ)
→ ((λxκ.C′)ρ′)(r_{2}ρ)((λr_{3}.C)ρ)
→ C′(ρ′[x := r_{2}ρ; κ := ((λr_{3}.C)ρ)])

Thus the body of the procedure is executed, with the actual parameter placed in the register that the procedure expects, and the continuation (with the caller’s registers saved) placed in the callee’s continuation register.

The return instruction returns from such a procedure. In the following, assume that in ρ, r_{1} contains the continuation (λr_{3}.C′)ρ′.

(return r_{1}r_{2})ρ → (r_{1}ρ)(r_{2}ρ)
→ ((λr_{3}.C′)ρ′)(r_{2}ρ)
→ C′(ρ′[r_{3} := r_{2}ρ])

Thus the caller’s registers are restored, and the result placed in r_{3}.

We can summarize the behavior of our machine as follows:

⟨move r_{1}(λr_{2}.C), ρ⟩  ⇒ ⟨C, ρ[r_{2} := ρr_{1}]⟩
⟨add r_{1}r_{2}(λr_{3}.C), ρ⟩  ⇒ ⟨C, ρ[r_{3} := ((ρr_{1}) + (ρr_{2}))]⟩
⟨halt r, ρ⟩  ⇒ rρ
⟨close(λxκ.C)(λr.C′), ρ⟩ ⇒ ⟨C′, ρ[r := ((λxκ.C)ρ)]⟩
⟨apply r_{1}r_{2}(λr_{3}.C), ρ⟩ ⇒ ⟨C′, ρ′[x := ρr_{2}; κ := ((λr_{3}.C)ρ)]⟩
(where r_{1}ρ = (λxκ.C′)ρ′)
⟨return r_{1}r_{2}, ρ⟩  ⇒ ⟨C′, ρ′[r_{3} := r_{2}ρ]⟩
(where r_{1}ρ = (λr_{3}.C′)ρ′)

7 Explicitly Closed Procedures

The instructions of the machine in the previous section need to save and restore an entire register state (like the calls and ret instructions on a VAX). While some machines have such instructions, it may still take some cleverness on the part of the compiler-writer to implement this abstract machine. One might argue that this is a virtue by leaving the compiler-writer more latitude (this is the point of view taken in [14]). On the other hand, we are concerned with finding a theory which can be used to justify the choices made by compiler-writers. We wish to study denotationally the tricks that are used to save and restore registers from a stack, represent procedures as closures, etc. For this reason, we next study a different representation technique.

We will use “continuation-passing, closure-passing style” [1], in which a procedure is represented by a record f whose first component (f.1) is a closed term (executable code). When the procedure is invoked, the executable portion is passed three items of data: the entire closure f, the argument, and the continuation. Each procedure body begins with a preamble that extracts the procedure’s local variables from the closure record and puts them in the registers where they belong, and that puts the argument in the register where the procedure body expects to find it.

As before, let the free variables of M be u_{1}, …, u_{n} and x. We can write down our representation as

abs x.M ≡ [(λ e a s .movem e (λdu_{1} … u_{n}.
move a (λx.
M s))),
u_{1}, …, u_{n}]
Ap_{p} = λf.(f.1)f

Here d is a fresh variable that receives the value of executable code in the closure, which is not used further in this representation. A cleverer representation might use the fact that Ap_{p} is passed the entire closure, rather than just the saved variables, to bind a register to the closure itself in order to handle recursion.

Theorem 2 This is a correct λ-representation.

Proof: The free-variable condition is clearly true. To verify the second condition, recall that abs x.M is a record, which we may abbreviate as [C, u_{1}, …, u_{n}]. Then we calculate:

Ap_{p} (abs x.M)
= (λ e a s . movem e (λdu⃗. move a (λx.M s)))[C, u_{1}, …, u_{n}]
= λ a s . movem [C, u_{1}, …, u_{n}] (λdu⃗. move a (λx.M s))
= λ a s . move a (λx.M s)
= λx s . move x (λx.M s)
= λx s .M s
= λx.M

QED

What is the significance of the fixed registers in this example? They establish standard registers in which to pass data to the procedure. To see how this works, let ρ be register state such that e ρ contains a closure, that is, a record r whose first component r.1 is a closed term of the form (λ e a s .C)^{o}. We use the superscript (−)^{o} as an indication that (λ e a s .C) is closed. Then we have

(Ap_{p} e a s)ρ → (e .1)ρ e ρ a ρ s ρ
→ (λ e a s .C)^{o} e ρ a ρ s ρ
→ Cρ

Hence, if the closure, argument, and continuation are put in registers e, a, and s, then calling the procedure requires no additional data movement, but only a jump to the body of the procedure. We will see how to take advantage of this in the next section.

To compile abstractions using this representation, we first substitute our choice for abs in the semantics. We then introduce suitable combinators, as we did in our previous design. Thus we have:

E[[(proc I.M)]] = λκ.κ(abs r_{I}.λκ.E[[M]](λv. Ap_{c} κv))
= λκ.κ([(λ e a s .movem e (λdu_{1} … u_{n}.
move a (λr_{I}.
(λκ.E[[M]](λv. Ap_{c} κv)) s))),
u_{1}, …, u_{n}])
= λκ.κ([(λ e a s .movem e (λdu_{1} … u_{n}.
move a (λr_{I}.
E[[M]](λ a . Ap_{c} s a)))),
u_{1}, …, u_{n}])

To produce a compiler action for this production, we introduce two new instructions: The first is the move-closure instruction movec, whose abstract syntax is given by

movec (λ e a s .C)^{o}[r_{1}, …, r_{n}](λr′.C′). movec forms a record consisting of its first argument (a pointer to some code) and the contents of the registers r_{1}, …, r_{n}, leaving (a pointer to) the record in the register r′. It is defined as movec v[v_{1}, …, v_{n}]κ = κ[v, v_{1}, …, v_{n}].

The second is the rts instruction. Its abstract syntax is given by C ::= rts s a, its concrete syntax is given by just rts, since all its fields are fixed, and its semantics is given by: rts = λsa. Ap_{c} sa.

Given these instructions, we can define the compiler action as

C[[(proc I.M)]](λr.C) = movec (λ e a s .movem e (λdu_{1} … u_{n}.
move a (λr_{I}.
C[[M]](λ a . rts s a)))),
[u_{1}, …, u_{n}])
(λr.
C)

It is easy to show, by simply expanding the definitions of the instructions, that this produces a HOAL term equal to the term given by the semantics.

We next proceed to the representation of continuations. Continuations correspond to control stacks, so we want to represent them as stacks. We will use the register s to contain (or point to) the stack representing the current continuation. Therefore we build a new continuation by pushing additional data on the top of s. In particular, a continuation is represented as a stack consisting of a closed HOAL term (a pointer to a return address), the saved registers, followed by the previous continuation. The code at the return address begins with a preamble (the preamble to the continuation, which will become the postamble to the procedure call!) that restores the local registers from the stack.

We can write this as follows, writing :: for a push operation:

cont x.M ≡ ((λ s a .popm s λu⃗ s .
move a λx.
M)
:: u_{1} :: …:: u_{n} :: s)
Ap_{c} = λk.(first k)(rest k)

where the free variables of M are x, u⃗, and s. Again, it is easy to verify that this is a correct λ-representation.

8 Compiling Procedure Calls

Our goal is to deduce what the compiler should do for a procedure call. By our correctness criterion, C[[(MN)]]K should produce an HOAL term which is convertible to E[[(MN)]]K. We begin by applying the structural induction hypothesis to E[[(MN)]]K:

E[[(MN)]]K = E[[M]](λm.E[[N]](λn. Ap_{p} mn(cont v.Kv)))
= C[[M]](λm.C[[N]](λn. Ap_{p} mn(cont v.Kv))) (by IH)

Hence, the induction step will succeed if we define

C[[(MN)]]K = C[[M]](λm.C[[N]]λn.C_{1})  (1)

for some HOAL term C_{1} such that

C_{1} = Ap_{p} mn(cont v.Kv)  (2)

To find C_{1}, we first expand (2) using the definition of cont and Ap_{p}:

C_{1} = Ap_{p} mn(cont v.Kv)
= (m.1)mn(C_{2}^{o} :: u_{1} :: …:: u_{n} :: s)
where C_{2}^{o} = λ s a .popm s (λu⃗ s .
move a λx.
K)
= pushm u⃗ s (λ s(m.1)mn(C_{2}^{o} :: s))

Here again we use the superscript (−)^{o} as an indication that C_{2} is closed.

We next move the various quantities into the registers e and a to take advantage of the fixed-register feature of our procedure representation. This gives us

C_{1} = pushm u⃗ s λ s .
move mλ e .
move nλ a .
move .1 e λm.
(m e a(C_{2}^{o} :: s))

Here we use the move .1 instruction, defined in Section 2, to move the first component of the closure into register m.

In order to reduce the last line of this formula to HOAL, we define a new instruction jsr, whose semantics is given by

jsr = λπeasκ.πea(κ :: s)

and whose abstract syntax is given by

C ::= jsr r e a s (λ s a .C)^{o}

where (−)^{o} again indicates that the last argument must be closed. Since all but the r is fixed, the concrete syntax can be given by: C ::= jsr r; C.

Now we can use this instruction to finish the derivation of C_{1}. We also use the assumption, from the compiler correctness criterion, that K is a λ-abstraction of the form λx.C_{3}.

C_{1} = pushm u⃗ s λ s . move mλ e . move nλ a . move .1 e λm. (m e a(C_{2}^{o} :: s))

= pushm u⃗ s λ s . move mλ e . move nλ a . move .1 e λm. jsr m e a s C_{2}^{o}

= pushm u⃗ s λ s . move mλ e . move nλ a . move .1 e λm. jsr m e a s λ s a popm s λu⃗ s . move a λx. C_{3}

Thus we have derived a procedure-calling sequence: we save whatever registers are needed on the stack, put the closure and argument to be passed in the right places, and then branch to the subroutine; on return we restore the saved registers, put the returned value in the place that the continuation expects to find it, and then continue with the remainder of the code. By using this HOAL term C_{1} in (1) above we get a compiling scheme which is guaranteed to be correct. This calling sequence can be optimized by doing a finer analysis of the free variables to eliminate unnecessary move instructions, but we will not do so here.

One thing remains to be done: we need to derive the action of the machine on the jsr and rts instructions. To do this, assume that rρ is a closed term of the form (λ e a s .C′)^{o} (that is, the executable portion of a closure, as given by the λ-representation adopted in Section 7). Then we calculate:

⟨jsr r e a s(λ s a .C)^{o}, ρ⟩ → (rρ)(e ρ)(a ρ)(s ρ)(λ s a .C)^{o} → (λ e a s .C′)^{o}(e ρ)(a ρ)(s ρ)(λ s a .C)^{o} → C′(ρ[s := ((λ s a .C)^{o} :: (ρ s))])

Hence we define the machine action as

⟨jsr r e a s(λ s a .C)^{o}, ρ⟩ ⇒ ⟨C′, ρ[s := ((λ s a .C)^{o} :: (ρ s))]⟩

Intuitively, jsr will push a return pointer (required to be already closed, so no closure is necessary) onto the stack pointed to by s and then jump to the code C′ whose address is in register r (Just as desired!).

Last, we derive the action of the rts instruction. Its reduction rule is derived as follows: If s contains ((λ s a .C′)^{o} :: s′), then we have

⟨(rts s a), ρ⟩ ≡ (λ s a .C′)s′(a ρ)
→ C′(ρ[s := s′])
≡ ⟨C′, ρ[s := s′]⟩

So a rts pops the stack, jumping to the address that was on the top of the stack. (Again, just as desired!)

We may summarize the behavior of the three machine instructions as follows:

⟨movec M[r_{1}, …, r_{n}](λr′.C), ρ⟩ ⇒ ⟨C, ρ[r′ := [M, r_{1}, …, r_{n}]]⟩
(where M = (λ e a s .C′)^{o})
⟨jsr r e a s(λ s a .C)^{o}, ρ⟩  ⇒ ⟨C′, ρ[s := ((λ s a .C)^{o} :: (ρ s))]⟩
⟨(rts s a), ρ⟩  ⇒ ⟨C′, ρ[s := s′]⟩
(where s ρ = ((λ s a .C′)^{o} :: s′))

Unfortunately, the code produced by this compiler is not properly tail-recursive, since every procedure call builds a stack frame. This can be fixed using an idea adapted from [5]. We divide the source language into two syntactic categories: ordinary expressions and tail-expressions. Tail-expressions are those expressions which are guaranteed to be executed in the continuation κ. For example, the grammar

⟨pgm⟩ ::= ⟨exp⟩
⟨exp⟩ ::= ⟨var⟩

::= (⟨exp⟩ + ⟨exp⟩) ::= (proc ⟨var⟩ . ⟨exp⟩) ::= (⟨exp⟩ ⟨exp⟩)

becomes

⟨pgm⟩ ::= ⟨tail-exp⟩
⟨tail-exp⟩ ::= ⟨var⟩

::= (⟨exp⟩ + ⟨exp⟩)

::= (proc ⟨var⟩ . ⟨tail-exp⟩) ::= (⟨exp⟩ ⟨exp⟩)

⟨exp⟩  ::= ⟨var⟩

::= (⟨exp⟩ + ⟨exp⟩)

::= (proc ⟨var⟩ . ⟨tail-exp⟩) ::= (⟨exp⟩ ⟨exp⟩)

Here all subexpressions are in non-tail position, except for the body of a procedure, because in the semantics every subexpression is executed in a non-trivial continuation, except for the body of procedure, which is executed with the continuation κ:

E[[(MN)]] = λκ.E[[M]](λm.E[[N]](λn. Ap_{p} mnκ))

Ordinary expressions are compiled as before, but tail-expressions are compiled using the correctness criterion

C_{tail}[[M]] = E[[M]] s

embodying the fact that the continuation is kept in the s register.

9 Representation Independence

The key trick in our treatment of procedure representations was to make the semantics of the source language (expressed above as Plotkin’s algorithm) parametric in the choice of representation (abs and cont). But is this legal? How do we know that our answers are independent of the choice of representation?

The short answer is that they are not: our source language is not type-secure, and therefore our λ-representations are not opaque. For example, if our language had recordselection primitives in its initial environment, we could look at (first(proc x.x)) and see the internal representation of procedures. Thus, the result of evaluating abs x.M will certainly depend on the choice of abs. (This was a central difficulty in early congruence proofs, e.g. [15]).

Nevertheless, we can formulate conditions under which the results of our computations are independent of the choice of representations.

We could add typing to the source language. In that case, the HOAL language could also be typed (as in [9, 20]). Then the representation-independence results of [10] would apply.

However, we can say something sensible about representation independence even in the untyped case. To do this, let us extend the language of the λ-calculus by adding a new class of terms of the form abs x.M and a new constant Ap. Note that here abs and Ap are uninterpreted. In order to make sense of β-reduction in the extended language, we extend substitution to abs-terms in the obvious way, noting that abs x.M binds x. Last, we add the axiom Ap(abs x.M) = λx.M. Let us call the resulting language and theory λ + AP. λ + AP ⊢ M = c means roughly that M reduces to c without knowing the implementation of abs or Ap.

Now, any λ-representation yields a translation from λ + AP into ordinary λ-calculus. If M is a term in the extended language, let \overline{M} denote its translation. Now it is easy to show that λ + AP ⊢ M = c implies λ ⊢ \overline{M} = c. So if a term in our extended language converts to a constant, then so does any translation, independent of the choice of λ-representation.

But we are not quite done: we need to know that λ + AP is a consistent extension of λ. This is important, because if it were possible to prove λ + AP ⊢ c = d for two distinct constants, then we would have λ ⊢ \overline{M} = d as well, and our machine might find either c or d depending on which λ-representation we used. (This is, of course, only the first horrible consequence!). To avoid this, we prove

Theorem 3 λ + AP is a conservative extension of λ.

Proof: We sketch a proof, following the slogan that definitional extensions are conservative. Let A be any λ-model, as defined in, say [8]. Given a λ-representation, we can extend A to a model of λ + AP by interpreting each term M of λ + AP as the meaning of \overline{M}. In particular, if we begin with the open term model of the lambda calculus, we obtain a model of λ + AP in which the only equations between λ-terms are those of convertibility. Hence λ + AP is a conservative extension of λ. QED

This shows that λ + AP ⊢ c = d iff c and d were already identical in λ, and therefore λ + AP is consistent. The same argument shows that T + AP is a conservative extension of any λ-theory T.

Thus, if the term generated by the semantics (with abs and cont uninterpreted except by the axioms AP) reduces to a constant, we are guaranteed that our compiled code will reduce to the same constant, independent of the choice of procedure representation. This demonstrates the correctness of our procedure representations.

10 Conclusion and Future Work

We have presented a formal machine model for higher-order assembly language, and shown how to prove the correctness of simple compilers and procedure representations. Higher-order assembly language preserves the major features of the combinator-based approach of [5, 17, 19]: we can reason about the semantics and the compiler in the same λ-theory, and the operational semantics is derived from the denotational semantics by looking at the reduction behavior of the λ-terms. In addition, higher-order assembly language lets us reason about register usage and allocation, since it inherits this from the λ-terms as well.

Higher-order assembly language appears to be a promising technique for modelling machine instructions on standard multi-register machines. We are currently studying how this model can be used for register allocation, how it complements the combinatorbased models of [5, 17, 19], and how compiler-correctness proofs in this model can be extended to optimizing compilers.

References

[1] Appel, A.W., and Jim, T., “Continuation-Passing, Closure-Passing Style,” Conf. Rec. 16th ACM Symp. on Principles of Programming Languages (1989), 293–302.

[2] Barendregt, H.P. The Lambda Calculus: Its Syntax and Semantics, North-Holland, Amsterdam, 1981.

[3] Boyer, R.S., and Moore, J S. “The Sharing of Structure in Theorem-Proving Programs,” in Machine Intelligence 7 (B. Meltzer & D. Michie, eds), Edinburgh University Press (1972), 101–116.

[4] Church, A. “A formulation of the simple theory of types,” J. of Symbolic Logic 5 (1940), 56–68.

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

[6] Hannan, J. “Making Abstract Machines Less Abstract,” Proc. 1991 ACM Conf. on Functional Programming, Languages, and Architectures, to appear.

[7] Kelsey, R., and Hudak, P. “Realistic Compilation by Program Transformation,” Conf. Rec. 16th Ann. ACM Symp. on Principles of Programming Languages (1989), 281–292.

[8] Meyer, A.R. “What Is a Model of the Lambda Calculus?” Information and Control 52 (1982), 87–122.

[9] Meyer, A.R., and Wand, M. “Continuation Semantics in Typed Lambda-Calculi,” Logics of Programs (Brooklyn, June, 1985) (R. Parikh, ed.) Springer Lecture Notes in Computer Science, vol. 193 (1985), pp. 219–224.

[10] Mitchell, J.C. “Representation Independence and Data Abstraction,” Proc. 13th ACM Symp. on Princ. of Programming Languages (1986), 263–276.

[11] Pfenning, F., and Elliott, C., “Higher-Order Abstract Syntax,” Proc. SIGPLAN ’88 Conf. on Prog. Lang. Design and Implementation, (June, 1988), 199–208.

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

[13] Schmidt, D.A. “Detecting Global Variables in Denotational Semantics,” ACM TOPLAS 7 (1985) 299–310.

[14] Sethi, R. “Control Flow Aspects of Semantics-Directed Compiling” ACM Trans. on Prog. Lang. and Sys. 5 (1983) 554–596.

[15] Stoy, J.E. “The Congruence of Two Programming Language Definitions,” Theoret. Comp. Sci. 13 (1981), 151–174.

[16] Turner, D.A. “A New Implementation Technique for Applicative Languages,” Software-Practice and Experience 9 (1979), 31–49.

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

[18] Wand, M. “Deriving Target Code as a Representation of Continuation Semantics” ACM Trans. on Prog. Lang. and Systems 4, 3 (July, 1982) 496–517.

[19] Wand, M. “Loops in Combinator-Based Compilers,” Conf. Rec. 10th ACM Symposium on Principles of Programming Languages (1983), 190–196.

[20] Wand, M. “Embedding Type Structure in Semantics” Conf. Rec. 12th ACM Symp. on Principles of Prog. Lang. (1985), 1–6.

[21] Wand, M. “A Short Proof of the Lexical Addressing Algorithm,” Information Processing Letters 35 (1990), 1–5.