School Homepage

Deriving Escape Analysis by Abstract Interpretation

Patricia M. Hill
School of Computing
The University of Leeds
Leeds LS2 9JT
England

Fausto Spoto
Dipartimento Scientifico e Tecnologico
Strada Le Grazie
15 Ca' Vignal
37134 Verona
Italy

Abstract:

Escape analysis of object-oriented languages determines, for every program point, the creation points of the objects reachable from the variables. This information allows us to stack allocate dynamically created objects and to reduce the overhead of synchronisation in Java-like languages. In this paper, we formalise the escape property E, computed by an escape analysis, as an abstract interpretation of concrete states. We show that it interacts with the static type information and with the late-binding mechanism. A static analysis based on the domain E can only be very imprecise. Therefore, we define a refinement ER of E, in the sense that ER is more concrete than E and, hence, leads to a more precise escape analysis than E. Our implementation of ER is a formally correct escape analyser, able to detect the stack allocatable creation points of middle-size Java (bytecode) applications.

Keywords: Semantics, static analysis, abstract interpretation, garbage collection.