Technical Report No. 822

MIT Laboratory for Computer Science

November 2001

Roles Are Really Great!
Viktor Kuncak, Patrick Lam, and Martin Rinard

arXiv:cs/0408013v1 [] 5 Aug 2004

Laboratory for Computer Science
Massachusetts Institute of Technology
Cambridge, MA 02139

{vkuncak, plam, rinard}@lcs.mit.edu

5.4

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

9
9
9
9
9
10

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

10
11
12
13
15
16
16

7 Interprocedural Role Analysis
7.1 Procedure Transfer Relations . . . . . . .
7.1.1 Initial Context . . . . . . . . . . .
7.1.2 Procedure Effects . . . . . . . . . .
7.1.3 Semantics of Procedure Effects . .
7.2 Verifying Procedure Transfer Relations . .
7.2.1 Role Graphs at Procedure Entry .
7.2.2 Verifying Basic Statements . . . .
7.2.3 Verifying Procedure Postconditions
7.3 Analyzing Call Sites . . . . . . . . . . . .
7.3.1 Context Matching . . . . . . . . .
7.3.2 Effect Instantiation . . . . . . . . .
7.3.3 Role Reconstruction . . . . . . . .

.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.

17
18
18
19
20
20
20
21
21
21
22
22
22

8 Extensions
8.1 Multislots . . . . . . . . . . . . . . . . . . . .
8.2 Cascading Role Changes . . . . . . . . . . . .

22
22
23

9 Related Work

24

10 Conclusion

25

ABSTRACT
We present a new role system for specifying changing referencing relationships of heap objects. The role of an object
depends, in large part, on its aliasing relationships with other
objects, with the role of each object changing as its aliasing
relationships change. Roles therefore capture important object and data structure properties and provide useful information about how the actions of the program interact with
these properties. Our role system enables the programmer
to specify the legal aliasing relationships that define the set
of roles that objects may play, the roles of procedure parameters and object fields, and the role changes that procedures
perform while manipulating objects. We present an interprocedural, compositional, and context-sensitive role analysis algorithm that verifies that a program respects the role
constraints.

Contents
1 Introduction

1

2 Example
2.1 Role Definitions . . . . . . . . . . . . . . . . .
2.2 Roles and Procedure Interfaces . . . . . . . .

2
2
3

3 Abstract Syntax and Semantics of Roles
3.1 Heap Representation . . . . . . . . . . . . . .
3.2 Role Representation . . . . . . . . . . . . . .
3.3 Role Semantics . . . . . . . . . . . . . . . . .

3
3
3
4

4 Role Properties
4.1 Formal Properties of Roles . . . . . . . . . . .

4
5

5 A Programming Model
5.1 A Simple Imperative Language . . . . . . . .
5.2 Operational Semantics . . . . . . . . . . . . .
5.3 Onstage and Offstage Objects . . . . . . . . .

7
7
7
7

∗

This research was supported in part by DARPA Contract F33615-00-C-1692, NSF Grant CCR00-86154, NSF
Grant CCR00-63513, and an NSERC graduate scholarship.

5.5

Role Consistency . . . . . . . . . . . .
5.4.1 Offstage Consistency . . . . . .
5.4.2 Reference Removal Consistency
5.4.3 Procedure Call Consistency . .
5.4.4 Explicit Role Check . . . . . .
Instrumented Semantics . . . . . . . .

6 Intraprocedural Role Analysis
6.1 Abstraction Relation . . . . .
6.2 Transfer Functions . . . . . .
6.2.1 Expansion . . . . . . .
6.2.2 Contraction . . . . . .
6.2.3 Symbolic Execution .
6.2.4 Node Check . . . . . .

1

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

.
.
.
.
.
.

Introduction

Types capture important properties of the objects that programs manipulate, increasing both the safety and readability
of the program. Traditional type systems capture properties
(such as the format of data items stored in the fields of the
object) that are invariant over the lifetime of the object. But
in many cases, properties that do change are as important

as properties that do not. Recognizing the benefit of capturing these changes, researchers have developed systems in
which the type of the object changes as the values stored in
its fields change or as the program invokes operations on the
object [44, 43, 10, 47, 48, 4, 20, 13]. These systems integrate
the concept of changing object states into the type system.
The fundamental idea in this paper is that the state of
each object also depends on the data structures in which it
participates. Our type system therefore captures the referencing relationships that determine this data structure participation. As objects move between data structures, their
types change to reflect their changing relationships with
other objects. Our system uses roles to formalize the concept of a type that depends on the referencing relationships.
Each role declaration provides complete aliasing information
for each object that plays that role—in addition to specifying roles for the fields of the object, the role declaration also
identifies the complete set of references in the heap that refer
to the object. In this way roles generalize linear type systems [45, 2, 30] by allowing multiple aliases to be statically
tracked, and extend alias types [42, 46] with the ability to
specify roles of objects that are the source of aliases.
This approach attacks a key difficulty associated with
state-based type systems: the need to ensure that any state
change performed using one alias is correctly reflected in the
declared types of the other aliases. Because each object’s
role identifies all of its heap aliases, the analysis can verify
the correctness of the role information at all remaining or
new heap aliases after an operation changes the referencing
relationships.
Roles capture important object and data structure properties, improving both the safety and transparency of the
program. For example, roles allow the programmer to express data structure consistency properties (with the properties verified by the role analysis), to improve the precision of
procedure interface specifications (by allowing the programmer to specify the role of each parameter), to express precise
referencing and interaction behaviors between objects (by
specifying verified roles for object fields and aliases), and to
express constraints on the coordinated movements of objects
between data structures (by using the aliasing information in
role definitions to identify legal data structure membership
combinations). Roles may also aid program optimization by
providing precise aliasing information.
This paper makes the following contributions:
• Role Concept: The concept that the state of an object depends on its referencing relationships; specifically, that objects with different heap aliases should be
regarded as having different states.
• Role Definition Language: It presents a language
for defining roles. The programmer can use this language to express data structure invariants and properties such as data structure participation.
• Programming Model: It presents a set of role consistency rules. These rules give a programming model
for changing the role of an object and the circumstances
under which roles can be temporarily violated.
• Procedure Interface Specification Language: It
presents a language for specifying the initial context
and effects of each procedure. The effects summarize

next
LiveHeader
next

next

DeadProc

proc

next

null

next

LiveList
proc

left

right

prev
RunningProc
next

prev
prev

SleepingProc
left
next

RunningHeader
next

right
root
SleepingTree

prev

Figure 1: Role Reference Diagram for Scheduler
the actions of the procedure in terms of the references
it changes and the regions of the heap that it affects.
• Role Analysis Algorithm: It presents an algorithm
for verifying that the program respects the constraints
given by a set of role definitions and procedure specifications. The algorithm uses a data-flow analysis to
infer intermediate referencing relationships between objects, allowing the programmer to focus on role changes
and procedure interfaces.

2

Example

Figure 1 presents a role reference diagram for a process
scheduler. Each box in the diagram denotes a disjoint set of
objects of a given role. The labelled arrows between boxes
indicate possible references between the objects in each set.
As the diagram indicates, the scheduler maintains a list of
live processes. A live process can be either running or sleeping. The running processes form a doubly-linked list, while
sleeping processes form a binary tree. Both kinds of processes have proc references from the live list nodes LiveList.
Header objects RunningHeader and SleepingTree simplify
operations on the data structures that store the process objects.
As Figure 1 shows, data structure participation determines the conceptual state of each object. In our example, processes that participate in the sleeping process tree
data structure are classified as sleeping processes, while processes that participate in the running process list data structure are classified as running processes. Moreover, movements between data structures correspond to conceptual
state changes—when a process stops sleeping and starts running, it moves from the sleeping process tree to the running
process list.

2.1

Role Definitions

Figure 2 presents the role definitions for the objects in our
example.1 Each role definition specifies the constraints that
an object must satisfy to play the role. Field constraints
1
In general, each role definition would specify the static
class of objects that can play that role. To simplify the

specify the roles of the objects to which the fields refer, while
slot constraints identify the number and kind of aliases of the
object.
role LiveHeader {
fields next : LiveList | null;
}
role LiveList {
fields next : LiveList | null,
proc : RunningProc | SleepingProc;
slots LiveList.next | LiveHeader.next;
acyclic next;
}
role RunningHeader {
fields next : RunningProc | RunningHeader,
prev : RunningProc | RunningHeader;
slots RunningHeader.next | RunningProc.next,
RunningHeader.prev | RunningProc.prev;
identities next.prev, prev.next;
}
role RunningProc {
fields next : RunningProc | RunningHeader,
prev : RunningProc | RunningHeader;
slots RunningHeader.next | RunningProc.next,
RunningHeader.prev | RunningProc.prev,
LiveList.proc;
identities next.prev, prev.next;
}
role SleepingTree {
fields root : SleepingProc | null,
acyclic left, right;
}
role SleepingProc {
fields left : SleepingProc | null,
right : SleepingProc | null;
slots SleepingProc.left | SleepingProc.right |
SleepingTree.root;
LiveList.proc;
acyclic left, right;
}
role DeadProc { }
Figure 2: Role Definitions for a Scheduler
Role definitions may also contain two additional kinds of
constraints: identity constraints, which specify paths that
lead back to the object, and acyclicity constraints, which
specify paths with no cycles. In our example, the identity
constraint next.prev in the RunningProc role specifies the
cyclic doubly-linked list constraint that following the next,
then prev fields always leads back to the initial object. The
acyclic constraint left, right in the SleepingProc role
specifies that there are no cycles in the heap involving only
left and right edges. On the other hand, the list of running processes must be cyclic because its nodes can never
point to null.
The slot constraints specify the complete set of heap
aliases for the object. In our example, this implies that no
process can be simultaneously running and sleeping.
presentation, we assume that all objects are instances of a
single class with a set of fields F .

In general, roles can capture data structure consistency
properties such as disjointness and can prevent representation exposure [8]. As a data structure description language,
roles can naturally specify trees with additional pointers.
Roles can also approximate non-tree data structures like
sparse matrices. Because most role constraints are local,
it is possible to inductively infer them from data structure
instances.

2.2

Roles and Procedure Interfaces

Procedures specify the initial and final roles of their parameters. The suspend procedure in Figure 3, for example, takes
two parameters: an object with role RunningProc p, and
the SleepingTree s. The procedure changes the role of the
object referenced by p to SleepingProc whereas the object
referenced by s retains its original role. To perform the role
change, the procedure removes p from its RunningList data
structure and inserts it into the SleepingTree data structure s. If the procedure fails to perform the insertions or
deletions correctly, for instance by leaving an object in both
structures, the role analysis will report an error.
procedure suspend(p : RunningProc ->> SleepingProc,
s : SleepingTree)
local pp, pn, r;
{
pp = p.prev;
pn = p.next;
r = s.root;
p.prev = null; p.next = null;
pp.next = pn; pn.prev = pp;
s.root = p;
p.left = r;
setRole(p : SleepingProc);
}
Figure 3: Suspend Procedure

3

Abstract Syntax and Semantics of Roles

In this section, we precisely define what it means for a given
heap to satisfy a set of role definitions. In subsequent sections we will use this definition as a starting point for a
programming model and role analysis.

3.1

Heap Representation

We represent a concrete program heap as a finite directed
graph Hc with nodes(Hc ) representing objects of the heap
and labelled edges representing heap references. A graph
edge ho1 , f, o2 i ∈ Hc denotes a reference with field name f
from object o1 to object o2 . To simplify the presentation, we
fix a global set of fields F and assume that all objects have
all fields in F . We do not consider subtyping or dynamic
dispatch in this paper.

3.2

Role Representation

Let R denote the set of roles used in role definitions, nullR be
a special symbol always denoting a null object nullc , and let

R0 = R ∪ {nullR }. We represent each role as the conjunction
of the following four kinds of constraints:
• Fields: For every field name f ∈ F we introduce a
function fieldf : R → 2R0 denoting the set of roles
that objects of role r ∈ R can reference through field
f . A field f of role r can be null if and only if
nullR ∈ fieldf (r). The explicit use of nullR and the possibility to specify a set of alternative roles for every field
allows roles to express both may and must referencing
relationships.
• Slots: Every role r has slotno(r) slots. A slot slotk (r) of
role r ∈ R is a subset of R×F . Let o be an object of role
r and o′ an object of role r ′ . A reference ho′ , f, oi ∈ Hc
can fill a slot k of object o if and only if hr ′ , f i ∈ slotk (r).
An object with role r must have each of its slots filled
by exactly one reference.
• Identities: Every role r ∈ R has a set of identities(r) ⊆
F × F . Identities are pairs of fields hf, gi such that
following reference f on object o and then returning on
reference g leads back to o.
• Acyclicities: Every role r ∈ R has a set acyclic(r) ⊆ F
of fields along which cycles are forbidden.

3.3

Role Semantics

We define the semantics of roles as a conjunction of invariants associated with role definitions. A concrete role assignment is a map ρc : nodes(Hc ) → R0 such that ρc (nullc ) =
nullR .
Definition 1 Given a set of role definitions, we say that
heap Hc is role consistent iff there exists a role assignment
ρc : nodes(Hc ) → R0 such that for every o ∈ nodes(Hc ) the
predicate locallyConsistent(o, Hc , ρc ) is satisfied. We call any
such role assignment ρc a valid role assignment.
The predicate locallyConsistent(o, Hc , ρc ) formalizes the constraints associated with role definitions.
Definition 2 locallyConsistent(o, Hc , ρc ) iff all of the following conditions are met. Let r = ρc (o).
1) For every field f ∈ F and ho, f, o′ i ∈ Hc , ρc (o′ ) ∈
fieldf (r).
2) Let {ho1 , f1 i, . . . , hok , fk i} = {ho′ , f i | ho′ , f, oi ∈ Hc }
be the set of all aliases of object o. Then k =
slotno(r) and there exists some permutation p of the
set {1, . . . , k} such that hρc (oi ), fi i ∈ slotpi (r) for all i.
3) If ho, f, o′ i ∈ Hc , ho′ , g, o′′ i ∈ Hc , and
hf, gi ∈ identities(r), then o = o′′ .
4) It is not the case that graph Hc contains a cycle
o1 , f1 , . . . , os , fs , o1 where o1 = o and
f1 , . . . , fs ∈ acyclic(r)
Note that a role consistent heap may have multiple valid
role assignments ρc . However, in each of these role assignments, every object o is assigned exactly one role ρc (o).
The existence of a role assignment ρc with the property
ρc (o1 ) 6= ρc (o2 ) thus implies o1 6= o2 . This is just one of
the ways in which roles make aliasing more predictable.

4

Role Properties

Roles capture important properties of the objects and provide useful information about how the actions of the program
affect those properties.
• Consistency Properties: Roles can ensure that the
program respects application-level data structure consistency properties. The roles in our process scheduler,
for example, ensure that a process cannot be simultaneously sleeping and running.
• Interface Changes: In many cases, the interface of an
object changes as its referencing relationships change.
In our process scheduler, for example, only running processes can be suspended. Because procedures declare
the roles of their parameters, the role system can ensure that the program uses objects correctly even as the
object’s interface changes.
• Multiple Uses: Code factoring minimizes code duplication by producing general-purpose classes (such as
the Java Vector and Hashtable classes) that can be
used in a variety of contexts. But this practice obscures the different purposes that different instances of
these classes serve in the computation. Because each instance’s purpose is usually reflected in its relationships
with other objects, roles can often recapture these distinctions.
• Correlated Relationships: In many cases, groups
of objects cooperate to implement a piece of functionality. Standard type declarations provide some information about these collaborations by identifying the
points-to relationships between related objects at the
granularity of classes. But roles can capture a much
more precise notion of cooperation, because they track
correlated state changes of related objects.
Programmers can use roles for specifying the membership
of objects in data structures and the structural invariants
of data structures. In both cases, the slot constraints are
essential.
When used to describe membership of an object in a data
structure, slots specify the source of the alias from a data
structure node that stores the object. By assigning different
sets of roles to data structures used at different program
points, it is possible to distinguish nodes stored in different
data structure instances. As an object moves between data
structures, the role of the object changes appropriately to
reflect the new source of the alias.
When describing nodes of data structures, slot constraints
specify the aliasing constraints of nodes; this is enough to
precisely describe a variety of data structures and approximate many others. Property 16 below shows how to identify
trees in role definitions even if tree nodes have additional
aliases from other sets of nodes. It is also possible to define
nodes which make up a compound data structure linked via
disjoint sets of fields, such as threaded trees, sparse matrices
and skip lists.
Example 3 The following role definitions specify a sparse
matrix of width and height at least 3. These definitions can
be easily constructed from a sketch of a sparse matrix, as in
Figure 4.

two

r

r

1

2
d

r

r

4

5

d

r
5

d

d

r

one

one

one

one

Figure 5: Sketch of a Two-Level Skip List

6

}

9

Example 4 We next give role definitions for a two-level
skip list [36] sketched in Figure 5.

d

r
8

one

null

2

d

r
5

d

6

d

r
4

one

2

1

r

5

d

2
1

d

two

two

SL

3

2

d

d

7

r

r
8

Figure 4: Roles of Nodes of a Sparse Matrix

role A1 {
fields right : A2, down : A4;
acyclic right, down;
}
role A2 {
fields right : A2 | A3, down : A5;
slots A1.right | A2.right;
acyclic right, down;
}
role A3 {
fields down : A6;
slots A2.right;
acyclic right, down;
}
role A4 {
fields right : A5, down : A4 | A7;
slots A1.down | A4.down;
acyclic right, down;
}
role A5 {
fields right : A5 | A6, down : A5 | A8;
slots A4.right | A5.right, A2.down | A5.down;
acyclic right, down;
}
role A6 {
fields down : A6 | A9;
slots A5.right, A3.down | A6.down;
acyclic right, down;
}
role A7 {
fields right : A8;
slots A4.down;
acyclic right, down;
}
role A8 {
fields right : A8 | A9;
slots A7.right | A8.right, A5.down;
acyclic right, down;
}
role A9 {
slots A8.right, A6.down;
acyclic right, down;

role SkipList {
fields one : OneNode | TwoNode | null;
two : TwoNode | null;
}
role OneNode {
fields one : OneNode | TwoNode | null;
two : null;
slots OneNode.one | TwoNode.one | SkipList.one;
acyclic one, two;
}
role TwoNode {
fields one : OneNode | TwoNode | null;
two : TwoNode | null;
slots OneNode.one | TwoNode.one | SkipList.one,
TwoNode.two | SkipList.two;
acyclic one, two;
}

4.1

Formal Properties of Roles

In this section we identify some of the invariants expressible
using sets of mutually recursive role definitions. A further
study of role properties can be found in [31].
The following properties show some of the ways role specifications make object aliasing more predictable. They are
an immediate consequence of the semantics of roles.
Property 5 (Role Disjointness)
If there exists a valid role assignment ρc for Hc such that
ρ(o1 ) 6= ρ(o2 ), then o1 6= o2 .
The previous property gives a simple criterion for showing
that objects o1 and o2 are unaliased: find a valid role assignment which assigns different roles to o1 and o2 . This
use of roles generalizes the use of static types for pointer
analysis [12]. Since roles create a finer partition of objects
than a typical static type system, their potential for proving
absence of aliasing is even larger.
Property 6 (Disjointness Propagation)
If ho1 , f, o2 i, ho3 , g, o4 i ∈ Hc , o1 6= o3 , and there exists a valid
role assignment ρc for Hc such that ρc (o2 ) = ρc (o4 ) = r but
fieldf (r) ∩ fieldg (r) = ∅, then o2 6= o4 .
Property 7 (Generalized Uniqueness)
If ho1 , f, o2 i, ho3 , g, o4 i ∈ Hc , o1 6= o3 , and there exists a
role assignment ρc such that ρc (o2 ) = ρc (o4 ) = r, but there
are no indices i 6= j such that hρc (o1 ), f i ∈ sloti (r) and
hρc (o2 ), gi ∈ slotj (r) then o2 6= o4 .

A special case of Property 7 occurs when slotno(r) = 1; this
constrains all references to objects of role r to be unique.
Role definitions induce a role reference diagram RRD
which captures some, but not all, role constraints.

Let ρc be a valid role assignment for Hc . Then every path in
Hc starting from an object o1 with role ρc (o1 ) ∈ RINTER and
containing only edges labelled with F0 is a prefix of a path
that terminates at some object o2 with ρc (o2 ) ∈ RFINAL .

Definition 8 (Role Reference Diagram)
Given a set of definitions of roles R, a role reference diagram
RRD is is a directed graph with nodes R0 and labelled edges
defined by

Property 13 (Upstream Path Termination)
Assume that for some set of fields F0 ⊆ F there are sets of
nodes RINTER ⊆ R, RINIT ⊆ R0 of the role reference diagram
RRD such that for every node r ∈ RINTER :

RRD = {hr, f, r ′ i | r ′ ∈ fieldf (r) and ∃i hr, f i ∈ sloti (r ′ )}
∪ {hr, f, nullR i | nullR ∈ fieldf (r)}
Each role reference diagram is a refinement of the corresponding class diagram in a statically typed language, because it partitions classes into multiple roles according to
their referencing relationships. The sets ρ−1
c (r) of objects
with role r change during program execution, reflecting the
changing referencing relationships of objects.
Role definitions give more information than a role reference diagram. Slot constraints specify not only that objects
of role r1 can reference objects of role r2 along field f , but
also give cardinalities on the number of references from other
objects. In addition, role definitions include identity and
acyclicity constraints, which are not present in role reference diagrams.
Property 9 Let ρc be any valid role assignment. Define
G = {hρc (o1 ), f, ρc (o2 )i | ho1 , f, o2 i ∈ Hc }
Then G is a subgraph of RRD.
It follows from Property 9 that roles give an approximation
of may-reachability among heap objects.
Property 10 (May Reachability)
If there is a valid role assignment ρc : nodes(Hc ) → R0 such
that ρc (o1 ) 6= ρc (o2 ) where o1 , o2 ∈ nodes(Hc ) and there is
no path from ρc (o1 ) to ρc (o2 ) in the role reference diagram
RRD, then there is no path from o1 to o2 in Hc .
The next property shows the advantage of explicitly specifying null references in role definitions. While the ability to
specify acyclicity is provided by the acyclic constraint, it
is also possible to indirectly specify must-cyclicity.
Property 11 (Must Cyclicity)
Let F0 ⊆ F and RCYC ⊆ R be a set of nodes in the role reference diagram RRD such that for every node r ∈ RCYC , if
hr, f, r ′ i ∈ RRD then r ′ ∈ RCYC . If ρc is a valid role assignment for Hc , then every object o1 ∈ Hc with ρc (o1 ) ∈ RCYC
is a member of a cycle in Hc with edges from F0 .
The following property shows that roles can specify a form
of must-reachability among the sets of objects with the same
role.
Property 12 (Downstream Path Termination)
Assume that for some set of fields F0 ⊆ F there are sets of
nodes RINTER ⊆ R, RFINAL ⊆ R0 of the role reference diagram
RRD such that for every node r ∈ RINTER :
1. F0 ⊆ acyclic(r)
2. if hr, f, r ′ i ∈ RRD for f ∈ F0 , then r ′ ∈ RINTER ∪ RFINAL

1. F0 ⊆ acyclic(r)
2. if hr ′ , f, ri ∈ RRD for f ∈ F0 , then r ′ ∈ RINTER ∪ RINIT
Let ρc be a valid role assignment for Hc . Then every path
in Hc terminating at an object o2 with ρc (o2 ) ∈ RINTER and
containing only edges labelled with F0 is a suffix of a path
which started at some object o1 , where ρc (o1 ) ∈ RINIT .
The next two properties guarantee reachability properties
by which there must exist at least one path in the heap,
rather than stating properties of all paths as in Properties
12 and 13.
Property 14 (Downstream Must Reachability)
Assume that for some set of fields F0 ⊆ F there are sets of
roles RINTER ⊆ R, RFINAL ⊂ R0 of the role reference diagram
RRD such that for every node r ∈ RINTER :
1. F0 ⊆ acyclic(r)
2. there exists f ∈ F0 such that fieldf (r) ⊆ RINTER ∪ RFINAL
Let ρc be a valid role assignment for Hc . Then for every
object o1 with ρc (o1 ) ∈ RINTER there is a path in Hc with edges
from F0 from o1 to some object o2 where ρc (o2 ) ∈ RFINAL .
Property 15 (Upstream Must Reachability)
Assume that for some set of fields F0 ⊆ F there are sets
of nodes RINTER ⊆ R, RINIT ⊆ R of the role reference diagram
RRD such that for every node r ∈ RINTER :
1. F0 ⊆ acyclic(r)
2. there exists k such that slotk (r) ⊆ (RINTER ∪ RINIT ) × F
Let ρc be a valid role assignment for Hc . Then for every
object o2 with ρc (o2 ) ∈ RINTER there is a path in Hc from
some object o1 with ρc (o1 ) ∈ RINIT to the object o2 .
Trees are a class of data structures especially suited for
static analysis. Roles can express graphs that are not trees,
but it is useful to identify trees as certain sets of mutually
recursive role definitions.
Property 16 (Treeness)
Let RTREE ⊆ R be a set of roles and F0 ⊆ F set of fields such
that for every r ∈ RTREE
1. F0 ⊆ acyclic(r)
2. |{i | sloti (r) ∩ (RTREE × F0 ) 6= ∅}| ≤ 1
Let ρc be a valid role assignment for Hc and S ⊆
{hn1 , f, n2 i | hn1 , f, n2 i ∈ Hc , ρ(n1 ), ρ(n2 ) ∈ RTREE , f ∈ F0 }.
Then S is a set of trees.

5

A Programming Model

In this section we define what it means for an execution of
a program to respect the role constraints. This definition
is complicated by the need to allow the program to temporarily violate the role constraints during data structure
manipulations. Our approach is to let the program violate
the constraints for objects referenced by local variables or
parameters, but require all other objects to satisfy the constraints.
We first present a simple imperative language with dynamic object allocation and give its operational semantics.
We then specify additional statement preconditions that enforce the role consistency requirements.

5.1

A Simple Imperative Language

Our core language contains, as basic statements, Load
(x=y.f), Store (x.f=y), Copy (x=y), and New (x=new). All
variables are references to objects in the global heap and all
assignments are reference assignments. We use an elementary test statement combined with nondeterministic choice
and iteration to express if and while statement, using the
usual translation [22, 1]. We represent the control flow of
programs using control-flow graphs.
A program is a collection of procedures proc ∈ Proc. Procedures change the global heap but do not return values.
Every procedure proc has a list of parameters param(proc) =
{parami (proc)}i and a list of local variables local(proc). We
use var(proc) to denote param(proc) ∪ local(proc). A procedure definition specifies the initial role preRk (proc) and the
final role postRk (proc) for every parameter paramk (proc). We
use procj for indices j ∈ N to denote activation records of
procedure proc. We further assume that there are no modifications of parameter variables so every parameter references
the same object throughout the lifetime of procedure activation.
Example 17 The following kill procedure removes a process from both the doubly linked list of running processes
and the list of all active processes. This is indicated by the
transition from RunningProc to DeadProc.
procedure kill(p : RunningProc ->> DeadProc,
l : LiveHeader)
local prev, current, cp, nxt, lp, ln;
{
// find ’p’ in ’l’
prev = l; current = l.next;
cp = current.proc;
while (cp != p) {
prev = current;
current = current.next;
cp = current.proc;
}
// remove ’current’ and ’p’ from active list
nxt = current.next;
prev.next = nxt; current.
current.proc = null;
setRole(current : IsolatedCell);
// remove ’p’ from running list
lp = p.prev;
ln = p.next;

p.prev = null; p.next = null;
lp.next = ln;
ln.prev = lp;
setRole(p : DeadProc);
}

5.2

Operational Semantics

In this section we give the operational semantics for our language. We focus on the first three columns in Figures 6 and
7; the safety conditions in the fourth column are detailed in
Section 5.4.
Figure 6 gives the small-step operational semantics for
the basic statements. We use A ⊎ B to denote the union
A ∪ B where the sets A and B are disjoint. The program
state consists of the stack s and the concrete heap Hc . The
stack s is a sequence of pairs p@proci ∈ ×(Proc × N ), where
p ∈ NCFG (proc) is a program point, and proci ∈ Proc × N
is an activation record of procedure proc. Program points
p ∈ NCFG (proc) are nodes of the control-flow graphs. There
is one control-flow graph for every procedure proc. An edge
of the control-flow graph hp, p′ i ∈ ECFG (proc) indicates that
control may transfer from point p to point p′ . We write
p : stat to state that program point p contains a statement
stat. The control flow graph of each procedure contains special program points entry and exit indicating procedure entry and exit, with no statements associated with them. We
assume that all conditions are of the form x==y or !(x==y)
where x and y are either variables or a special constant null
which always points to the nullc object.
The concrete heap is either an error heap errorc or a nonerror heap. A non-error heap Hc ⊆ N ×F ×N ∪((Proc×N )×
V × N ) is a directed graph with labelled edges, where nodes
represent objects and procedure activation records, whereas
edges represent heap references and local variables. An edge
ho1 , f, o2 i ∈ N × F × N denotes a reference from object o1
to object o2 via field f ∈ F . An edge hproci , x, oi ∈ Hc
means that local variable x in activation record proci points
to object o.
A load statement x=y.f makes the variable x point to
node of , which is referenced by the f field of object oy ,
which is in turn referenced by variable y. A store statement
x.f=y replaces the reference along field f in object ox by
a reference to object oy that is referenced by y. The copy
statement x=y copies a reference to object oy into variable
x. The statement x=new creates a new object on with all
fields initially referencing nullc , and makes x point to on .
The statement test(c) allows execution to proceed only if
condition c is satisfied.
Figure 7 describes the semantics of procedure calls. Procedure call pushes new activation record onto stack, inserts
it into the heap, and initializes the parameters. Procedure
entry initializes local variables. Procedure exit removes the
activation record from the heap and the stack.

5.3

Onstage and Offstage Objects

At every program point the set of all objects of heap Hc can
be partitioned into:

Statement

Transition

p : x=y.f

hp@proci ; s, Hc ⊎ {hproci , x, ox i}i −→
hp′ @proci ; s, Hc′ i

p : x.f=y

hp@proci ; s, Hc ⊎ {hox , f, of i}i −→
hp′ @proci ; s, Hc′ i

p : x=y

hp@proci ; s, Hc ⊎ {hproci , x, ox i}i −→
hp′ @proci ; s, Hc′ i

p : x=new

hp@proci ; s, Hc ⊎ {hproci , x, ox i}i −→
hp′ @proci ; s, Hc′ i

p : test(c)

hp@proci ; s, Hc i −→
hp′ @proci ; s, Hc i

Constraints
x, y ∈ local(proc),
hproci , y, oy i, hoy , f, of i ∈ Hc ,
hp, p′ i ∈ ECFG (proc),
Hc′ = Hc ⊎ {proci , x, of }
x, y ∈ local(proc),
hproci , x, ox i, hproci , y, oy i ∈ Hc ,
hp, p′ i ∈ ECFG (proc),
Hc′ = Hc ⊎ {hox , f, oy i}
x ∈ local(proc),
y ∈ var(proc),
hproci , y, oy i ∈ Hc ,
hp, p′ i ∈ ECFG (proc),
′
Hc = Hc ⊎ {hproci , x, oy i}
x ∈ local(proc),
on fresh,
hp, p′ i ∈ ECFG (proc),
Hc′ = Hc ⊎ {hproci , x, on i} ⊎ nulls,
nulls = {on } × F × {null}
satisfiedc (c, proci , Hc ),
hp, p′ i ∈ ECFG (proc)

Role Consistency
accessible(of , proci , Hc ),
con(Hc′ , offstage(Hc′ ))

of ∈ onstage(Hc , proci )
con(Hc′ , offstage(Hc′ ))

con(Hc′ , offstage(Hc′ ))

con(Hc′ , offstage(Hc′ ))

con(Hc , offstage(Hc ))

satisfiedc (x==y, proci , Hc ) iff {o | hproci , x, oi ∈ Hc } = {o | hproci , y, oi ∈ Hc }
satisfiedc (!(x==y), proci , Hc ) iff not satisfiedc (x==y, proci , Hc )
accessible(o, proci , Hc )

:=

(∃p ∈ param(proc) : hproci , p, oi ∈ Hc )
or not (∃proc′j ∃v ∈ var(proc′ ) : hproc′j , v, oi ∈ Hc )

Figure 6: Semantics of Basic Statements

Statement
entry :

p : proc′ (xk )k

exit :

Transition
hp@proci ; s, Hc i −→
hp′ @proci ; s, Hc ⊎ nullsi
hp@proci ; s, Hc i −→
hentry@proc′j ; p′ @proci ; s, Hc′ i

hp@proci ; s, Hc i −→
hs, Hc \ AFi

Constraints
nulls = {hproci , v, nullc i |
v ∈ local(proc),
hp, p′ i ∈ ECFG (proc)
j fresh in p@proci; s,
hp, p′ i ∈ ECFG (proc),
ok : hproci , xk , ok i ∈ Hc ,
Hc′ = Hc ⊎ {hproc′j , pk , ok i}k ,
∀k pk = paramk (proc′ )
AF = {hproci , v, ni |
hproci , v, ni ∈ Hc }

Role Consistency
con(Hc , offstage(Hc ))

conW(ra, Hc , S),
ra = {hok , preRk (proc′ )i}k ,
S = offstage(Hc ) ∪ {ok }k
conW(ra, Hc , S),
ra = {hparndk (proci ), postRk (proc)i}k ,
S = offstage(Hc ) ∪
{o | hproci , v, oi ∈ Hc }

parndk (proci ) = o where hproci , paramk (proc), oi ∈ Hc

Figure 7: Semantics of Procedure Call

1. onstage objects (onstage(Hc )) referenced by a local
variable or parameter of some activation frame;
onstage(Hc , proci ):={o | ∃x ∈ var(proc)
Shproci , x, oi ∈ Hc }
onstage(Hc ):=
onstage(Hc , proci )
proci
2. offstage objects (offstage(Hc )) unreferenced by local
or parameter variables.
offstage(Hc ) := nodes(Hc ) \ onstage(Hc )
Onstage objects need not have correct roles. Offstage objects
must have correct roles assuming some role assignment for
onstage objects; the exception is that acyclicity constraints
for offstage objects can be violated due to cycles that pass
through the onstage objects.
Definition 18 Given a set of role definitions and a set of
objects Sc ⊆ nodes(Sc ), we say that heap Hc is role consistent for Sc , and we write con(Hc , Sc ), iff there exists a
role assignment ρc : nodes(Hc ) → R0 such that the predicate locallyConsistent(o, Hc , ρc , Sc ) is satisfied for every object o ∈ Sc .
We define locallyConsistent(o, Hc , ρc , Sc ) to generalize the
locallyConsistent(o, Hc , ρc ) predicate, weakening the acyclicity condition.
Definition 19 locallyConsistent(o, Hc , ρc , Sc ) holds iff conditions 1), 2), and 3) of Definition 2 are satisfied and the
following condition holds:
4’) It is not the case that graph Hc contains a cycle
o1 , f1 , . . . , os , fs , o1 such that
o1 = o, f1 , . . . , fs ∈ acyclic(r), and
additionally o1 , . . . , os ∈ Sc .
Here Sc is the set of onstage objects that are not allowed
to create a cycle; objects in nodes(Hc ) \ Sc are exempt from
the acyclicity condition. The locallyConsistent(o, Hc , ρc , Sc )
and con(Hc , Sc ) predicates are monotonic in Sc , so a larger
Sc implies a stronger invariant. For Sc = nodes(Hc ), consistency for Sc is equivalent with heap consistency from Definition 1. Note that the role assignment ρc specifies roles even
for objects o ∈ nodes(Hc ) \ Sc . This is because the role of
o may influence the role consistency of objects in Sc which
are adjacent to o.
At procedure calls, the role declarations for parameters
restrict the set of potential role assignments. We therefore
generalize con(Hc , Sc ) to conW(ra, Hc , Sc ), which restricts
the set of role assignments ρc considered for heap consistency.
Definition 20 Given a set of role definitions, a heap Hc , a
set Sc ⊆ nodes(Hc ), and a partial role assignment ra ⊆ Sc →
R, we say that the heap Hc is consistent with ra for Sc , and
write conW(ra, Hc , Sc ), iff there exists a (total) role assignment ρc : nodes(Hc ) → R0 such that ra ⊆ ρc and for every
object o ∈ Sc the predicate locallyConsistent(o, Hc , ρc , Sc ) is
satisfied.

5.4

Role Consistency

We are now able to precisely state the role consistency requirements that must be satisfied for program execution.
The role consistency requirements are in the fourth row of
Figures 6 and 7. We assume the operational semantics is
extended with transitions leading to a program state with
heap errorc whenever role consistency is violated.

5.4.1 Offstage Consistency
At every program point, we require con(Hc , offstage(Hc )) to
be satisfied. This means that offstage objects have correct
roles, but onstage objects may have their role temporarily
violated.

5.4.2 Reference Removal Consistency
The Store statement x.f=y has the following safety precondition. When a reference hox , f, of i ∈ Hc for hprocj , x, ox i ∈
Hc , and hox , f, of i ∈ Hc is removed from the heap, both ox
and of must be referenced from the current procedure activation record. It is sufficient to verify this condition for
of , as ox is already onstage by definition. The reference removal consistency condition enables the completion of the
role change for of after the reference hox , f, of i is removed
and ensures that heap references are introduced and removed
only between onstage objects.

5.4.3 Procedure Call Consistency
Our programming model ensures role consistency across procedure calls using the following protocol.
A procedure call proc′ (x1 , ..., xp ) in Figure 7 requires the
role consistency precondition conW(ra, Hc , Sc ), where the
partial role assignment ra requires objects ok , corresponding
to parameters xk , to have roles preRk (proc′ ) expected by the
callee, and Sc = offstage(Hc )∪{ok }k for hprocj , xk , ok i ∈ Hc .
To ensure that the callee proc′j never observes incorrect
roles, we impose an accessibility condition for the callee’s
Load statements (see the fourth column of Figure 6). The
accessibility condition prohibits access to any object o referenced by some local variable of a stack frame other than
proc′j , unless o is referenced by some parameter of proc′j .
Provided that this condition is not violated, the callee proc′j
only accesses objects with correct roles, even though objects
that it does not access may have incorrect roles. In Section 7
we show how the role analysis ensures that the accessibility
condition is never violated.
At the procedure exit point (Figure 7), we require correct roles for all objects referenced by the current activation
frame proc′j . This implies that heap operations performed
by proc′j preserve heap consistency for all objects accessed
by proc′j .

5.4.4 Explicit Role Check
The programmer can specify a stronger invariant at any program point using statement roleCheck(x1 , . . . , xp , ra). As
Figure 8 indicates, roleCheck requires the conW(ra, Hc , Sc )
predicate to be satisfied for the supplied partial role assignment ra where Sc = offstage(Hc ) ∪ {ok }k for objects ok referenced by given local variables xk .

Statement

Transition

p : roleCheck(x1 , . . . , xn , ra)

Constraints

hp@proci ; s, Hc i −→
hp′ @proci ; s, Hc i

hp, p′ i ∈ ECFG

S

Role Consistency
conW(ra, Hc , S),
= offstage(Hc ) ∪
{o | hproci , xk , oi ∈ Hc }

Figure 8: Operational Semantics of Explicit Role Check

5.5

Instrumented Semantics

We expect the programmer to have a specific role assignment
in mind when writing the program, with this role assignment
changing as the statements of the program change the referencing relationships. So when the programmer wishes to
change the role of an object, he or she writes a program that
brings the object onstage, changes its referencing relationships so that it plays a new role, then puts it offstage in its
new role. The roles of other objects do not change.2
To support these programmer expectations, we introduce
an augmented programming model in which the role assignment ρc is conceptually part of the program’s state. The
role assignment changes only if the programmer changes it
explicitly using the setRole statement. The augmented programming model has an underlying instrumented semantics
as opposed to the original semantics.
Example 21 The original semantics allows asserting different roles at different program points even if the structure of
the heap was not changed, as in the following procedure foo.
role A1 { fields f : B1; }
role B1 { slots A1.f; }
role A2 { fields f : B2; }
role B2 { slots A2.f; }
procedure foo()
var x, y;
{
x = new; y = new;
x.f = y;
roleCheck(x,y, x:A1,y:B1);
roleCheck(x,y, x:A2,y:B2);
}
Both role checks would succeed since each of the specified partial role assignments can be extended to a
valid role assignment. On the other hand, the check
roleCheck(x,y, x:A1,y:B2) would fail.
The procedure foo in the instrumented semantics can be
written as folllows.
procedure foo()
var x, y;
{
x = new; y = new;
x.f = y;
setRole(x:A1); setRole(y:B1);
roleCheck(x,y, x:A1,y:B1);
2

An extension to the programming model supports cascading role changes in which a single role change propagates
through the heap changing the roles of offstage objects, see
Section 8.2.

setRole(x:A2); setRole(y:B2);
roleCheck(x,y, x:A2,y:B2);
}
The setRole statement makes the role change of object explicit.
The instrumented semantics extends the concrete heap
Hc with a role assignment ρc . Figure 9 outlines the changes
in instrumented semantics with respect to the original semantics. We introduce a new statement setRole(x:r),
which modifies a role assignment ρc , giving ρc [ox 7→ r],
where ox is the object referenced by x. All statements
other than setRole preserve the current role assignment.
For every consistency condition conW(ra, Hc , Sc ) in the original semantics, the instrumented semantics uses the corresponding condition conW(ρc ∪ ra, Hc , Sc ) and fails if ρc
is not an extension of ra. Here we consider con(Hc , S)
to be a shorthand for conW(∅, Hc , S). For example, the
new role consistency condition for the Copy statement
x=y is conW(ρc , Hc , offstage(Hc )). The New statement assigns an identifier unknown to the newly created object on .
By definition, a node with unknown does not satisfy the
locallyConsistent predicate. This means that setRole must
be used to set a a valid role of on before on moves offstage.
By introducing an instrumented semantics we are not suggesting an implementation that explicitly stores roles of objects at run-time. We instead use the instrumented semantics as the basis of our role analysis and ensure that all role
checks can be statically removed. Because the instrumented
semantics is more restrictive than the original semantics, our
role analysis is a conservative approximation of both the instrumented semantics and the original semantics.

6

Intraprocedural Role Analysis

This section presents an intraprocedural role analysis algorithm. The goal of the role analysis is to statically verify
the role consistency requirements described in the previous
section.
The key observation behind our analysis algorithm is that
we can incrementally verify role consistency of the concrete
heap Hc by ensuring role consistency for every node when it
goes offstage. This allows us to represent the statically unbounded offstage portion of the heap using summary nodes
with “may” references. In contrast, we use a “must” interpretation for references from and to onstage nodes. The
exact representation of onstage nodes allows the analysis to
verify role consistency in the presence of temporary violations of role constraints.
Our analysis representation is a graph in which nodes represent objects and edges represent references between ob-

Statement

p : x=new

p:
setRole(x:r)

p : stat

Transition

hp@proci ; s, Hc ⊎ {hproci , x, ox i}, ρc i −→
hp′ @proci ; s, Hc′ , ρ′c i

hp@proci ; s, Hc , ρc i −→
hp′ @proci ; s, Hc , ρ′c i
hs, Hc , ρc i −→
hs′ , Hc′ , ρc i

Constraints
x ∈ local(proc),
on fresh,
hp, p′ i ∈ ECFG (proc),
Hc′ = Hc
⊎{hproci , x, on i}
⊎{on } × F × {null},
ρ′c = ρc [on 7→ unknown]
x ∈ local(proci ),
hproci , x, ox i ∈ Hc ,
ρ′c = ρc [ox 7→ r],
hp, p′ i ∈ ECFG
hs, Hc i −→hs

′

, Hc′ i

Role Consistency

conW(ρ′c , Hc′ , offstage(Hc′ ))

conW(ρ′c , Hc , offstage(Hc ))
P ∧ conW(ρc ∪ ra, Hc′′ , S)
for every original condition
P ∧ conW(ra, Hc′′ , S)

Figure 9: Instrumented Semantics
jects. There are two kinds of nodes: onstage nodes represent onstage objects, with each onstage node representing
one onstage object; and offstage nodes, with each offstage
node corresponding to a set of objects that play that role.
To increase the precision of the analysis, the algorithm occasionally generates multiple offstage nodes that represent
disjoint sets of objects playing the same role. Distinct offstage objects with the same role r represent disjoint sets of
objects of role r with different reachability properties from
onstage nodes.
We frame role analysis as a data-flow analysis operating
on a distributive lattice P(RoleGraphs) of sets of role graphs
with set union ∪ as the join operator. In this section we
present an algorithm for intraprocedural analysis. We use
procc to denote the topmost activation record in a concrete
heap Hc . In Section 7 we generalize the algorithm to the
compositional interprocedural analysis.

6.1

Abstraction Relation

Every data-flow fact G ⊆ RoleGraphs is a set of role graphs
G ∈ G. Every role graph G ∈ RoleGraphs is either a bottom role graph ⊥G representing the set of all concrete heaps
(including errorc ), or a tuple G = hH, ρ, Ki representing nonerror concrete heaps, where
• H ⊆ N × F × N is the abstract heap with nodes N
representing objects and fields F . The abstract heap
H represents heap references hn1 , f, n2 i and variables of
the currently analyzed procedure hproc, x, ni where x ∈
local(proc). Null references are represented as references
to abstract node null. We define abstract onstage nodes
onstage(H) = {n | hproc, x, ni ∈ H, x ∈ local(proc) ∪
param(proc)} and abstract offstage nodes offstage(H) =
nodes(H) \ onstage(H) \ {proc, null}.
• ρ : nodes(H) → R0 is an abstract role assignment,
ρ(null) = nullR ;
• K : nodes(H) → {i, s} indicates the kind of each node;
when K(n) = i, then n is an individual node representing at most one object, and when K(n) = s, n is a
summary node representing zero or more objects. We

require K(proc) = K(null) = i, and require all onstage
nodes to be individual, K[onstage(H)] ⊆ {i}.
The abstraction relation α relates a pair hHc , ρc i of concrete heap and concrete role assignment with an abstract
role graph G.
Definition 22 We say that an abstract role graph G represents concrete heap Hc with role assignment ρc and write
hHc , ρc i α G, iff G = ⊥G or: Hc 6= errorc , G = hH, ρ, Ki,
and there exists a function h : nodes(Hc ) → nodes(H) such
that
1) Hc is role consistent: conW(ρc , Hc , offstage(Hc )),
2) identity constraints of onstage nodes with offstage nodes
hold: if ho1 , f, o2 i ∈ Hc and ho2 , g, o3 i ∈ Hc for o1 ∈
onstage(Hc ), o2 ∈ offstage(Hc ), and
hf, gi ∈ identities(ρc (o1 )), then o3 = o1 ;
3) h is a graph homomorphism: if ho1 , f, o2 i ∈ Hc then
hh(o1 ), f, h(o2 )i ∈ H;
4) an individual node represents at most one concrete object: K(n) = i implies |h−1 (n)| ≤ 1;
5) h is bijection on edges which originate or terminate at
onstage nodes: if hn1 , f, n2 i ∈ H and n1 ∈ onstage(H)
or n2 ∈ onstage(H), then there exists exactly one
ho1 , f, o2 i ∈ Hc such that h(o1 ) = n1 and h(o2 ) = n2 ;
6) h(nullc ) = null and h(procc ) = proc;
7) the abstract role assignment ρ corresponds to the concrete role assignment: ρc (o) = ρ(h(o)) for every object
o ∈ nodes(Hc ).
Note that the error heap errorc can be represented only by
the bottom role graph ⊥G . The analysis uses ⊥G to indicate
a potential role error.
Condition 3) implies that role graph edges are a conservative approximation of concrete heap references. These edges
are in general “may” edges. Hence it is possible for an offstage node n that hn, f, n1 i, hn, f, n2 i ∈ H for n1 6= n2 . This
cannot happen when n ∈ onstage(H) because of 5). Another
consequence of 5) is that an edge in H from an onstage node

✲ hHc′ , ρ′c i

hHc , ρc i

L

h

next

α

✠

LN

h

next

G1



❅ α
❅
❘
❅

α

❄
G2

st

=⇒

G3



G4

L
LN

h

next

next

proc

LN
prev

LN

h

proc

Figure 11: Simulation Relation Between Abstract and Concrete Execution

current

6.2

next

prev

next

current next
LN
LN

h

LN

h

next

next
LN
next

next

h

LN
next

next

LN

next
null
null

Figure 10: Abstraction Relation

n0 to a summary node ns implies that ns represents at least
one object. Condition 2) strengthens 1) by requiring certain
identity constraints for onstage nodes to hold, as explained
in Section 6.2.4.
Example 23 Consider the following role declaration for an
acyclic list.
role L { // List header
fields first : LN | null;
}
role LN { // List node
fields next : LN | null;
slots LN.next | L.first;
acyclic next;
}
Figure 10 shows a role graph and one of the concrete heaps
represented by the role graph via homomorphism h. There
are two local variables, prev and current, referencing distinct onstage objects. Onstage objects are isomorphic to
onstage nodes in the role graph. In contrast, there are two
objects mapped to each of the summary nodes with role LN
(shown as LN-labelled rectangles in Figure 10). Note that the
sets of objects mapped to these two summary nodes are disjoint. The first summary LN-node represents objects stored
in the list before the object referenced by prev. The second
summary LN-node represents objects stored in the list after
the object referenced by current.

Transfer Functions

The key complication in developing the transfer functions
for the role analysis is to accurately model the movement
of objects onstage and offstage. For example, a load statement x=y.f may cause the object referred to by y.f to move
onstage. In addition, if x was the only reference to an onstage object o before the statement executed, object o moves
offstage after the execution of the load statement, and thus
must satisfy the locallyConsistent predicate.
The analysis uses an expansion relation  to model the
movement of objects onstage and a contraction relation 
to model the movement of objects offstage. The expansion
relation uses the invariant that offstage nodes have correct
roles to generate possible aliasing relationships for the node
being pulled onstage. The contraction relation establishes
the role invariants for the node going offstage, allowing the
node to be merged into the other offstage nodes and represented more compactly.
We present our role analysis as an abstract execution rest
lation ❀. The abstract execution ensures that the abstraction relation α is a forward simulation relation [33] from
the space of concrete heaps with role assignments to the set
RoleGraphs. The simulation relation implies that the traces
of ❀ include the traces of the instrumented semantics −→.
To ensure that the program does not violate constraints associated with roles, it is thus sufficient to guarantee that ⊥G
is not reachable via ❀.
To prove that ⊥G is not reachable in the abstract execution, the analysis computes for every program point p a set
of role graphs G that conservatively approximates the possible program states at point p. The transfer function for a
st
statement st is an image [[st]](G) = {G′ | G ∈ G, G ❀ G′ }.
st

The analysis computes the relation ❀ in three steps:
1. ensure that the relevant nodes are instantiated using
expansion relation  (Section 6.2.1);
st

2. perform symbolic execution =⇒ of the statement st
(Section 6.2.3);
3. merge nodes if needed using contraction relation  to
keep the role graph bounded (Section 6.2.2).
Figure 11 shows how the abstraction relation α relates ,
st

=⇒, and  with the concrete execution −→ in instrumented
semantics. Assume that a concrete heap hHc , ρc i is represented by the role graph G1 . Then one of the role graphs G2
obtained after expansion remains an abstraction of hHc , ρc i.

Transition

Definition

x=y.f

′

hH, ρ, Ki ❀ G
x=y

ny ,f

′

hH, ρ, Ki  G1 =⇒ G2  G
n1

x=y

′

hH, ρ, Ki ❀ G
x=new

Conditions
nx

x=y.f

hproc, x, nx i, hproc, y, ny i ∈ H

′

hH, ρ, Ki =⇒ G1  G
x=new

′

hH, ρ, Ki ❀ G

n1

hproc, x, n1 i ∈ H
′

hH, ρ, Ki =⇒ G1  G

s

s

hH, ρ, Ki ❀ G′

hH, ρ, Ki =⇒ G′

hproc, x, n1 i ∈ H
s ∈ {x.f=y,
test(c),
setRole(x:r),
roleCheck(x1..p , ra)}

Figure 12: Abstract Execution ❀
st

The symbolic execution =⇒ followed by the contraction relation  corresponds to the instrumented operational semantics →.
Figure 12 shows rules for the abstract execution relation
st
❀. Only Load statement uses the expansion relation, because the other statements operate on objects that are already onstage. Load, Copy, and New statements may remove a local variable reference from an object, so they use
contraction relation to move the object offstage if needed.
For the rest of the statements, the abstract execution reduces to symbolic execution =⇒ described in Section 6.2.3.
st

Nondeterminism and Failure The ❀ relation is not a
function because the expansion relation  can generate a set
of role graphs from a single role graph. Also, there might be
st
no ❀ transitions originating from a given state G if the symbolic execution =⇒ produces no results. This corresponds
to a trace which cannot be extended further due to a test
statement which fails in state G. This is in contrast to a
transition from G to ⊥G which indicates a potential role consistency violation or a null pointer dereference. We assume
that =⇒ and  relations contain the transition h⊥G , ⊥G i
to propagate the error role graph. In most cases we do not
write the explicit transitions to error states.

6.2.1 Expansion
n,f

Figure 13 shows the expansion relation  . Given a role
graph hH, ρ, Ki expansion attempts to produce a set of role
graphs hH ′ , ρ′ , K ′ i in each of which hn, f, n0 i ∈ H ′ and
K(n0 ) = i. Expansion is used in abstract execution of the
Load statement. It first checks for null pointer dereference
and reports an error if the check fails. If hn, f, n′ i ∈ H and
K(n′ ) = i already hold, the expansion returns the original
state. Otherwise, hn, f, n′ i ∈ H with K(n′ ) = s. In that
case, the summary node n′ is first instantiated using instann0

n0

tiation relation ⇑ . Next, the split relation k is applied. Let
n′

ρ(n0 ) = r. The split relation ensures that n0 is not a member
of any cycle of offstage nodes which contains only edges in
acyclic(r). We explain instantiation and split in more detail
below.

generates the set of role graphs hH ′ , ρ′ , K ′ i such that each
concrete heap represented by hH, ρ, Ki is represented by one
of the graphs hH ′ , ρ′ , K ′ i. Each of the new role graphs contains a fresh individual node n0 that satisfies localCheck.
The edges of n0 are a subset of edges from and to n′ .
Let H0 be a subset of the references between n′ and onstage nodes, and let H1 be a subset of the references between
n′ and offstage nodes. References in H0 are moved from n′
to the new node n0 , because they represent at most one reference, while references in H1 are copied to n0 because they
may represent multiple concrete heap references. Moving a
reference is formalized via the swing operation in Figure 14.
The instantiation of a single graph can generate multiple
role graphs depending on the choice of H0′ and H1′ . The number of graphs generated is limited by the existing references
of node n′ and by the localCheck requirement for n0 . This is
where our role analysis takes advantage of constraints associated with role definitions to reduce the number of aliasing
possibilities that need to be considered.
Split The split relation is important for verifying operations on data structures such as skip lists and sparse matrices. It is also useful for improving the precision of the initial
set of role graphs on procedure entry (Section 7.2.1).
The goal of the split relation is to exploit the acyclicity
constraints associated with role definitions. After a node n0
is brought onstage, split represents the acyclicity condition
of ρ(n0 ) explicitly by eliminating impossible paths in the
role graph. It uses additional offstage nodes to encode the
reachability information implied by the acyclicity conditions.
This information can then be used even after the role of node
n0 changes. In particular, it allows the acyclicity condition
of n0 to be verified when n0 moves offstage.
Example 24 Consider a role graph for an acyclic list with
nodes LN and a header node L. The instantiated node n0 is
in the middle of the list. Figure 16 a) shows a role graph
with a single summary node representing all offstage LNnodes. Figure 16 b) shows the role graph after applying
the split relation. The resulting role graph contains two
LN summary nodes. The first LN summary node represents
objects definitely reachable from n0 along next edges; the
second summary NL node represents objects definitely not
reachable from n0 .

Figure 14 presents the instantiation rela-

Figure 15 shows the definition of the split operation on

tion. Given a role graph G = hH, ρ, Ki, instantiation ⇑

node n0 , denoted by k . Let G = hH, ρ, Ki be the initial

Instantiation

n0
n′

n0

Transition

Definition

Condition

n,f

hH, ρ, Ki  hH, ρ, Ki
n0

n,f

hH, ρ, Ki  G′

n0

hH, ρ, Ki ⇑ hH1 , ρ1 , K1 i k G′
n′

hn, f, n′ i ∈ H, n′ ∈ onstage(H)
hn, f, n′ i ∈ H, n′ ∈ offstage(H)
hn, f, n0 i ∈ H1

Figure 13: Expansion Relation

n0

hH, ρ, Ki ⇑ hH ′ , ρ′ , K ′ i
n′

swing(nold , nnew , H)

H ′ = H \ H0 ∪ H0′ ∪ H1′
n′ ∈
/ nodes(H ′ ), if K(n′ ) = i
′
ρ = ρ[n0 7→ ρ(n′ )]
K ′ = K[n0 7→ i]
localCheck(n0 , hH ′ , ρ′ , K ′ i)

H0 ⊆ H ∩ onstage(H) × F × {n′ } ∪ {n′ } × F × onstage(H) 
H1 ⊆ H ∩ offstage(H) × F × {n′ } ∪ {n′ } × F × offstage(H)
H0′ = swing(n′ , n0 , H0 )
H1′ ⊆ swing(n′ , n0 , H1 )
{hnnew , f, ni | hnold , f, ni ∈ H} ∪ {hn, f, nnew i | hn, f, nold i ∈ H} ∪
{hnnew , f, nnew i | hnold , f, nold i ∈ H}

=

Figure 14: Instantiation Relation ⇑

n0

hH, ρ, Ki k hH, ρ, Ki,
n0

′

′

′

hH, ρ, Ki k hH , ρ , K i,

acycCheck(n0 , hH, ρ, Ki, offstage(H))
¬acycCheck(n0 , hH, ρ, Ki, offstage(H))

where
H ′ = (H \ Hcyc ) ∪ Hoff ∪ BfNR ∪ BfR ∪ BtNR ∪ BtR ∪ Nf ∪ Nt
Hcyc = {hn1 , f, n2 i | n1 or n2 ∈ Scyc }
Hoff = { hn′1 , f, n′2 i | n1 = c(n′1 ), n2 = c(n′2 ),
n1 , n2 ∈ offstage1 (H), n1 or n2 ∈ Scyc ,
hn1 , f, n2 i ∈ H }
\(SR × acyclic(r) × SNR )
H ∩ (onstage(H) × F ∪ {n0 } × acyclic(r)) × Scyc = AfNR ⊎ AfR
H ∩ Scyc × (acyclic(r) × {n0 } ∪ F × onstage(H)) = AtNR ⊎ AtR
BfNR = {hn1 , f, hNR (n2 )i | hn1 , f, n2 i ∈ AfNR }
BfR = {hn1 , f, hR (n2 )i | hn1 , f, n2 i ∈ AfR }
BtNR = {hhNR (n1 ), f, n2 i | hn1 , f, n2 i ∈ AtNR }
BtR = {hhR (n1 ), f, n2 i | hn1 , f, n2 i ∈ AtR }
Nf = {hn0 , f, n′ i | n′ ∈ SR , hn0 , f, c(n′ )i ∈ H, f ∈ acyclic(r)}
Nt = {hn′ , f, n0 i | n′ ∈ SNR , hc(n′ ), f, n0 i ∈ H, f ∈ acyclic(r)}
Scyc = {n | ∃n1 , . . . , np−1 ∈ offstage(H) :
hn0 , f0 , n1 i, . . . , hnk , fk , ni, hn, fk+1 , nk+2 i, hnp−1 , fp−1 , n0 i ∈ H,
f0 , . . . , fp−1 ∈ acyclic(r)}
offstage1 (H) = offstage(H) \ {n0 }
r = ρ(n0 )
ρ′ (c(n)) = ρ(n)
K ′ (c(n)) = K(n)
Figure 15: Split Relation

n0
LN

LN
null

L

a) Before Split
LN

n

0

LN

LN
null
L

b) After Split

Figure 16: A Role Graph for an Acyclic List

role graph and ρ(n0 ) = r. If acyclic(r) = ∅, then the split
operation returns the original graph G; otherwise it proceeds
as follows. Call a path in graph H cycle-inducing if all of its
nodes are offstage and all of its edges are in acyclic(r). Let
Scyc be the set of nodes n such that there is a cycle-inducing
path from n0 to n and a cycle-inducing path from n to n0 .
The goal of the split operation is to split the set Scyc into
a fresh set of nodes SNR representing objects definitely not
reachable from n0 along edges in acyclic(r) and a fresh set of
nodes SR representing objects definitely reachable from n0 .
Each of the newly generated graphs H ′ has the following
properties:
1) merging the corresponding nodes from SNR and SR in
H ′ yields the original graph H;
2) n0 is not a member of any cycle in H ′ consisting of
offstage nodes and edges in acyclic(r);
3) onstage nodes in H ′ have the same number of fields and
aliases as in H.
Let S0 = nodes(H) \ Scyc and let hNR : Scyc → SNR and hR :
Scyc → SR be bijections. Define a function c : nodes(H ′ ) →
nodes(H) as follows:
c(n) =

(

n,
h−1
R (n),
h−1
NR (n),

n ∈ S0
n ∈ SR
n ∈ SNR

Then H ′ ⊆ {hn′1 , f, n′2 i | hc(n′1 ), f, c(n′2 )i ∈ H}.
Because there are two copies of S0 in H ′ , there might be
multiple edges hn′1 , f, n′2 i in H ′ corresponding to an edge
hc(n1 ), f, c(n2 )i ∈ H.

If both n′1 and n′2 are offstage nodes other than n0 , we
always include hn′1 , f, n′2 i in H ′ unless hn′1 , f, n′2 i ∈ SR ×
acyclic(r) × SNR . The last restriction prevents cycles in H ′ .
For an edge hn1 , f, n2 i ∈ H where n1 ∈ onstage(H) and
n2 ∈ Scyc we include in H ′ either the edge hn1 , f, hNR (n2 )i
or hn1 , f, hR (n2 )i but not both. Split generates multiple
graphs H ′ to cover both cases. We proceed analogously if
n2 ∈ onstage(H) and n1 ∈ Scyc . The node n0 itself is treated
in the same way as onstage nodes for f ∈
/ acyclic(r). If
f ∈ acyclic(r) then we choose references to n0 to have a
source in SNR , whereas the reference from n0 have the target
in SR .
Details of the split construction are given in Figure 15.
The intuitive meaning of the sets of edges is the following:
Hoff : edges between offstage nodes
BfNR : edges from onstage nodes to SNR
BfR : edges from onstage nodes to SR
BtNR : edges from SNR to onstage nodes
BtR : edges from SR to onstage nodes
Nf : acyclic(r)-edges from n0 to SR
Nt : acyclic(r)-edges from SNR to n0
The sets BfNR and BfR are created as images of the sets
AfNR and AfR which partition edges from onstage nodes to
nodes in Scyc . Similarly, the sets BtNR and BtR are created
as images of the sets AtNR and AtR which partition edges
from nodes in Scyc to onstage nodes.
We note that if in the split operation Scyc = ∅ then the
operation has no effect and need not be performed. In Figure 16, after performing a single split, there is no need to
split for subsequent elements of the list. Examples like this
indicate that split will not be invoked frequently during the
analysis.

6.2.2 Contraction
Figure 17 shows the non-error transitions of the contraction
n

relation . The analysis uses contraction when a local variable reference to node n is removed. If there are other local
references to n, the result is the original graph. Otherwise
n has just gone offstage, so analysis invokes nodeCheck. If
the check fails, the result is ⊥G . If the role check succeeds,
the contraction invokes normalization operation to ensure
that the role graph remains bounded. For simplicity, we use
normalization whenever nodeCheck succeeds, although it is
sufficient to perform normalization only at program points
adjacent to back edges of the control-flow graph.
Normalization Figure 18 shows the normalization relation. Normalization accepts a role graph hH, ρ, Ki and produces a normalized role graph hH ′ , ρ′ , K ′ i which is a factor
graph of hH, ρ, Ki under the equivalence relation ∼. Two
offstage nodes are equivalent under ∼ if they have the same
role and the same reachability from onstage nodes. Here we
consider node n to be reachable from an onstage node n0
iff there is some path from n0 to n whose edges belong to
acyclic(ρ(n0 )) and whose nodes are all in offstage(H). Note
that, by construction, normalization avoids merging nodes
which were previously generated in the split operation k,
while still ensuring a bound on the size of the role graph.
For a procedure with l local variables, f fields and r roles the
number of nodes in a role graph is on the order of r2l so the

n

∃x ∈ var(proc) :
hproc, x, ni ∈ H

hH, ρ, Ki  normalize(hH, ρ, Ki)

nodeCheck(n, hH, ρ, Ki, offstage(H))

hH, ρ, Ki hH, ρ, Ki
n

Figure 17: Contraction Relation
normalize(hH, ρ, Ki) = hH ′ , ρ′ , K ′ i
where

H ′ = {hn1/∼ , f, n2/∼ i | hn1 , f, n2 i ∈ H}
ρ′ (n/∼ ) = ρ(n)

i, n/∼ = {n}, K(n) = i
K ′ (n/∼ ) =
s, otherwise
n1 ∼ n2 iff n1 = n2 or
(n1 , n2 ∈ offstage(H), ρ(n1 ) = ρ(n2 ),
∀n0 ∈ onstage(H) : (reach(n0 , n1 ) iff reach(n0 , n2 ))
reach(n0 , n) iff ∃n1 , . . . , np−1 ∈ offstage(n), ∃f1 , . . . , fp ∈ acyclic(ρ(n0 )) :
hn0 , f1 , n1 i, . . . , hnp−1 , fp , ni ∈ H
Figure 18: Normalization
l

maximum size of a chain in the lattice is of the order of 2r2 .
To ensure termination we consider role graphs equal up to
isomorphism. Isomorphism checking can be done efficiently
if normalization assigns canonical names to the equivalence
classes it creates.

1. r ∈ fieldf (ρ(n)) for all hn, f, nx i ∈ H, and

6.2.3 Symbolic Execution
st

Figure 19 shows the symbolic execution relation =⇒. In
most cases, the symbolic execution of a statement acts on
the abstract heap in the same way that the statement would
act on the concrete heap. In particular, the Store statement
always performs strong updates. The simplicity of symbolic
execution is due to conditions 3) and 5) in the abstraction
relation α. These conditions are ensured by the  relation
which instantiates nodes, allowing strong updates. The symbolic execution also verifies the consistency conditions that
are not verified by  or .
Verifying Reference Removal Consistency

for offstage nodes are consistent with the new role r. The
acyclicity constraint involves only offstage nodes, so it remains satisfied. The other role constraints are local, so they
can only be violated for offstage neighbors of nx . To make
sure that no violations occur, we require:

The ab-

2. hr, f i ∈ sloti (ρ(n)) for all hnx , f, ni ∈ H and every slot
i such that hr0 , f i ∈ sloti (ρ(n))
This is sufficient to guarantee conW(ρc , Hc , offstage(Hc )).
To ensure condition 2) in Definition 22 of the abstraction
relation, we require that for every hf, gi ∈ identities(r),
1. hf, gi ∈ identities(r0 ) or
2. for all hnx , f, ni ∈ H: K(n) = i and (hn, g, n′ i ∈ H
implies n′ = nx ).
We use roleChOk(nx , r, hH, ρ, Ki) to denote the check just
described.

st

stract execution ❀ for the Store statement can easily verify
the Store safety condition from section 5.4.2, because the
set of onstage and offstage nodes is known precisely for every role graph. It returns ⊥G if the safety condition fails.
Symbolic Execution of setRole The setRole(x:r)
statement sets the role of node nx referenced by variable
x to r. Let G = hH, ρ, Ki be the current role graph and
let hproc, x, nx i ∈ H. If nx has no adjacent offstage nodes,
the role change always succeeds. In general, there are restrictions on when the change can be done. Let hHc , ρc i
be a concrete heap with role assignment represented by G
and h be a homomorphism from Hc to H. Let h(ox ) = nx .
Let r0 = ρc (ox ). The symbolic execution must make sure
that the condition conW(ρc , Hc , offstage(Hc )) continues to
hold after the role change. Because the set of onstage nodes
does not change, it suffices to ensure that the original roles

Symbolic Execution of roleCheck To symbolically execute roleCheck(x1 , . . . , xp , ra), we ensure that the conW
predicate of the concrete semantics is satisfied for the concrete heaps which correspond to the current abstract role
graph. The symbolic execution for roleCheck returns the
error graph ⊥G if ρ is inconsistent with ra or if any of the
nodes ni referenced by xi fail to satisfy nodeCheck.

6.2.4 Node Check
The analysis uses the localCheck, acycCheck, acycCheckAll,
and nodeCheck predicates to incrementally maintain the abstraction relation.
We first define the predicate localCheck, which roughly
corresponds to the predicate locallyConsistent (Definition 2),
but ignores the nonlocal acyclicity condition and additionally ensures condition 2) from Definition 22.

Statement s

Transition

Conditions

s

hproc, y, ny i, hny , f, nf i ∈ H
hproc, x, nx i, hproc, y, ny i ∈ H
nf ∈ onstage(H)
hproc, y, ny i ∈ H
nn fresh
ρ′ = ρ[nn 7→ unknown]
satisfied(c, H)
hproc, x, nx i ∈ H
roleChOk(nx , r, hH, ρ, Ki)
∀i hproc, xi , ni i ∈ H
nodeCheck(ni , hH, ρ, Ki, S)
S = offstage(H) ∪ {ni }i
ρ(ni ) = ra(ni )

x = y.f

hH ⊎ {proc, x, nx }, ρ, Ki =⇒ hH ⊎ {proc, x, nf }, ρ, Ki

x.f = y

s

hH ⊎ {nx , f, nf }, ρ, Ki =⇒ hH ⊎ {nx , f, ny }, ρ, Ki

x = y

hH ⊎ {proc, x, nx }, ρ, Ki =⇒ hH ⊎ {proc, x, ny }, ρ, Ki

x = new

hH ⊎ {proc, x, nx }, ρ, Ki =⇒ hH ⊎ {proc, x, nn }, ρ′ , Ki

test(c)

hH, ρ, Ki =⇒ hH, ρ, Ki

setRole(x:r)

hH, ρ, Ki =⇒ hH, ρ[nx 7→ r], Ki

roleCheck(x1..p , ra)

hH, ρ, Ki =⇒ hH, ρ, Ki

s

s

s

s

s

satisfied(x==y, Hc ) iff {o | hproc, x, oi ∈ Hc } = {o | hproc, y, oi ∈ Hc }
satisfied(!(x==y), Hc ) iff not satisfied(x==y, Hc )

Figure 19: Symbolic Execution of Basic Statements
Definition 25 For a role graph G = hH, ρ, Ki, an individual node n and a set S, the predicate localCheck(n, G) holds
iff the following conditions are met. Let r = ρ(n).

S, and we write acycCheck(n, G, S), iff it is not the case
that H contains a cycle n1 , f1 , . . . , ns , fs , n1 where n1 = n,
f1 , . . . , fs ∈ acyclic(ρ(n)) and n1 , . . . , ns ∈ S.

1A. (Outgoing fields check) For fields f ∈ F , if hn, f, n′ i ∈
H then ρ(n′ ) ∈ fieldf (r).

The analysis uses the predicate acycCheckAll(n, G, S) in
the contraction relation (Section 6.2.2) to make sure that n
is not a member of any cycle that would violate the acyclicity
condition of any of the nodes in S, including n.

2A. (Incoming slots check) Let {hn1 , f1 i, . . . , hnk , fk i} =
{hn′ , f i | hn′ , f, ni ∈ H} be the set of all aliases of
node n in abstract heap H. Then k = slotno(r) and
there exists a permutation p of the set {1, . . . , k} such
that hρ(ni ), fi i ∈ slotpi (r) for all i.
3A. (Identity Check) If hn, f, n′ i ∈ H, hn′ , g, n′′ i ∈ H,
hf, gi ∈ identities(r), and K(n′ ) = i, then n = n′′ .
4A. (Neighbor Identity Check) For every edge hn′ , f, ni ∈ H,
if K(n′ ) = i, ρ(n′ ) = r ′ and hf, gi ∈ identities(r ′ ) then
hn, g, n′ i ∈ H.
5A. (Field Sanity Check) For every f ∈ F there is exactly
one edge hn, f, n′ i ∈ H.
Conditions 1A and 2A correspond to conditions 1) and 2)
in Definition 2. Condition 3) in Definition 19 is not necessarily implied by condition 3A) if some of the neighbors of
n are summary nodes. Condition 3) cannot be established
based only on summary nodes, because verifying an identity
constraint for field f of node n where hn, f, n′ i ∈ H requires
knowing the identity of n′ , not only its existence and role.
We therefore rely on Condition 2) of the Definition 22 to
ensure that identity relations of neighbors of node n are satisfied before n moves offstage.
The predicate acycCheck(n, G, S) verifies the acyclicity
condition from Definition 19 for the node that has just been
brought onstage. The split operation uses acycCheck to
check whether it should split any nodes (Section 6.2.1). The
set S represents offstage nodes.
Definition 26 We say that a node n satisfies an acyclicity check in graph G = hH, ρ, Ki with respect to the set

Definition 27 We say that a node n satisfies a strong
acyclicity check in graph G = hH, ρ, Ki with respect to a
set S, and we write acycCheckAll(n, G, S), iff it is not the
case that: H contains a cycle n1 , f1 , . . . , ns , fs , n1 where
n1 = n, f1 , . . . , fs ∈ acyclic(ρ(ni )), for some 1 ≤ i ≤ s,
and n1 , . . . , ns ∈ S.
acycCheckAll is a stronger condition than acycCheck because
it ensures the absence of cycles containing n for acyclic(ρ(ni ))
fields of all offstage nodes ni , and not only for the fields
acyclic(ρ(n)).
The analysis uses the predicate nodeCheck to verify that
bringing a node n offstage does not violate role consistency
for offstage nodes.
Definition 28 nodeCheck(n, G, S) holds iff both predicates
localCheck(n, G) and acycCheckAll(n, G, S) hold.

7

Interprocedural Role Analysis

This section describes the interprocedural aspects of our role
analysis. Interprocedural role analysis can be viewed as an
instance of the functional approach to interprocedural dataflow analysis [41]. For each program point p, role analysis
approximates program traces from procedure entry to point
p. The solution in [41] proposes tagging the entire data-flow
fact G at point p with the data flow fact G0 at procedure entry. In contrast, our analysis computes the correspondence
between heaps at procedure entry and heaps at point p at

the granularity of sets of objects that constitute role graphs.
This allows our analysis to detect which regions of the heap
have been modified. We approximate the concrete executions of a procedure with procedure transfer relations consisting of 1) an initial context and 2) a set of effects. Effects
are fine-grained transfer relations which summarize load and
store statements and can naturally describe local heap modifications. In this paper we assume that procedure transfer
relations are supplied and we are concerned with a) verifying
that transfer relations are a conservative approximation of
procedure implementation b) instantiating transfer relations
at call sites.

7.1

Procedure Transfer Relations

A transfer relation for a procedure proc extends the procedure signature with an initial context context(proc), and
procedure effects effect(proc).

imply that parameters p1 and p2 must be aliased,
p1 -> n1
p2 -> n2
force p1 and p2 to be unaliased, whereas
p1 -> n1|n2
p2 -> n1|n2
allow for both possibilities. A heap edge n -f-> m denotes
hn, f, mi ∈ HIC . The shorthand notation
n1 -f-> n2
-g-> n3
denotes two heap edges hn1, f, n2i, hn1, g, n3i ∈ HIC . An expression n1 -f-> n2|n3 denotes two edges n1 -f-> n2 and
n1 -f-> n3. We use similar shorthands for parameter edges.

7.1.1 Initial Context
Figures 20 and 21 contain examples of initial context specification. An initial context is a description of the initial role
graph hHIC , ρIC , KIC i where ρIC and KIC are determined by a
nodes declaration and HIC is determined by a edges declaration. The initial role graph specifies a set of concrete heaps
at procedure entry and assigns names for sets of nodes in
these heaps. The next definition is similar to Definition 22.
Definition 29 We say that a concrete heap hHc , ρc i is represented by the initial role graph hHIC , ρIC , KIC i and write
hHc , ρc i α0 hHIC , ρIC , KIC i, iff there exists a function h0 :
nodes(Hc ) → nodes(HIC ) such that

proc
p
l
lx

ph

proc
P1

LL1

null

proc
proc
px

proc l2
SleepingProc

1. conW(ρc , Hc , h−1
0 (read(proc));
2. h0 is a graph homomorphism;
3. KIC (n) = i implies

|h−1
0 (n)|

≤ 1;

proc
P2

proc
LL2

proc

4. h0 (nullc ) = null and h0 (procc ) = proc;
5. ρc (o) = ρIC (h0 (o)) for every object o ∈ nodes(Hc ).
Here read(proc) is the set of initial-context nodes read by
the procedure (see below). For simplicity, we assume one
context per procedure; it is straightforward to generalize the
treatment to multiple contexts.
A context is specified by declaring a list of nodes and a
list of edges.
A list of nodes is given with nodes declaration. It specifies
a role for every node at procedure entry. Individual nodes
are denoted with lowercase identifiers, summary nodes with
uppercase identifiers. By using summary nodes it is possible
to indicate disjointness of entire heap regions and reachability between nodes in the heap.
There are two kinds of edges in the initial role graph: parameter edges and heap edges. A parameter edge p->pn is
interpreted as hproc, p, pni ∈ HIC . We require every parameter edge to have an individual node as a target, we call such
node a parameter node. The role of a parameter node referenced by parami (proc) is always preRi (proc). Since different
nodes in the initial role graph denote disjoint sets of concrete
objects, parameter edges
p1 -> n1
p2 -> n1

nodes ph : RunningHeader,
P1, px, P2 : RunningProc,
lx : LiveHeader,
LL1, l2, LL2 : LiveList;
edges p-> px, l-> px,
ph -next-> P1|px
-prev-> px|P2,
P1 -next-> P1|px
-prev-> ph|P1,
px -next-> P2|ph
-prev-> P1|ph,
P2 -next-> P2|ph
-prev-> P2|px,
lx -next-> LL1|l2,
LL1 -next-> LL1|l2
-proc-> P1|P2|SleepingProc
l2 -next-> LL2|null
-proc-> px,
LL2 -next-> LL2|null
-proc-> P1|P2|SleepingProc
Figure 20: Initial Context for kill Procedure

Example 30 Figure 20 shows an initial context graph for
the kill procedure from Example 17. It is a refinement of
the role reference diagram of Figure 1 as it gives description
of the heap specific to the entry of kill procedure. The
initial context makes explicit the fact that there is only one
header node for the list of running processes (ph) and one
header node for the list of all active processes (lx). More importantly, it shows that traversing the list of active processes
reaches a node l2 whose proc field references the parameter
node px. This is sufficient for the analysis to conclude that
there will be no null pointer dereferences in the while loop
of kill procedure since l2 is reached before null.
We assume that the initial context always contains the role
reference diagram RRD (Definition 8). Nodes from RRD are
called anonymous nodes and are referred to via role name.
This further reduces the size of initial context specifications
by leveraging global role definitions. In Figure 20 there is
no need to specify edges originating from SleepingProc or
even mention the node SleepingTree, since role definitions
alone contain enough information on this part of the heap
to enable the analysis of the procedure. Note, however, that
all edges between anonymous nodes and named nodes must
be explicitly specified.

7.1.2 Procedure Effects
Procedure effects conservatively approximate the region of
the heap that the procedure accesses and indicate changes
to the referencing relationships in that region. There are two
kinds of effects: read effects and write effects.
A read effect specifies a set read(proc) of initial graph
nodes accessed by the procedure. It is used to ensure that
the accessibility condition in Section 5.4.3 is satisfied. If the
set of nodes denoted by read(proc) is mapped to a node n
which is onstage in the caller but is not an argument of the
procedure call, a role check error is reported at the call site.
Write effects are used to modify caller’s role graph to conservatively model the procedure call. A write effect e1 .f = e2
approximates Store operations within a procedure. The expression e1 denotes objects being written to, f denotes the
field written, and e2 denotes the set of objects which could
be assigned to the field. Write effects are may effects by default, which means that the procedure is free not to perform
them. It is possible to specify that a write effect must be
performed by prefixing it with a “!” sign.
Example 31 In Figure 21, the insert procedure inserts
an isolated cell into the end of an acyclic singly linked list.
As a result, the role of the cell changes to LN. The initial
context declares parameter nodes ln and xn (whose initial
roles are deduced from roles of parameters), and mentions
anonymous LN node from a default copy of the role reference
diagram RRD. The code of the procedure is summarized
with two write effects. The first write effect indicates that
the procedure may perform zero or more Store operations
to field next of nodes mapped to ln or LN in context(proc).
The second write effect indicates that the execution of the
procedure must perform a Store to the field next of xn node
where the reference stored is either a node mapped onto
anonymous LN node or null.

procedure insert(l : L,
x : IsolatedN ->> LN)
nodes ln, xn;
edges l-> ln, x-> xn,
ln -next-> LN|null;
effects ln|LN . next = xn,
! xn.next = LN|null;
local c, p;
{
p = l;
c = l.next;
while (c!=null) {
p = c;
c = p.next;
}
p.next = x;
x.next = c;
setRole(x:LN);
}
Figure 21: Insert Procedure for Acyclic List
procedure insertSome(l : L)
nodes ln;
edges l-> ln,
ln -next-> LN|null;
effects ln|LN . next = NEW,
NEW.next = LN|null;
aux c, p, x;
{
p = l;
c = l.next;
while (c!=null) {
p = c;
c = p.next;
}
x = new;
p.next = x;
x.next = c;
setRole(x:LN);
}
Figure 22: Insert Procedure with Object Allocation
Effects also describe assignments that procedures perform
on the newly created nodes. Here we adopt a simple solution
of using a single summary node denoted NEW to represent
all nodes created inside the procedure. We write nodes0 (HIC )
for the set nodes(HIC ) ∪ {NEW}.
Example 32 Procedure insertSome in Figure 22 is similar
to procedure insert in Figure 21, except that the node inserted is created inside the procedure. It is therefore referred
to in effects via generic summary node NEW.
We represent all may write effects as a set mayWr(proc) of
triples hnj , f, n′j i where n, n′j ∈ nodes0 (HIC ) and f ∈ F . We
represent must write effects as a sequence mustWrj (proc) of
subsets of the set KIC−1 (i) × F × nodes0 (HIC ). Here 1 ≤ j ≤
mustWrNo(proc).
To simplify the interpretation of the declared procedure effects in terms of concrete reads and writes, we re-

quire the union ∪i mustWri (proc) to be disjoint from the
set mayWr(proc). We also require the nodes n1 , . . . , nk in
a must write effect n1 | · · · |nk .f = e2 to be individual nodes.
This allows strong updates when instantiating effects (Section 7.3.2).

7.1.3 Semantics of Procedure Effects
We now give precise meaning to procedure effects. Our definition is slightly complicated by the desire to capture the
set of nodes that are actually read in an execution while still
allowing a certain amount of observational equivalence for
write effects.
The effects of procedure proc define a subset of permissible program traces in the following way. Consider
a concrete heap Hc with role assignment ρc such that
hHc , ρc i α0 hHIC , ρIC , KIC i with graph homomorphism h0 from
Definition 29. Consider a trace T starting from a state with
heap Hc and role assignment ρc . Extract the subsequence
of all loads and stores in trace T . Replace Load x=y.f by
concrete read read ox where ox is the concrete object referenced by x at the point of Load, and replace Store x.f=y by
a concrete write ox .f = oy where ox is the object referenced
by x and oy object referenced by y at the point of Store. Let
p1 , . . . , pk be the sequence of all concrete read statements
and q1 , . . . , qk the sequence of all concrete write statements.
We say that trace T starting at Hc conforms to the effects
iff for all choices of h0 the following conditions hold:
1. h0 (o) ∈ read(proc) for every pi of the form read o
2. there exists a subsequence qi1 , . . . , qit of q1 , . . . , qk such
that
(a) executing qi1 , . . . , qit on Hc yields the same result
as executing the entire sequence q1 , . . . , qk
(b) the sequence qi1 , . . . , qit implements write effects
of procedure proc
A typical way to obtain a sequence qi1 , . . . , qit from the sequence q1 , . . . , qk is to consider only the last write for each
pair hoi , f i of object and field.
We say that a sequence qi1 , . . . , qit implements write effects mayWr(proc) and mustWri (proc) for 1 ≤ i ≤ i0 ,
i0 = mustWrNo if and only if there exists an injection
s : {1, . . . , i0 } → {i1 , . . . , it } such that
1. hh′ (o), f, h′ (o′ )i ∈ mustWri (proc) for every concrete
write qs(i) of the form o.f = o′ , and
2. hh′ (o), f, h′ (o′ )i ∈ mayWr(proc) for all concrete writes
qi of the form o.f = o′ for i ∈ {i1 , . . . , it } \
{s(1), . . . , s(i0 )}.
Here h′ (n) = h0 (n) for n ∈ nodes(Hc ) where Hc is the initial
concrete heap and h′ (n) = NEW otherwise.
It is possible (although not very common) for a single
concrete heap Hc to have multiple homomorphisms h0 to
the initial context HIC . Note that in this case we require the
trace T to conform to effects for all possible valid choices
of h0 . This places the burden of multiple choices of h0 on
procedure transfer relation verification (Section 7.2) but in
turn allows the context matching algorithm in Section 7.3.1
to select an arbitrary homomorphism between a caller’s role
graph and an initial context.

7.2

Verifying Procedure Transfer Relations

In this section we show how the analysis makes sure that a
procedure conforms to its specification, expressed as an initial context with a list of effects. To verify procedure effects,
we extend the analysis representation from Section 6.1. A
non-error role graph is now a tuple hH, ρ, K, τ, Ei where:
1. τ : nodes(H) → nodes0 (HIC ) is initial context transformation that assigns an initial context node τ (n) ∈
nodes(HIC ) to every node n representing objects that
existed prior to the procedure call, and assigns NEW to
every node representing objects created during procedure activation;
2. E ⊆ ∪i mustWri (proc) is a list of must write effects that
procedure has performed so far.
The initial context transformation τ tracks how objects have
moved since the beginning of procedure activation and is
essential for verifying procedure effects which refer to initial
context nodes.
We represent the list E of performed must effects as a partial map from the set KIC−1 (i)×F to nodes0 (HIC ). This allows
the analysis to perform must effect folding by recording only
the last must effect for every pair hn, f i of individual node
n and field f .

[[entry•]] =

n

hH, ρ, K, τ, Ei
P : {proc} × {parami (proc)}i → N, P ⊆ HIC
H0 = (HIC \ {proc} × param(proc) × N ) ∪ P
ni = P (proc, parami (proc))
H1 ⊆ H0
H1 \ H0 ⊆ {hn′ , f, n′′ i | {n1 , n2 } ∩ {ni }i 6= ∅}
∀j : localCheck(nj , hH, ρ, Ki, nodes(H1 ))
n1

n2

np

H1 k H2 k · · · k H
ρ = ρIC
K = KIC
τ = ρICo
E=∅

Figure 23: The Set of Role Graphs at Procedure Entry

7.2.1 Role Graphs at Procedure Entry
Our role analysis creates the set of role graphs at procedure entry point from the initial context context(proc). This
is simple because role graphs and the initial context have
similar abstraction relations (Sections 6.1 and 7.1). The difference is that parameters in role graphs point to exactly one
node, and parameter nodes are onstage nodes in role graphs
which means that all their edges are “must” edges.
Figure 23 shows the construction of the initial set of role
graphs. First the graph H0 is created such that every parameter parami (proc) references exactly one parameter node
ni . Next graph H1 is created by using localCheck to ensure
that parameter nodes have the appropriate number of edges.
Finally, the instantiation is performed on parameter nodes
to ensure acyclicity constraints if the initial context does not
make them explicit already.

Statement s

Transition

Constraints
hproc, y, ny i, hny , f, nf i ∈ H
τ (nf ) ∈ read(proc)
hproc, y, ny i, hny , f, nf i ∈ H
τ (nf ) ∈
/ read(proc)
hproc, x, nx i, hproc, y, ny i ∈ H
hτ (nx ), f, τ (ny )i ∈ mayWr(proc)
hproc, x, nx i, hproc, y, ny i ∈ H
hτ (nx ), f, τ (ny )i ∈ ∪i mustWri (proc)
E ′ = updateWr(E, hτ (nx ), f, τ (ny )i)
hproc, x, nx i, hproc, y, ny i ∈ H
hτ (nx ), f, τ (ny )i ∈
/ mayWr(proc)∪
∪i mustWri (proc)
nn fresh
τ ′ = τ [nn 7→ NEW]

s

x = y.f

hH ⊎ {proc, x, nx }, ρ, K, τ, Ei =⇒ hH ⊎ {proc, x, nf }, ρ, K, τ, Ei

x = y.f

hH ⊎ {proc, x, nx }, ρ, K, τ, Ei =⇒ ⊥G

x.f = y

hH ⊎ {nx , f, nf }, ρ, K, τ, Ei =⇒ hH ⊎ {nx , f, ny }, ρ, K, τ, Ei

x.f = y

hH ⊎ {nx , f, nf }, ρ, K, τ, Ei =⇒ hH ⊎ {nx , f, ny }, ρ, K, τ, E ′ i

x.f = y

hH ⊎ {nx , f, nf }, ρ, K, τ, Ei =⇒ ⊥G

x = new

hH ⊎ {proc, x, nx }, ρ, K, τ, Ei =⇒ hH ⊎ {proc, x, nn }, ρ, K, τ ′ , Ei

s

s

s

s

s

updateWr(E, hn1 , f, n2 i) = E[hn1 , f i 7→ n2 ]

Figure 24: Verifying Load, Store, and New Statements

7.2.2 Verifying Basic Statements
To ensure that a procedure conforms to its transfer relation
the analysis uses the initial context transformation τ to assign every Load and Store statement to a declared effect.
Figure 24 shows new symbolic execution of Load, Store and
New statements.
The symbolic execution of Load statement x=y.f makes
sure that the node being loaded is recorded in some read
effect. If this is not the case, an error is reported.
The symbolic execution of the Store statement x.f=y first
retrieves nodes τ (nx ) and τ (ny ) in the initial role graph
context that correspond to nodes nx and ny in the current
role graph. If the effect hτ (nx ), f, τ (ny )i is declared as a may
write effect the execution proceeds as usual. Otherwise, the
effect is used to update the list E of must-write effects. The
list E is checked at the end of procedure execution.
The symbolic execution of the New statement updates the
initial context transformation τ assigning τ (nn ) = NEW for
the new node nn .
The τ transformation is similarly updated during other
abstract heap operations. Instantiation of node n′ into node
n0 assigns τ (n0 ) = τ (n′ ), split copies values of τ into the new
set of isomorphic nodes, and normalization does not merge
nodes n1 and n2 if τ (n1 ) 6= τ (n2 ).

7.2.3 Verifying Procedure Postconditions
At the end of the procedure, the analysis verifies that ρ(ni ) =
postRi (proc) where hproc, parami (proc), ni i ∈ H, and then
performs node check on all onstage nodes using predicate
nodeCheck(n, hH, ρ, Ki, nodes(H)) for all n ∈ onstage(H).
At the end of the procedure, the analysis also verifies
that every performed effect in E = {e1 , . . . , ek } can be attributed to exactly one declared must effect. This means
that k = mustWrNo(proc) and there exists a permutation s
of set {1, . . . , k} such that es(i) ∈ mustWri (proc) for all i.

[[proc′ (x1 , . . . , xp )]](G) =
if ∃G ∈ G : ¬paramCheck(G) then {⊥G }
else try G1 = matchContext(G)
if failed then {⊥G }
else {G′′ | hG, µi ∈ G1
FX

RR

haddNEW(G), µi −→hG′ , µi −→ G′′ }
paramCheck(hH, ρ, K, τ, Ei) iff
∀ni : nodeCheck(ni , G, offstage(H) ∪ {ni }i )
ni are such that hproc, xi , ni i ∈ H
addNEW(hH, ρ, K, τ, Ei) =
hH ∪ {n0 } × F × {null},
ρ[n0 7→ unknown],
K[n0 7→ s],
τ [n0 7→ NEW],
Ei
where n0 is fresh in H
Figure 25: Procedure Call

7.3

Analyzing Call Sites

The set of role graphs at the procedure call site is updated based on the procedure transfer relation as follows.
Consider procedure proc containing call site p ∈ NCFG (proc)
with procedure call proc′ (x1 , . . . , xp ). Let hHIC , ρIC , KIC i =
context(proc′ ) be the initial context of the callee.
Figure 25 shows the transfer function for procedure call
sites. It has the following phases:
1. Parameter Check ensures that roles of parameters
conform to the roles expected by the callee proc′ .
2. Context Matching (matchContext) ensures that the
caller’s role graphs represent a subset of concrete heaps
represented by context(proc′ ). This is done by deriving
a mapping µ from the caller’s role graph to nodes(HIC ).

FX

3. Effect Instantiation (−→ ) uses effects mayWr(proc′ )
and mustWri (proc′ ) in order to approximate all structural changes to the role graph that proc′ may perform.
RR

4. Role Reconstruction (−→) uses final roles for parameter nodes and global role declarations postRi (proc′ ) to
reconstruct roles of all nodes in the part of the role
graph representing modified region of the heap.

the inverse image S of the performed effects. The effects in
S are grouped by the source n and field f . Each field n.f
is applied in sequence. There are three cases when applying
an effect to n.f :
1. There is only one node target of the write in nodes(H)
and the effect is a must write effect. In this case we do
a strong update.
2. The condition in 1) is not satisfied, and the node n is
offstage. In this case we conservatively add all relevant
edges from S to H.

The parameter check requires nodeCheck(ni , G, offstage(H)∪
{ni }i ) for the parameter nodes ni . The other three phases
are explained in more detail below.

3. The condition in 1) is not satisfied, but the node n is
onstage i.e. it is a parameter node3 . In this case there
is no unique target for n.f , and we cannot add multiple edges either as this would violate the invariant for
onstage nodes. We therefore do case analysis choosing
which effect was performed last. If there are no must effects that affect n, then we also consider the case where
the original graph is unchanged.

7.3.1 Context Matching
Figure 26 shows our context matching function. The
matchContext function takes a set G of role graphs and produces a set of pairs hG, µi where G = hH, ρ, K, τ, Ei is a role
graph and µ is a homomorphism from H to HIC . The homo′
morphism µ guarantees that α−1 (G) ⊆ α−1
0 (context(proc ))
since the homomorphism h0 from Definition 29 can be constructed from homomorphism h in Definition 22 by putting
h0 = µ ◦ h. This implies that it is legal to call proc′ with any
concrete graph represented by G.
The algorithm in Figure 26 starts with empty maps µ =
nodes(G) × {⊥} and extends µ until it is defined on all
nodes(G) or there is no way to extend it further. It proceeds by choosing a role graph hH, ρ, K, τ, Ei and node n0
for which the mapping µ is not defined yet. It then finds
candidates in the initial context that n0 can be mapped to.
The candidates are chosen to make sure that µ remains a
homomorphism. The accessibility requirement—that a procedure may see no nodes with incorrect role—is enforced
by making sure that nodes in inaccessible are never mapped
into nodes in read for the callee. As long as this requirement
holds, nodes in inaccessible can be mapped onto nodes of any
role since their role need not be correct anyway. We generally require that the set µ−1 (n′0 ) for individual node n′0 in
the initial context contain at most one node, and this node
must be individual. In contrast, there might be many individual and summary nodes mapped onto a summary node.
We relax this requirement by performing instantiation of a
summary node of the caller if, at some point, that is the only
way to extend the mapping µ (this corresponds to the first
recursive call in the definition of match in Figure 26).
The algorithm is nondeterministic in the order in which
nodes to be matched are selected. One possible ordering
of nodes is depth-first order in the role graph starting from
parameter nodes. If some nondeterministic branch does not
succeed, the algorithm backtracks. The function fails if all
branches fail. In that case the procedure call is considered
illegal and ⊥G is returned. The algorithm terminates since
every procedure call lexicographically increases the sorted
list of numbers |µ[nodes(H)]| for hhH, ρ, K, τ, Ei, µi ∈ Γ.

7.3.2 Effect Instantiation
The result of the matching algorithm is a set of pairs hG, µi
of role graphs and mappings. These pairs are used to instantiate procedure effects in each of the role graphs of the caller.
Figure 30 gives rules for effect instantiation. The analysis
first verifies that the region read by the callee is included in
the region read by the caller. Then it uses map µ to find

7.3.3 Role Reconstruction
Procedure effects approximate structural changes to the
heap, but do not provide information about role changes
for non-parameter nodes. We use the role reconstruction
RR
algorithm −→ in Figure 27 to conservatively infer possible
roles of nodes after the procedure call based on role changes
for parameters and global role definitions.
Role reconstruction first finds the set N0 of all nodes that
might be accessed by the callee since these nodes might have
their roles changed. Then it splits each node n ∈ N0 into |R|
different nodes ρ(n, r), one for each role r ∈ R. The node
ρ(n, r) represents the subset of objects that were initially
represented by n and have role r after procedure executes.
The edges between nodes in the new graph are derived by
simultaneously satisfying 1) structural constraints between
nodes of the original graph; and 2) global role constraints
from the role reference diagram. The nodes ρ(n, r) not connected to the parameter nodes are garbage collected in the
role graph. In practice, we generate nodes ρ(n, r) and edges
on demand starting from parameters making sure that they
are reachable and satisfy both kinds of constraints.

8

Extensions

This section presents two extensions of the basic role system.
The first extension allows statically unbounded number of
aliases for objects. The second extension allows the analysis
to verify more complex role changes. Additional ways of
extending roles are given in [31].

8.1

Multislots

A multislot hr ′ , f i ∈ multislots(r) in the definition of role r
allows any number of aliases ho′ , f, oi ∈ Hc for ρc (o′ ) = r ′
and ρc (o) = r. We require multislots multislots(r) to be
disjoint from all sloti (r). To handle multislots in role analysis
we relax the condition 5) in Definition 22 of the abstraction
3
Non-parameter onstage nodes are never affected by effects, as guaranteed by the matching algorithm.

matchContext(G) = match({hG, nodes(G) × {⊥}i | G ∈ G})
match : P(RoleGraphs × (N ∪ {⊥})N ) ⇀ P(RoleGraphs × N N )
match(Γ) =
Γ0 := {hG, µi ∈ Γ | µ−1 (⊥) 6= ∅};
if Γ0 = ∅ then return Γ;
hhH, ρ, K, τ, Ei, µi := choose Γ0 ;
Γ′ = Γ \ hhH, ρ, K, τ, Ei, µi;
paramnodes := {n | ∃i : hproc, xi , ni ∈ H};
inaccessible := onstage(H) \ paramnodes;
n0 := choose µ−1 (⊥);
candidates := {n′ ∈ nodes(HIC ) |
(n0 ∈
/ inaccessible and ρIC (n′ ) = ρ(n0 )) or
(n0 n
∈ inaccessible and n′ ∈
/o
read(proc′ ))}

T

n′ hn′ , f, µ(n)i ∈ HIC

hn0 ,f,ni∈H
µ(n)6=⊥

T

hn,f,n0 i∈H
µ(n)6=⊥

o

n

n′ hµ(n), f, n′ i ∈ HIC ;

if candidates = ∅ then fail ;
if candidates = {n′0 }, K(n0 ) = s, KIC (n′0 ) = i, µ−1 (n′0 ) = ∅
n1

then match(Γ′ ∪ {hG′ , µ[n1 7→ n′0 ]i | hH, ρ, K, τ, Ei ⇑ G′ })
else n′0 := choose {n′ ∈ candidates | K(n′ ) = s or
(K(n0 ) = i, µ−1 (n′ ) = ∅)}
′
match(Γ ∪ hhH, ρ, K, τ, Ei, µ[n0 7→ n′0 ]i);

n0

Figure 26: The Context Matching Algorithm
relation by allowing h to map more than one concrete edge
ho′ , f, oi onto abstract edge hn′ , f, ni ∈ H terminating at an
onstage node n provided that hρ(n′ ), f i ∈ multislots(ρ(n)).
The nodeCheck and expansion relation  are then extended
appropriately. Note that a role graph does not represent
the exact number of references that fill each multislot. The
analysis therefore does not attempt to recognize actions that
remove the last reference from the multislot. Once an object
plays a role with a multislot, all subsequent roles that it plays
must also have the multislot.

8.2

Cascading Role Changes

In some cases it is desirable to change roles of an entire set of
offstage objects without bringing them onstage. We use the
statement setRoleCascade(x1 : r1 , . . . , xn : rn ) to perform
such cascading role change of a set of nodes. The need for
cascading role changes arises when roles encode reachability
properties.
Example 33 The code fragment in Figure 28 manipulates
object m of role Data. The role Data has fields buffer and
work, each being a root for a singly linked acyclic list. Elements of the first list have BufferNode role and elements
of the second list have WorkNode role. At some point procedure swaps the contents of the fields buffer and work, which
requires all nodes in both lists to change the roles. These
role changes are triggered by the setRoleCascade statement.

role BufferNode {
fields next : BufferNode | null;
slots BufferNode.next | Data.buffer;
acyclic next;
}
role WorkNode {
fields next : WorkNode | null;
WorkNode.next | Data.work;
acyclic next;
}
role Data {
fields buffer : BufferNode | null,
work
: WorkNode | null;
}
{
...
roleCheck(m : Data);
x = m.buffer;
y = m.work;
m.buffer = y;
m.work = x;
setRoleCascade(x:WorkNode, y:BufferNode);
...
}
Figure 28: Example of a Cascading Role Change

RR

hhH, ρ, K, τ, Ei, µi −→hH ′ , ρ′ , K ′ , τ ′ , E ′ i
hproc, xi , ni i ∈ H
N0 = µ−1 [read(proc′ )]
s : N0 × R → N where s(n, r) are all different nodes fresh in H
ρ′ = ρ \ (N0 × R) ∪ {hs(n, r), ri | n ∈ N0 , r ∈ R}
\({ni }i × R) ∪ {hni , postRi (proc)i}
K ′ (s(n, r)) = K(n)
τ ′ (s(n, r)) = τ (n)
E′ = E
H0 = H \ {hn1 , f, n2 i | n1 ∈ N0 or n2 ∈ N0 }
∪ {hs(n1 , r1 ), f, s(n2 , r2 )i | hn1 , f, n2 i ∈ H, hr1 , f, r2 i ∈ RRD}
∪ {hn1 , f, s(n2 , r2 )i | hn1 , f, n2 i ∈ H, hρIC (µ(n1 )), f, r2 i ∈ RRD}
∪ {hs(n1 , r1 ), f, n2 i | hn1 , f, n2 i ∈ H, hr1 , f, ρIC (µ(n2 ))i ∈ RRD}
H ′ = GC(H0 )
Figure 27: Call Site Role Reconstruction
The statement indicates new roles for onstage nodes, and the
analysis cascades role changes to offstage nodes.
Given a role graph hH, ρ, K, Ei cascading role change finds
a new valid role assignment ρ′ where the onstage nodes
have desired roles and the roles of offstage nodes are adjusted appropriately. Figure 29 shows abstract execution
of the setRoleCascade statement. Here neighbors(n, H)
denotes nodes in H adjacent to n.
The condition
cascadingOk(n, H, ρ, K, ρ′ ) makes sure it is legal to change
the role of node n from ρ(n) to ρ′ (n) given that the neighbors of n also change role according to ρ′ . This check resembles the check for setRole statement in Section 6.2.3. Let
r = rho(n) and r ′ = ρ′ (n). Then cascadingOk(n, H, ρ, K, ρ′ )
requires the following conditions:
1. hn, f, n1 i ∈ H implies ρ′ (n1 ) ∈ fieldf (r ′ )
2. slotno(r ′ ) = slotno(r) = k, and for every list
hn1 , f1 , ni, . . . , hnk , fk , ni ∈ H if there is a permutation p : {1, . . . , k} → {1, . . . , k} such that hρ(ni ), fi i ∈
slotpi (r), then there is a permutation p′ : {1, . . . , k} →
{1, . . . , k} such that hρ(ni ), fi i ∈ slotpi (r ′ ).
3. identity relations were already satisfied or can be explicitly checked: hf, gi ∈ identities(ρ′ (n)) implies
(a) hf, gi ∈ identities(ρ(n)) or
(b) for all hn, f, n′ i ∈ H: K(n′ ) = i, and
if hn′ , g, n′′ i ∈ H then n′′ = n
4. either acyclic(ρ′ (n)) ⊆ acyclic(ρ(n)) or
acycCheck(n, hH, ρ′ , Ki, offstage(H)).
In practice there may be zero or more solutions that satisfy
constraints for a given cascading role change. Selecting any
solution that satisfies the constraints is sound with respect
to the original semantics. A useful heuristic for searching
the solution space is to first explore branches with as few
roles changed as possible. If no solutions are found, an error
is reported.

9

Related Work

Typestate, as a type system extension for statically verifying
dynamically changing properties, was proposed in [44, 43].
Aliasing causes problems for typestate-based systems because the declared typestates of all aliases must change
whenever the state of the referred object changes. Faced
with the complexity of aliasing, [44] resorted to a more controlled language model which avoids aliasing. More recently
proposed typestate approaches use linear types for heap references to support state changes of dynamic allocated objects without addressing aliasing issues [10].
Motivated by the need to enforce safety properties in lowlevel software systems, [42, 46, 9] use extensions of linear
types to describe aliasing of objects and rely on language
design to avoid non-local type inference. These systems take
a construction based approach that specifies data structures
as unfoldings of basic elaboration steps [46]. Similarly to
shape types [15, 14] and graph types [29, 34], this allows
tree-like data structures to be expressed more precisely than
using our roles, but cannot approximate data structures such
as sparse matrices. More importantly, this approach makes
it difficult to express nodes that are members of multiple
data structures. Handling multiple data structures is the
essential ingredient of our approach because the role of an
object depends on data structures in which it participates.
Like shape analysis techniques [5, 17, 39, 40] we have
therefore adopted the constraint based approach which characterizes data structures in terms of the constraints that they
satisfy. The constraint based approach allows us to handle a
wider range of data structure while giving up some precision.
Like [47, 48] we perform non-local inference of program properties, but while [47, 48] focus on linear integer constraints
and handle recursive data structures conservatively, we do
not handle integer arithmetic but have a more precise representation of the heap. At a higher level, these approaches
all focus on detailed properties of individual data structures.
We view our research as focusing more on global aspects such
as the participation of objects in multiple data structures.
The path matrix approaches [18, 17] have been used to
implement efficient interprocedural analyses that infer one
level of referencing relationships, but are not sufficiently pre-

s

′

hH, ρ, K, τ, Ei ❀hH, ρ , K, τ, Ei
s = setRoleCascade(x1 : r1 , . . . , xn : rn )

ni : hproc, xi , ni i ∈ H
ρ′ (ni ) = ri
ρ′ (n) = ρ(n), n ∈ onstage(H) \ {ni }i
N0 = {n ∈ offstage(H) | ∃n′ ∈ neighbors(n, H) : ρ(n′ ) 6= ρ′ (n′ )}
∀n ∈ N0 : cascadingOk(n, H, ρ, K, ρ′ )

Figure 29: Abstract Execution for setRoleCascade
cise to track must aliases of heap objects for programs with
destructive updates of more complex data structures.
The use of the instantiation relation in role analysis is
analogous to the materialization operation of [39, 40]. Role
analysis can also track reachability properties, but we use an
abstraction relation based on graph homomorphism rather
than 3-valued logic. Our split operation achieves a similar
goal to the focus operation of [40]. However, the generic
focus algorithm of [32] cannot handle the reachability predicate which is needed for our split operation. This is because
it conservatively refuses to focus on edges between two summary nodes to avoid generating an infinite number of structures. Rather than requiring definite values for reachability
predicate, our role analysis splits by reachability properties
in the abstract role graph, which illustrates the flexibility
of the homomorphism-based abstraction relation. Another
difference with [40] is that our role analysis does not require
the developer to supply the predicate update formulae for
instrumentation predicates.
A precise interprocedural analysis [38] extends shape analysis techniques to treat activation records as dynamically allocated structures. The approach also effectively synthesizes
an application-specific set of contexts. Our approach differs
in that it uses a less precise but more scalable treatment of
procedures. It also uses a compositional approach that analyzes each procedure once to verify that it conforms to its
specification. Like [48] our interprocedural analysis can apply both may and must effects, but our contexts are general
graphs with summary nodes and not trees.
Roles are similar to the ADDS and ASAP data structure
description languages [25, 26, 23]. These systems use sound
techniques to apply the data structure invariants for parallelization and general dependence testing but do not verify
that the data structure invariants are preserved by destructive updates of data structures [24].
The object-oriented community has long been aware of
benefits that dynamically changing classes give in large systems [37]. Recognizing these benefits, researchers have proposed dynamic techniques that change the class of an object
to reflect its state changes [16, 20, 4, 13]. These systems
illustrate the need for a static system that can verify the
correct use of objects with changing roles.

10

Conclusion

This paper proposes two key ideas: aliasing relationships
should determine, in large part, the state of each object,
and the type system should use the resulting object states
as its fundamental abstraction for describing procedure interfaces and object referencing relationships. We present a
role system that realizes these two key ideas in a concrete

system, and present an analysis algorithm that can verify
that the program correctly respects the constraints of this
role system. The result is that programmers can use roles
for a variety of purposes: to ensure the correctness of extended procedure interfaces that take the roles of parameters
into account, to verify important data structure consistency
properties, to express how procedures move objects between
data structures, and to check that the program correctly implements correlated relationships between the states of multiple objects. We therefore expect roles to improve the reliability of the program and its transparency to developers
and maintainers.
Note. This November 2001 version of the technical report
corrects some errors in the formal description of the analysis
algorithm of the original technical report from July 2001.

REFERENCES
[1] Thomas Ball, Rupak Majumdar, Todd Millstein, and
Sriram K. Rajamani. Automatic predicate abstraction
of C programs. In Proc. ACM PLDI, 2001.
[2] Barendsen and J. E. W. Smetsers. Conventional and
uniqueness typing in graph rewrite systems. In Proceedings of the 13th Conference on the Foundations of
Software Technology and Theoretical Computer Science.
Springer-Verlag, 1993.
[3] R. Cartwright and M. Fagan. Soft typing. In Proceedings of the ACM SIGPLAN ’91 Conference on Programming Language Design and Implementation (PLDI),
number 6 in 26, pages 278–292, 1991.
[4] Craig Chambers. Predicate classes.
ECOOP, pages 268–296, 1993.

In Proc. 7th

[5] David R. Chase, Mark Wegman, and F. Kenneth
Zadeck. Analysis of pointers and structures. In Proc.
ACM PLDI, 1990.
[6] Ramkrishna Chatterjee, Barbara G. Ryder, and
William Landi. Relevant context inference. In Proc.
26th ACM POPL, pages 133–146, 1999.
[7] Ben-Chung Cheng and Wen mei W. Hwu. Modular
interprocedural pointer analysis using access paths. In
Proc. ACM PLDI, 2000.
[8] David G. Clarke, John M. Potter, and James Noble. Ownership types for flexible alias protection. In
Proc. 13th Annual ACM Conference on Object-Oriented
Programming, Systems, Languages, and Applications,
1998.

FX

hhH, ρ, K, τ, Ei, µi −→h⊥G , µi where
FX

hhH, ρ, K, τ, Ei, µi −→ Gt where

τ [µ−1 [read(proc′ )]] 6⊆ read(proc)

τ [µ−1 [read(proc′ )]] ⊆ read(proc)
n1 ,f1

nt ,ft

hH, ρ, K, τ, Ei ⊢ G1 ⊢ · · · ⊢ Gt
S = {hn, f, n′ i ∈ H | hµ(n), f, µ(n′ )i ∈ mayWr(proc′ ) ∪ ∪i mustWri (proc′ )}
{hn1 , f1 i, . . . , hnt , ft i} = {hn, f i | hn, f, n′ i ∈ S}
Single Write Effect Instantiation:
n,f

hH1 , ρ1 , K1 , τ1 , E1 i ⊢ G′
iff
case

condition

deterministic effect

{n1 | hn, f, n1 i ∈ S} = {n0 } and
∃i : hµ(n), f, µ(n0 )i ∈ mustWri (proc′ )
|{n1 | hn, f, n1 i ∈ S}| > 1 or
∃n1 : hµ(n), f, µ(n1 )i ∈ mayWr(proc′ )
n ∈ offstage(H)
{hτ (n), f, τ (n1 )i | hn, f, n1 i ∈ S} ⊆ mayWr(proc)
|{n1 | hn, f, n1 i ∈ S}| > 1 or
∃n1 : hµ(n), f, µ(n1 )i ∈ mayWr(proc′ )
n ∈ offstage(H)
{hτ (n), f, τ (n1 )i | hn, f, n1 i ∈ S} 6⊆ mayWr(proc)
|{n1 | hn, f, n1 i ∈ S}| > 1 or
∃n1 : hµ(n), f, µ(n1 )i ∈ mayWr(proc′ )
n∈
/ offstage(H)
{hτ (n), f, τ (n1 )i | hn, f, n1 i ∈ S} ⊆ mayWr(proc)
¬({n1 | hn, f, n1 i ∈ S} = {n1 } and
∃i : hµ(n), f, µ(n0 )i ∈ mustWri (proc′ ))
n∈
/ offstage(H)
{hτ (n), f, τ (n1 )i | hn, f, n1 i ∈ S} 6⊆ mayWr(proc)

nondeterministic effect
for non-parameters

nondeterministic effect
for parameters

orem(H1 ) =



result
G′ = hH2 , ρ1 , K1 , τ1 , E2 i
H2 = H1 \ {hn, f, n1 i | hn, f, n1 i ∈ H1 }
∪{hn, f, n0 i}
E2 = updateWr(E1 , hτ (n), f, τ (n0 )i)
G′ = hH2 , ρ1 , K1 , τ1 , E2 i
H2 = orem(H1 )∪
{hn, f, n1 i | hn, f, n1 i ∈ S}
G′ = ⊥G
G′ = hH2 , ρ1 , K1 , τ1 , E2 i
H0 = H1 \ {hn, f, n1 i | hn, f, n1 i ∈ H1 }
H2 = H1 or H2 = H0 ∪ {hn, f, n1 i}
hn, f, n1 i ∈ S
G′ = ⊥G

H1 \ {hn, f, n′ i | hn, f, n′ i ∈ H1 }, if ∃i ∃n′ : hµ(n), f, µ(n′ )i ∈ mustWri (proc′ )
H1 , otherwise
Figure 30: Effect Instantiation

[9] Karl Crary, David Walker, and Greg Morrisett. Typed
memory management in a calculus of capabilities. In
Proc. 26th ACM POPL, 1999.
[10] Robert DeLine and Manuel Fähndrich. Enforcing highlevel protocols in low-level software. In Proc. ACM
PLDI, 2001.
[11] Alain Deutsch.
Interprocedural may-alias analysis
for pointers: beyond k-limiting. SIGPLAN Notices,
29(6):230–241, 1994.
[12] Amer Diwan, Kathryn McKinley, and J. Elliot B. Moss.
Type-based alias analysis. In Proc. ACM PLDI, 1998.

[25] Joseph Hummel, Laurie J. Hendren, and Alexandru
Nicolau. Abstract description of pointer data structures: An approach for improving the analysis and optimization of imperative programs. ACM Letters on
Programming Languages and Systems, 1(3), September
1993.
[26] Joseph Hummel, Laurie J. Hendren, and Alexandru
Nicolau. A language for conveying the aliasing properties of dynamic, pointer-based data structures. In
Proc. 8th International Parallel Processing Symposium,
Cancun, Mexico, April 26–29 1994.
[27] Samin Ishtiaq and Peter W. O’Hearn. BI as an assertion
language for mutable data structures. In Proc. 28th
ACM POPL, 2001.

[13] S. Drossopoulou, F. Damiani, M. Dezani-Ciancaglini,
and P. Giannini.
Fickle:
Dynamic object reclassification. In Proc. 15th ECOOP, LNCS 2072, pages
130–149. Springer, 2001.

[28] Pierre Jouvelot and David K. Gifford. Algebraic reconstruction of types and effects. In Proc. 18th ACM
POPL, 1991.

[14] Pascal Fradet and Daniel Le Metayer. Structured
gamma. Technical Report 989, IRISA, 1996.

[29] Nils Klarlund and Michael I. Schwartzbach. Graph
types. In Proc. 20th ACM POPL, Charleston, SC, 1993.

[15] Pascal Fradet and Daniel Le Métayer. Shape types. In
Proc. 24th ACM POPL, 1997.

[30] Naoki Kobayashi. Quasi-linear types. In Proc. 26th
ACM POPL, 1999.

[16] Erich Gamma, Richard Helm, Ralph Johnson, and John
Vlisside. Design Patterns. Elements of Reusable ObjectOriented Software. Addison-Wesley, Reading, Mass.,
1994.
[17] Rakesh Ghiya and Laurie Hendren. Is it a tree, a DAG,
or a cyclic graph? In Proc. 23rd ACM POPL, 1996.
[18] Rakesh Ghiya and Laurie J. Hendren. Connection analysis: A practical interprocedural heap analysis for C. In
Proc. 8th Workshop on Languages and Compilers for
Parallel Computing, 1995.
[19] Rakesh Ghiya and Laurie J. Hendren. Putting pointer
analysis to work. In Proc. 25th ACM POPL, 1998.
[20] Georg Gottlob, Michael Schrefl, and Brigitte Roeck.
Extending object-oriented systems with roles. ACM
Transactions on Information Systems, 14(3), 1994.
[21] Samuel Z. Guyer and Calvin Lin. An annotation language for optimizing software libraries. In Second Conference on Domain Specific Languages, 1999.
[22] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. The MIT Press, Cambridge, Mass., 2000.
[23] Laurie J. Hendren, Joseph Hummel, and Alexandru
Nicolau. A general data dependence test for dynamic,
pointer-based data structures. In Proc. ACM PLDI,
1994.
[24] Joseph Hummel. Data Dependence Testing in the Presence of Pointers and Pointer-Based Data Structures.
PhD thesis, Dept. of Computer Science, Univ. of California at Irvine, 1998.

[31] Viktor Kuncak. Designing an algorithm for role analysis. Master’s thesis, MIT Laboratory for Computer
Science, 2001.
[32] Tal Lev-Ami. TVLA: A framework for kleene based
logic static analyses. Master’s thesis, Tel-Aviv University, Israel, 2000.
[33] Nancy Lynch and Frits Vaandrager. Forward and backward simulations – Part I: Untimed systems. Information and Computation, 121(2), 1995.
[34] Anders Møller and Michael I. Schwartzbach. The
Pointer Assertion Logic Engine. In Proc. ACM PLDI,
2001.
[35] John Plevyak, Vijay Karamcheti, and Andrew A.
Chien. Analysis of dynamic structures for efficient parallel execution. In Workshop on Languages and Compilers for Parallel Architectures, 1993.
[36] William Pugh. Skip lists: A probabilistic alternative
to balanced trees. In Communications of the ACM
33(6):668–676, 1990.
[37] Trygve Reenskaug. Working With Objects. Prentice
Hall, 1996.
[38] Noam Rinetzky and Mooly Sagiv. Interprocedual shape
analysis for recursive programs. In Proc. 10th International Conference on Compiler Construction, 2001.
[39] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
Solving shape-analysis problems in languages with destructive updating. In Proc. 23rd ACM POPL, 1996.
[40] Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm.
Parametric shape analysis via 3-valued logic. In Proc.
26th ACM POPL, 1999.

[41] Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis problems. In Program
Flow Analysis: Theory and Applications. Prentice-Hall,
Inc., 1981.
[42] Frederick Smith, David Walker, and Greg Morrisett.
Alias types. In Proc. 9th ESOP, Berlin, Germany,
March 2000.
[43] Robert E. Strom and Daniel M. Yellin. Extending typestate checking using conditional liveness analysis. IEEE
Transactions on Software Engineering, May 1993.
[44] Robert E. Strom and Shaula Yemini. Typestate: A
programming language concept for enhancing software
reliability. IEEE Transactions on Software Engineering,
January 1986.

[45] Philip Wadler. Linear types can change the world! In
IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel, 1990.
[46] David Walker and Greg Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, 2000.
[47] Zhichen Xu, Barton Miller, and Thomas Reps. Safety
checking of machine code. In Proc. ACM PLDI, 2000.
[48] Zhichen Xu, Thomas Reps, and Barton Miller. Typestate checking of machine code. In Proc. 10th ESOP,
2001.

