Abstract Models of Memory Management^{∗}

Greg Morrisett  Matthias Felleisen  Robert Harper
Carnegie Mellon  Rice University  Carnegie Mellon

jgmorris@cs.cmu.edu  matthias@cs.rice.edu  rwh@cs.cmu.edu

Abstract

Most specifications of garbage collectors concentrate on the low-level algorithmic details of how to find and preserve accessible objects. Often, they focus on bit-level manipulations such as “scanning stack frames,” “marking objects,” “tagging data,” etc. While these details are important in some contexts, they often obscure the more fundamental aspects of memory management: what objects are garbage and why?

We develop a series of calculi that are just low-level enough that we can express allocation and garbage collection, yet are sufficiently abstract that we may formally prove the correctness of various memory management strategies. By making the heap of a program syntactically apparent, we can specify memory actions as rewriting rules that allocate values on the heap and automatically dereference pointers to such objects when needed. This formulation permits the specification of garbage collection as a relation that removes portions of the heap without affecting the outcome of the evaluation.

Our high-level approach allows us to specify in a compact manner a wide variety of memory management techniques, including standard trace-based garbage collection (i.e., the family of copying and mark/sweep collection algorithms), generational collection, and type-based, tag-free collection. Furthermore, since the definition of garbage is based on the semantics of the underlying language instead of the conservative approximation of inaccessibility, we are able to specify and prove the idea that type inference can be used to collect some objects that are accessible but never used.

1 Memory Safety

Advanced programming languages manage memory allocation and deallocation automatically. Automatic memory managers, or garbage collectors, significantly facilitate the programming process because programmers can rely on the language implementation for the delicate tasks of finding and freeing unneeded objects. Indeed, the presence of a garbage collector ensures memory safety in the same way that a type system guarantees type safety: no program written in an advanced programming language will crash due to dangling pointer problems while allocation, access, and deallocation are transparent. However, in contrast to type systems, memory management strategies and particularly garbage collectors rarely come with a compact formulation and a formal proof of soundness. Since garbage collectors work on the machine representations of abstract values, the very idea of providing a proof of memory safety sounds unrealistic given the lack of simple models of memory operations.

The recently developed syntactic approaches to the specification of language semantics by Felleisen and Hieb [11] and Mason and Talcott [18, 19] are the first execution models that are intensional enough to permit the specification of memory management actions and yet are sufficiently abstract to permit compact proofs of important properties. Starting from the λ_{v}-S calculus of Felleisen and Hieb, we design compact specifications of a number of memory management ideas and prove several correctness theorems.

The basic idea underlying the development of our garbage collection calculi is the representation of a program’s run-time memory as a global series of syntactic declarations. The program evaluation rules allocate large objects in the global declaration, which represents the heap, and automatically dereference pointers to such objects when needed. As a result, garbage collection can be specified as any relation that removes portions of the current heap without affecting the result of a program’s execution.

In Section 2, we present a small functional programming language, λgc, with a rewriting semantics that makes allocation explicit. We define a semantic notion of garbage collection for λgc and prove that there is no optimal collection strategy that is computable. In Section 3, we specify the “free-variable” garbage collection rule which models tracebased collectors including mark/sweep and copying collectors. We prove that the free-variable rule is correct and provide two “implementations” at the syntactic level: the first corresponds to a copying collector, the second to a generational one.

In Section 4, we formalize so-called “tag-free” collection algorithms for explicitly-typed, monomorphic languages such as Pascal and Algol [7, 29, 8]. We show how to recover necessary shape information about values from types during garbage collection. We are able to prove the correctness of the garbage collection algorithm by using a well known type preservation argument.

∗This work was sponsored in part by the Advanced Research Projects Agency (ARPA), CSTO, under the title “The Fox Project:

Advanced Development of Systems Software,” ARPA Order No. 8313, issued by ESD/AVS under Contract No. F19628–91–C–0168, Wright Laboratory, Aeronautical Systems Center, Air Force Materiel Command, USAF, and ARPA grant No. F33615-93-1-1330. Views and conclusions contained in this document are those of the authors and should not be interpreted as necessarily representing official policies or endorsements, either expressed or implied, of Wright Laboratory or the United States Government.

In Section 5, we justify our semantic definition of garbage by showing that Milner-style type inference can be used to prove that an object is semantically garbage even though the object is still reachable. While previous authors have sketched this idea [3, 5, 14, 12], we are the first to present a formal proof of this result. The proof is obtained by casting the well known interpretation of types as logical relations into our framework.

Section 6 discusses related work and Section 7 closes with a summary.

Due to a lack of space, most of the proofs for lemmas are omitted in this paper. However, full details may be recovered from our companion technical report [20].

2 Modeling Allocation: λgc

Syntax: The syntax of λgc (see Figure 1) is that of a conventional, higher-order, applicative programming language based on the λ-calculus. Following the tradition of functional programming, a λgc program (P) consists of some mutually recursive definitions (H) and an expression (e). The global definitions are useful for defining mutually recursive procedures, but their primary purpose here is to represent the run-time heap of a program. In general, there can be cycles in a heap, so we use letrec instead of let as the binding form. Expressions are either variables (x), integers (i), pairs (⟨e_{1}, e_{2}⟩), projections (π_{i}), abstractions (λx.e), or applications (e_{1} e_{2}).

Formally, the heap is a series of pairs, called bindings, consisting of variables and heap values. Heap values are a semantically significant subset of expressions. The order of the bindings is irrelevant and each variable must be bound to at most one heap value in a heap. Hence, we treat heaps as sets and, when convenient, as finite functions. We write Dom(H) to denote the bound variables of H, and Rng(H) to denote the heap values bound in H. We sometimes refer to variables bound in the heap as locations or pointers.

The language contains two binding constructs: λx.e binds x in e and letrec H in e binds the variables in Dom(H) to the expressions Rng(H) in both the values in Rng(H) and in e. Following convention, we consider programs to be equivalent up to a consistent α-conversion of bound variables.

Considering programs equivalent modulo α-conversion and the treatment of heaps as sets instead of sequences hides many of the complexities of memory management. In particular, programs are automatically considered equivalent if the heap is re-arranged and locations are re-named as long as the “graph” of the program is preserved. This abstraction allows us to focus on the issues of determining what bindings in the heap are garbage without specifying how such bindings are represented in a real machine.

Mathematical Notation: We use X ⊎ X′ to denote the union of two disjoint sets, X and X′. We use H ⊎ H′ to denote the union of two heaps whose domains are disjoint. We use {e_{1}/x}e_{2} to denote capture-avoiding substitution of the expression e_{1} for the free variable x in the expression e_{2}. We use X \ X′ to denote {x ∈ X | x ∉ X′}.

Semantics: The rewriting semantics for λgc is an adaptation of the standard reduction function of the λ_{v}-S calculus [11]. Roughly speaking, this kind of semantics describes an abstract machine whose states are programs and whose instructions are relations between programs. The desired final state of this abstract machine is an answer program (A) whose body is a pointer to some value, such as an integer, in the heap.

Each rewriting step of a program letrec H in e proceeds according to a simple algorithm. If the body of the program, e, is not a variable, it is partitioned into an evaluation context E (an expression with a hole [ ] in the place of a sub-expression), which represents the control state, and an instruction expression I , which roughly corresponds to a program counter: e = E[I]. The instruction expression determines the next expression e′ and any changes to the heap resulting in a new heap H′. Putting the pieces together yields the next program in the evaluation sequence: letrec H′ in E[e′]. Each instruction determines one transition rule of the abstract machine. Formally, a rule denotes a relation between programs. A set of rules denotes the union of the respective relations.

We use the following conventions: Let G be a set of program relations, and let P and P′ be programs. Then,

P ⟼^{G} P′ means P rewrites to P′ according to one of the rules in G and ⟼^{G} ^{∗} is the reflexive, transitive closure of ⟼^{G}.

G + r is the union of G with the rule r.

A program P is irreducible with respect to G iff there is no rule in G and no P′ such that P ⟼^{G} P′.

P ⇓_{G} P′ means that P ⟼^{G} ^{∗}P′ and P′ is irreducible with respect to G.

P ⇑_{G} means that there exists an infinite sequence of programs P_{i} such that P ⟼^{G} P_{1} ⟼^{G} P_{2} ⟼^{G} · · ·.

Figure 1 defines the set of evaluation contexts and instruction expressions for λgc. The definition of evaluation contexts (E) reflects the left-to-right, call-by-value evaluation order of the language. All terms to the left of the path from the root to the hole are variables; the terms on the right are arbitrary. Instruction expressions (I) consist of heap values (h), applications of (pointers to heap-allocated) procedures to (pointers to heap-allocated) values, and projections of (pointers to heap-allocated) tuples.

The evaluation rules for λgc reflect the intentions behind our choice of instruction expressions. The transition rule alloc models the allocation of values in the heap by binding the value to a new variable and using this variable in its place in the program. Note that the “⊎” notation carries the implicit requirement that the newly allocated variable x cannot be in the domain of the heap H. The transition proj specifies how a projection instruction extracts the appropriate component from a pointer to a heap-allocated pair. Similarly, app is a transliteration of the conventional β-value rule into our modified setting. It binds the formal parameter of a heap-allocated procedure to the value of the pointer given as the actual argument, and places the expression part of the procedure into the evaluation context. Multiple applications of the same procedure require α-conversion to ensure that the formal parameter does not conflict with bindings already in the heap^{1}. We use R to abbreviate the union of the rules alloc, proj, and app.

1An alternative rule for application substitutes the actual argument (y) for the formal (z) within e and performs no allocation. This rule is essentially equivalent to app, but the definition above simplifies the proofs of Section 5.

Programs:

(variables)  x, y, z ∈ Var
(integers)  i ∈ Int ::= ⋯ | − 2 | − 1 | 0 | 1 | 2 | ⋯
(expressions)  e ∈ Exp ::= x | i | ⟨e_{1}, e_{2}⟩ | π_{1} e | π_{2} e | λx.e | e_{1} e_{2}
(heap values)  h ∈ Hval ::= i | ⟨x_{1}, x_{2}⟩ | λx.e
(heaps)  H ∈ Heap ::= {x_{1} = h_{1}, …, x_{n} = h_{n}}
(programs)  P ∈ Prog ::= letrec H in e
(answers)  A ∈ Ans ::= letrec H in x

Evaluation Contexts and Instruction Expressions:

(contexts)  E ∈ Ctxt ::= [ ] | ⟨E, e⟩ | ⟨x, E⟩ | π_{i} E | E e | x E
(instructions) I ∈ Instr ::= h | π_{i} x | x y

Rewriting Rules

(alloc) letrec H in E[h] ⟼^{alloc} letrec H ⊎ {x = h} in E[x]
(proj)  letrec H in E[π_{i} x] ⟼^{π_{i}} letrec H in E[x_{i}]  (H(x) = ⟨x_{1}, x_{2}⟩ and i = 1, 2)
(app)  letrec H in E[x y] ⟼^{app} letrec H ⊎ {z = H(y)} in E[e]  (H(x) = λz.e)

Figure 1: The Syntax and Operational Semantics of λgc

The irreducible programs of λgc are either answers or stuck programs. The latter correspond to machine states that result from the misapplication of primitive program operations or unbound variables.

Definition 2.1 (Stuck Programs) A program is stuck if it is of one of the following forms:

letrec H in E[π_{i} x] (x ∉ Dom(H) or H(x) ≠ ⟨x_{1}, x_{2}⟩)
letrec H in E[x y] (x ∉ Dom(H) or H(x) ≠ λz.e or
y ∉ Dom(H))

All programs either diverge or evaluate to an answer or a stuck program. Put differently, the evaluation process defines a partial function from λgc programs to irreducible programs [11, 30].

A Semantic Definition of Garbage Since the semantics of λgc makes the allocation of values explicit, including the implicit pointer dereferencing in the language, we can also define what it means to garbage collect a value in the heap and then analyze some basic properties. A binding x = h in the heap of a program is garbage if removing the binding has no “observable” effect on running the program. In our case, we consider only integer results and non-termination to be observable.

Definition 2.2 (Kleene Equivalence) (P_{1}, G_{1}) ≃ (P_{2}, G_{2}) means P_{1} ⇓_{G_{1}} letrec H_{1} in x where H_{1}(x) = i if and only if P_{2} ⇓_{G_{2}} letrec H_{2} in y and H_{2}(y) = i. If G_{1} = G_{2} = R, then we simply write P_{1} ≃ P_{2}.

A binding is garbage if removing it results in a program that is Kleene equivalent to the original program:

Definition 2.3 (Garbage) If P = letrec H ⊎ {x = h} in e, then the binding x = h is garbage with respect to P iff P ≃ letrec H in e. A collection of a program is the same program with some garbage bindings removed. An optimal collection of a program is a program with as many garbage bindings removed as possible.

Unfortunately, there can be no optimal garbage collector because determining whether a binding is garbage or not is undecidable.

Proposition 2.4 (Garbage Undecidable) Determining if a binding is garbage in an arbitrary closed λgc program is undecidable.

Proof (sketch): We can reduce the halting problem to an optimal collector by taking an arbitrary program, adding a binding to the heap and modifying the program so that if it terminates, it accesses the extra binding. An optimal collector will collect the binding if and only if the original program does not terminate. □

3 Reachability-Based Garbage Collection

Since computing an optimal collection is undecidable, a garbage collection algorithm must conservatively approximate the set of garbage bindings. Most garbage collectors compute the reachable set of bindings in a program given the variables in use in the current instruction expression and control state. All reachable bindings are preserved; the others are eliminated.

Following Felleisen and Hieb [11], reachability in λgc is formalized by considering free variables. The following “freevariable” GC rule describes bindings as garbage if there are no references to these bindings in the other bindings, nor in the currently evaluating expression:

(fv)

letrec H_{1} ⊎ H_{2} in e ⟼^{fv} letrec H_{1} in e
if Dom(H_{2}) ∩ FV(letrec H_{1} in e) = ∅

The fv rule is correct in that it only removes garbage, and thus computes valid collections. The keys to the proof of correctness of fv are a postponement lemma and a diamond lemma.

Lemma 3.1 (Postponement) If P_{1} ⟼^{fv} P_{2} ⟼^{R} P_{3}, then there exists a P′_{2} such that P_{1} ⟼^{R} P′_{2} ⟼^{fv} P_{3}.

Proof (sketch): By cases on the elements of R. □

Lemma 3.2 (Diamond) If P_{1} ⟼^{fv} P_{2} and P_{1} ⟼^{R} P′_{2}, then there exists a P_{3} such that P_{2} ⟼^{R} P_{3} and P′_{2} ⟼^{fv} P_{3}.

Proof (sketch): Assume P_{1} = letrec H_{1} ⊎ H_{2} in E[I], P_{2} = letrec H_{1} in E[I], and P_{1} ⟼^{fv} P_{2}. We can easily show by case analysis on the elements of R that if P_{1} ⟼^{R} P′_{2} where P′_{2} = letrec H_{1} ⊎ H_{2} ⊎ H_{3} in E[e], for some H_{3} and e, then P′_{2} ⟼^{fv} P_{3} and P_{2} ⟼^{R} P_{3} where P_{3} = letrec H_{1} ⊎ H_{3} in E[e]. □

With the Postponement and Diamond Lemmas in hand, it is straightforward to show that fv is a correct GC rule.

Theorem 3.3 (Correctness of fv) If P ⟼^{fv} P′, then P′ is a collection of P.

Proof: Let P = letrec H_{1} ⊎ H_{2} in e and let P′ = letrec H_{1} in e such that P ⟼^{fv} P′. We must show P evaluates to an integer value iff P′ evaluates to the same integer. Suppose P′ ⇓_{R} letrec H in x and H(x) = i. By induction on the number of rewriting steps using the Postponement Lemma, we can show that P ⇓_{R} letrec H ⊎ H_{2} in x and clearly (H ⊎ H_{2})(x) = H(x) = i. Now suppose P ⇓_{R} letrec H in x and H(x) = i. By induction on the number of rewriting steps using the Diamond Lemma, we know that there exists an H′ such that P′ ⇓_{R} letrec H′ in x and letrec H in x ⟼^{fv} letrec H′ in x. Thus, x must be bound in H′ and since fv only drops bindings, H′(x) = i. □

This theorem shows that a single application of fv results in a Kleene equivalent program. A real implementation interleaves garbage collection with evaluation. The following theorem shows that adding fv to R preserves evaluation.

Theorem 3.4 For all programs P, (P, R) ≃ (P, R + fv).

Proof: Clearly any evaluation under R can be simulated by R + fv simply by not performing any fv steps. Thus, if P ⇓_{R} A then P ⇓_{R+fv} A. Now suppose P ⇓_{R+fv} letrec H_{1} in x_{1} and H_{1}(x_{1}) = i. Then there exists a finite rewriting sequence using R + fv as follows:

P ⟼^{R+fv} P_{1} ⟼^{R+fv} P_{2} ⟼^{R+fv} ⋯ ⟼^{R+fv} letrec H_{1} in x_{1}

We can show by induction on the number of rewriting steps in this sequence, using the Postponement Lemma, that all fv steps can be performed at the end of the evaluation sequence. This provides us with an alternative evaluation sequence where all the R steps are performed at the beginning:

P ⟼^{R} P′_{1} ⟼^{R} P′_{2} ⟼^{R} ⋯ ⟼^{R} P′_{n} ⟼^{fv}

P_{n+1} ⟼^{fv} P_{n+2} ⟼^{fv} ⋯ ⟼^{fv} letrec H_{1} in x_{1}

Since fv does not affect the expression part of a program and only removes bindings from the heap, P′_{n} = letrec H_{1} ⊎ H_{2} in x for some H_{2}. Thus, P ⇓_{R} letrec H_{1}⊎H_{2} in x. Since H_{1}(x) = i, (H_{1} ⊎ H_{2})(x) = i. □

3.1 The Free-Variable Tracing Algorithm

The free-variable GC rule is a specification of a garbage collection algorithm. It assumes some mechanism for partitioning the set of bindings into two disjoint pieces such that one set of bindings is unreachable from the second set of bindings and the body of the program. Real garbage collection algorithms need a deterministic mechanism for generating this partitioning. It is possible to formulate an abstract version of such a mechanism, the free-variable tracing algorithm, by lifting the ideas of mark-sweep and copying collectors to the level of program syntax.

We adopt the terminology of copying collection in the description of the free-variable tracing algorithm. We use two heaps and a set: a “from-heap” (H_{f}), a “scan-set” (S), and a “to-heap” (H_{t}). The from-heap is the set of bindings in the current program and the to-heap will become the set of bindings preserved by the algorithm. The scan-set records the set of variables reachable from the to-heap that have not yet been moved from the from-heap to the to-heap. The scan-set is often referred to as the “frontier.”

The body of the algorithm proceeds as follows: A variable x is removed from S such that H_{f} has a binding for x. If no such locations are in S, the algorithm terminates. Otherwise, it scans the heap value h to which x is bound in the from-set H_{f}, looking for free variables. For each y ∈ FV(h), it checks to see if y has already been forwarded to the to-set H_{t}. Only if y is not bound in H_{t} does it add the variable to the scan-set S. This ensures that a variable moves at most once from the from-heap to the scan-set.

Formulating the free-variable tracing algorithm as a rewriting system is easy. It requires only one rule that relates triples of from-sets, scan-sets, and to-sets:

\begin{matrix}⟨H_{f} ⊎ \{x = h\}, S ⊎ \{x\}, H_{t}⟩ ⟹ \\ ⟨H_{f} , S ∪ (FV(h) \ (Dom(H_{t}) ⊎ \{x\})), H_{t} ⊎ \{x = h\}⟩ \end{matrix}

Initially the free variables of the evaluation context and instruction expression, which correspond to the “roots” of a computation, are placed in S. Computing the free variables of the context represents the scanning of the “stack” of a conventional implementation while computing the free variables of the instruction expression corresponds to scanning the “registers.” The initial tuple is re-written until we reach a state where no variable in the scan-set is bound in the from-heap. At this point, we have forwarded enough bindings to the to-heap. This leads to the following free-variable tracing algorithm rule:

letrec H in e ⟼^{fva} letrec H′ in e
(fva) if ⟨H, FV(e), ∅⟩ ⟹^{∗} ⟨H′′, S, H′⟩
and Dom(H′′) ∩ S = ∅

Clearly, the algorithm always terminates since the size of the from-heap strictly decreases with each step. Furthermore, this new rewriting rule is a subrelation of the rule fv, which implies the correctness of the algorithm.

Theorem 3.5 If P ⟼^{fva} P′, then P ⟼^{fv} P′.

Proof: Let P = letrec H in e be a λgc program. The first step is to prove the basic invariants of the garbage collection rewriting system: If ⟨H, FV(e), ∅⟩ ⟹^{∗} ⟨H_{f} , S, H_{t}⟩, then H_{f} ⊎ H_{t} = H and FV(letrec H_{t} in e) = S. Now let P′ = letrec H_{1} in e and suppose P ⟼^{fva} P′. Then,

⟨H_{1} ⊎ H_{2}, FV(e), ∅⟩ ⟹^{∗} ⟨H_{2}, S, H_{1}⟩.

and Dom(H_{2}) ∩ S = ∅. By the invariants, FV(letrec H_{1} in e) = S, so Dom(H_{2}) ∩ FV(P′) = ∅. Consequently, P ⟼^{fv} P′. □

If we require that a collection algorithm produce a closed program, then fva is “optimal” in the following weak sense: if P is a closed program and P ⟼^{fva} P′, then P′ has the fewest bindings needed to keep the program closed without affecting evaluation. Assuming each step in the freevariable tracing algorithm takes time proportional to the size (in symbols) of the heap object forwarded to the toheap, the time cost of the algorithm is proportional to the amount of data preserved, not the total amount of data in the original heap.

3.2 Generational Garbage Collection

The free-variable tracing algorithm examines all of the reachable bindings in the heap to determine that a set of bindings may be removed. By carefully partitioning the heap into smaller heaps, a garbage collector can scan less than the whole heap and still free significant amounts of memory. A generational partition of a program’s heap is a sequence of sub-heaps ordered in such a way that “older” generations never have pointers to “younger” generations.

Definition 3.6 (Generational Partition) A generational partition of a heap H is a sequence of heaps H_{1}, H_{2}, …, H_{n} such that H = H_{1}⊎H_{2}⊎⋯⊎H_{n} and for all i such that 1 ≤ i < n, FV(H_{i})∩Dom(H_{i+1}⊎H_{i+2}⊎⋯⊎H_{n}) = ∅. The H_{i} are referred to as generations and H_{i} is said to be an older generation than H_{j} if i < j.

Given a generational partition of a program’s heap, a free-variable based garbage collector can eliminate a set of bindings in younger generations without looking at any older generations.

Theorem 3.7 (Generational Collection) Let H_{1}, …, H_{n} be a generational partition of the heap of P = letrec H in e. Suppose H_{i} = (H_{i}^{1} ⊎ H_{i}^{2}), and Dom(H_{i}^{2}) ∩ FV(letrec H_{i}^{1} ⊎ H_{i+1} ⊎ ⋯ ⊎ H_{n} in e) = ∅. Then P ⟼^{fv} letrec (H \ H_{i}^{2}) in e.

Proof: We must show that Dom(H_{i}^{2}) ∩ FV(letrec (H \ H_{i}^{2}) in e) = ∅. Since H_{1}, ⋯, H_{n} is a generational partition of H, for all j, 1 ≤ j < i, FV(H_{j})∩Dom(H_{j+1}⊎⋯⊎H_{n}) = ∅. Hence, FV(H_{1} ⊎ ⋯ ⊎ H_{i−1}) ∩ Dom(H_{i}^{2}) = ∅. Now,

FV(letrec H \ H_{i}^{2} in e) ∩ Dom(H_{i}^{2})

= (FV(H \ H_{i}^{2}) ∪ FV(e)) ∩ Dom(H_{i}^{2})
= (FV(H_{1} ⊎ ⋯ ⊎ H_{i−1}) ∪ FV(H_{i}^{1} ⊎ ⋯ ⊎ H_{n}) ∪ FV(e))

∩Dom(H_{i}^{2})

= (FV(H_{1} ⊎ ⋯ ⊎ H_{i−1}) ∩ Dom(H_{i}^{2}))∪

((FV(H_{i}^{1} ⊎ ⋯ ⊎ H_{n}) ∪ FV(e)) ∩ Dom(H_{i}^{2}))

= ∅ ∪ ((FV(H_{i}^{1} ⊎ ⋯ ⊎ H_{n}) ∪ FV(e)) ∩ Dom(H_{i}^{2}))
= FV(letrec H_{i}^{1} ⊎ ⋯ ⊎ H_{n} in e) ∩ Dom(H_{i}^{2})
= ∅

□

Generational collection is important for three practical reasons: First, evaluation of closed, pure λgc programs makes it easy to maintain generational partitions.

Theorem 3.8 Let P = letrec H in e be a closed program. If H_{1}, …, H_{n} is a generational partition of H and P ⟼^{R} letrec H ⊎ H′ in e, then H_{1}, …, H_{n}, H′ is a generational partition of H ⊎ H′.

The second reason generational collection is important is that, given a generational partition, we can directly use the free-variable tracing algorithm to generate a collection of a program. The following rule invokes the free-variable algorithm on the program letrec H_{2} in e where H_{1}, H_{2} is a generational partition of the original program’s heap. The resulting heap is glued onto H_{1} to produce a collection of the program.

(gen)

letrec H in e ⟼^{gen} letrec H_{1} ⊎ H′_{2} in e
if letrec H_{2} in e ⟼^{fva} letrec H′_{2} in e

and H_{1}, H_{2} form a generational partition of H

The rule’s soundness follows directly from the Generational Collection theorem, together with the soundness of the freevariable tracing algorithm.

The third reason generational collection is important is that empirical evidence shows that “objects tend to die young” [28]. That is, recently allocated bindings are more likely to become garbage in a small number of evaluation steps. Thus, if we place recently allocated bindings in younger generations, we can concentrate our collection efforts on these generations, ignoring older generations, and still eliminate most of the garbage.

4 Garbage Collection via Type Recovery

The delimiters and other tokens of the abstract syntax mark or “tag” heap values with enough information that we can distinguish pairs from functions, pointers from integers, etc. This allows us to navigate through the memory unambiguously, but placing tags on heap values and stripping them off to perform a computation can impose a heavy overhead on the running time and space requirements of programs [26]. An alternative to tagging is the use of types to determine the shape of an object. If types are determined at compile time and evaluation maintains enough information that the types of reachable objects can always be recovered, then there is no need to tag values.

A number of researchers have made attempts to explore this alternative [7, 8, 3, 13, 27, 2], but none of them presented concise characterizations of the underlying techniques with correctness proofs. In this section, we present the basic idea behind type-recovery based garbage collection. We then introduce λgc-mono, an explicitly typed, monomorphic variant of λgc. We show how to adapt the free-variable tracing algorithm to recover types of objects in the heap and to use these types in the traversal of heap objects instead of abstract syntax. The proof of correctness for this garbage collection algorithm is given by extending the proof of soundness of the type system for λgc-mono.

4.1 λgc-mono

λgc-mono is an explicitly typed, monomorphic variant of λgc. The set of types (τ) of λgc-mono contains the conventional basic types and constructed types for typing a functional programming language like λgc. The expressions of λgc-mono are the same as for λgc, except that each raw expression (u) is paired with some type information (see Figure 2). Heap values are not paired with their type, reflecting the fact that the memory is “almost tag free.” Of course, some type information is recorded within heap values that are functions. In a low-level model that uses closures (an explicit value environment paired with code), this corresponds to maintaining a type environment, recording the types of the values in the closure’s environment. The type environment for a closure can be computed at compile time and shared among multiple instances, just like the code.

The evaluation contexts (E) consist of a raw context (U) and a type (τ). Raw contexts are filled with instructions (I)

Types:

(types) τ ∈ Type ::= int | τ_{1} × τ_{2} | τ_{1} → τ_{2}

Programs:

(expressions) e ∈ TExp ::= (u : τ)
u ∈ UExp ::= x | i | ⟨e_{1}, e_{2}⟩ | π_{i} e | λx:τ.e | e_{1} e_{2}
(heap values) h ∈ Hval ::= i | ⟨x_{1}, x_{2}⟩ | λx:τ.e
(heaps)  H ∈ Heap ::= {x_{1} = h_{1}, …, x_{n} = h_{n}}
(programs)  P ∈ Prog ::= letrec H in e
(answers)  A ∈ Ans ::= letrec H in (x : τ)

Evaluation Contexts and Instructions:

(contexts)  E ∈ TCtxt ::= (U : τ)
U ∈ UCtxt ::= [ ] | ⟨E, e⟩ | ⟨(x:τ), E⟩ | π_{i} E | E e | (x:τ) E
(instructions) I ∈ Instr ::= i | ⟨(x_{1}:τ_{1}), (x_{2}:τ_{2})⟩ | λx:τ.e | π_{i} (x:τ) | (x:τ_{1}) (y:τ_{2})

Rewriting Rules:

(alloc-int)  letrec H in E[i] ⟼^{alloc} letrec H ⊎ {x = i} in E[x]
(alloc-pair) letrec H in E[⟨x_{1}:τ_{1}, x_{2}:τ_{2}⟩] ⟼^{alloc} letrec H ⊎ {x = ⟨x_{1}, x_{2}⟩} in E[x]
(alloc-fn)  letrec H in E[λy:τ.e] ⟼^{alloc} letrec H ⊎ {x = λy:τ.e} in E[x]
(proj) letrec H in E[π_{i} (x:τ)] ⟼^{π_{i}} letrec H in E[x_{i}] (H(x) = ⟨x_{1}, x_{2}⟩, i = 1, 2)
(app)  letrec H in E[(x:τ_{1}) (y:τ_{2})] ⟼^{app} letrec H ⊎ {z = H(y)} in E[e] (H(x) = λz:τ′.e)

Figure 2: The Syntax and Operational Semantics of λgc-mono

which are a subset of the raw expressions (u). The evaluation rules for λgc-mono, named RM, are variants of the rules for λgc that largely ignore the type information on the sub-expressions of the program’s body. Allocation of integers, tuples and functions strips the type tag off the heap value before placing it in the heap. Allocation of tuples also removes the tags from the components of the tuple. The removal of type information corresponds to the passage of a value from code to data and does not necessarily reflect a runtime cost. Projection and application are essentially the same as for λgc. Note that substitution of a result expression for an instruction occurs “in place,” and hence the type of the instruction is ascribed to the expression.

The notion of a stuck state is adapted in accordance with the type structure of the language.

Definition 4.1 (λgc-mono Stuck Programs) A program is stuck if it is of one of the following forms:

letrec H in E[π_{i} (x:τ)]  (x ∉ Dom(H) or
H(x) ≠ ⟨x_{1}, x_{2}⟩)
letrec H in E[(x:τ_{1}) (y:τ_{2})] (x or y ∉ Dom(H) or
H(x) ≠ λz:τ.e)

The static semantics of λgc-mono consists of four judgements about program components. The first judgement, Γ ▷ e, is a binary relation between a type assignment Γ, mapping a finite set of variables to types, and a typed expression e. Figure 3 contains the fairly conventional inference rules for expressions that generate the static semantics. Typing heaps and complete programs requires three additional judgements. The first is Γ ▷ h : τ which asserts that the heap value h has type τ under the assumptions in Γ. The judgement is defined using inference rules (not shown here) similar to the expression-level rules. The second is Γ ▷ H : Γ′, which asserts that the variables given type τ in Γ′ are bound to heap values in H of the appropriate type, under the assumptions in Γ. The judgement’s definition via the heap rule requires “guessing” the types of the values in the heap and verifying these guesses simultaneously. The third judgement, ▷ P, asserts the well-typing of a complete program.

The calculus λgc-mono is type sound in that evaluation of well formed programs cannot get stuck [30]. A key to the proof of soundness is a type preservation lemma:

Lemma 4.2 (Type Preservation) If ▷ P and P ⟼^{RM} P′, then ▷ P′.

Theorem 4.3 (Type Soundness) If ▷ P then either P is an answer or else there exists some P′ such that P ⟼^{RM} P′ and ▷ P′.

4.2 Using Types in Garbage Collection

Specifying a valid garbage collection rule that exploits types is straightforward. The key property that the rule must preserve is type preservation. That is, if P ⟼^{gc} P′, and P is well typed, then P′ must be well typed. One way to achieve this goal is to make it into a side-condition of the GC rule:

(mono)

letrec H_{1} ⊎ H_{2} in e ⟼^{mono} letrec H_{1} in e
if ▷ letrec H_{1} in e

Theorem 4.4 For all well formed λgc-mono programs P, (P, RM) ≃ (P, RM + mono).

Proof: Since mono preserves types, the type soundness proof trivially extends to the dynamic semantics with mono. This implies that, since P is well formed, P cannot get stuck under either system. Since bindings are only dropped and not updated by mono, the results of evaluating under either system must be the same. □

Like the free-variable rule of λgc, mono needs to be refined before it can serve as the basis for an implementation.

(var) \overline{Γ ⊎ \{x:τ\} ▷ (x : τ)} (int) \overline{Γ ▷ (i : int)}

(pair) \frac{Γ ▷ (u_{1}:τ_{1})  Γ ▷ (u_{2}:τ_{2})}{Γ ▷ (⟨(u_{2}:τ_{1}), (u_{2}:τ_{2})⟩ : τ_{1} × τ_{2})}  (proj) \frac{Γ ▷ (u : τ_{1} × τ_{2})}{Γ ▷ (π_{i} (u : τ_{1} × τ_{2}) : τ_{i})} (i = 1, 2)

(fn) \frac{Γ ⊎ \{x:τ_{1}\} ▷ (u : τ_{2})}{Γ ▷ (λx:τ_{1}.(u:τ_{2}) : τ_{1} → τ_{2})}  (app) \frac{Γ ▷ (u_{1} : τ_{1} → τ_{2})  Γ ▷ (u_{2}:τ_{1})}{Γ ▷ ((u_{1} : τ_{1} → τ_{2}) (u_{2}:τ_{1}) : τ_{2})}

(heap) \frac{∀ x ∈ Dom(Γ′) . Γ ⊎ Γ′ ▷ H(x) : Γ′(x)}{Γ ▷ H : Γ′}  (prog) \frac{∅ ▷ H : Γ  Γ ▷ e}{▷ letrec H in e}

Figure 3: The Static Semantics of λgc-mono

The refinement is similar to the one from fv to fva but uses the types embedded in programs to traverse heap values. The basis for the collection algorithm is a function that determines a minimal, with respect to set-inclusion, type assignment Γ for any expression e such that Γ ▷ e:

MTA(x:τ) = {x:τ}
MTA(i:τ) = ∅
MTA(⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2}) = MTA(e_{1}) ∪ MTA(e_{2})
MTA(π_{i} e : τ) = MTA(e)
MTA(λx:τ_{1}.e : τ_{1} → τ_{2}) = MTA(e) \ {x:τ_{1}}
MTA(e_{1} e_{2} : τ) = MTA(e_{1}) ∪ MTA(e_{2})

Lemma 4.5 If Γ ▷ e, then MTA(e) ▷ e and MTA(e) ⊆ Γ.

If P = letrec H in e and P is closed, then MTA(e) determines the types of the locations in the heap H that are immediately reachable from the expression e. A garbage collector can use this type information together with the following Tag function to traverse the reachable heap values based on their types instead of their abstract syntax.

Tag[int](i)  = (i:int)
Tag[τ_{1} × τ_{2}](⟨x_{1}, x_{2}⟩) = (⟨(x_{1}:τ_{1}), (x_{2}:τ_{2})⟩ : τ_{1} × τ_{2})
Tag[τ_{1} → τ_{2}](λx:τ_{1}.e) = ((λx:τ_{1}.e) : τ_{1} → τ_{2})

Tag is a curried function that takes a type and then takes a heap value of that type, and annotates that heap value with enough information to turn it back into an expression. It is important to note that Tag pattern-matches and operates according to the type argument given and not the abstract syntax of the heap value given. MTA can be used on the resulting expression to find the minimal type assignment for the heap value. This provides us with the free locations and their types for the heap value. The following lemma summarizes the relationship between Tag and MTA:

Lemma 4.6 If ∅ ▷ H : Γ ⊎ {x:τ} then there exists an h such that {x = h} ⊆ H, MTA(Tag[τ](h)) ▷ h : τ, and MTA(Tag[τ](h)) ⊆ Γ ⊎ {x:τ}

Equipped with MTA, we can now redefine the freevariable tracing algorithm so that it uses Tag to traverse heap values. The algorithm is specified in the same manner as fva, i.e., as a rewriting system among tuples of the form ⟨H_{f} , Γ_{s}, H_{t}, Γ_{t}⟩ where H_{f} is the from-heap, Γ_{s} is a type assignment corresponding to the scan-set, H_{t} is the to-heap, and Γ_{t} is a type assignment for the to-heap:

⟨H_{f} ⊎ {x = h}, Γ_{s} ⊎ {x:τ}, H_{t}, Γ_{t}⟩ ⟹^{mono}

⟨H_{f} , Γ′_{s}, H_{t} ⊎ {x = h}, Γ′_{t}⟩

where  Γ′_{s} = (Γ_{s} ∪ MTA(Tag[τ](h)) \ Γ′_{t}
Γ′_{t} = Γ_{t} ⊎ {x:τ}

The algorithm is initialized by taking the program heap H as the initial from-heap and the minimal type assignment of the program expression as Γ_{s}. At each step in the algorithm, Γ_{s} describes the types of all locations that are immediately reachable from e or H_{t}, but have not yet been forwarded to H_{t}. Γ_{t} describes the types of all locations that have been forwarded to H_{t}.^{2}

When a variable x is found in Γ_{s} with type τ and x is bound in H_{f} to the heap value h, the collector forwards the binding x = h to H_{t} and adds x:τ to Γ_{t}. It then uses Tag[τ] to traverse h, placing the necessary type information on the components so that MTA can determine the heap value’s minimal type assignment. This step provides the locations (and their types) that are immediately reachable from h. Finally, the collector adds each of these locations to Γ_{s} unless they have already been forwarded to H_{t}.

Using this algorithm instead of an a priori partitioning of the heaps, mono-a becomes a high-level specification of a collector whose traversal of heap values uses types instead of tag information:

(mono-a)

letrec H in e ⟼^{mono-a} letrec H′ in e

if

⟨H, MTA(e), ∅, ∅⟩ ⟹^{mono}^{∗}⟨H′′, ∅, H′, Γ⟩

The following definition gives the primary invariants of the algorithm:

Definition 4.7 (mono-a Invariants) ⟨H_{f} , Γ_{s}, H_{t}, Γ_{t}⟩ satisfies the mono-a invariants with respect to a program letrec H in e and type assignment Γ_{0} iff:

1. H = H_{f} ⊎ H_{t}
2. Γ_{s} ⊎ Γ_{t} ▷ e
3. Dom(Γ_{s}) ⊆ Dom(H_{f})
4. Γ_{s} ▷ H_{t} : Γ_{t}
5. Γ_{s} ⊎ Γ_{t} ⊆ Γ_{0}

Intuitively, the invariants guarantee (1) that each binding is accounted for, (2) every binding needed for e is in the scan-set or to-heap, (3) the scan-set corresponds to bindings in the from-heap, (4) the scan-set holds all free variables in the to-heap, and (5) the scan-set and to-heap agree with Γ_{0}.

Lemma 4.8 If ∅ ▷ H : Γ_{0}, T has the mono-a invariant properties with respect to P and Γ_{0}, and T ⟹^{mono} T′, then T′ has the mono-a invariant properties with respect to P and Γ_{0}.

2The garbage collection rewriting system only maintains Γ_{t} to simplify the presentation and proof; an implementation will not have to construct Γ_{t}.

The correctness of the algorithmic type-based garbage collection rule can now easily be verified.

Theorem 4.9 If P is a well formed program and P ⟼^{mono-a} P′, then P ⟼^{mono} P′.

Proof: We must verify that the mono-a garbage collection rule preserves typability in order for mono to apply. That is, we must show that if P is a well formed program, and P ⟼^{mono-a} P′, then ▷ P′.

Let P = letrec H in e and suppose ▷ P. Then, for some Γ_{0}, ∅ ▷ H : Γ_{0} and Γ_{0} ▷ e. If

⟨H, MTA(e), ∅, ∅⟩ ⟹^{mono}^{∗}⟨H′′, ∅, H′, Γ_{t}⟩,

then by Lemma 4.8 taking Γ_{s} = ∅, we know that ∅ ▷ H′ : Γ_{t} and Γ_{t} ▷ e . Thus, by the prog rule of the static semantics, ▷ letrec H′ in e. □

Furthermore, the algorithm never gets stuck, so it always applies:

Theorem 4.10 If P is a well formed program, then there exists a program P′ such that P ⟼^{mono-a} P′.

Proof: If the algorithm takes a step, the size of the from-heap strictly decreases, so we know the collection either terminates or gets stuck. Here we show that the collection cannot get stuck, so it must terminate. Suppose P = letrec H in e and ⟨H, MTA(e), ∅, ∅⟩ ⟹^{mono} ^{∗}⟨H_{f} , Γ_{s} ⊎ {x:τ}, H_{t}, Γ_{t}⟩. By Lemma 4.8, we know that x ∈ Dom(H_{f}), since the domain of the scan type-assignment is a subset of the from-heap. Consequently, there exists an h such

that H_{f} = H′_{f} ⊎ {x = h} and ⟨H_{f} , Γ_{s} ⊎ {x:τ}, H_{t}, Γ_{t}⟩ ⟹^{mono}

∗⟨H′_{f} , Γ′_{s}, H_{t} ⊎ {x = h}, Γ′_{t}⟩ with appropriate Γ′_{t} and Γ′_{s}. □

Extending the mono-a collection algorithm to work for a language with explicit polymorphism, where types are passed to polymorphic routines at run time as suggested by various language implementors [21, 1, 27, 15], is straightforward because enough information is preserved by evaluation to always reconstruct the type of a polymorphic object. In our technical report [20], we show how this may be accomplished.

5 Collecting Reachable Garbage Using Type Inference

Thus far, we have only considered specifications and algorithms for collecting unreachable bindings. In this section, we show that by using type inference during the garbage collection process, some bindings that are reachable can still be safely collected. That is, type inference can be used to prove that an object is garbage even though it is reachable.

For a simple example, consider the following λgc program:

letrec {x_{1} = 1, x_{2} = 2, x_{3} = ⟨x_{2}, x_{2}⟩, x_{4} = ⟨x_{1}, x_{3}⟩} in π_{1} x_{4}

Every binding in the heap is accessible from the program’s expression (π_{1} x_{4}), so the free-variable based collection rules can collect nothing. But clearly the program will never dereference x_{3} nor x_{2}. The inference-based collection scheme described in this section will allow us to conclude that replacing the binding x_{3} = ⟨x_{2}, x_{2}⟩ with x_{3} = 0 (or any other binding) will have no observable effect on evaluation. That is, the inference collection scheme shows that

letrec {x_{1} = 1, x_{2} = 2, x_{3} = 0, x_{4} = ⟨x_{1}, x_{3}⟩} in π_{1} x_{4}

is Kleene equivalent to the original program. Now by applying the free-variable rule, we can conclude that the binding x_{2} = 2 can be safely collected.

We start by considering the original λgc language as an implicitly typed, monomorphic language, where the types of the language are the same as for λgc-mono except for the addition of type variables:

(types) τ ∈ Type ::= t | int | τ_{1} × τ_{2} | τ_{1} → τ_{2}

By implicitly typed, we mean that the terms of the language are not decorated with types as in λgc-mono. We add type variables to the set of types so that each well-formed expression has a principal or most general type (explained below).

Type inference is the process of decorating λgc programs with types so that the resulting program type checks under the λgc-mono rules. (Refer to Figure 1 for the syntax and dynamic semantics of λgc and Figure 3 for the typing rules for λgc-mono.) Alternatively, we may directly specify a set of typing rules for λgc programs by taking the typing rules for λgc-mono and erasing the type information from the terms, resulting in the inference system of Figure 4. These rules define judgements of the form Γ ⊢ e : τ, where Γ is a type assignment, e is a λgc expression, and τ is a type.

A given λgc expression can have multiple typing derivations according to these rules and consequently multiple typings, but an expression’s typings may be ordered so that there is a most general, or principal typing and every other typing is an instance of this principal typing and is thus derivable.

We will show that if we can find a typing for a program that assigns a heap location a type variable, then the contents of that location has no effect on the rest of evaluation. Consequently, any pointers contained in the location’s binding do not need to be scanned and traced during garbage collection. The intuition behind the theorem is that a location’s type is unconstrained only if the location is not used in some manner that would constrain the type. Consequently, we can replace the binding in the heap with any binding we choose. In particular, if the location is bound to a large heap value, we can bind the location to an integer or dummy piece of code without affecting evaluation. This replacement allows us to collect any bindings that used to be reachable through this binding without knowing anything about the shape of the original heap value.

The proof of the theorem relies upon a semantic interpretation of types as logical relations. In our case, the relations are a type-indexed family of binary relations relating programs to programs, answers to answers, and heaps to heaps. The relations are contrived so that, if two programs are related, then they are Kleene equivalent, so one program converges to an answer iff the other converges to a related answer and related answers at base type (int) yield equal values. Roughly speaking, the relations are logically extended to relate answers of functional type (→) if, whenever such answers are applied to appropriately related answers, the resulting computations yield related results. Our proof only covers programs without cycles in their heaps, but it should be possible to extend our arguments to all programs (see below for more details).

The relations are defined in Figure 5 by induction on types. The definitions are parameterized by an arbitrary

(var) \overline{Γ ⊎ \{x:τ\} ⊢ x : τ} (int) \overline{Γ ⊢ i : int}

(tuple) \frac{Γ ⊢ e_{1} : τ_{1}  Γ ⊢ e_{2} : τ_{2}}{Γ ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2}}  (proj) \frac{Γ ⊢ e : τ_{1} × τ_{2}}{Γ ⊢ π_{i} e : τ_{i}} (i = 1, 2)

(fn) \frac{Γ ⊎ \{x:τ_{1}\} ⊢ e : τ_{2}}{Γ ⊢ λx.e : τ_{1} → τ_{2}}  (app) \frac{Γ ⊢ e_{1} : τ_{1} → τ_{2}  Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}

(heap) \frac{∀ x ∈ Dom(Γ′) . Γ ⊎ Γ′ ⊢ H(x) : Γ′(x)}{Γ ⊢ H : Γ′}  (prog) \frac{∅ ⊢ H : Γ  Γ ⊢ e : τ}{⊢ letrec H in e : τ}

Figure 4: Type Inference Rules for λgc

relational interpretation of type variables, Θ. If t is a type variable, then Θ(t) determines some fixed, but arbitrary relation between answer programs. This is consistent with the idea that well-typed programs have an implicit “∀” quantifier for the type variables in a program. The parameterization of the interpretation of type variables makes it straightforward to extend the definition of the relations to account for predicative polymorphism.

Two well-typed programs P_{1} and P_{2} are related at a type τ, written Θ ⊧ P_{1} ∼ P_{2} : τ iff, whenever one of the programs terminates with an answer, then the other program terminates with a related answer at type τ.

Two answers A_{1} and A_{2} are related at type τ, written Θ ⊧ A_{1} ≈ A_{2} : τ, as follows: If τ is a type variable t, then the answers are related iff they are in the relation Θ(t). The relation is extended to the other types in a natural fashion. For example, if τ is an arrow type τ_{1} → τ_{2}, the answers are related iff, whenever we apply the answer variables to related arguments at type τ_{1}, we get related programs at type τ_{2}. Even though the relations between programs and answers are defined in terms of one another, the relations are well-founded because the size of the type index always decreases when one relation refers to another.

The definition of the relations ensures that related programs remain related even if more bindings are added to the programs’ heaps. Since evaluation only adds new bindings and leaves existing bindings intact, it is clear that evaluation preserves the relations. If the language permitted assignment, then this property would not necessarily hold.

For the statement of the following lemma, we need to extend the logical relation on answers to heaps. Two heaps, H_{1} and H_{2}, are related at a context Γ, written Θ ⊧ H_{1} ≈ H_{2} : Γ if for all variables x in Γ, the answers letrec H_{1} in x and letrec H_{2} in x are related at Γ(x).

The following lemma is the key to establishing our result: an expression is related to itself in the context of any two related heaps.

Lemma 5.1 For all Θ : T var → P(Ans × Ans), if Γ ⊢ e : τ and Θ ⊧ H_{1} ≈ H_{2} : Γ, then Θ ⊧ letrec H_{1} in e ∼ letrec H_{2} in e : τ.

Proof (sketch): By induction on the derivation of Γ ⊢ e : τ. Here we give the interesting case (fn). Suppose Γ ⊢ λx.e : τ_{1} → τ_{2} and Θ ⊧ H_{1} ≈ H_{2} : Γ. By alloc,

letrec H_{1} in λx.e ⟼^{alloc} letrec H_{1} ⊎ {y_{1} = λx.e} in y_{1}
letrec H_{2} in λx.e ⟼^{alloc} letrec H_{2} ⊎ {y_{2} = λx.e} in y_{2}

for some fresh y_{1} and y_{2}. We must show that the two resulting answers are appropriately related.

Let H′_{1} and H′_{2} be heaps such that H_{i}⊎{y_{i} = λx.e} ⊆ H′_{i} for i = 1, 2, and

Θ ⊧ letrec H′_{1} in z_{1} ≈ letrec H′_{2} in z_{2} : τ_{1}

for some z_{1} and z_{2}. We must show that

Θ ⊧ letrec H′_{1} in y_{1} z_{1} ∼ letrec H′_{2} in y_{2} z_{2} : τ_{2}.

Taking H′′_{i} = H′_{i} ⊎ {x = H′_{i}(z_{i})}, this follows if

Θ ⊧ letrec H′′_{1} in e ∼ letrec H′′_{2} in e : τ_{2}.

By the induction hypothesis, it suffices to show that

Θ ⊧ H′′_{1} ≈ H′′_{2} : Γ ⊎ {x : τ_{1}}.

since e has a smaller typing derivation than λx.e. By the lemma’s hypothesis, we know that Θ ⊧ H_{1} ≈ H_{2} : Γ, and since heaps remain related under extensions, Θ ⊧ H′′_{1} ≈ H′′_{2} : Γ. By assumption,

Θ ⊧ letrec H′′_{1} in z_{1} ≈ letrec H′′_{2} in z_{2} : τ_{1}.

Since H′′_{i} = H′_{i} ⊎ {x = H′_{i}(z_{i})}, it is easy to show that

Θ ⊧ letrec H′′_{1} in x ≈ letrec H′′_{2} in x : τ_{1}

Consequently, H′′_{1} and H′′_{2} have related heap-values for each variable in Γ⊎{x : τ_{1}} and thus Θ ⊧ H′′_{1} ≈ H′′_{2} : Γ⊎{x : τ_{1}}. The other cases follow in a similar manner. □

Our goal is to show that if Γ is a type assignment, e an expression, and H a heap such that Γ ⊢ e : τ and ∅ ⊢ H : Γ, then letrec H′ in e is Kleene equivalent to letrec H in e where H′ is defined as follows:

H′ = {x = H(x) | Γ(x) ∉ T var} ⊎ {x = 0 | Γ(x) ∈ T var}

This follows from Lemma 5.1 if we can show that, taking Θ_{0}(t) to be the everywhere-defined relation on answer programs, Θ_{0} ⊧ H ≈ H′ : Γ. This in turn follows if we can show that Θ_{0} ⊧ H ≈ H : Γ (H is related to itself), since Θ_{0}(t) relates every program and H′(x) differs from H(x) only when Γ(x) = t.

Unfortunately, we cannot directly show that a well formed heap is related to itself! The problem is that if we attempt to argue by induction on the derivation of ∅ ⊢ H : Γ, the uses of the heap rule require that we assume what we Computations:

Θ ⊧ P_{1} ∼ P_{2} : τ iff ⊢ P_{1} : τ and ⊢ P_{2} : τ and

P_{1} ⇓_{R} A_{1} implies P_{2} ⇓_{R} A_{2} and Θ ⊧ A_{1} ≈ A_{2} : τ and P_{2} ⇓_{R} A_{2} implies P_{1} ⇓_{R} A_{1} and Θ ⊧ A_{1} ≈ A_{2} : τ

Answers:

Θ ⊧ A_{1} ≈ A_{2} : t  iff ⟨A_{1}, A_{2}⟩ ∈ Θ(t)
Θ ⊧ letrec H_{1} in x_{1} ≈ letrec H_{2} in x_{2} : int  iff H_{1}(x_{1}) = H_{2}(x_{2}) = i
Θ ⊧ letrec H_{1} in x_{1} ≈ letrec H_{2} in x_{2} : τ_{1} × τ_{2} iff Θ ⊧ letrec H_{1} in π_{1} x_{1} ∼ letrec H_{2} in π_{1} x_{2} : τ_{1}

and Θ ⊧ letrec H_{1} in π_{2} x_{1} ∼ letrec H_{2} in π_{2} x_{2} : τ_{2}

Θ ⊧ letrec H_{1} in x_{1} ≈ letrec H_{2} in x_{2} : τ_{1} → τ_{2} iff ∀H′_{1}, H′_{2}, y_{1}, y_{2},

Θ ⊧ letrec H_{1} ⊎ H′_{1} in y_{1} ≈ letrec H_{2} ⊎ H′_{2} in y_{2} : τ_{1} implies Θ ⊧ letrec H_{1} ⊎ H′_{1} in x_{1} y_{1} ∼ letrec H_{2} ⊎ H′_{2} in x_{2} y_{2} : τ_{2}

Figure 5: Relational Interpretation of Types

are trying to prove. The same problem is encountered when using logical relations to reason about conventional calculi with recursion or iteration operators.

If we forbid cycles in the heap, then we can transform the derivation of the heap’s well formedness into a derivation that only uses a let-style rule instead of the recursive letrecstyle heap rule:

(let-heap) \frac{Γ_{1} ⊎ Γ_{2} ⊢ h : τ Γ_{1} ⊢ H : Γ_{2}}{Γ_{1} ⊢ H ⊎ \{x = h\} : Γ_{2} ⊎ \{x:τ\}}

Consequently, if a heap is cycle free, we may show by induction on the derivation using the let-heap rule that the heap is related to itself.

Lemma 5.2 If Γ_{1} ⊢ H : Γ_{2}, Θ ⊧ H_{1} ≈ H_{2} : Γ_{1} and H is cycle free, then Θ ⊧ H_{1} ⊎ H ≈ H_{2} ⊎ H : Γ_{1} ⊎ Γ_{2}.

Finally, we can state and prove the following Inference GC specification: Given a cycle-free program, if we can find a typing that assigns a heap location a type variable, then that location can be bound to “0” without effecting evaluation.

Theorem 5.3 (Inference GC) Let Γ_{1} = {x_{1}:t_{1}, …, x_{n}:t_{n}} and H_{1} = {x_{1} = h_{1}, …, x_{n} = h_{n}} and H′_{1} = {x_{1} = 0, …, x_{n} = 0}. If

1. Γ_{1} ⊎ Γ_{2} ⊢ e : τ (τ ∉ T var), and

2. Γ_{1} ⊢ H_{2} : Γ_{2}, and

3. ∃S.∅ ⊢ H_{1} : SΓ_{1}, and

4. H_{2} is cycle free,

then letrec H_{1} ⊎ H_{2} in e ≃ letrec H′_{1} ⊎ H_{2} in e.

Proof: Taking Θ_{0}(t) to be the everywhere defined relation, Θ_{0} ⊧ H_{1} ≈ H′_{1} : Γ_{1} holds trivially. By Lemma 5.2, since H_{2} is cycle free and Γ_{1} ⊢ H_{2} : Γ_{2}, we know that

Θ_{0} ⊧ H_{1} ⊎ H_{2} ≈ H′_{1} ⊎ H_{2} : Γ_{1} ⊎ Γ_{2}.

Since Γ_{1} ⊎ Γ_{2} ⊢ e : τ, we know by Lemma 5.1 that

Θ_{0} ⊧ letrec H_{1} ⊎ H_{2} in e ∼ letrec H′_{1} ⊎ H_{2} in e : τ.

Thus, letrec H_{1} ⊎ H_{2} in e ⇓ letrec H_{a} in x iff letrec H′_{1} ⊎ H_{2} in e ⇓ letrec H_{b} in y and

Θ_{0} ⊧ letrec H_{a} in x ≈ letrec H_{b} in y : τ.

Suppose H_{a}(x) = i (or H_{b}(y) = i). Then τ must be int since τ ∉ T var by the first hypothesis. By the definition of ≈ at int, H_{b}(y) = i (or H_{a}(x) = i). Thus,

letrec H_{1} ⊎ H_{2} in e ≃ letrec H′_{1} ⊎ H_{2} in e.
□

Using the Inference GC theorem, we can now show that the binding x_{3} = ⟨x_{2}, x_{2}⟩ in the program:

letrec {x_{1} = 1, x_{2} = 2, x_{3} = ⟨x_{2}, x_{2}⟩, x_{4} = ⟨x_{1}, x_{3}⟩} in π_{1} x_{4}

can be replaced by x_{3} = 0. Taking Γ_{1} = {x_{2}: t_{2}, x_{3}: t_{3}}, Γ_{2} = {x_{1}: int, x_{4}: int × t_{3}}, H_{1} = {x_{2} = 2, x_{3} = ⟨x_{2}, x_{2}⟩}, H_{2} = {x_{1} = 1, x_{4} = ⟨x_{1}, x_{3}⟩} it is easy to show that the preconditions of the theorem hold. Consquently, replacing H_{1} with H′_{1} = {x_{2} = 0, x_{3} = 0} results in a Kleene equivalent program:

letrec {x_{1} = 1, x_{2} = 0, x_{3} = 0, x_{4} = ⟨x_{1}, x_{3}⟩} in π_{1} x_{4}.

Now by invoking fv, we can collect the binding x_{2} = 0:

letrec {x_{1} = 1, x_{3} = 0, x_{4} = ⟨x_{1}, x_{3}⟩} in π_{1} x_{4}

and we know that the resulting program is Kleene equivalent to the original program.

6 Related Work

The literature on garbage collection in sequential programming languages per se contains few papers that attempt to provide a compact characterization of algorithms or correctness proofs. Demers et al. [10] give a model of memory parameterized by an abstract notion of a “points-to” relation. As a result, they can characterize reachability-based algorithms including mark-sweep, copying, generational, “conservative,” and other sophisticated forms of garbage collection. However, their model is intentionally divorced from the programming language and cannot take advantage of any semantic properties of evaluation, such as type preservation. Consequently, their framework cannot model the type-based collectors of Sections 4 and 5. Nettles [22] provides a concrete specification of a copying garbage collection algorithm using the Larch specification language. Our specification of the free-variable tracing algorithm is essentially a high-level, one-line description of his specification.

Hudak gives a denotational model that tracks reference counts for a first-order language [16]. He presents an abstraction of the model and gives an algorithm for computing approximations of reference counts statically. Chirimar, Gunter, and Riecke give a framework for proving invariants regarding memory management for a language with a linear type system [9]. Their low-level semantics specifies explicit memory management based on reference counting. Both Hudak and Chirimar et al. assume a weak approximation of garbage (reference counts). Barendsen and Smetsers give a Curry-like type system for functional languages extended with uniqueness information that guarantees an object is only “locally acccessible” [6]. This provides a compiler enough information to determine when certain objects may be garbage collected or over-written.

Tolmach [27] built a type-recovery collector for a variant of SML that passes type information to polymorphic routines during execution, effectively implementing a polymorphic version of our language and collector described in Section 4. Aditya and Caro gave a type-recovery algorithm for an implementation of Id that uses a technique that appears to be equivalent to type passing [1] and Aditya, Flood, and Hicks extended this work to garbage collection for Id [2].

Over the past few years, a number of papers on inferencebased collection in monomorphic [7, 29, 8] and polymorphic [3, 13, 14, 12] languages appeared in the literature. Appel [3] argued informally that “tag-free” collection is possible for polymorphic languages such as SML by a combination of recording information statically and performing what amounts to type inference during the collection process, though the connections between inference and collection were not made clear. Baker [5] recognized that Milnerstyle type inference can be used to prove that reachable objects can be safely collected, but did not give a formal account of this result. Goldberg and Gloger [14] recognized that it is not possible to reconstruct the concrete types of all reachable values in an implementation of an ML-style language that does not pass types to polymorphic routines. They gave an informal argument based on traversal of stack frames to show that such values are semantically garbage. Fradet [12] gave another argument based on Reynolds’s abstraction/parametricity theorem [24]. Fradet’s formulation is closer to ours than Goldberg and Gloger’s, since he represented the evaluation “stack” as a source-language term. However, none of these papers give a complete formulation of the underlying dynamic and static semantics of the language and thus the proofs of correctness are necessarily ad hoc.

Finally, Purushothaman and Seaman [23, 25] and Launchbury [17] have proposed “natural” semantics for callby-need (lazy) languages where the semantic objects include an explicit heap. This allows sharing and memoization of computations to be expressed in the semantics. More recently, Ariola et al. [4] have presented a purely syntactic theory of the call-by-need λ-calculus that is largely compatible with our work.

7 Summary and Future Work

Our paper provides a unifying framework for a variety of garbage collection ideas including standard copying and marksweep collection, generational collection, tag-free collection, and inference-based collection. By making allocation and the heap explicit, we are able to reason about memory management using traditional λ-calculus techniques. In particular, we are able to make strong connections between garbage collection and type theory. By abstracting away such lowlevel details as evaluation stacks, registers, and addresses, we are able to formulate complicated collection algorithms in a compact manner and yet give a formal proof of correctness.

The framework is flexible, as demonstrated by the breadth of topics covered in this paper, and we expect that the framework can be extended to deal with other work on garbage collection. In the future, we hope to extend the Inference GC theorem of Section 5 to cover programs with cyclic heaps. One approach is to interpret types as CPOs and prove that programs have a suitable compactness property: every cyclic heap is appropriately approximated by some finite “unwinding” of the heap. An alternative approach might be to provide a purely syntactic argument that locations assigned a type variable never arise in an “active” position during evaluation. We also hope to provide a proof of correctness for an algorithm that simultaneously infers types and performs garbage collection.

8 Acknowledgements

Thanks to Edo Biagoni, Andrzej Filinski, Mark Leone, Jack Morrisett, Chris Okasaki, Andrew Tolmach, and Jeannette Wing for proofreading earlier drafts of this document and for providing valuable insight. This manuscript is submitted for publication with the understanding that the U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes, notwithstanding any copyright notation thereon.

References

[1] S. Aditya and A. Caro. Compiler-directed type reconstruction for polymorphic languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture, pages 74–82, Copenhagen, Denmark, June 1993.

[2] S. Aditya, C. Flood, and J. Hicks. Garbage collection for strongly-typed languages using run-time type reconstruction. In Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, pages 12–23, Orlando, FL, June 1994.

[3] A. W. Appel. Runtime tags aren’t necessary. Journal of Lisp and Symbolic Computation, 2:153–162, 1989.

[4] Z. M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages, San Francisco, CA, Jan. 1995.

[5] H. Baker. Unify and conquer (garbage, updating, aliasing ...) in functional languages. In Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 218–226, Nice, France, June 1990.

[6] E. Barendsen and S. Smetsers. Conventional and uniqueness typing in graph rewrite systems. In Proceedings of the 13th Conference on the Foundations of Software Technology and Theoretical Computer Science 1993, Bombay, New York, NY, 1993. Springer-Verlag. Extended abstract.

[7] P. Branquart and J. Lewi. A scheme for storage allocation and garbage collection for Algol-68. In Algol-68 Implementation. North-Holland Publishing Company, Amsterdam, 1970.

[8] D. E. Britton. Heap storage management for the programming language Pascal. Master’s thesis, University of Arizona, 1975.

[9] J. Chirimar, C. A. Gunter, and J. G. Riecke. Proving memory management invariants for a language based on linear logic. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 139–150, San Francisco, CA, June 1992.

[10] A. Demers, M. Weiser, B. Hayes, H. Boehm, D. Bobrow, and S. Shenker. Combining generational and conservative garbage collection: Framework and implementations. In Conference Record of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 261–269, San Francisco, CA, Jan. 1990.

[11] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Technical Report 89-100, Rice University, June 1989. Also appears in: Theoretical Computer Science, 102, 1992.

[12] P. Fradet. Collecting more garbage. In Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, pages 24–33, Orlando, FL, June 1994.

[13] B. Goldberg. Tag-free garbage collection for strongly typed programming languages. In Proceedings of the ACM SIGPLAN ’91 Conference on Programming Language Design and Implementation, pages 165–176, Toronto, Ontario, Canada, June 1991.

[14] B. Goldberg and M. Gloger. Polymorphic type reconstruction for garbage collection without tags. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 53–65, San Francisco, CA, June 1992.

[15] R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Conference Record of the 22nd Annual ACM Symposium on Principles of Programming Languages, San Francisco, CA, Jan. 1995.

[16] P. Hudak. A semantic model of reference counting and its abstraction. In Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, pages 351–363, Cambridge, MA, 1986.

[17] J. Launchbury. A natural semantics for lazy evaluation. In Conference Record of the 20th Annual ACM Symposium on Principles of Programming Languages, Charleston, SC, Jan. 1993.

[18] I. Mason and C. Talcott. Reasoning about programs with effects. In Proceedings of Programming Language Implementation and Logic Programming, LNCS 582. Springer-Verlag, 1990.

[19] I. Mason and C. Talcott. Equivalences in functional languages with effects. Journal of Functional Programming, 2(1), 1991.

[20] G. Morrisett, M. Felleisen, and R. Harper. Abstract models of memory management. Technical Report CMU–CS–95–110, School of Computer Science, Carnegie Mellon University, Jan. 1995. Available as

ftp://reports.adm.cs.cmu.edu/usr/anon/1995/CMU-CS-95-
110.ps.

[21] R. Morrison, A. Dearle, R. C. H. Connor, and A. L. Brown. An ad hoc approach to the implementation of polymorphism. ACM Trans. Prog. Lang. Syst., 13(3):342–371, July 1991.

[22] S. Nettles. A Larch specification of copying garbage collection. Technical Report CMU–CS–92–219, School of Computer Science, Carnegie Mellon University, Dec. 1992.

[23] Purushothaman and J. Seaman. An adequate operational semantics of sharing in lazy evaluation. In Proceedings of the 4th European Symposium on Programming, LNCS 582. Springer-Verlag, 1992.

[24] J. Reynolds. Types, abstraction, and parametric polymorphism. In Proceedings of Information Processing 83, pages 513–523, 1983.

[25] J. M. Seaman. An Operational Semantics of Lazy Evaluation for Analysis. PhD thesis, Pennsylvania State University, 1993.

[26] P. Steenkiste and J. Hennessey. Tags and type checking in LISP: Hardware and software approaches. In Proceedings of the Second International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS-II), pages 50–59, Palo Alto, CA, Oct. 1987.

[27] A. Tolmach. Tag-free garbage collection using explicit type parameters. In Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, pages 1–11, Orlando, FL, June 1994.

[28] D. Ungar. Generational scavenging: A non-disruptive high performance storage management reclamation algorithm. In ACM SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 15–167, Pittsburgh, PA, Apr. 1984.

[29] P. Wodon. Methods of garbage collection for Algol-68. In Algol-68 Implementation. North-Holland Publishing Company, Amsterdam, 1970.

[30] A. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Department of Computer Science, Rice University, Apr. 1991.