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

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.

[ bib ] Back