Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java synchronisation locks on such objects are not needed. In this paper, we formalise a basic escape domain E as an abstract interpretation of concrete states, which we then refine into an abstract domain ER which is more concrete than E and, hence, leads to a more precise escape analysis than E. We provide optimality results for both E and ER, in the form of Galois insertions from the concrete to the abstract domains and of optimal abstract operations. The Galois insertion property is obtained by restricting the abstract domains to those elements which do not contain garbage, by using an abstract garbage collector. Our implementation of ER is hence an implementation of a formally correct escape analyser, able to detect the stack allocatable creation points of Java (bytecode) applications.

Deriving Escape Analysis by Abstract Interpretation

SPOTO, Nicola Fausto
2006-01-01

Abstract

Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java synchronisation locks on such objects are not needed. In this paper, we formalise a basic escape domain E as an abstract interpretation of concrete states, which we then refine into an abstract domain ER which is more concrete than E and, hence, leads to a more precise escape analysis than E. We provide optimality results for both E and ER, in the form of Galois insertions from the concrete to the abstract domains and of optimal abstract operations. The Galois insertion property is obtained by restricting the abstract domains to those elements which do not contain garbage, by using an abstract garbage collector. Our implementation of ER is hence an implementation of a formally correct escape analyser, able to detect the stack allocatable creation points of Java (bytecode) applications.
2006
Escape analysis; static analysis; abstract interpretation; object-oriented languages
File in questo prodotto:
File Dimensione Formato  
DerivingEscapeAnalysis.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 1.3 MB
Formato Adobe PDF
1.3 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/32040
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact