Memory Management with Use-Counted Regions

Tachio Terauchi

Alex Aiken

Report No. UCB/CSD-4-1314
March 2004
Computer Science Division (EECS)University of California
Berkeley, California 94720

Memory Management with Use-Counted Regions ∗Tachio Terauchi

Alex Aiken

EECS Department
University of California, Berkeley
Berkeley, CA 94720-1776
tachio@cs.berkeley.edu
March 29, 2004

Abstract
We introduce a new region-based memory management technique that allows flexible memory usage
patterns and is provably safe. Our technique is explicit and manual like C’s malloc and free, and it
allows programmers to exert a similar degree of control over program behavior. Our method is quite
simple in spite of this expressiveness and safety.
We apply the technique to a small functional language to formally describe the core concepts, prove
its safety, and argue its usability and efficiency analytically. In particular, we show that the system canefficiently encode more rigid, traditional regions whose lifetime is bounded by that of a stack frame. We
also show that the technique works nicely with multi-threaded and imperative programs.

1

Introduction

In software practice, there are two widely-used heap memory management approaches: explicit management
via malloc and free or implicit management via garbage collection. Both approaches have well-known
disadvantages. The problem with malloc and free is that verifying memory safety is difficult. Garbage
collection overcomes this problem at the cost of making it difficult to control when objects are deallocated,which makes garbage collection unattractive in situations that require tight space or timing guarantees.
In addition, experienced programmers can often produce more efficient code given the ability to do manual
memory management. Thus a memory management system that allows programmers to exert manual control
and yet be provably safe is of practical interest.
Recently, there have been a number of proposals [4, 18, 9, 2, 11] based on the concept of regions [14, 15],
that allow safe, explicitly controlled memory management. All of these systems (with the exception of
portions of the work by Hicks et al. [11] which was developed independently from our work around the sametime) guarantee safety at compile time.
This paper presents a new mostly-static, memory-safe region system. It is not totally static in the same
sense as the systems listed above because the deletion of a region could fail and result in a run-time error,
and the programmer is required to add run-time checks to see if regions are alive at strategic points in the
program. The system is mostly static because it guarantees at compile time that no other run-time checks
are necessary for the program to be memory safe. Also, unlike dangling pointer dereferences, our run-timeerrors are well-behaved and the program can recover by, for example, catching the thrown exception as in
ML and Java.
Compared to a totally-static approach, our system has a slightly weaker memory-safety guarantee. 1 But
we believe that there are enough benefits with our mostly-static approach to justify the trade-off. One∗ This research was supported in part by Subcontract no. PY-1099 to Stanford, Dept. of the Air Force prime contract no.
F33615-00-C-1693.
1 Though in principle, any well-behaved run-time error is a part of the program semantics, and therefore we could argue that
our system is just as static.

1

U, V, W, X, Y, Z ∈ RegVars ∪ {Xsr }types
expressions

τ
e

::=
::=

u, v, w, x, y, z ∈ Vars ∪ {sr}L ⊆finite RegVars ∪ {Xsr }r, s, t ∈ Regions

L(∀~X.τ1 −→ τ2 )@Y | ~τ @X | reg(X)@Y | ∃X.τx | let x = e1 in e2 | Λ~Xλx:τ.e1 at e2 | e[X] | e1 e2 | ~e at e | e.i | pack e as ∃X.τ | open x = e1 as τ in e2 |newregion at e | freeregion e | useregion e 1 in e2

Figure 1: Small region language: source syntax
drawback of a totally static approach is that it often trades simplicity and ease-of-use for expressivenessbecause a simple static system often limits the kind of programs that can be proven safe. In contrast, oursystem allows a high degree of expressiveness without complicating the static system. In particular, a region’s
lifetime is not tied to a stack frame, and instead regions may be created and deleted at any program point.
We also argue in Section 4.2 that a run-time error is likely to indicate a bug in the programmer’s thinking
rather than a limitation of the system.
Our technique is best understood by conceptually dividing it into a static part and a dynamic part.
The static part is simple, based on a type system resembling that of Tofte et al. [15]. The dynamic part is
simple for the most basic implementation, which we shall stick with until Section 3. The run-time behavior
is transparent to the programmer. That is, the programmer can easily tell from the source code when each
dynamic check occurs, which is important for control.
We now describe the core concepts of our technique, which we call use counting. (We shall slightly modify
these concepts in Section 3 to enable further flexibility). The run-time system maintains two data values
per region:• Validity bit: indicating whether region has been deleted (= 0) or not (= 1).
• Use counter: a non-negative integer which starts from 0 and is incremented and decremented explicitly
by the program.
Via a combination of static and dynamic checks, we enforce the following:(1) When accessing a memory location, the use counter of the region containing the memory location isgreater than 0.
(2) When deleting a region, the region’s use counter is 0.
(3) When incrementing the use counter of a region, the region’s validity bit is 1.
It is not hard to see that these conditions are sufficient for memory safety: dangling references are neveraccessed. We check the condition (1) statically and check (2) and (3) dynamically. Since deletions are
explicit, dynamic checks for (2) are transparent. Incrementing a use counter is also explicit, so dynamic
checks for (3) are also transparent.
The trick, then, is to make the static check for (1) simple. To this end, we design the language so that
programs adhere to a certain syntactic pattern when incrementing and decrementing use counters. Consider
the following pseudo-code. Suppose r denotes some region.
increment uc(r). . . use r . . .
decrement uc(r)The operations increment uc(r) and decrement uc(r) respectively increment and decrement the use
counter of r. Our proposal is to force programs to adhere to this block pattern when manipulating a
use counter. To this end, instead of increment uc(r) and decrement uc(r), we introduce a single language
construct for increment and decrement:
useregion e1 in e22values
expressions

v
e

::=
::=

pack v as • | Λ•λx:•.e at r | ~v at r | reg r at s | abortx | let x = e1 in e2 | Λ•λx:•.e1 at e2 | e[•] | e1 e2 | ~e at e | e.i | pack e as • | open x = e1 as • in e2 |newregion at e | freeregion e | useregion e 1 in e2 | v | inuse (reg r at s) in econtexts

E::=[ ] | let x = E in e | Λ•λx:•.e at E | E[•] | E e | v E |(~v, E, ~e) at e | ~v at E | pack E as • | open x = E as • in e |newregion at E | freeregion E | useregion E in e | inuse (reg r at s) in E

Figure 2: Small region language: type-erased intermediate expressions and evaluation contexts
R(r) = (1, −)R(s) = (1, −)R, E[Λ•λx:•.e at (reg r at s)]→ R, E[Λ•λx:•.e at r]

R(r) = (1, −)R, E[(Λ•λx:•.e at r) v]→ R, E[e[v/x]][F1]

R, E[open x = (pack v as •) as • in e] → R, E[e[v/x]]

R(s) = (1, −)R ] {r 7→ (−, 0)}, E[freeregion (reg r at s)]→ R ] {r 7→ (0, 0)}, E[reg r at s]

[E]

[R2]

[F2]

R, E[v[•]] → R, E[v]R(r) = (1, −)R(s) = (1, −)R, E[newregion at (reg r at s)]→ R ] {t 7→ (1, 0)}, E[pack (reg t at r) as •]R(s) = (1, −)i>0
R ] {r 7→ (−, i)}, E[freeregion (reg r at s)]→ R ] {r 7→ (−, i)}, abort

R(s) = (1, −)R ] {r 7→ (1, i)}, E[useregion (reg r at s) in e] → R ] {r 7→ (1, i + 1)}, E[inuse (reg r at s) in e]R(s) = (1, −)R ] {r 7→ (0, i)}, E[useregion (reg r at s) in e2 ]→ R ] {r 7→ (0, i)}, abort[R5]

R(s) = (1, −)R ] {r 7→ (b, i)}, E[inuse (reg r at s) in v]→ R ] {r 7→ (b, i − 1)}, E[v]which evaluates e1 to a use counter, increments it, executes e2 , then decrements the use counter after e2
finishes. From a programmer’s point of view, useregion enables access to the region within the lexical scope.
The resulting system is simple and easy to use, like stack-of-regions systems [9, 2], but enjoys expressivenesscomparable to more complex approaches.

Contributions and Overview

The main technical contributions of the paper are:• a formal presentation of the basic use-counting system and the proof of safety (Section 2).
• an improvement to the base system that increases usability (Section 3). This feature is not introduced
immediately in the paper since it is more natural to understand it as a modification to the base system.
• an analytical evaluation of the system, including efficient encoding of stack-of-regions style memory
management and multi-threaded programming (Sections 4 and 5).
In addition to the above, we provide small but illustrative examples throughout the paper. Section 6 discusses
our own experience with a toy implementation. Section 7 discusses related work, and Section 8 concludes.

3

[R1]

[R3]

[R4]

Figure 3: Small region language: selected reduction rules

1.1

[F3]

[R6]

2

Regions for a Small Language

We first apply use counting to a call-by-value monomorphic lambda calculus with tuples shown in Figure 1.
This small region language is designed to illustrate the new technique in a self-contained manner and therefore omits features such as parametric polymorphism over types and effect sets, recursive types, non-heap
allocated (i.e., unboxed) tuples, and mutable values. But these features can be incorporated with little additional effort by leveraging off previous research on region-based memory management (see, e.g., the work by
Grossman et al. [8] for an extensive study incorporating these features and more in a stack-of-regions styleframework). Appendix A shows the system extended with some of these features.
RegVars is an infinite set of region variables. Each region variable refers to some region. For example,La function closure allocated in the region referred to by Y has a type of the form (∀~X.τ1 −→ τ2 )@Y with τ1
as the argument type and τ2 as the return type. Note that the function may be polymorphic in the region
variables ~X, which are assumed to be distinct. (We use the notation ~a to mean some tuple (a1 , a2 , ..., an ).) In
addition, each function type carries a set of region variables, an effect set L. Similarly, a tuple of values (ofthe types ~τ ) allocated in X has the type ~τ @X. The type reg(X)@Y is the type of a region handle of the region
referred to by X. A region handle is a program value, so it is allocated in a region just like other program
values. Region handles are necessary because the validity bit and use counter for each region must be stored
somewhere; that is, each region handle is a pointer to a triple containing a pointer to the head of the region,a validity bit, and a use counter.2 The type ∃X.τ is an existential type, which is handy when typing data
structures containing region handles. (In theory, we can always encode them as higher-order polymorphic
functions, but existential packages are more natural.) We assume that expressions and types are equivalent
up to consistent renaming of bound variables and bound region variables.
A program is an expression whose only free variable is sr. The set of free variables for an expression isdefined in the usual way. The variable sr denotes a region handle of a special region, r sr . (It doesn’t matter
which region we pick to be special; we just need to pick one from Regions, an infinite set of regions, before
the program starts.) The region rsr is special because it is the only region that exists prior to the executionof the program; all other regions are created by the program. To see why we need this starting region, recall
that each region handle must itself be allocated somewhere. The core concepts described in Section 1 implies
that in order for a region to be deleted, its region handle cannot be allocated within the region itself. By
chain of reasoning, there must be at least one pre-existing region in which the first program-created region
handle is allocated. We show a way to remove this constraint in Section 3.

2.1

Dynamic Semantics

The dynamic semantics is a series of small-step reductions from states to states. A state is a pair (R, e)
where e is a program and R is a region map, which maps each region r in its domain to a pair (b, i) withr’s validity bit b and r’s use counter i. The starting state for the program e is ({r sr 7→ (1, 1)}, e). Notethat the starting region is accessible from the start. In fact, the starting region cannot be deleted and willremain always accessible, so the program never needs to manipulate its use counter. Single step reductions
are written
R1 , e1 → R 2 , e2
(We usually omit the parentheses.) Type and region variable information is irrelevant in reductions, so weerase it from expressions by replacing each occurrence of a type or a region variable by •. The result of thiserasure is an expression in the language of Figure 2.
Figure 3 shows selected reduction rules. Reductions may give rise to expressions in the intermediate
language and use evaluation contexts defined in Figure 2. We now discuss the reduction rules. To reduce afunction allocation Λ•λx:•.e1 at e2 , first e2 is reduced to a region handle reg r at s. Then [F1] reduces thewhole expression to a function closure Λ•λx:•.e1 at r. The expression reg r at s is a region handle for theregion r allocated in the region s. Every region handle is represented in this form. (So before the program
starts reducing, we replace every occurrence of sr by reg rsr at rsr .) In fact, every allocated program
2 Alternatively, we can implement a region handle as a double-word value consisting of a pointer to the head of the region

and a pointer to the pair containing the validity bit and the use counter to save dynamic checks at allocation sites.

4

value has the form
a at rmeaning the value denoted by a is allocated in the region r. So, Λ•λx:•.e1 at r is a function closure value
allocated in r.3 The condition R(r) = (1, −) of [F1] says that the region where the function is being allocatedmust be alive. (The symbol − is a wild card.) In addition, the condition R(s) = (1, −) is required becausea region handle also stores a pointer to the head of the region and this needs to be looked up.
The rule [F2] is for function application. It shows function application as the usual capture-avoiding
substitution assuming r, the region where the function is allocated, is alive. A region variable application,[F3], is essentially a no-op in this type-erasure semantics.
The rule [E] is for opening existential packages and is straightforward.
Once e in newregion at e is reduced to a region handle reg r at s, [R1] reduces newregion at (reg r at s)
by creating a new region t and reducing to a region handle of t allocated at r. The binary operation R 1 ] R2
is the union R1 ∪ R2 if dom(R1 ) ∩ dom(R2 ) = ∅ and undefined otherwise. For reasons explained later, the
new region handle is existentially packed. The conditions R(r) = (1, −) and R(s) = (1, −) are required
because allocating a region handle is like allocating any other program value, that is, the region where theregion handle is allocated must be alive as well as the region where the region handle itself resides.
The rules [R2] and [R3] handle freeregion e. We first reduce e to a region handle. Assuming that theuse counter of the region being deleted is 0, [R2] sets the validity bit of the region to 0, indicating that theregion is deleted. Otherwise the use counter of the region is greater than 0, and [R3] reduces the whole
program to the special value abort which signals a failure of the dynamic check. Alternatively, the language
could have been designed so that a dynamic check failure reduces to a special error value or raises a run-time
exception. Exactly what to do when a dynamic check fails is up to the language designer. Note that both
[R2] and [R3] require the assumption R(s) = (1, −) because the region handle for r allocated at s must be
looked up to see which of [R2] or [R3] applies.
The form useregion e1 in e2 increments and decrements a use counter. First, e1 is reduced to a region
handle of some region r, then if r’s validity bit is 1, the use counter is incremented and the whole expression
is reduced to inuse (reg r at s) in e2 as shown in [R4]. Otherwise the region’s validity bit is 0, and [R5]aborts the program. Both [R4] and [R5] require the assumption R(s) = (1, −) because the use counter andthe validity bit of r are accessed.
The rule [R6] reduces inuse (reg r at s) in e. First, e is reduced to the value v, then the use counter ofr is decremented and v is returned, assuming that the region where the use counter is allocated is alive.
Note that the run-time system does not physically check the conditions of the form R(r) = (1, −)appearing in any of the hypotheses in Figure 3. Violation of these conditions correspond to dangling pointerdereferences, and we show in Section 2.4 that a well-typed program never violates them.
However, a cautious reader may wonder how we can make safety claims by assuming that the validity
bits even exist in these hypothesis. What if the validity bit is deallocated prior to the reduction? To seethat such situation never occurs, observe that the dynamic semantics never deallocates any value; it justsets some validity bits to 0. In order to actually deallocate, we first argue as in the previous paragraph thatthe conditions of the form R(r) = (1, −) are not required if the program is known not to get stuck, which inturn lets us physically delete regions at [R2] as argued in Section 2.4.

2.2

Static Checking

As stated in Section 1, the role of the static checking is to check that when accessing a memory location,
the use counter of the region in which the memory location is allocated is greater than 0. The use counter isincremented before reducing e2 of useregion e1 in e2 and decremented after e2 reduces to a value. Therefore
3 This a at r notation may look strange to some readers. More commonly, when an expression allocates a program value,
the expression reduces to a pointer pointing to the memory location where the program value is stored. But because every
program value in the language except region handles is immutable, we save a few characters by not showing the extra level ofindirection. If some readers are uncomfortable with our notation, they may, for each state, imagine a store partitioned into
regions and replace each a at r with a pointer to the memory location containing a in the r partition of the store. Note that
region handles are mutable because the validity bit and the use counter may change. For this reason, we have region maps tohandle the extra level of indirection.

5Γ(x) = τΓ ` x : τ; L

Γ ` e 1 : τ1 ; L
Γ ] {x 7→ τ1 } ` e2 : τ2 ; LΓ ` let x = e1 in e2 : τ2 ; L

(V)

~Y ∈
Γ ` e2 : reg(X)@Z; L2/ fregvars(Γ)Γ ] {x 7→ τ1 } ` e1 : τ2 ; L1
X, Z ∈ L2
L

(L)

L

(F1)

1
Γ ` Λ~Yλx:τ1 .e1 at e2 : (∀~Y.τ1 −→τ2 )@X; L2

1
Γ ` e1 : (∀().τ1 −→τ2 )@Z; L2
Γ ` e 2 : τ1 ; L 2
L1 ∪ {Z} ⊆ L2
Γ ` e 1 e 2 : τ2 ; L 2

(F2)

L

2
Γ ` e : (∀(Y, ~Z).τ1 −→τ2 )@W; L2

L2 [X/Y](F3)

Γ ` e[X] : (∀~Z.τ1 [X/Y] −→ τ2 [X/Y])@W; L1
Γ ` ~e : ~τ ; LΓ ` e : reg(X)@Y; LΓ ` ~e at e : ~τ @X; LΓ ` e : τ [Y/X]; LΓ ` pack e as ∃X.τ : ∃X.τ ; L(E1)

X, Y ∈ L(T1)

Γ ` e : (τ1 , τ2 , ..., τi , ...)@X; LΓ ` e.i : τi ; LX∈LΓ ` e1 : ∃X.τ1 ; L
X∈/ fregvars(Γ) ∪ L ∪ fregvars(τ2 )Γ ] {x 7→ τ1 } ` e2 : τ2 ; LΓ ` open x = e1 as τ1 in e2 : τ2 ; LΓ ` e : reg(Y)@Z; L
Y, Z ∈ L
X 6= YΓ ` newregion at e : ∃X.reg(X)@Y; L(R1)Γ ` e : reg(X)@Y; LY∈LΓ ` freeregion e : reg(X)@Y; LΓ ` e1 : reg(X)@Y; LΓ ` e2 : τ ; L ∪ {X}Γ ` useregion e1 in e2 : τ ; L

Y∈L

(T2)

(E2)

(R2)

(R3)

Figure 4: Small region language: type checking rules
the plan is to disallow accesses to a region r except in the context of some useregion e 1 in e2 such that e1
is a region handle of r.
We use a type and effect system [7, 12] where the type judgement Γ ` e : τ ; L reads e has the type τ inthe environment Γ and the effect set L. In the above judgement, Γ, a type environment, is a mapping fromvariables to types. Figure 4 shows the type checking rules.
We briefly discuss the type checking rules. In (V), note that any L including ∅ can appear in the
conclusion because any expression substituted for x must be a value and therefore already reduced (becauseof call-by-value semantics).
The rule (L) for local variable definition is self-explanatory.
The rule (F1) types function allocation.
The notation fregvars(τ ) denotes the set of free region variablesSof τ . We define fregvars(Γ) to be τ ∈ran(Γ) fregvars(τ ). The function will be allocated in the region specified
by the region handle e2 , referred to by the region variable X. The pointer to the region is stored in the region
referred to by Z. Hence X, Z ∈ L2 is required. The assumption Γ ] {x 7→ τ1 } ` e1 : τ2 ; L1 types the body ofthe function. Note that L1 also appears in the function type; this set is the latent effect of the function thattakes place when the function is applied.
The rule (F2) types function application. The latent effect L1 is carried in the type of the function,
therefore L1 [~X/~Y] ⊆ L2 is required because reducing the function application leads to reducing the body ofthe function. Furthermore, Z ∈ L2 is required because the function closure value is accessed. The rule (F3)types region variable application.
The rule (T1) types tuple allocation. The judgement Γ ` ~e : ~τ ; L is a short-hand for Γ ` e 1 : τ1 ; L, . . . ,Γ ` en : τn ; L. Like in (F1), X, Y ∈ L is required. The rule (T2) types tuple projection. The condition X ∈ L
is required because the tuple is accessed.
The rules (E1) and (E2) are for existential packaging and opening and are straightforward.
The rule (R1) types region creation. The type of the expression is an existentially quantified region
handle type, matching the reduction rule [R1]. Existential types statically distinguish different regions, thatis, different regions are assigned different region variables if they appear free in a piece of code. For a reason
similar to that in (F1) and (T1), the condition Y, Z ∈ L is required.

6

The rule (R2) types region deletion. The condition Y ∈ L is required because the validity bit stored in
the region referred to by Y must be set to 0 and the use counter needs to be checked.
The rule (R3) types manipulation of use counters. Since the use counter for the region referred to by X isincremented on entry into e2 , we allow e2 to access X; hence e2 is type-checked with the effect L ∪ {X}. The
use counter may be decremented within e2 , but this does not pose a problem because it must be the case that
decrementing happens at the end of reducing some useregion − in e3 reachable by reducing e2 . Therefore
the use counter must have been incremented on entry to e3 . Therefore it follows that the use counter at theend of reducing e2 is at least as large as it was immediately before reducing e2 (in this single-threaded case,they are actually equal). We shall formalize the argument later so that it works even for multi-threaded
programs.
Given a program e, we say that e is well-typed iff {Xsr }; {sr 7→ reg(Xsr )@Xsr } ` e : τ ; {Xsr } for some τ .
All the rules are syntax directed, and type checking is clearly decidable. Readers familiar with stack-ofregions style systems should be able to easily recognize all rules except for (R1), (R2), and (R3).

2.3

Example 1

The expression below shows a function to be allocated at the starting region such that the function takes aregion handle of any region r (referred to by X in the function body) as the argument, creates a new region,
say s, whose region handle gets allocated in r, creates another new region, say t, whose region handle getsallocated in s, and returns both of the new region handles in a tuple allocated in r.
ΛX, Yλx:reg(X)@Y.
open z = (newregion at x) as reg(Z)@X
in useregion z
in pack (z, newregion at z) at x
as ∃Z.(reg(Z)@X, ∃W.reg(W)@Z)@X
at sr
The expression is well-typed and has the type
{X,Y}(∀X, Y.reg(X)@Y −→ τ )@Xsr
where τ is ∃Z.(reg(Z)@X, ∃W.reg(W)@Z)@X.
Now let us use this function. We call this function with some region handle and then delete the region t
returned, which requires accessing the region handle for t, which is allocated in the region s, which is itself
allocated by the function. In the code fragment below, assume that x is bound to some region handle oftype reg(X)@Xsr and that u is bound to the function.
useregion x
in open v = (u[X, Xsr ] x) as (reg(Z)@X, ∃W.reg(W)@Z)@X
in open w = v.2 as reg(W)@Z
in useregion v.1 in freeregion w

2.4

Proof of Safety

A program is stuck if we reach a state (R, e) such that e is not a value and also cannot be reduced further.
We show that if a program is well-typed then it does not get stuck, which implies that we can eliminate
all conditions of the form R(r) = (1, −) in the hypotheses of the reduction rules because they only serve to
make programs get stuck. Also, since no reduction turns a validity bit from 0 to 1, it is easy to see that
region can be physically deleted once its validity bit goes to 0, that is, [R2] may actually free the region r.
Hence this implies that a well-typed program is memory safe.
The proof is in the style of the work by Wright et al.[19]. For the proof, we need to type intermediate
expressions. To this end, we extend the type environment so that it can map regions to region variables (e.g.,Γ(r) = X) as well as variables to types. We omit detailed presentation of type checking rules for intermediate7expressions. However, we note that abort has any type under any environment and that the following ruleis used to type-check inuse’s:
Γ(r) = X Γ(s) = YΓ ` e : τ ; L ∪ {X}Γ ` inuse (reg r at s) in e : τ ; L

Y∈L

We need the following definition for the proof.
Definition 1 A state (R, e) is well-typed under the environment Γ iff(1) dom(Γ) = dom(R) and Γ ` e : −; {Xsr}.
(2) Γ is injective.
(3) For each subexpression of the form Λ•λ− : •.e1 at − of e, e1 does not contain a subexpression of theform inuse − in −.
(4) For each r ∈ dom(R) such that r 6= rsr , the number of occurrences of subexpressions of the form
inuse (reg r at −) in − of e is equal to i where R(r) = (−, i).
(5) If R(r) = (b, i) and i > 0 then b = 1.
We write Γ ` (R, e) to mean that (R, e) is well typed under Γ. Given this definition, we prove the following
theorem.
Theorem 1 (Subject Reduction) If Γ1 ` (R1 , e1 ) and R1 , e1 → R2 , e2 , then there exists Γ2 such that
Γ2 ` (R2 , e2 ).
Proof: The conditions (3), (4), and (5) can be proven independent of the choice of Γ2 . The condition (3)follows from inspection of the reduction rules. Given (3), (4) is straightforward by inspection of [R4] and[R6]. The condition (5) is straightforward by inspection of [R4].
It remains to find Γ2 to satisfy (1) and (2). We can do so by a straightforward case analysis on the redex
using the substitution lemma and the replacement lemma.
2 We next prove the following theorem.
Theorem 2 (Progress) If Γ ` (R, e) and e is not a value, then there is a reduction from (R, e).
Proof: The main part of the proof is in showing that conditions of the form R(r) = (1, −) in the hypothesesof each reduction rule are satisfied. To this end, we need the following lemma.
Lemma 1 If Γ ` E[e] : −; {Xsr } then there is a sub-derivation Γ ` e : −; L such that if X ∈ L and X 6= Xsr
then there is an occurrence of inuse (reg r at −) in − in E[e] such that Γ(r) = X.
The lemma can be proven by inspection of the type checking rules. Given this lemma, we can show by (2),(4) and (5) of Definition 1 that R(. . .) = . . . is satisfied. 2 It is easy to see that for a well-typed program e,
we have {Xsr }; {rsr 7→ Xsr } ` ({rsr 7→ (1, 1)}, e) where rsr is the starting region. So by the two theorems
above, it follows that a well-typed program does not get stuck, that is, it is memory safe.
A more detailed proof for the extended version of the system appears in Appendix A.1.

3

Self-allocated Region Handles

One problem with the system as described thus far is that every region handle, namely the use counter andthe validity bit, needs to be allocated in a separate region from its own region (except for sr). This problem
leads to inconvenience. For example, one cannot just create a region temporarily, use it, delete it, and thenget back to the same memory state because the system leaves the region handle as garbage. In order tocollect this garbage, one needs to delete the region which contains this region handle, which leads back tothe same problem.
While this may be a small problem in practice since a region handle takes up only a small amount of
space, it may become a serious problem for severely resource limited applications. It is also annoying from8~Y ∈
Γ ` e2 : reg(X); L2/ fregvars(Γ)Γ ] {x 7→ τ1 } ` e1 : τ2 ; L1
X ∈ L2L(F1-m)1Γ ` Λ~Yλx:τ1 .e1 at e2 : (∀~Y.τ1 −→τ2 )@X; L2

Γ ` newregion : ∃X.reg(X); LΓ ` ~e : ~τ ; LΓ ` e : reg(X); LΓ ` ~e at e : ~τ @X; LΓ ` e : reg(X); LΓ ` freeregion e : reg(X); L(R1-m)Γ ` e1 : reg(X); LΓ ` e2 : τ ; L ∪ {X}Γ ` useregion e1 in e2 : τ ; L

X∈L(T1-m)(R2-m)(R3-m)

Figure 5: Modifications to (R1), (R2), and (R3)the technical point of view; in almost all other manual region systems, a region handle is essentially just a
pointer to the head of the region and hence requires no separate heap space (i.e., all region information isstored within the region itself).
In this section, we solve this problem at the cost of a small run-time overhead. The idea is to modify
the basic system slightly so that each use counter is allocated within the region itself and the validity bit isdispensed with. Therefore a region handle no longer requires a separate space, and deleting a region does
not leave a garbage region handle.
We first make a few small changes to the language to reflect the fact that region handles are self-allocated.
We replace newregion at e withnewregionand reg(X)@Y withreg(X)We also change the intermediate representation of a region handle from reg r at s toreg r
We make a few straightforward changes to the type checking rules to reflect the changes we made. Figure 5
shows the new rules. The new rules are slightly simpler. We no longer need the starting region, so we get
rid of sr and Xsr . A program e is well-typed iff ∅; ∅ ` e : −; ∅.
Next, we introduce a new intermediate value dr of type reg(Xdr ) where Xdr is a special region variable.
Note that the constant dr is not available to source programs.
The basic idea behind the modification is to replace each reference to a handle of a deleted region with dr.
For each region r, the run-time system maintains two data-structures in r itself: a doubly linked list called
reglocs1 (r) and a singly linked list called reglocs2 (r). The run-time system stores pointers to all occurrencesof reg r in reglocs1 (r). In addition, for each region s, reglocs2 (r) stores a pointer to each occurrence of reg s
allocated within r.
More concretely, at each allocation a at reg r, for each direct occurrence of reg s in a, the runtime system stores the address of the occurrence in reglocs1 (s) and in reglocs2 (r). For example, evaluating((reg s, reg t) at r, reg t) at reg r allocates an element containing the heap location of the second elementof the outermost tuple (the second reg t) in reglocs1 (t) and in reglocs2 (r). Note that other two region
handles are already allocated so nothing else needs to be done. In general, for a tuple (v 1 , . . . , vn ) at reg r,
only the vi of the form reg r needs to be considered assuming that we treat pack • as v as v. A similar
treatment is done when allocating function closures, that is, the address of any free variable bound to aregion handle reg t gets stored in reglocs1 (t) and in reglocs2 (r) when the closure is allocated in the region
r. Region handles allocated at non-heap locations (e.g., stack variables) are handled similarly.
A region handle is implemented as a double-word value. This implementation choice warrants further
discussion later in the section (Section 3.2). A region handle reg r is a pair of pointers, one pointing to thehead of the region r and the other pointing to the element of reglocs1 (r) corresponding to this reference.
When the program tries to delete a region r via some freeregion reg r, the run-time system goesover each element of reglocs1 (r) overwriting each region handle with dr. Then it goes over each element of9reglocs2 (r) such that if it finds a region handle of t that is not dr, it follows the pointer to an element of
reglocs1 (t) and deletes the element from the doubly-linked list. Finally the region r is deleted. Similarly,
when a non-heap location containing a region handle of t is deallocated, the run-time system follows thepointer to the corresponding element of reglocs1 (t) and deletes the element.
Now the use counter can be stored within the same region. We no longer need the validity bit as the runtime system just needs check for dr at useregion’s. The run-time system pays the price for the modification
when allocating a value containing a reference to a region handle and when deleting a region containing suchreference. As we shall see in Section 3.2, a suitable restriction to the static system guarantees that no otherrun-time cost needs to be paid. For example, the run-time system does no extra work when allocating avalue that contains no immediate reference to a region handle. Deleting a region costs time proportional
to the number of references to region handles allocated in that region and references to its region handle,
which is independent of the number of other type of values and should be a small factor in a reasonable
program. Note that unlike with a tracing or reference-counting garbage collector, neither operation requires
any reachability computation.

3.1

Mutable Values

Suppose that we extended the language with mutable values. In order to maintain the invariants justdiscussed, when a location containing a region handle of r is modified to refer to a region handle of t, therun-time system follows the pointer to an element of reglocs 1 (r), deletes the element from the list, and thenallocates an element in reglocs1 (t) containing a pointer to this location.

3.2

Polymorphism

In order to allow smooth integration of our system with a polymorphic language, one might prefer a singleword implementation of a region handle as opposed to the double-word implementation described above.
This can be accomplished by storing a pointer to the head of the region r in each element of reglocs 1 (r) and
implementing the region handle as a pointer to the corresponding element. This change incurs an extra-levelof pointer-lookup at allocation sites.
But there is a strong reason not to allow instantiating a type variable with a region handle type. The
problem is that, at allocation sites, the run-time system needs to check if a value whose type is some typevariable (at compile time) is a region handle, because if so the corresponding linked lists need to be extended.
For example, when allocating a value of the type (α, reg(Y))@X where α is a type variable, the run-time systemneeds to test if the first element of the tuple is a region handle. A similar run-time overhead is incurred
when updating a mutable value that has a type-variable type.
In contrast, if we forbid abstraction over a region handle type, then all references to region handles will
be known at compile time. Note that programs are still allowed to instantiate a “boxed” type that contains
a region handle type (e.g., a heap-allocated tuple containing a region handle: τ [(reg(X), reg(Y))@Z/α]). This
design also lets us keep the double-word region handle implementation. Because unboxed multi-word values
appear to be important for efficient manual memory management in a full-scale programming language [9],having a region handle type as just another non-generalizable type might not cause further damage to theoverall uniformity of the language.
It is worth noting that, in case one wants abstraction over region handle types despite its shortcomings,
it is possible to alleviate the run-time overhead via static analysis. For example, a flow analysis can conservatively estimate which value may not evaluate to a region handle. We leave the choice open to the language
designer.

4

Analysis and Discussion

In this section, we evaluate our use-counting technique analytically and discuss several pragmatic issues.
First, we show an efficient encoding of stack-of-regions style memory management within our system toshow that use counting is at least as powerful as this well-known region technique.

10

4.1

Encoding Stack-of-Regions

Stack-of-regions refers to a region-based memory management technique where each region’s lifetime isbounded by the lifetime of some stack frame. This technique is the basis of many region proposals, bothmanual and automatic [15, 1, 9, 2].
In this paper, we are concerned with the manual interpretation. The basic manual stack-of-regions can beobtained by removing newregion, freeregion, and useregion from our small region language and adding
letregion x as reg(X) in e
Reducing this expression creates a new region referred to by X, substitutes the region handle of the new
region for x in e, reduces e to a value v, deletes the region, and then returns v.
The type checking rule isΓ ] {x 7→ reg(X)} ` e : τ ; L ∪ {X}X∈/ fregvars(Γ)
fregvars(τ ) ⊆ fregvars(Γ)Γ ` letregion x as reg(X) in e; τ ; L
We show that letregion can be efficiently encoded using newregion, freeregion, and useregion. Let
e1 ; e2 be an abbreviation for let x = e1 in e2 where x ∈/ fvars(e2 ). Now consider:
open x = (newregion) as reg(X)in let y = (useregion x in e) in freeregion x; y
It is easy to see that this encoding has the same behavior as letregion. That is, before entering e, a new
region is created and bound to x, then after e reduces to a value, the region is deleted. It is also easy to seethat the encoding preserves well-typedness.
The resulting program is efficient. There is only a constant time overhead for each occurrence ofletregion. That is, before evaluating the body, a new region and its use counter is allocated, and theuse counter is incremented after checking that the region has not been deleted. Once the body evaluates,
the use counter is decremented, and the region is deleted after checking that the use counter is 0.
It is also easy to see that a stack-of-regions program translated to the use-counting version never aborts.

4.2

Dynamic Check Failures

However, the full potential of use counting is realized when the program does not use regions in a stack-wiseorder. For example, stack-of-regions is insufficient to express the example in Section 2.3 since every function
is forced to delete all regions it creates before it returns.
In the general case, however, programs do not enjoy the abort-free property. But we argue that it is rare
for a well-written program to encounter a dynamic check failure. Recall that there are two kinds of dynamic
checks: the dr check (or the validity bit check) at useregion and the use counter check at freeregion.
Consider a situation in which the first check fails, that is, useregion reg r in e is encountered after the regionr has been deleted. Suppose that the programmer adheres to the discipline that, by useregion reg r in e,
he/she means that r is definitely going to be used in e. Then a dynamic check failure indicates a real
programming bug instead of a spurious dynamic check failure since r was deleted before executing the code
which was supposed to use r.
On the other hand, the second dynamic check fails when freeregion reg r is encountered within somecontext inuse reg r in E (at least for the single-thread case). This type of failure is harder to characterize.
But it is worth noting that detecting such failures at compile time is possible to some degree via known static
analysis techniques. For example, a variation of the algorithm from the work by Foster et al.[5] could be
used to produce compile-time warnings for potentially dangerous freeregion occurrences. Also, this typeof failure is easier to recover from, since the worst the programmer could do is to ignore and leak memory.

11

4.3

Annotation Cost

To use the system, the programmer needs to annotate code with useregion constructs in addition to writing
type and effect annotations. Somewhat surprisingly, useregion and type and effect annotations are mutuallycompensating. Intuitively, the more useregion annotations the programmer writes, the fewer type and effectannotations required.
To illustrate this point, consider a large block of code e0 that uses many regions, say r, s, .... Assume
that e0 does not delete these regions. Then it is a good idea to wrap e0 with corresponding useregion’s toamortize the cost of dynamic checks since e0 is large. That is,useregion e1
in useregion e2
in useregion . . . in e0
where e1 , e2 , . . . are region handles for r, s, ..., respectively. Now consider a function which contains
e0 as a subexpression, say, λx : τ1 .e0 at − for the sake of brevity. Then, the type of this function is just∅(τ1 −→ τ2 )@X for some τ2 and X assuming that e0 uses no other regions.
In general, an occurrence of useregion eliminates the corresponding region variable from the effect setsof the parent expressions, which in turn relieves the programmer from having to annotate them in the latenteffect sets. We can see a glimpse of this property in action in the examples in Section 6 where every function
has a rather trivial latent effect set annotation. This property also has an compounding benefit because acontext calling such function requires neither useregion nor effect annotations for the regions accessed by
the callee. This is in contrast to conventional region-based approaches where function types are required tocarry identifications of all non-local regions accessed by the function (up to abstraction over sets of region
identifiers).
On the other hand, for run-time efficiency, it is desirable to leave the body of a short-running function
free of useregion’s. Such a small function is likely to use few regions, and therefore the effort required toannotate its latent effect set is correspondingly small.
The system presented in this paper is explicitly typed. While outside of the scope of the paper, it is easy
to see that inferring type and effect annotations is possible with some suitable restrictions. Some amount ofinference (e.g., in the spirit of local type inference [13]) will be important for incorporating use counting ina full-scale programming language.

5

Regions and Threads

A problem common with many manual memory management systems is that they have difficulty supporting
multi-threading while retaining safety and controllability. Consider the stack-of-regions approach. To handle
thread-shared memory, the run-time system must be aware of threads that may potentially access a region
so that the region may be deleted only after all potentially accessing threads terminate. If the thread that
allocated the region is allowed to continue after the stack pops regardless of future behavior of other threads,
then memory behavior becomes difficult to control because the lifetime of the region is no longer tied to thelifetime of the stack but to the longest living thread having access to the region. On the other hand, if thethread that allocated the region is forced to stall until it is safe to delete, then the run-time behavior of theallocating thread becomes less predictable.
Thread-based concurrency is common in many modern programs. One of the nicest features of theuse-counting approach is that thread-based concurrency is supported for free.
We extend the small region language with the form fork e and extend the dynamic semantics withconcurrently executing threads. Each state has the form (R, ~e) where each e i ∈ {~e} is a thread. Reductions
are still from states to states, and each reduction rule can be applied to any thread in ~e. The reduction rule
for fork e isR, (e~1 , E[fork e], e~2 ) → R, (e~1 , E[unit], e~2 , e)where the constant unit is a place holder value of type unit. The type checking rule for fork e is justΓ ` e : τ; ∅
Γ ` fork e : unit; L
12

No other changes are needed.
The argument used in the proof of safety for the single-thread case still works. The key observation isthat the proof of safety was based on the number of syntactic occurrences of inuses. Hence to prove safety
for multi-thread case, we can simply add up the number of inuses from all threads and compare the sumwith the use counter in the region map. Since Γ ` e : τ ; ∅ and since e does not contain any inuse, the newly
forked thread e satisfies the invariants in Definition 1, and therefore the induction argument goes through.
Appendix A.1 discusses the reasoning in more detail.
As in the single-thread case, deleting a region that is being used or trying to use a region that has
been deleted results in a dynamic check failure. The difference is that such situations may now involve
concurrently running threads, for example, when thread A attempts to delete some region that thread B isusing. To avoid dynamic check failures, programs must synchronize threads so that region uses and deletions
are correctly scheduled.
How such synchronization is done, whether explicitly by the programmer or implicitly by concurrency
abstractions in the programming language, is another issue. Our proposal provides a simple and sound basis
for incorporating safe memory management with any synchronization mechanism.

6

Experience with Regions

We informally discuss our experience with a toy implementation. Instead of creating an entirely new language
from scratch, we extend an existing language with use-counted regions. We choose C for this purpose,
mainly because we had prior experience with manual, though sometimes unsafe, region programming in thislanguage.
The ideal goal is to replace malloc and free with newregion and freeregion. But more realistically,
our implementation provides use-counted regions as a safe alternative while keeping the rest of C available
and unsafe. Hence we leave features such as casting in the language. The implementation covers only themonomorphic fragment of the system. (Monomorphic as in the sense of Section 2, and so we do permit
quantification over region variables.) However, we support non-heap-allocated (i.e., unboxed) records in theform of structs, which turns out to be useful for writing short but interesting examples. One reason forthis section is to provide ample examples in easy-to-read syntax. The examples are designed to illustrate
the expressiveness of our system such that other safe, explicit memory management approaches would havedifficulty expressing them.

6.1

SyntaxThe basic syntax is identical to that of the small region language. The built-in function region newregion(void)
creates a new region and returns its region handle, and the built-in function void freeregion(region)
deletes the region passed. We also have useregion, which is now written useregion(e 1) { e2 }.
However, C has a number of differences with the lambda calculus (to put it mildly) which dictate asomewhat different design. The major changes are:
1 Instead of the “@” notation, we now indicate where a value is stored as part of its pointer type. For
example, int * X is a pointer to an integer in region referred to by X. We allow NULL to have any pointertype.
2 We use syntax resembling C++ templates to write data structure types parametrized by region variables.
struct<~X>structname{ def }The region variables ~X are binding occurrences, and therefore ~X may appear free in def . For such a type
τ , its region variables can be instantiated: τ <~Y>. What is unique about our structs is that when it is notinstantiated, the value is said to be closed, which roughly corresponds to an existential type with the boundregion variables ~X. For example, a newly created region handle has the type region and is therefore closed.
For example, the type IntCell consisting of a region handle reg to some region r and a pointer data
pointing to an integer allocated in r can be written as13

struct<Z> IntCell { region<Z> reg; int * Z data };An instantiated type can be closed at any time, which intuitively corresponds to an automatic pack.
3 We use the same angle-bracket notations to denote bound region variables in function declarations. Whenomitted (as in the examples in this section) we assume that the function is polymorphic in all region variables
that appear in its type.
4 The built-in polymorphic function
τ * X ralloc(region<X>,τ ) {X}
allocates values of type τ in the region passed and returns a pointer to the allocated memory block. The
allocated memory blocks are initialized to zero. The set {X} denotes the latent effect of the function. Latenteffect annotations are omitted for functions whose latent effect is ∅.
5 We use C conventions of compound statement scope. For example, to open e of a closed type τ byinstantiating it with region variables X,Y,Z, write
open τ <X,Y,Z> x = e;Then X,Y,Z are new region variables that are available in the current scope. The variable x is forced to beconst.

6.2

Example 2: Linked List

Element-wise deallocatable linked lists can be implemented in our system with full imperative, destructive
goodness expected from C. To this end, we use one region per list element; the definition of elt in Figure 6
shows that a list element consists of a region handle, a next pointer, and a content data. The content data
is just an integer, so the example is probably not an economical use of regions; it is just for demonstration.
Figure 6 shows three functions that do insertion, deletion, and list printing, respectively. 4 Note that
deleting a list element actually deallocates the space for the element while keeping the rest of the list intact.
All functions are written in an imperative fashion common in C programs; there is no need to rebuild thelist when an element is inserted or deleted.
Now to make the example more economically realistic, instead of an integer as a list element, we supposea large data structure potentially consisting of many connecting pointers to be allocated in the same region
where the element is allocated (at the element creation or later). To this end, we need a region variablereferring to the region where the element is allocated. We add a new binding region variable in the definitionof elt and using this binding to equate the region where this instance of elt is allocated and the region
where the data structure is (or is going to be) allocated.
The updated definition of a list element appears below. Note that the struct type data type (thedefinition not shown) is instantiated with Y to allow values in the data structure to be allocated in the same
region.
struct<Y> elt {struct<X> wrapper {region<X> reg;
struct elt<X> * X next;} wrap;struct data type<Y> * Y data;};

14

struct elt {struct<X> wrapper {region<X> reg;
struct elt * X next;} wrap;int data;};<X> void insert(struct elt * X cur, int data) {X} {open region<Y> newreg = newregion();struct elt * Y newelt;
useregion(newreg) {newelt = ralloc(newreg, struct elt);
newelt->data = data;
newelt->wrap = cur->wrap;}
cur->wrap = {reg:newreg, next:newelt};}<X> void delete(struct elt * X cur) {X} {open struct wrapper<Y> cw = cur->wrap;
useregion(cw.reg) {cur->wrap = cw.next->wrap;}
freeregion(cw.reg);}void print list(struct wrapper list) {do { open struct wrapper<X> cw = list;
if (cw.next == NULL) return;useregion(cw.reg) {printf(‘%d‘,cw.next->data);
list = cw.next->wrap;} } while (1);}Figure 6: Element-wise deallocatable linked list

6.3

Example 3: Game of Life

An example simulating the Game of Life for n iterations is used in the paper by Henglein et al. [10] to illustrate
varying expressiveness of different region systems. In Figure 7, we show a use counting implementation whichclosely matches the original code found in their paper.5 The function nextgen creates and returns the newgeneration.
The resulting function life satisfies both of the two criteria suggested by their paper: it is tail recursiveand does not have the region endomorphism problem (i.e., using the same region to allocate the generations,which leads to memory leak).

6.4

Existing Region Programs

We also looked at several existing C programs that use regions (safely or not) to do part of their memory
management and found that use counting seems capable of expressing many region usage patterns found in
4 Strictly speaking, the last statement in insert is not valid C syntax because a = {b} can be used only at initializations.
This can be overcome by either extending the syntax or adding an extra scope at the end initializing a new variable of typeelt which gets immediately assigned to cur->wrap.
5 Henglein et al. also allocates the integer argument n in the heap. Here we just stack-allocate it for brevity.

15

struct<X> gen {region<X> reg;
struct game<X> * X g;};struct gen nextgen(struct gen);struct gen life(int n, struct gen g) {if (n == 0) { return g; }else {
struct gen newg = nextgen(g);open struct gen<X> x = g; freeregion(x.reg);
return life(n-1, newg);}}
Figure 7: Game of Life simulationthese programs.
One common pattern is in which a fixed number of regions exists at any time such that these regions are
stored in global variables (or accessed by calling global functions). For example, lcc, a C compiler, uses three
regions placed in a global array of size three called arena: one for functions, one for statements, and one
permanent region. The region deletion function deallocate(int i) is called to delete the current arena[i]after each function (or each statement) is compiled. Each arena[i] (except of course the permanent one)is assigned a newly created region before the next allocation in arena[i].
It is easy to express such a pattern in our system. We store the region handle with the data in a globally
accessible closed struct and open it wherever the data is requested. We reset the region by deleting theregion, creating a new one and closing it in a struct, and assigning the closed value to the same global
variable.
Because most of these programs are neither written to use regions for safety nor pressured with tightspace or timing requirements, they do not contain too many exciting region usage patterns. But it gives us
some practical evidence for the technique’s usability.

7

Related Work

Ruggeieri et al. [14] introduced the stack-of-regions concept, and Tofte et al. [15] extended it to work withhigher-order functions and polymorphic regions. Both systems were formulated for automatic memory
management, but manual variants of the idea have also been proposed [9, 2]. We have given comparisons ofuse-counted regions versus stack-of-regions in the earlier parts of the paper. We should note that issues thatare not formally discussed in the main body of our paper, such as parametric polymorphism over types andeffect sets, recursive types, non-heap allocated values, and mutable values, have been extensively studied in
the aforementioned papers. It is straightforward to incorporate these features formally into our system inmuch the same way (with the minor exception of the issue discussed in Section 3.2). Appendix A shows thesmall region language extended with ML-style mutable refs and parametric polymorphism over types andeffect sets.
Hicks et al. have developed a similar technique called dynamic regions independently from our workaround the same time. In the technical report [11], they briefly outline this technique along with twoother memory management ideas that are of independent interest. Their dynamic regions can be roughlyinterpreted in our small region language by assuming that region handles are always existentially packed.
Opening such package in their system corresponds to open immediately followed by useregion. They haveincorporated dynamic regions in Cyclone [9] and report positive results. Our paper’s main contributions
over their report are: a formal presentation of the technique and the proof of soundness, analysis anddiscussion including the exposition on multi-threading support, and the following two technical differences
regarding region handles. As mentioned, Hicks et al.’s formulation ties dynamic operations on region handles
16

to existential types, whereas we use an arguably more natural formulation which treats existential types aspurely a static construct as in the standard type theory. In addition to being somewhat cleaner in theory, ourformulation has practical advantages. For example, our system allows two different existential abstractions
over the same region handle, which in turn, for example, enables sharing of a region among different data
structures without having to syntactically equate the region variables. The second difference is the extension
shown in Section 3 which allows a region handle to be allocated within its own region.
Walker et al. [18] combine regions with linear types to create a static system that allows interesting region
usage patterns. In their system, each region handle must be linear when the region is deleted and non-linear(and therefore allowed to be aliased) when the region needs to be accessed. Wadler’s let!-like construct[16] turns a linear region handle non-linear in a designated scope and then back to linear when exiting thescope. Walker et al.’s system uses these linear/non-linear phases to statically prevent a region from being
deleted while program is in one of its non-linear scopes. Hence the underlying idea is somewhat similar to
our useregion, and so our use-counting method may be viewed as a way to remove limitations imposedby linear types by inserting dynamic checks. Their paper also shows how to integrate a reference-counting
interpretation of linear types [3] with regions.
Crary et al. [4] present a region system that uses the notion of linearity to statically track aliasing ofregion handles. Their system is very expressive but seems to require non-trivial program annotations, forexample, when deallocating individual elements of recursive data structures ala our example in Section 6.2[17]. However, their intention is not to expose the region system at the source level but instead to certify
memory safety of intermediate-level code.
Henglein et al. [10] take a different approach toward region-based memory management by employing
a Floyd-Hoare style proof system. Their primary goal is to create an automatic system for a conventional
non-region language. Hence their system is not meant to be exposed to programmers and also not quite as
manual as the systems discussed above. In particular, there is no language construct to explicitly delete a
region. Instead, the system maintains reference counts on region handles6 so that a region is automaticallydeleted when the reference count becomes zero. To this end, they use a reference-counting scheme similarin spirit to the one by Chirimar et al. [3]. It is left open whether their system could be extended to handle
function closures and polymorphism.
In contrast, Gay et al. [6] uses reference counting as the main device for memory safety by counting
references to the content of regions in addition to region handles. Their system allows explicit deletion ofregions but does not statically guarantee its success, similar to our freeregion. Their system demands very
little from the static side, relying largely on dynamic reference counting for safety. To recover efficiency,
they use compile-time optimization to reduce the number of reference-counting operations and also provide
optional type qualifier annotations to help the optimizing compiler.
This reference-counting approach is related to use counting in the following way. Both approaches countthe “users” of each memory location so that the memory location may be deallocated only when the numberof users is zero. Both approaches group memory locations via regions to amortize the number of runtime counter operations. The difference between the two approaches is in the meaning of a “user”: in thereference-counting approach, a user is a pointer pointing to the region whereas in our approach, a user isa piece of code that is actually using the region (as in accessing memory locations in the region). Henceto group memory locations, the reference-counting approach prefers connecting pointers to be in the samegroup, whereas our approach encourages grouping memory locations that are accessed together in the same
piece of code. This observation has led us to coin the term “use counting” to describe our technique.
Our use-counting approach has the following advantages over the reference-counting approach. One isthat use counting does not require the references to be dead for a region to be deleted. Another advantage
is that, when deciding which locations should be grouped together in a region, use counting can capitalize
directly on the program’s memory access pattern instead of being dependent on the points-to relationship.
6 Region variables in their paper.

178Conclusion

We have presented a new, mostly-static, safe region-based memory management technique. Our methodscales naturally to a variety of modern language features, including multi-threading, and offers flexible
manual control while being relatively simple. We hope to have provided a new insight into designing highlevel languages for resource-conscious applications.

References[1] A. Aiken, M. Fähndrich, and R. Levien. Better Static Memory Management: Improving RegionBased Analysis of Higher-Order Languages. In Proceedings of the 1995 ACM SIGPLAN Conference on
Programming Language Design and Implementation, pages 174–185, La Jolla, California, June 1995.
[2] C. Boyapati, A. Salcianu, W. Beebee, Jr., and M. Rinard. Ownership Types for Safe Region-Based
Memory Management in Real-Time Java. In Proceedings of the 2003 ACM SIGPLAN Conference on
Programming Language Design and Implementation, San Diego, California, June 2003.
[3] J. Chirimar, C. A. Gunter, and J. G. Riecke. Reference Counting as a Computational Interpretation ofLinear Logic. Journal of Functional Programming.
[4] K. Crary, D. Walker, and G. Morrisett. Typed Memory Management in a Calculus of Capabilities. In
Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, pages 262–275, San Antonio, Texas, Jan. 1999.
[5] J. S. Foster and A. Aiken. Checking Programmer-Specified Non-Aliasing. Technical Report UCB//CSD01-1160, University of California, Berkeley, Oct. 2001.
[6] D. Gay and A. Aiken. Language Support for Regions. In Proceedings of the 2001 ACM SIGPLAN
Conference on Programming Language Design and Implementation, pages 70–80, Snowbird, Utah, June
2001.
[7] D. K. Gifford, P. Jouvelot, J. M. Lucassen, and M. A. Sheldon. FX-87 Reference Manual. Technical
Report MIT/LCS/TR-407, MIT Laboratory for Computer Science, Sept. 1987.
[8] D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-Based Memory Management in Cyclone. Technical Report 2001, Department of Computer Science, Cornell University,
2001.
[9] D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-Based Memory Management in Cyclone. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language
Design and Implementation, Berlin, Germany, June 2002.
[10] F. Henglein, H. Makholm, and H. Niss. A direct approach to control-flow sensitive region-based memory management. In Proceedings of the 3rd International Conference on Principles and Practice ofDeclarative Programming, pages 175–186, Montréal, Canada, 2001. ACM.
[11] M. Hicks, G. Morrisett, D. Grossman, and T. Jim. Safe and Flexible Memory Management in Cyclone.
Technical Report CS-TR-4514, Department of Computer Science, University of Maryland, July 2003.
[12] J. M. Lucassen and D. K. Gifford. Polymorphic Effect Systems. In Proceedings of the 15th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 47–57, San Diego,
California, Jan. 1988.
[13] B. C. Pierce and D. N. Turner. Local Type Inference. In Proceedings of the 25th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages, pages 252–265, San Diego, California,
Jan. 1998.

18

U, V, W, X, Y, Z ∈ RegVars ∪ {Xsr }a, b, c ∈ TypeVarsu, v, w, x, y, z ∈ Vars ∪ {sr}A, B, C ∈ EffectVars

r, s, t ∈ Regions
k, l, m ∈ Locations

static vars
instantiations
effect sets

α
γ
L

::=
::=
::=

a|A|X
τ |L|X∅ | L ∪ {X} | L ∪ A

types
expressions

τ
e

::=
::=

(∀~
α.τ1 −→ τ2 )@Y | ~τ @X | reg(X)@Y | ∃α.τ | unit | A | ref (τ )@X
x | let x = e1 in e2 | Λ~
αλx:τ.e1 at e2 | e[γ] | e1 e2 | ~e at e | e.i | pack e as ∃α.τ | open x = e1 as τ in e2 |newregion at e | freeregion e | useregion e 1 in e2 | fork e | ref e1 at e2 | !e | e1 := e2L

Figure 8: Extended small region language: source syntax
valuesexpressions

v
e

::=
::=

pack v as • | Λ•λx:•.e at r | ~v at r | reg r at s | abort | unit | loc l at r
x | let x = e1 in e2 | Λ•λx:•.e1 at e2 | e[γ] | e1 e2 | ~e at e | e.i | pack e as • | open x = e1 as • in e2 |newregion at e | freeregion e | useregion e 1 in e2 | v | inuse (reg r at s) in e |fork e | ref e1 at e2 | !e | e1 := e2contexts

E::=[ ] | let x = E in e | Λ•λx:•.e at E | E[•] | E e | v[•] E |(~v, E, ~e) at e | ~v at E | pack E as • | open x = E as • in e |newregion at E | freeregion E | useregion E in e | inuse (reg r at s) in E |ref E at e | ref v at E | !E | E := e | (loc l at r) := E

Figure 9: Extended small region language: type-erased intermediate expressions and evaluation contexts[14] C. Ruggieri and T. P. Murtagh. Lifetime analysis of dynamically allocated objects. In Proceedings ofthe 15th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages
285–293, San Diego, California, Jan. 1988.
[15] M. Tofte and J.-P. Talpin. Implementation of the Typed Call-by-Value λ-Calculus using a Stack ofRegions. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, pages 188–201, Portland, Oregon, Jan. 1994.
[16] P. Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, pages 347–359. North
Holland, 1990.
[17] D. Walker and G. Morrisett. Alias Types for Recursive Data Structures. In International Workshop on
Types in Compilation, Montreal, Canada, Sept. 2000.
[18] D. Walker and K. Watkins. On Regions and Linear Types. In Proceedings of the sixth ACM SIGPLAN
International Conference on Functional Programming, pages 181–192, Florence, Italy, Sept. 2001.
[19] A. K. Wright and M. Felleisen. A Syntactic Approach to Type Soundness. Information and Computation,
115(1):38–94, 1994.

A

Imperative, Concurrent and Polymorphic Small Region Language

Figure 8 shows the small region language extended with quantification over type and effect variables andML-style mutable refs. Recursive functions can be easily expressed using refs. We also formally add themulti-thread extension discussed in Section 5. The bound static variabes appearing in a function typeare assumed to be distinct. Figure 9 shows the corresponding type-erased intermediate expressions and19

R(r) = (1, −)R(s) = (1, −)R, T [Λ•λx:•.e at (reg r at s)]→ R, T [Λ•λx:•.e at r]

R(r) = (1, −)R, T [(Λ•λx:•.e at r) v]→ R, T [e[v/x]][F1-e]

R(s) = (1, −)S, R ] {r 7→ (−, 0)}, T [freeregion (reg r at s)]→ S, R ] {r 7→ (0, 0)}, T [reg r at s]

R, T [v[•]] → R, T [v]R(s) = (1, −)i>0
S, R ] {r 7→ (−, i)}, T [freeregion (reg r at s)]→ S, R ] {r 7→ (−, i)}, abort[R2-e]

R(s) = (1, −)S, R ] {r 7→ (1, i)}, T [useregion (reg r at s) in e] → R ] {r 7→ (1, i + 1)}, T [inuse (reg r at s) in e]R(s) = (1, −)S, R ] {r 7→ (0, i)}, T [useregion (reg r at s) in e2 ]→ S, R ] {r 7→ (0, i)}, abort[T1-e]

R(r) = (1, −)S, R, T [(~v at r).i] → S, R, T [vi ]S, R, T [let x = v in e] → S, R, T [e[v/x]]
R(r) = (1, −)R(s) = (1, −)S, R, T [ref v at (reg r at s)] → S ] {l 7→ v}, R, T [loc l at r]

R(r) = (1, −)S ] {l 7→ −}, R, T [(loc l at r) := v]→ S ] {l 7→ v}, R, T [v][M3-e][M1-e]

R(r) = (1, −)S ] {l 7→ v}, R, T [!(loc l at r)]→ S ] {l 7→ v}, R, T [v]S, R, (e~1 , E[fork e2 ], e~3 ) → S, R, (e~1 , E[unit], e~3 , e2 )Figure 10 shows the corresponding reductions rules.
Figure 11 shows the type checking rules for the source language. The set fvars(τ ) denotes the set of freestaticvariables (i.e., region variables, type variables, and effect variables) in τ . We define fvars(Γ) to beSτ ∈ran(Γ) fvars(τ ). The bound static variables that appear in a function type are assumed to be distinct.
We assume that the substitutions in (F3-e) and (E1-e) are sort-consistent (i.e., a type variable is substituted
by a type, a region variable is substituted by a region variable, and an effect set variable is substituted byan effect set). The relation L1 ⊆ L2 is defined as follows:
L1 ⊆ L 2
L3 ⊆ L 4
L1 ∪ L 3 ⊆ L 2 ∪ L 4

in addition to the usual axioms for the set theoretic interpretation of ⊆. We also assume that A ∪ A = A andthat ∪ is commutative and associative.

20[R6-e][L-e]

evaluation contexts. For the purpose of exposition, we stick with the notation from Section 2 and do not use
the extension described in Section 3.
The dynamic semantics is a series of small-step reductions from states to states where state is a triple(S, R, ~e) where S is a store mapping each location l in its domain to a value. For brevity, we define themulti-thread-evaluation context:
T ::= (e~1 , E, e~2 )∅⊆A[R3-e][T2-e]

Figure 10: Extended small region language: reduction rules

A⊆A[R1-e][R4-e]

R(s) = (1, −)S, R ] {r 7→ (b, i)}, T [inuse (reg r at s) in v]→ S, R ] {r 7→ (b, i − 1)}, T [v][R5-e]

R(r) = (1, −)R(s) = (1, −)S, R, T [~v at (reg r at s)] → S, R, T [~v at r][F3-3]

R(r) = (1, −)R(s) = (1, −)S, R, T [newregion at (reg r at s)]→ S, R ] {t 7→ (1, 0)}, T [pack (reg t at r) as •][E-e]

S, R, T [open x = (pack v as •) as • in e] → S, R, T [e[v/x]][F2-e][S-e][M2-e]

Γ(x) = τΓ ` x : τ; L

Γ ` e 1 : τ1 ; L
Γ ] {x 7→ τ1 } ` e2 : τ2 ; LΓ ` let x = e1 in e2 : τ2 ; L(V-e)

Γ ` e2 : reg(X)@Z; L2
Γ ] {x 7→ τ1 } ` e1 : τ2 ; L1

(L-e)

L

α
~ ∈
/ fvars(Γ)
X, Z ∈ L21
Γ ` e1 : (∀().τ1 −→τ2 )@Z; L2
Γ ` e 2 : τ1 ; L 2
L1 ∪ {Z} ⊆ L2
Γ ` e 1 e 2 : τ2 ; L 2(F1-e)

L1Γ ` Λ~
αλx:τ1 .e1 at e2 : (∀~α.τ1 −→
τ2 )@X; L2(F2-e)

L2Γ ` e : (∀(α1 , α~2 ).τ1 −→τ2 )@W; L2

Γ ` e[γ] : (∀α~2 .τ1 [γ/α1 ]Γ ` ~e : ~τ ; LΓ ` e : reg(X)@Y; LΓ ` ~e at e : ~τ @X; LΓ ` e : τ [γ/α]; LΓ ` pack e as ∃α.τ : ∃α.τ ; L

X, Y ∈ L(E1-e)

L2 [γ/α1 ]−→(T1-e)(F3-e)

τ2 [γ/α1 ])@W; L1
Γ ` e : (τ1 , τ2 , ..., τi , ...)@X; LΓ ` e.i : τi ; LX∈LΓ ` e1 : ∃α.τ1 ; Lα∈/ fvars(Γ) ∪ fvars(L) ∪ fvars(τ2 )Γ ] {x 7→ τ1 } ` e2 : τ2 ; LΓ ` open x = e1 as τ1 in e2 : τ2 ; LΓ ` e : reg(Y)@Z; L
Y, Z ∈ L
X 6= YΓ ` newregion at e : ∃X.reg(X)@Y; L(R1-e)Γ ` e : reg(X)@Y; LY∈LΓ ` freeregion e : reg(X)@Y; LΓ ` e1 : reg(X)@Y; LΓ ` e2 : τ ; L ∪ {X}Γ ` useregion e1 in e2 : τ ; LΓ ` e1 : τ ; LΓ ` e2 : reg(X)@Y; L
X, Y ∈ LΓ ` ref e1 at e2 : ref (τ )@X; LΓ ` e1 : ref (τ )@X; LΓ ` e2 : τ ; LΓ ` e1 := e2 : τ ; L(M1-e)

X∈L(M3-e)Y∈L(T2-e)(E2-e)(R2-e)(R3-e)Γ ` e : ref (τ )@X; LΓ ` !e : τ ; L

X∈LΓ ` e : τ ; {Xsr }Γ ` fork e : unit; L(M2-e)(S-e)

Figure 11: Extended small region language: type checking rules
A source program e is well-typed iff {Xsr }; {sr 7→ reg(Xsr )@Xsr } ` e : τ ; {Xsr }. Figure 12 shows the
additional rules for typing the intermediate expressions. The type environment is extended to map locations
to types (e.g., Γ(l) = τ ).

A.1

Proof of Safety

We reformulate the proof for the extended system. We also fill some of the details omitted from the proof
in Section 2.4.
All expressions mentioned in the rest of the section are assumed to be in the intermediate language unlessspecified otherwise.
Definition 2 A state (S, R, ~e) is well-typed under the environment Γ iff(1) dom(Γ) = dom(R) ∪ dom(S) and Γ ` ei : −; {Xsr} for each ei ∈ {~e}.
(2) If Γ restricted to dom(R) is injective.
(3) For each subexpression of the form Λ•λ− : •.e1 at − of ~e, e1 does not contain a subexpression of theform inuse − in −.
(4) For each r ∈ dom(R) such that r 6= rsr , the number of occurrences of subexpressions of the form
inuse (reg r at −) in − of ~e is equal to i where R(r) = (−, i).
(5) If R(r) = (b, i) and i > 0 then b = 1.

21Γ ` e2 : reg(X)@Z; L2α~ ∈/ fvars(Γ)Γ ] {x 7→ τ1 } ` e1 : τ2 ; L1
X, Z ∈ L2

LL1τ2 )@X; L2
Γ ` Λ•λx:•.e1 at e2 : (∀~α.τ1 −→Γ ` e : τ [γ/α]; LΓ ` pack e as • : ∃α.τ ; LΓ ` e[•] : (∀α~2 .τ1 [γ/α1 ]L2 [γ/α1 ]

−→

Y∈L

α
~ ∈
/ fvars(Γ)Γ ] {x 7→ τ1 } ` e : τ2 ; L1

(R4-e)

Γ(r) = X
L1

Γ ` abort : unit; L(FV-e)Γ ` Λ•λx:•.e at r : (∀~α.τ1 −→ τ2 )@X; L2
Γ(r) = X
Γ(s) = YΓ ` reg r at s : reg(X)@Y; L(RV-e)(A-e)(E4-e)Γ ` unit : unit; LΓ ` ~v : ~τ ; L
Γ(r) = XΓ ` ~v at r : ~τ @X; LΓ(l) = τΓ(r) = XΓ ` loc l at r : ref (τ )@X; L(F5-e)

τ2 [γ/α1 ])@W; L1

Γ ` e1 : ∃α.τ1 ; Lα∈/ fvars(Γ) ∪ fvars(L) ∪ fvars(τ2 )Γ ] {x 7→ τ1 } ` e2 : τ2 ; LΓ ` open x = e1 as • in e2 : τ2 ; L(E3-e)

Γ(r) = X
Γ(s) = YΓ ` e : τ ; L ∪ {X}Γ ` inuse (reg r at s) in e : τ ; L2Γ ` e : (∀(α1 , α~2 ).τ1 −→τ2 )@W; L1(F4-e)(TV-e)(MV-e)

Figure 12: Extended small region language: additional type rules for intermediate expressions(6) For each l ∈ dom(S), Γ ` S(l) : Γ(l); −.
We write Γ ` (S, R, ~e) to mean that (S, R, ~e) is well typed under Γ.
Lemma 2 (Substitution 1) If Γ ] {x 7→ τ1 } ` e : τ2 ; L and Γ ` v : τ1 ; −, then Γ ` e[v/x] : τ2 ; L.
Proof: By induction on the type checking derivation.

2

Lemma 3 (Substitution 2) If Γ ` e : τ ; L then Γ[γ/α] ` e : τ [γ/α]; L[γ/α].
Proof: By induction on the type checking derivation.

2

Lemma 4 (Replacement) Suppose Γ ` E[e1 ] : −; L1 . Let Γ ` e1 : τ ; L2 be the subderivation. If Γ ` e2 :
τ ; L2 , then Γ ` E[e2 ] : −; L1 .
Proof: Trivial.

2

Lemma 5 If Γ1 ` e : τ ; L1 , Γ1 ⊆ Γ2 , and L1 ⊆ L2 , then Γ2 ` e : τ ; L2 .
Proof: By induction on the type checking derivation.

2

Theorem 3 (Subject Reduction) If Γ1 ` (S1 , R1 , e1 ) and S1 , R1 , e1 → S2 , R2 , e2 , then there exists Γ2such that Γ2 ` (S2 , R2 , e2 ).
Proof: The conditions (2), (3), and (4) can be proved independent of the choice of Γ2 . The condition (2)follows from inspection of the reduction rules. Given (2), (3) is straightforward by inspection of [R4-e] and[R6-e]. The condition (4) is straightforward by inspection of [R4-e].
It remains to find Γ2 to satisfy (1), (2), and (5). We do this via case analysis on the reduction rules.

22

(U-e)

[F1-e] Let Γ2 = Γ1 . LetE[Λ•λx:•.e at (reg r at s)] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` reg r at s : reg(X)@Z; L2
Γ2 ] {x 7→ τ1 } ` e : τ2 ; L1

α~∈/ fvars(Γ)
X, Z ∈ L2
L

1
Γ2 ` Λ•λx:•.e at (reg r at s) : (∀~α.τ1 −→
τ2 )@X; L2

By inspection of (RV-e), it must be the case that Γ2 (r) = X. Hence by (FV-e),L1Γ2 ` Λ•λx:•.e at r : (∀~α.τ1 −→
τ2 )@X; L2

By Lemma 4, it follows that
Γ2 ` E[Λ•λx:•.e at r] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[F2-e] Let Γ2 = Γ1 . Let
E[(Λ•λx:•.e at r) v] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivationL1
Γ2 ` (Λ•λx:•.e at r) : (∀().τ1 −→τ2 )@X; L2
Γ2 ` v : τ 1 ; L 2
L1 ∪ {X} ⊆ L2
Γ2 ` (Λ•λx:•.e at r) v : τ2 ; L2

By inspection of (FV-e), it must be the case thatΓ2 ] {x 7→ τ1 } ` e : τ2 ; L1
Hence by Lemma 2, it follows that
Γ2 ` e[v/x] : τ2 ; L1
By Lemma 5,
Γ2 ` e[v/x] : τ2 ; L2
By Lemma 4, it follows that
Γ2 ` E[e[v/x]] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[F3-e] Let Γ2 = Γ1 . Let
E[v[•]] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, v = Λ•λx : •.e at r and there is asubderivation
L2
Γ2 ` v : (∀(α1 , α~2 ).τ1 −→τ2 )@W; L1
Γ2 ` v[•] : (∀α~2 .τ1 [γ/α1 ]L2 [γ/α1 ]−→τ2 [γ/α1 ])@W; L1

By inspection of (FV-e), it must be the case thatΓ2 ] {x 7→ τ1 } ` e : τ2 ; L2and α1 , α~2 ∈/ fvars(Γ2 ). Hence by Lemma 3, it follows thatΓ2 ] {x 7→ τ1 [γ/α1 ]} ` e : τ2 [γ/α1 ]; L2 [γ/α1 ]23

Since bound static variables are assumed to be distinct, α1 ∈/ {α~2 }. Hence by (FV-e),Γ2 ` v : (∀α~2 .τ1 [γ/α1 ]L2 [γ/α1 ]−→τ2 [γ/α1 ])@W; L1

By Lemma 4, it follows that
Γ2 ` E[v] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[E-e] Let Γ2 = Γ1 . Let
E[open x = (pack v as •) as • in e] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` pack v as • : ∃α.τ1 ; L α ∈/ fvars(Γ) ∪ fvars(L) ∪ fvars(τ2 )
Γ2 ] {x 7→ τ1 } ` e : τ2 ; LΓ2 ` open x = (pack v as •) as • in e : τ2 ; L
By inspection of (E3-e), it must be the case that Γ2 ` v : τ [γ/α]; L. Hence by Lemma 2 and 3, it followsthatΓ2 [~γ /~α] ` e[v/x] : τ2 [~γ /~α]; L[~γ /~α]We have Γ2 [~γ /~α] = Γ2 , τ2 [~γ /~α] = τ2 and L[~γ /~α] = L. Hence we have
Γ2 ` e[v/x] : τ2 ; L
By Lemma 4, it follows that
Γ2 ` E[e[v/x]] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[R1-e] Let W ∈/ fvars(Γ1 ). Let Γ2 = Γ1 ] {t 7→ W}. It is easy to see that dom(Γ2 ) = dom(R ] {t 7→(1, 0)}) ∪ dom(S). Also, (2) holds.
For each thread e ∈ {e~1 }, Γ2 ` e : −; {Xsr } by Lemma 5.
Let
E[newregion at (reg r at s)] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` reg r at s : reg(Y)@Z; L Y, Z ∈ L X 6= Y
Γ2 ` newregion at (reg r at s) : ∃X.reg(X)@Y; L
By inspection of (RV-e), it must be the case that Γ2 (r) = Y. Hence by (RV-e) again Γ2 ` reg t at r :reg(W)@Y. By (E3-e),Γ2 ` pack (reg t at r) as • : ∃X.reg(X)@Y; L
By Lemma 4, it follows that
Γ2 ` E[pack (reg t at r) as •] : −; {Xsr }Hence (1) holds. (5) is trivial.
[R2-e] Let Γ2 = Γ1 . Let
E[freeregion (reg r at s)] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` reg r at s : reg(X)@Y; LY∈LΓ2 ` freeregion (reg r at s) : reg(X)@Y; L
Hence Γ2 ` reg r at s : reg(X)@Y; L. By Lemma 4, it follows that
Γ2 ` E[reg r at s] : −; {Xsr}
Hence (1) holds. (2) and (5) are trivial.
24[R3-e] Let Γ2 = Γ1 . By (A-e),Γ2 ` abort : −; {Xsr}
Hence (1) holds. (2) and (5) are trivial.
[R4-e] Let Γ2 = Γ1 . Let
E[useregion (reg r at s) in e] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` reg r at s : reg(X)@Y; LΓ2 ` e : τ ; L ∪ {X}Y∈L
Γ2 ` useregion (reg r at s) in e : τ ; L
By inspection of (RV-e), it must be the case that Γ2 (r) = X and Γ2 (s) = Y. Hence by (R4-e),Γ2 ` inuse (reg r at s) in e : τ ; L
By Lemma 4, it follows that
Γ2 ` E[inuse (reg r at s) in e] : −; {Xsr}
Hence (1) holds. (2) and (5) are trivial.
[R5-e] Similar to the case [R3-e].
[R6-e] Let Γ2 = Γ1 . Let
E[inuse (reg r at s) in v] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 (r) = X Γ2 (s) = Y Γ2 ` v : τ ; L ∪ {X}Γ2 ` inuse (reg r at s) in v : τ ; L

Y∈LSince v is a value, by inspection of the type checking rules, Γ2 ` v : τ ; L. By Lemma 4, it follows that
Γ2 ` E[v] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[T1-e] Similar to the case [F1-e].
[T2-e] Similar to the case [F2-e].
[L-e] Similar to the case [F2-e].
[M1-e] Let E[ref v at reg r at s] ∈ {e~1 } be the active thread. Then by inspection of the type checking
rules, there is a subderivation
Γ1 ` v : τ ; L
Γ1 ` reg r at s : reg(X)@Y; L X, Y ∈ L
Γ1 ` ref v at reg r at s : ref (τ )@X; L
Let Γ2 = Γ1 ] {l 7→ τ }. Clearly, dom(Γ2 ) = dom(R) ∪ dom(S ] {l 7→ v}).
For each thread e ∈ {e~1 }, Γ2 ` e : −; {Xsr} by Lemma 5. By inspection of (RV-e), it must be the casethat Γ2 (r) = X. Hence by (MV-e),Γ2 ` loc l at r : ref (τ )@X; L
By Lemma 4, it follows that
Γ2 ` E[loc l at r] : −; {Xsr}
Hence (1) holds. Since Γ2 ` v : τ ; L, (5) holds. (2) is trivial.
25[M2-e] Let Γ2 = Γ1 . Let E[!(loc l at r)] ∈ {e~1 } be the active thread. Then by inspection of the typechecking rules, there is a subderivation
Γ2 ` loc l at r : ref (τ )@X; L
X∈LΓ2 ` !(loc l at r) : τ ; L
By inspection of (MV-e), it must be the case that Γ2 (l) = τ . Hence by (5) (on the left state), Γ2 ` v : τ ; L.
By Lemma 4, it follows that
Γ2 ` E[v] : −; {Xsr }Hence (1) holds. (2) and (5) are trivial.
[M3-e] Let Γ2 = Γ1 . Let
E[(loc l at r) := v] ∈ {e~1 }be the active thread. Then by inspection of the type checking rules, there is a subderivation
Γ2 ` loc l at r : ref (τ )@X; LΓ2 ` v : τ ; LX∈L
Γ2 ` (loc l at r) := v : τ ; L
By Lemma 4, it follows that
Γ2 ` E[v] : −; {Xsr }Hence (1) holds.
By inspection of (MV-e), it must be the case that Γ2 (l) = τ . Hence (5) holds. (2) is trivial.
[S-e] Let Γ2 = Γ1 . There is a subderivation for the thread E[fork e2 ]
Γ2 ` e2 : τ ; {Xsr }Γ2 ` fork e2 : unit; L
By (U-e), Γ2 ` unit : unit; L. By Lemma 4, it follows that
Γ2 ` E[unit] : −; {Xsr}
We also have Γ2 ` e2 : −; {Xsr}. Hence (1) holds. (2) and (5) are trivial.

2

Lemma 6 If ∆; Γ ` E[e] : −; {Xsr} then there is a sub-derivation ∆; Γ ` e : −; L such that if X ∈ L and
X 6= Xsr then there is an occurrence of inuse (reg r at −) in − in E[e] such that Γ(r) = X.
Proof: By inspection on the definition of evaluation contexts and the corresponding type checking rules. 2
Theorem 4 (Progress) If ∆; Γ ` (S, R, ~e) and not all of ~e is a value, then there is a reduction from
(S, R, ~e).
Proof: The main part of the proof is in showing that conditions of the form R(r) = (1, −) in the hypothesesof each reduction rule are satisfied. These hypotheses appears across multiple reduction rules, but essentiallythe same argument can be used for all of them. We shall show this for the case ~e contains E[Λ•λx:•.e at v]
By inspection of the type checking rules, it must be the case that v = (reg r at s) for some r and s, andthat there is a subderivationΓ ` reg r at s : reg(X)@Z; L2
Γ ] {x 7→ τ1 } ` e : τ2 ; L1

α~∈/ fvars(Γ)
X, Z ∈ L2L1τ2 )@X; L2
Γ ` Λ•λx:•.e at (reg r at s) : (∀~α.τ1 −→

By (RV-e), Γ2 (r) = X and Γ2 (r) = Z. By Lemma 6 and Definition 2 (2), there is an occurrence of
inuse (reg r at −) in − and an occurrence of inuse (reg s at −) in −. By Definition 2 (4) and (5),this implies that R(r) = (1, −) and R(s) = (1, −). Hence [F1-e] can be applied to reduce the state.
Other cases can be proved analogously.
2
26

Theorem 5 Let e1 be a well-typed program in the source language. Let e2 be its corresponding type-erased
program in the intermediate language. Then {Xsr }; {rsr 7→ Xsr }(∅, {rsr 7→ (1, 1)}, e2 ) where rsr is thestarting region.
Proof: Trivial.

2

Corollary 1 (Type Soundness) If a source program e is well typed then it does not get stuck, that is, e
is memory safe.
Proof: By Theorem 3, Theorem 4 and Theorem 5227