Designing an Algorithm for Role Analysis

paper ps   
This thesis presents a system for specifying constraints on dynamically changing referencing relationships of heap objects, and an analysis for static verification of these constraints. The constraint specification system is based on the concept of role. 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. In this way roles capture object and data structure properties such as unique references, membership of objects in data structures, disjointness of data structures, absence of representation exposure, bidirectional associations, treeness, and absence or presence of cycles in the heap. Roles generalize linear types by allowing multiple aliases of heap objects that participate in recursive data structures. Unlike graph grammars and graph types, roles contain sufficiently general constraints to conservatively approximate any data structure. We give a semantics for mutually recursive role definitions and derive properties of roles as an invariant specification language. We introduce a programming model that allows temporary violations of role constraints. We describe a static role analysis for verifying that a program conforms to the programming model. The analysis uses fixpoint computation to synthesize loop invariants in each procedure. We introduce a procedure interface specification language and its semantics. We present an interprocedural, compositional, and context-sensitive role analysis that verifies that a program respects the role constraints across procedure calls.

Citation

Viktor Kuncak. Designing an algorithm for role analysis. Master's thesis, MIT LCS, 2001.

BibTex Entry

@mastersthesis{Kuncak01DesigningRoleAnalysis,
  author = {Viktor Kuncak},
  title = {Designing an Algorithm for Role Analysis},
  school = {MIT LCS},
  year = 2001,
  abstract = {
This thesis presents a system for specifying constraints on
dynamically changing referencing relationships of heap
objects, and an analysis for static verification of these
constraints.  The constraint specification system is based
on the concept of role.  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.  In this way roles capture
object and data structure properties such as unique
references, membership of objects in data structures,
disjointness of data structures, absence of representation
exposure, bidirectional associations, treeness, and absence
or presence of cycles in the heap.

Roles generalize linear types by allowing multiple aliases
of heap objects that participate in recursive data
structures.  Unlike graph grammars and graph types, roles
contain sufficiently general constraints to conservatively
approximate any data structure.

We give a semantics for mutually recursive role definitions
and derive properties of roles as an invariant specification
language.  We introduce a programming model that allows
temporary violations of role constraints.  We describe a
static role analysis for verifying that a program conforms
to the programming model.  The analysis uses fixpoint
computation to synthesize loop invariants in each procedure.

We introduce a procedure interface specification language
and its semantics.  We present an interprocedural,
compositional, and context-sensitive role analysis that
verifies that a program respects the role constraints across
procedure calls.
}
}