Memory Usage Verification for OO Programs⋆
Wei-Ngan Chin1,2 , Huu Hai Nguyen1, Shengchao Qin3 , and Martin Rinard4
1

Computer Science Programme, Singapore-MIT AllianceDepartment of Computer Science, National University of Singapore
3
Department of Computer Science, University of Durham
4
Laboratory for Computer Science, Massachusetts Institute of Technology
2{chinwn,nguyenh2}@comp.nus.edu.sg
shengchao.qin@durham.ac.uk, rinard@lcs.mit.edu

Abstract. We present a new type system for an object-oriented (OO) languagethat characterizes the sizes of data structures and the amount of heap memory
required to successfully execute methods that operate on these data structures.
Key components of this type system include type assertions that use symbolic
Presburger arithmetic expressions to capture data structure sizes, the effect of
methods on the data structures that they manipulate, and the amount of memorythat methods allocate and deallocate. For each method, we conservatively capture
the amount of memory required to execute the method as a function of the sizesof the method’s inputs. The safety guarantee is that the method will never attempt
to use more memory than its type expressions specify. We have implemented a
type checker to verify memory usages of OO programs. Our experience is thatthe type system can precisely and effectively capture memory bounds for a wide
range of programs.

1 Introduction
Memory management is a key concern for many applications. Over the years researchers have developed a range of memory management approaches; examples include explicit allocation and deallocation, copying garbage collection, and region-based
memory allocation. However, an important aspect that has been largely ignored in pastwork is the safe estimation of memory space required for program execution. Overallocation of memory may cause inefficiency, while underallocation may cause software
failure. In this paper, we attempt to make memory usage more predictable by static
verification on the memory usage of each program.
We present a new type system, based on dependent type[21], that characterizes theamount of memory required to execute each program component. The key componentsof this type system include:– Data Structure Sizes and Size Constraints: The type of each data structure includes index parameters to characterize its size properties, which are expressed interms of the sizes of data structures that it contains. In many cases the sizes of thesedata structures are correlated; our approach uses size constraints expressed using
symbolic Presburger arithmetic terms to precisely capture these correlations.
– Heap Recovery: Our type system captures the distinction between shared and unaliased objects and supports explicit deallocation of unaliased objects.
⋆

slightly revised from SAS’05 version

– Preconditions and Postconditions: Each method comes with a precondition that
captures both the expected sizes of the data structures on which it operates and any
correlations between these sizes. The method’s postcondition expresses the newsize and correlations of these data structures after the method executes as a functionof the original sizes when the method was invoked.
– Heap Usage Effects: Each method comes with two memory effects. These effects
use symbolic values (present in method precondition) to capture (i) memory requirement which specify the maximum heap space that the method may consume,(ii) memory release which specify the minimum heap space that the method will
recover. Heap effects are expressed at the granularity of classes and can capture
the net change in the number of instances of each class.
Our paper makes several new technical contributions. Firstly, we design a formal
verification system in the form of a type system, that can formally and statically capture
memory usage for the object-oriented (OO) paradigm. We believe that ours is the firstsuch formal type system for OO paradigm. Secondly, we advocate for explicit heap recovery to provide more timely reclamation of dead objects in support of tighter bounds
on memory usage. We show how such recovery commands may be automatically inserted. Thirdly, we have proven the soundness of our type checking rules. Each welltyped program is guaranteed to meet its memory usage specification, and will never faildue to insufficient memory whenever its memory precondition is met. Lastly, we have
implemented a type checker and have shown that it is fairly precise and can handle areasonably large class of programs. Runtime stack space to hold methods’ parameters and local variables is another aspect of memory needed. For simplicity, we omit its
consideration in this paper.

2 Overview
Memory usage occurs primarily in the heap to hold dynamically created objects. In ourmodel, heap space is consumed via the new operation for newly created objects, while
unused objects may be recovered via an explicit deallocation primitive, called dispose.
Memory usage (based on consumption and recovery) should be calculated over theentire computation of each program. This calculation is done in a safe manner to help
identify the high watermark on memory space needed. We achieve this through the useof a conservative upper bound on memory consumed, and a conservative lower boundon memory recovered for each expression (and method).
To safely predict the memory usage of each program, we propose a size-polymorphic
type system for object-oriented programs with support for interprocedural size analysis.
In this type system, size properties of both user-defined types and primitive types arecaptured. In the case of primitive integer type inthvi, the size variable v captures its integer value, while for boolean type boolhbi, the size variable b is either 0 or 1 denoting
false or true, respectively. (Note that size variables capture some integer-based properties of the data structure. For simple types, the values are directly captured.) For userdefined class types, we use chn1 , . . . , np i where φ ; φI with size variables n1 , . . . , np todenote size properties that are defined in size relation φ, and invariant constraint φI . As

an example, consider a user-defined stack class, that is implemented with a linked list,
and a binary tree class as shown below.
class Listhni where n=m+1 ; n≥0 { Objecthi@S val; Listhmi@U next; · · · }class Stackhni where n=m ; n≥0 { Listhmi@U head; · · · }class BTreehs, di where s=1+s1 +s2 ∧d=1+max(d1 , d2 ) ; s≥0∧d≥0 {Objecthi@S val; BTreehs1 , d1 i@U left; BTreehs2 , d2 i@U right; · · · }Listhni denotes a linked-list data structure of size n, and similarly for Stackhni. The
size relations n=m+1 and n=m define some size properties of the objects in terms of
the sizes of their components, while the constraint n≥0 signifies an invariant associatedwith the class type. Class BTreehs, di represents a binary tree with size variables s andd denoting the total number of nodes and the depth of the tree, respectively. Due tothe need to track the states of mutable objects, our type system requires the support ofalias controls of the form A=U | S | R | L. We use U and S to mark each reference thatis (definitely) unaliased and (possibly) shared, respectively. We use R to mark readonly fields which must never be updated after object initialization. We use L to markunique references that are temporarily borrowed by a parameter for the duration ofits method’s execution. Our alias annotation mechanism are adapted from [5, 8, 1] andreported in [9]. Briefly, they allow us to track unique objects from mutable fields, aswell as shareable objects from read-only fields.
To specify memory usage, we decorate each method with the following declaration:t mn (t1 v1 , . . . , tn vn ) where φpr ; φpo ; ǫc ; ǫr {e}where φpr and φpo denote the precondition and postcondition of the method, expressedin terms of constraints/formulae on the size variables of the method’s parameters andresult. Precondition φpr denotes an applicability condition of the method in terms of
the sizes of its parameters. Postcondition φpo can provide a precise size relation for theparameters and result of the declared method. The memory effect is captured by ǫc andǫr . Note that ǫc denotes memory requirement, i.e., the maximum memory space that
may be consumed, while ǫr denotes net release, i.e., the minimum memory space thatwill be recovered at the end of method invocation. Memory effects (consumption andrecovery) are expressed using a bag notation of the form {(ci , αi )}m
i=1 , where ci denotes
a class type, while αi denotes its symbolic count.
class Stackhni where n=m ; n≥0 { Listhmi@U head;
L | voidhi@S push(Objecthi@S o) where true; n′ =n+1; {(List, 1)}; {}{ Listhi@U tmp=this.head; this.head=new List(o, tmp)}
L | voidhi@S pop() where n>0; n′ =n−1; {}; {(List, 1)}{ Listhi@U t1 = this.head; Listhi@U t2 = t1.next; t1.dispose(); this.head = t2}
L | boolhbi@S isEmpty() where n≥0; n′ =n ∧ (n=0∧b=1 ∨ n>0∧b=0); {}; {}{ Listhi@U t = this.head; boolhi@S v = isNull(t); this.head = t; v}
L | voidhi@S emptyStack() where n≥0∧d=n; n′ =0; {}; {(List, d)}{ boolhi@S v = this.isEmpty(); if v then () else {this.pop(); this.emptyStack()}}L | voidhi@S push3pop2(Objecthi@S o) where true; n′ =n+1; {(List, 2)}; {(List, 1)}{ this.push(o); this.push(o); this.pop(); this.push(o); this.pop()}}Fig. 1. Methods for the Stack ClassExamples of method declarations for the Stack class are given in Fig 1. The notation (A | ) prior to each method captures the alias annotation of the current this parameter. Note our use of the primed notation, advocated in [13, 16], to capture imperativechanges on size properties. For the push method, n′ =n+1 captures the fact that the sizeof the stack object has increased by 1; similarly, the postcondition for the pop method,n′ =n−1, denotes that the size of the stack is decreased by 1 after the operation. The
memory requirement for the push method, ǫr ={(List, 1)}, captures the fact that one
List node will be consumed. For the pop method, ǫr ={(List, 1)} indicates that one
List node will be recovered.
For the isEmpty method,n′ =n captures the fact thatNet
Releasethe size of the receiver obMem.
Req.
ject (this) is not changed bytime
the method. Furthermore, itspush push
pop push
pop
output of type boolhbi@S isrelated to the object’s size
Fig. 2. push3pop2: Heap Consumption and Recovery
through a disjunctive constraint n=0∧b=1∨n>0∧b=0.
Primitive types are annotated with alias S because their values are immutable and can be
freely shared and yet remain trackable. The emptyStack method releases all List nodesof the Stack object. For push3pop2 method, the memory consumed (or required) fromthe heap is {(List, 2)}, while the net release is {(List, 1)}, as illustrated in Fig. 2.
Size variables and their constraints are specified at method boundary, and need not
be specified for local variables. Hence, we may use boolhi@S instead of boolhvi@S for
the type of a local variable.

{}

3 Language and Annotations
We focus on a core object-oriented language, called M EM J, with size, alias, and memory annotations in Fig 3. M EM J is designed to be an intermediate language for Java
with either supplied or inferred annotations. A suffix notation y ∗ denotes a list of zeroor more distinct syntactic terms that are suitably separated. For example, (t v)∗ denotes(t1 v1 , . . . , tn vn ) where n≥0. Local variable declarations are supported by block structure of the form: (t v = e1 ; e2 ) with e2 denoting the result. We assume a call-by-value
semantics for M EM J, where values (primitives or references) are passed as arguments
to parameters of methods. For simplicity, we do not allow the parameters to be updated(or re-assigned) with different values. There is no loss of generality, as we can always
copy such parameters to local variables for updating.
The M EM J language is deliberately kept simple to facilitate the formulation of staticand dynamic semantics. Typical language constructs, such as multi-declaration block,sequence, calls with complex arguments, etc. can be automatically translated to constructs in M EM J. Also, loops can be viewed as syntactic abbreviations for tail-recursive
methods, and are supported by our analysis. Several other language features, including downcast and a field-binding construct are also supported in our implementation.
For simplicity, we omit them in this paper, as they play supporting roles and are notP ::= def∗ meth∗def ::= class c1 hn1..p i [ extends c2 hn1..q i ] where φ ; φI { fd∗ (A | meth)∗ }meth ::= t mn ((t v)∗ ) where φpr ; φpo ; ǫc ; ǫr {e}fd ::= t f
τ ::= c | prt ::= τ hn∗ i@A
w ::= v | v.f

A ::= U | L | S | R
pr ::= int | bool | voide ::=(c) null | k | w | w = e | t v = e1 ; e2 | new c(v ∗ )| v.mn (v ∗ ) | mn (v ∗ ) | if v then e1 else e2 | v.dispose()ǫ = {(c, α)∗ }φ∈ F(Memory Space Abstraction)(Presburger Size Constraint)::= b | φ1 ∧ φ2 | φ1 ∨ φ2 | ¬φ | ∃n · φ | ∀n · φb ∈ BExp(Boolean Expression)::= true | false | α1 = α2 | α1 < α2 | α1 ≤ α2α ∈ AExp(Arithmetic Expression)::= kint | n | kint ∗ α | α1 +α2 | −α | max(α1 ,α2 ) | min(α1 ,α2 )where kint ∈ Z is an integer constant; n ∈ SV is a size variablef ∈ Fd is a field name; v ∈ Var is an object variable
Fig. 3. Syntax for the M EM J Language

core to the main ideas proposed here. The interested reader may refer to our companion
technical report[10] for more information.
To support sized typing, our programs are augmented with size variables and constraints. For size constraints, we restrict to Presburger form, as decidable (and practical)
constraint solvers exist, e.g. [19]. We are primarily interested in tracking size propertiesof objects. We therefore restrict the relation φ in each class declaration of c1 hn1 , .., np i
Vwhich extends c2 hn1 , .., nq i to the form pi=q+1 ni =αi whereby V(αi ) ∩ {n1 , .., np } = ∅.
Note that V(αi ) returns the set of size variables that appeared in αi . This restricts size
properties to depend solely on the components of their objects.
Note that each class declaration has a set of instance methods whose main purpose
is to manipulate objects of the declared class. For convenience, we also provide a setof static methods with the same syntax as instance methods, except for its access to thethis object. One important feature of M EM J is that memory recovery is done safely(without creating dangling references) through a v.dispose() primitive.

4 Heap Usage Specification
To allow memory usage to be precisely specified, we propose a bag abstraction of
the form {(ci , αi )}ni=1 where ci denotes its classification, while αi is its cardinality. In
this paper, we shall use ci ∈ CN where CN denotes all class types. For instance, Υ1 ={(c1 , 2), (c2 , 4), (c3 , x + 3)} denotes a bag with c1 occurring twice, c2 four times andc3 x + 3 times. We provide the following two basic operations for bag abstraction tocapture both the domain and the count of its element, as follows:dom(Υ ) =df {c | (c, n) ∈ Υ }Υ (c) =df

 n, if (c, n) ∈ Υ
0, otherwiseWe define union, difference, exclusion over bags as:
Υ1 ⊎ Υ2 =df {(c, Υ1 (c)+Υ2 (c)) | c ∈ dom(Υ1 ) ∪ dom(Υ2 )}Υ1 − Υ2 =df {(c, Υ1 (c)−Υ2 (c)) | c ∈ dom(Υ1 ) ∪ dom(Υ2 )}Υ \ X =df {(c, Υ (c)) | c ∈ dom(Υ ) − X}

To check for adequacy of memory, we provide a bag comparator operation under asize constraint ∆, as follows:∆ ⊢ Υ1 ⊒ Υ2 =df (∆ ⇒ (∀c ∈ Z · Υ1 (c) ≥ Υ2 (c))) where Z = dom(Υ1 ) ∪ dom(Υ2 )The bag abstraction notation for memory is quite general and can be made more precise by refining its operations. For example, some class types are of the same size andcould replace each other to increase memory reuse. To achieve this we can use a bag
abstraction that is grouped by size(ci ) instead of class type ci .
4.1 Heap Consumption
Heap space is consumed when objects are created by the new primitive, and also by
method calls, except that the latter is aggregated to include recovery prior to consumption. Our aggregation (of recovery prior to consumption) is designed to identify a highwatermark of maximum memory needed for safe program execution. For each expression, we predict a conservative upper bound on the memory that the expression may
consume, and also a conservative lower bound on the memory that the expression will
release. If the expression releases some memory before consumption, we will use thereleased memory to obtain a lower memory requirement. Such aggregated calculations
on both consumption and recovery can help capture both a net change in the level ofmemory, as well as the high watermark of memory needed for safe execution.
For example, consider a recursive function which does p pops from one stackobject, followed by the same number of pushes on another stack.
voidhi@S moverec(Stackhai@L s, Stackhbi@L t, inthpi@S i)
where a≥p≥0; a′ =a−p∧b′ =b+p; {} ; {}{ if i<1 then ()else {Objecthi@S o = s.top(); s.pop(); moverec(s, t, i−1); t.push(o)} }Due to aggregation (involving recovery before consumption), the heap space that
may be consumed is zero. For each recursive call, the space for a List node is released
by s.pop() before it is reused by t.push(o). Aggregated over the recursive calls, we will
have p number of List nodes that have been released before the same number of nodes
are consumed. Hence, no new heap space is needed. Such aggregation is sensitive tothe order of the operations.
Consider now a different function which performs p pushes on t, followed by thesame number of pops from s.
voidhi@S moverec2(Stackhai@L s, Stackhbi@L t, inthpi@S i)
where a≥p≥0; a′ =a−p∧b′ =b+p; {(List, p)}; {(List, p)}{ if i<1 then ()else {Objecthi@S o = s.top(); t.push(o); moverec2(s, t, i−1); s.pop()} }Though the net change in memory usage is also zero, the memory effect for thisfunction is different as we require p number of List nodes to be consumed on entry,

before the same number of List nodes are recovered. This new memory effect has thepotential to push up the high watermark of memory needed by p List nodes.
4.2 Heap Recovery
Explicit heap space recovery via dispose has several advantages. It facilitates thetimely recovery of dead objects, which allows memory usage to be predicted moreaccurately (with tighter bounds). It also permits the use of more efficient custom allocators[4], where desired. Moreover, we shall provide an automatic technique to insert
dispose primitives with the help of alias annotation. With such a technique, we only
need to ensure that objects that are being disposed are non-null. This non-nullness property can be captured by a non-nullness analyser, such as [12]. This property is required
as we always recover memory space for each dispose primitive.
Memory recovery via dispose should occur when unique references that are still
alive (not in dead-set) are being discarded. This could occur at four places1 : (i) end
of local block, (ii) end of method block, (iii) prior to assignment operation, and (iv)at conditional expression. We would like to recover the memory space for each nonnull reference that is about to become dead. For example, consider the pop method’s
definition:
L | voidhi@S pop() where · · · { Listhi@U t1 = this.head; head = t1.next}

The object pointed to by head is about to become dead prior to the operation,
head = t1.next. To recover this dead object, we insert a dispose command to obtainhead = (t1.next <; head.dispose()) where e1 <;e2 ≡(t v = e1 ;e2 ;v). Consider the definition of the destroy method which calls emptyStack with an L-mode parameter.
voidhi@S destroy(Stackhni@U s) where · · · {emptyStack(s)}A unique s object is about to become dead at the end of the destroy method. To
recover this space, we can insert s.dispose() prior to the method’s exit.
Let us formalise an automatic technique for the explicit recovery of dead objects
that are known at compile-time. Given an expression e, we utilize the alias annotation
to obtain a new expression e1 where suitable explicit heap dispose operations have beensafely inserted. This is achieved by a translation below with Γ to denote a type environment mapping program variables to their annotated types, and Θ(Θ1 ) to denote the setof dead references (of the form v or v.f ) before (after) the evaluation of expression e.
Γ ; Θ ⊢ e ֒→H e1 :: t, Θ1

Most rules are structure-preserving (or identity) rewritings, except for four rules given
in Fig 4. A sequence of disposals can be effected through dispose(D), with D containing
a set of variable/field references that are about to be dead at the end of expression e.
For the assignment rule [H:ASSIGN], we add w to the disposal set if it is unique andis not yet in dead-set using D = {w | ann(t)=U}−Θ1 . The function isParam(w) returns
true if w is a parameter variable, otherwise it returns false (for fields and local variables). The function ann extracts the alias of an annotated type, ann(τ hv ∗ i@A) = A. A
1

Note that unique reference cannot escape through e1 in e1 ; e2 as we require e1 to be of thevoid type.

[H:ASSIGN]¬ isParam(w) Γ (w) = t
D = {w | ann(t) = U} − Θ1
Γ ; Θ ⊢ e ֒→H e1 :: t1 , Θ1
⊢ t1 <: te2 = (e1  D=∅  e1 <; dispose(D))[H:IF]
Γ (v) = boolhbi@SΓ ; Θ ⊢ ei ֒→H êi :: ti , Θi i = 1, 2
t = msst(t1 , t2 ) Θ3 = Θ1 ∪ Θ2
Di = Θ3 −Θi i = 1, 2
Ei = (êi  Di =∅  êi <; dispose(D)) i = 1, 2

Γ ; Θ ⊢ w = e ֒→H
w = e2 :: void@S, Θ1 \w

Γ ; Θ ⊢ if v then e1 else e2 ֒→H
if v then E1 else E2 :: t, Θ3[H:METH]Γ1 = Γ + {v1 :: t1 , .., vp :: tp }
Γ1 ; ∅ ⊢ e ֒→H e1 :: t, Θ
⊢ t <: t0 ann(t0 ) 6= L∀i∈1..p·(ann(ti ) =L)⇒(∀f ·vi .f 6∈Θ)
D = {w | (w :: t) ∈ Γ1 , ann(t)=U}−Θ
e2 = (e1  D=∅  e1 <; dispose(D))[H:LOCAL]Γ ; Θ ⊢ e1 ֒→H e3 :: t1 , Θ1
⊢ t1 <: tann(t) 6∈ {L, R}Γ +{v :: t}; Θ1 ⊢ e2 ֒→H e4 :: t2 , Θ2
D = {v | ann(t) = U} − Θ2e5 = (e4  D=∅  e4 <; dispose(D))Γ ⊢meth t0 mn((ti vi )i:1..p ){e}֒→H t0 mn((ti vi )i:1..p ) {e2 }Γ ; Θ ⊢ (t v = e1 ; e2 ) ֒→H(t v = e3 ; e5 ) :: t2 , Θ2 \v

Fig. 4. Automatic Insertion of dispose operation

conditional is expressed as ξ1  b  ξ2 =df
Θ\v =df Θ − {v, v.f ∗ } ξ1 , if b;
ξ2 , otherwise.

Furthermore, we have:Θ\v.f =df Θ − {v.f }For the method declaration rule [H:METH], we add to the disposal set those parameterswhich are unique but not yet dead using {w | (w :: t) ∈ Γ1 , ann(t) = U} − Θ . For the local
declaration rule [H:LOCAL], we add v to the disposal set if it is unique but not yet deadusing {v | ann(t) = U} − Θ2 . For the [H:IF] rule, the uniqueness that are consumed in one
branch may have their heap spaces recovered in the other branch. This is captured by
Di = Θ3 −Θi , i = 1, 2. Notice that msst(t1 , t2 ) returns the minimal supertype of both t1
and t2 , as follows:τ1 <: τA1 ≤a A

τ2 <: τ ∀τ3 · (τ1 , τ2 <: τ3 ⇒τ <: τ3 )A2 ≤a A ∀A3 · (A1 , A2 ≤a A3 ⇒A≤a A3 )msst(τ1 @A1 , τ2 @A2 ) =df τ @A

Note that τ1 <: τ2 denotes the subtype relation for underlying types (without annotations). Alias subtyping rules (shown below) allow unique references to be passed toshared and lent-once locations (in addition to other unique locations), but not vice-versa.
A ≤a AU ≤a LU ≤a SIn the rest of this paper, we shall present a new static type system for verifying
memory heap usage, followed by a set of safety theorems on the type rules.

5 Rules for Memory Checking
We present type judgements for expressions, method declarations, class declarations
and programs to check for adequacy of memory, using relations of the form:Γ ; ∆; Υ ⊢ e :: t, ∆1 , Υ1

Γ ⊢meth meth⊢class def⊢P

Note that Γ is the type environment as explained earlier; ∆(∆1 ) denotes the size
constraint, which holds for the size variables associated with Γ (Γ and t) for expression
e before (after) its evaluation; t is an annotated type. Also, Υ (Υ1 ) is used to denote theavailable memory space in terms of bag abstraction before (after) the evaluation.
We present a few key syntax-directed type rules in Fig 5, with the rest of the rules inthe technical report. Before that, let us describe some notations used by the type rules.

[ASSIGN]Γ ; ∆; Υ ⊢ e :: t1 , ∆1 , Υ1 Γ ⊢ w :: t, φ, Y
⊢ t1 <:t, ρ X=V(t1 )∪V(t) ∆2 =∃X·(∆1 ◦Y ρφ)Γ ; ∆; Υ ⊢ w = e :: voidhi@S, ∆2 , Υ1
[DISPOSE]Γ (v) = chn∗ i@U Υ1 = Υ ⊎ {(c, 1)}Γ ; ∆; Υ ⊢ v.dispose() :: voidhi@S, ∆, Υ1[IF]
Γ (v) = boolhbi@SΓ ; ∆ ∧ b′ = 1; Υ ⊢ e1 :: t1 , ∆1 , Υ1
Γ ; ∆ ∧ b′ = 0; Υ ⊢ e2 :: t2 , ∆2 , Υ2(t, Υ3 , ∆3 ) = unify(t1 , t2 , Υ1 , Υ2 , ∆1 , ∆2 )
Γ ; ∆; Υ ⊢ if v then e1 else e2 :: t, ∆3 , Υ3[NEW]
fdList(chn∗ i) = ([(t̂i fi )]pi=1 , φ′ )r ∗ = fresh() ti = prime(Γ (vi ))⊢ ti <: [R 7→ S]t̂i , ρSi i∈1..pρ = [n∗ 7→ r ∗ ] ∪ pi=1
S ρi
∆ ⊢ Υ ⊒ {(c, 1)} X = pi=1 V(t̂i )∆1 = ∆∧(∃X·ρφ′ ) Υ1 = Υ −{(c, 1)}Γ ; ∆; Υ ⊢ new c(v1..p ) :: chr ∗ i@U, ∆1 , Υ1

[OVERRIDE]
methk = t mn((ti vi )i:1..p ) whereφpr k ; φpo k ; ǫkm ; ǫkn {· · · }, k = 1, 2
φpr 1 ⇒φpr 2 φpo 2 ⇒φpo 1
φpr 1 ⊢ ǫ1m ⊒ǫ2m φpr 1 ⊢ ǫ2n ⊒ǫ1n
⊢ OverridesOK(meth1 , meth2 )[IMI]⊢ (A | t̂ mn((t̂i v̂i )i:1..p ) where φpr ; φpo ; ǫc ; ǫr {e})∈chn∗ it = fresh(t̂) St0 = chn∗ i@A Γ (vi ) = ti i ∈ 0..p ⊢ ti <: t̂i , ρi i ∈ 1..p
ρp = pi=1 ρi ∆1 ⊢ Υ ⊒ǫc ρ=rename(t̂, t)∪ρp ∪prime(ρp )∆ ≈>V(Γ ) ∃V(ǫc )∪V(ǫS r )·ρ φpr ∆1 = ∆ ◦L ∃Y · ρ(φpr ∧φSpo )Υ1 = Υ −ǫc ⊎ǫr X = pi=1 V(t̂i ) Y = X ∪ prime(X) L = pi=0 V(ti )Γ ; ∆; Υ ⊢ v0 .mn(v1..p ) :: t, ∆1 , Υ1
[METH]
Γ1 = Γ ∪ {v1 :: t̂1 , .., vp :: t̂p } ∆ = noX (Γ1 )∧φpr ∧inv(Γ1 )∆ ⊢ǫc ⊒∅
Γ1 ; ∆; ǫc ⊢ e :: t, ∆1 , Υ1 φpr ∧∆1 ⊢Υ1 ⊒ ǫr ∆ ⊢ǫr ⊒∅ ⊢ t <: t̂, ρS( , , Ni ) = Vfield (t̂i ), i ∈ 1..p Y = pi=1 Ni (∃ prime(Y)·∆1 )⇒ρ(φpo )Γ ⊢meth t̂ mn((t̂i vi )i:1..p ) where φpr ; φpo ; ǫc ; ǫr {e}Fig. 5. Some Type Rules for Memory Checking

5.1 Notations
We use function V to return size variables of a formula, e.g. V(x′ =z+1∧y=2)={x′ , y, z}.
We extend it to annotated type, type environment, and memory specification, e.g.,V(τ hn∗ i@A)={n∗ }, V({(c, 4×d+8)})={d}. The function prime takes a set of size variables and returns their primed version, e.g. prime({s1 , . . . , sn })={s′1 , . . . , s′n }. Note thatprime operation is idempotent, namely (v ′ )′ =v ′ . We extend this to (annotated) type, typeenvironment, and even substitution. For example, prime(τ hn1 , . . . , nk i) = τ hn′1 , . . . , n′k i,and prime([x7→a, y7→b]) = [x′ 7→a′ , y ′ 7→b′ ]. Often, we need to express a no-change condition on a set of size variables. We define a noX operation as follows which returns aformula for which the original and primed variables are made equal.
noX ({}) =df true

noX ({x}∪X) =df (x′ =x)∧noX (X)We extend this function to annotated types (and type environments), as follows: noX (t)=df noX (V(t)). Also, we use n∗ = fresh() to generate new size variables n∗ . We extend it
to annotated type, so that t̂ = fresh(t) will return a new type t̂ with the same underlying
type as t but with fresh size variables instead.
Function rename(t1 , t2 ) returns anequality substitution, e.g. rename(Inthri, Inths′ i)=[r7→s′ ]. The operator ∪ combines twodomain disjoint substitutions into one.
The function fdList is used to retrieve a full list of fields for a given class, together
with its size relation. The function inv is used to retrieve the size invariant that is associated with each type. This function shall also be extended to type environment and listof types. The function Vfield classifies size variables from each field into three groups :(i) immutable, (ii) mutable but unique, (iii) otherwise (non-trackable).
To effect a change φ to an existing poststate ∆, we provide an operator, ◦Y , with
Y = {s∗ } to denote the set of size variables that is to be updated, as follows:∆ ◦Y φ =df ∃ r1 · · · rn · ρ2 (∆) ∧ ρ1 (φ)′
nwhere Y = {s1 , . . . , sn } ; {r1 , . . . , rn } = fresh() ; ρ1 = [si 7→ ri ]ni=1 ; ρ2 = [si 7→ ri ]i=1

5.2 Assignment
The [ASSIGN] rule captures imperative updates (to object fields and variables) by modifying the current size constraint to a new updated state with changes to the imperative
size variables from the LHS. From the rule, note that Γ ⊢ w :: t, φ, Y is to identify Y as aset of imperative size variables and also to gather a constraint φ for this set. The subtype
relation ⊢ t1 <: t, ρ will return a substitution that maps the size variables of supertype
to that of the subtype. This mapping ignores all non-trackable size variables that may
be globally aliased, but immutable and unique mutable size variables are captured.
5.3 Memory Operations
The heap space is directly changed by the new and dispose primitives. Their corresponding type rules, [NEW] and [DISPOSE], would ensure that sufficient memory isavailable for consumption by new and will credit back space relinquished by dispose.
The memory effect is accumulated according to the flow of computation. Consider:∆⊢Υ ⊒{(List, 1)} ∆1 =∆◦{x} x′ =x+1
Γ ; ∆; Υ ⊢ x = new List(o, x) :: voidhi@S, ∆1 , Υ −{(List, 1)}
Υ1 =(Υ −{(List, 1)})⊎{(List, 1)}Γ ; ∆1 ; Υ −{(List, 1)} ⊢ y.dispose() :: voidhi@S, ∆1 , Υ1
Γ ; ∆; Υ ⊢ x = new List(o, x); y.dispose() :: voidhi@S, ∆1 , ΥThe new operation consumes a List node, while the dispose operation releases
back a List node. The net effect is that available memory Υ is unchanged. However,
due to the order of the two operations, we require ∆⊢Υ ⊒{(List, 1)} which affects the
maximum memory required.
Another rule which has a direct effect on memory is the method invocation rule
[IMI]. Sufficient memory must be available for consumption prior to each call (as specified by ∆1 ⊢ Υ ⊒ǫc ), with the net memory release added back in the end (as specifiedby Υ1 = Υ −ǫc ⊎ǫr ). Each method precondition must be met by the pre-state of its caller.
This is checked by ∆ ≈>V(Γ ) ∃V(ǫc )∪V(ǫr )·ρ φpr which uses a relation ≈>X , defined as:∆ ≈>X φ =df (∆ ⇒ ρφ), where ρ = [s1 7→ s′1 , .., sn 7→ s′n ] ∧ Vu (φ) ∩ X = {s1 , .., sn }.

Note that Vu returns size variables in unprimed form, e.g. Vu (x′ =z+1∧y=2) = {x, y, z}.
5.4 Conditional
Our type rule for conditional [IF] is able to track both the size-constraints and memory
usages in a path-sensitive manner. Path-sensitivity is encoded by adding b′ =1 and b′ =0
to the pre-states of the two branches, respectively. We achieve path-sensitivity for memory usage specification by integrating it with relational size constraints derived. Take
note that the unify operation merges the post-state constraints and memory usages fromthe two branches via a disjunction, a formal definition and an example can be found in
our report [10]. Path-sensitivity makes our analysis more accurate and is critical for
analysing the memory requirement of recursive methods.
5.5 Method Declaration
Each method declaration is checked to see if its definition is consistent with the memory usage specification given in its declaration header by the [METH] rule. The initialmemory is ǫc . The final available memory of the method body e is Υ1 which must not
be less than the declared net memory release (as specified by φpr ∧∆1 ⊢ Υ1 ⊒ ǫr ).
Function subtyping for the OO paradigm is used to support method overriding. Thisis captured by the [OVERRIDE] rule in Fig 5. Each method which overrides anotheris expected to be contravariant on its precondition (and memory consumption) andcovariant on its postcondition (and memory releases)

6 Soundness of Type System
We have proposed a small-step operational semantics (denoted by ֒→ transitions) instrumented with alias and size notations[10], and have also formalised two safety theorems
for our type rules. The first theorem states that each well-typed expression preserves
its type under reduction with a runtime environment Π and a store ̟ that are consistent
with the compile-time counterparts, Γ (type environment) and Σ (store typing). Also,
final size constraint is consistent with the value obtained on termination.

Theorem 1 (Preservation).
(a) (Expression) IfΓ ; Σ; ∆; Θ; Υ ⊢ e :: t, ∆1 , Θ1 , Υ1

Γ ; Σ; ∆; Θ; Υ |= hΠ, ̟, σihΠ, ̟, σi [e] ֒→ hΠ1 , ̟1 , σ1 i [e1 ]then there exist Σα ⊇ Σ , Γα , ∆α , Θα , and Υα , such thatΓ − diff(e, e1 ) = Γα − diff(e1 , e)Γα ; Σα ; ∆α ; Θα ; Υα ⊢ e1 :: t, ∆1 , Θ1 , Υ1Γα ; Σα ; ∆α ; Θα ; Υα |= hΠ1 , ̟1 , σ1 i .

(b) (Value) If Γ ; Σ; ∆; Θ; Υ ⊢ (A, δ) :: t, ∆1 , Θ1 ; Υ1then the following hold:Θ = Θ1

Γ ; Σ; ∆; Θ; Υ |= hΠ, ̟, σi

Γ + {x :: t}; Σ; ∆2 ; Θ1 ; Υ1 |= hΠ + {x 7→ (A, δ)}, ̟, σ iwhere x = fresh() , ∆2 = [v 7→ v ′ ]v∈V(t) ∆1 .
Proof: By induction over the depth of type derivation for expression e. Details are givenin the technical report [10].
2
The second safety theorem on progress captures the fact that well-typed programs
cannot go wrong. Specifically, this theorem guarantees that no memory adequacy errors
are ever encountered for well-typed M EM J programs, as follows:
Theorem 2 (Progress). If Γ ; Σ; ∆; Θ; Υ ⊢e :: t, ∆1 , Θ1 , Υ1 and Γ ; Σ; ∆; Θ; Υ |= hΠ, ̟, σi ,then either e is a value, or hΠ, ̟, σi [e] ֒→ Err-Null, or there exist Π1 , ̟1 , σ1 , e1 suchthat hΠ, ̟, σi [e] ֒→ hΠ1 , ̟1 , σ1 i [e1 ].
Proof: By induction over the depth of type derivation for expression e. Details are givenin the technical report [10].
2

7 Implementation
We have constructed a type checker for M EM J, and have also built a preprocessor toallow a more expressive language to be accepted. The entire prototype was built usinga Haskell compiler[18] where we have added a library (based on [19]) for Presburger
arithmetic constraint-solving.
The main objective of our initial experiments is to show that our memory usage
specification mechanism is expressive and that such an advanced form of type checking
is viable. We converted to M EM J a set of programs from the Java version of the Oldenbenchmark suite [7] and another set of smaller programs from the RegJava benchmark[11], before subjecting them to memory adequacy checking. Our initial experimental results are encouraging; however this is a proof-of-concept implementation andthere is scope for optimization and more exhaustive experimentation.

Figure 6 summarises the statistics obtained for each programthat we have verified via our typechecker. Column 3 illustrates thesize and memory annotation overheads which must be made in
the header declarations of eachclass and method. Columns 4 and5 highlight the CPU times used(in seconds) for alias and memory checking, respectively. Our experiments were done under Redhat Linux 9.0 platform on Pentium 2.4 GHz with 768MB main
memory. Except for the perimeter
program (which has more conditionals from using a quadtree data
structure), all programs take under
10 seconds to verify, despite themFig. 6. Type Checking Experimental Results
being medium-sized programs andthe high complexity of Presburger solving. We attribute this to the fact that memory declarations are verified in a summary-based fashion for each method definition. The lastcolumn highlights the number of methods that have been successfully verified as using
memory spaces that are bounded by symbolic Presburger formulae. All methods’ heap
usage could be statically bounded, except2 for a method in Voronoi that has an allocation
inside a loop, with a complex termination condition. Apart from the memory checking system described above, we have also conducted some preliminary investigation on
memory inference which is described in [17].
Programs Size (lines) Checking (in sec.) Verified
Source Ann. Alias Memory Methods
bisort340
7 0.01
2.56
6/6
em3d
462 19 0.05
1.14
20/20
health562 22 0.05
6.37
15/15
mst
473 31 0.02
1.26
22/22
power
765 24 0.06
4.28
19/19
treeadd
195
6 0.02
0.32
4/4
tsp
545 10 0.02
3.54
9/9
perimeter 745 12 0.02
21.81
8/8
n-body1128 31 0.60
1.25
22/22
Voronoi 1000 45 0.03
3.51
39/40
stack
122 12 0.01
0.08
10/10
sieve
88
7 0.01
0.09
6/6
m-sort183 13 0.01
0.36
12/12
life
164
9 0.022.95
7/7
Mandelbrot 194 11 0.01
1.72
10/10
Reynolds3 98
6 0.01
0.18
4/4

8 Related Work
Past research on memory models for object-oriented paradigm have focused largely on
efficiency and safety. We are unaware of any prior type-based work on analysing heap
memory usage by OO programs for the purpose of checking for memory adequacy. The
closest related work on memory adequacy are based on first-order functional paradigm,
where data structures are mostly immutable and thus easier to handle.
Hughes and Pareto [15] proposed a type and effect system on space usage estimation
for a first-order functional language, extended with region language constructs of Tofteand Talpin’s[20]. The use of region model facilitates recovery of heap space. However,as each region is only deleted when all its objects become dead, more memory thannecessary may be used, as reported by [4].
Hofmann and Jost [14] proposed a solution to obtain linear bounds on the heap
space usage of first-order functional programs. A key feature of their solution is the use
2

For Olden programs which built tree-like data structure, we make a minor change to take total
nodes rather than heights as parameters. This avoids exponential formulae.

of linear typing which allows the space of each last-use data constructor (or record) to
be directly recycled by a matching allocation. With this approach, memory recovery canbe supported within each function, but not across functions in general. Moreover, theirmodel does not track the symbolic sizes of data structures. Nevertheless, one significant
advance of their work is an inference mechanism through linear programming (LP)technique. The main advantage of LP technique is that no fix-point analysis is required,
but it restricts the memory effects to a linear form without disjunction.
Apart from the above memory analysis work on high level languages, Aspinall andCompagnoni [3] presented a first-order linearly typed assembly language to allow safe
reuse of heap space. Their system is a target for the compilation of a functional programming language with a similar type systems (e.g. Hofmann’s LFPL) . More recently,
Cachera et. al. [6] proposed a constraint-based memory analysis for Java Bytecode-likelanguages. For a given program their loop-detecting algorithm can detect methods andinstructions that execute an unbounded number of times, thus can be used to check
whether the memory usage is bounded or not. However, their analysis cannot check
whether a given amount of memory is adequate or not, while our system does.

9 Concluding Remarks
We have proposed a memory usage type system for a non-trivial object-oriented corelanguage. We have designed a flexible specification mechanism to allow memory needsof user programs to be declared abstractly, and then verifies if memory adequacy property holds for the given definitions. Our approach requires heap space to be explicitly
deallocated, which can be handled automatically. We have also built a prototype typechecker to confirm the viability and practicality of our approach. We envision our framework to be useful for embedded system, where memory is considered to be a criticalresource. We also envision the synergy of predicable memory bounds with region-based
memory management systems. In particular, bounded memory regions can result in better performance. Synergistically, region-based system can provide timely recovery forshared objects that are dead, providing us with tighter memory bounds.
Acknowledgement The authors would like to acknowledge the invaluable help of Florin
Craciun with the evaluation of a set of the benchmark programs.

References
1. J. Aldrich, V. Kostadinov, and C. Chambers. Alias Annotation for Program Understanding.
In ACM OOPSLA, Seattle, Washington, November 2002.
2. B. Alpern, D. Attanasio, J. J. Barton, A. Cocchi, S. F. Hummel, D. Lieber, M. Mergen,
T. Ngo, J. Shepherd, and S. Smith. Implementing Jalapeño in Java. In ACM OOPSLA,
Denver, Colorado, November 1999.
3. D. Aspinall and A. Compagnoni. Heap bounded assembly language. Journal of AutomatedReasoning, 31:261–302, 2003.
4. E. D. Berger, B. G. Zorn, and K. S. Mckinley. Reconsidering Custom Memory Allocation.
In ACM OOPSLA, November 2002.
5. J. Boyland, J. Noble, and W. Retert. Capabilities for Sharing: A Generalization of Uniqueness and Read-Only. In ECOOP, Budapest, Hungary, June 2001.

6. D. Cachera, T. Jensen, D. Pichardie, and G. Schneider. Certified Memory Usage Analysis.
In 13th International Symposium of Formal Methods Europe (FM’05), July 2005.
7. M. C. Carlisle and A. Rogers. Software caching and computation migration in Olden. In 4th
Principles and Practice of Parallel Programming, Santa Barbara, California, May 1993.
8. E. C. Chan, J. Boyland, and W. L. Scherlis. Promises: Limited Specifications for Analysis
and Manipulation. In Proceedings of the International Conference on Software Engineering,
pages 167–176, Kyoto, Japan, April 1998.
9. W.N. Chin, S.C. Khoo, S.C. Qin, C. Popeea, and H.H. Nguyen. Verifying Safety Policies
with Size Properties and Alias Controls. In 27th International Conference on Software Engineering (ICSE05), St. Louis, Missouri, May 2005.
10. W.N. Chin, H.H. Nguyen, S.C. Qin, and M. Rinard. Predictable Memory Usage for ObjectOriented Programs. Technical report, SoC, Natl Univ. of Singapore, November 2004. avail.
at http://www.dur.ac.uk/shengchao.qin/papers/memj.ps.gz.
11. M. V. Christiansen and P. Velschow. Region-Based Memory Management in Java. Master’s
Thesis, Department of Computer Science (DIKU), University of Copenhagen, 1998.
12. M. Fahndrich and R. Leino. Declaring and checking non-null types in an object-oriented
language. In ACM OOPSLA, Anaheim, CA, October 2003.
13. C. A. R. Hoare and J. He. Unifying Theories of Programming. Prentice-Hall, 1998.
14. M. Hofmann and S. Jost. Static prediction of heap space usage for first order functional
programs. In ACM POPL, New Orleans, Louisiana, January 2003.
15. J. Hughes and L. Pareto. Recursion and Dynamic Data-Structures in Bounded Space: Towards Embedded ML Programming. In Proceedings of the International Conference on
Functional Programming (ICFP ’99), September 1999.
16. L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages andSystems, 16(3):872–923, May 1994.
17. H. H. Nguyen. Memory Usage Inference for Object-Oriented Programs. Technical report,
CS Programme, Singapore-MIT Alliance, July 2004. (Term Paper).
18. S Peyton-Jones and et al. Glasgow Haskell Compiler. http://www.haskell.org/ghc.
19. W. Pugh. The Omega Test: A fast practical integer programming algorithm for dependence
analysis. Communications of the ACM, 8:102–114, 1992.
20. M. Tofte and J. Talpin. Region-based memory management. Information and Computation,132(2), 1997.
21. H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In ACM
PLDI. ACM Press, June 1998.

A

Alias Checking

We introduce four alias control mechanisms U | S | R | L adopted from [5, 8, 1]. These
alias mechanisms shall be used to support precise size tracking in the presence of mutable objects, and also for the automatic recovery of dead unique objects. For sizetracking, we introduce R-mode fields to allow size-immutable properties to be accurately tracked for all objects. For example, an alternative class declaration for the list
data type is given below, where its next field is marked as read-only (or immutable).
Note that the val field remains mutable.
class RListhni where n=m+1 ; n≥0 { Objecthi@S val; RListhmi@R next; · · · }The size property of such an RList type can be analysed at compile-time, whileallowing its objects to be freely shared. However, this comes at the cost of losing bothmutability and uniqueness.

We make use of L-mode parameters, with the limited unique (or lent-once) property[8], to capture unique references that are temporarily lent out to method calls. They
allow the preservation of uniqueness together with precise size-tracking across methods.
Consider the following method with two List parameters.
voidhi@S join(Listhmi@L x, Listhni@U y) where n > 0; m′ =n+m; · · ·{ if isNull(x.next) then x.next = y else join(x.next, y) }The first parameter is annotated as lent-once and can thus be tracked for size properties without loss of uniqueness. However, the second parameter is marked unique as its
reference escapes the method body (into the tail of the List from the first parameter). In
other words, the parameter y can have its uniqueness consumed but not x, as reflectedin the body of the above method declaration. Given two unique lists, a and b, the calljoin(a, b) would consume the uniqueness of b but not that of a. Our lent-once policy ismore restrictive than normal lending [1] as we require each lent-once parameter to beunaliased within the scope of its method. For example, join(a, a) is allowed by the typerules of [1], but disallowed by our lent-once’s policy.
In our alias type system, uniqueness may be transferred from one location (variable,
field or parameter) to another location. Consider a type environment {x::Objecthi@U,
y::Objecthi@U, z::Objecthi@S} where variables x and y are unique, while z is shared. In
the following code, {x = y; z = x}, the uniqueness of y is first transferred to location x,
followed by the consumption of uniqueness of x that is lost to the shared variable z. In
our type judgement, we track variables/fields that have become dead using:Γ ; Θ ⊢ e :: t, Θ1

Here, each dead-set Θ(Θ1 ) captures the set of references with consumed uniquenessbefore(after) the evaluation of expression e. Γ is a type enviroment which maps variables to their annotated types. Other type judgements for methods, classes and programs
have the following forms.
Γ ⊢meth meth⊢def def⊢P defi:1..p methi:1..q

The full set of alias checking rules are given in our technical report [10]).