BlanchetPOPL98

Bruno Blanchet Back to publications
Bruno Blanchet. Escape Analysis: Correctness Proof, Implementation and Experimental Results. In 25th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL'98), pages 25-37, San Diego, California, January 1998. ACM Press.

Copyright

Copyright © 1998 by the Association for Computing Machinery, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1(212)869-0481, or permissions@acm.org.

If you agree with this copyright notice, you can get the paper:

Get the paper

.ps.gz, 127 Kb

Links

Official ACM version (you can download the full text from there):

ACM DL Author-ize serviceEscape analysis: correctness proof, implementation and experimental results
Bruno Blanchet
POPL '98 Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1998

Abstract

We describe an escape analysis, used to determine whether the lifetime of data exceeds its static scope.

We give a new correctness proof starting directly from a semantics. Contrary to previous proofs, it takes into account all the features of functional languages, including imperative features and polymorphism. The analysis has been designed so that it can be implemented under the small complexity bound of O(n log2 n) where n is the size of the analyzed program. We have included it in the Caml Special Light compiler (an implementation of ML), and applied it to very large programs. We plan to apply these techniques to the Java programming language.

Escape analysis has been applied to stack allocation. We improve the optimization technique by determining minimal lifetime for stack allocated data, and using inlining. We manage to stack allocate 25% of data in the theorem prover Coq. We analyzed the effect of this optimization, and noticed that its main effect is to improve data locality, which is important for efficiency.

Bibtex


@INPROCEEDINGS{BlanchetPOPL98,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Escape {A}nalysis: Correctness {P}roof, {I}mplementation
		  and {E}xperimental {R}esults},
  BOOKTITLE = {25th ACM SIGACT-SIGPLAN Symposium on Principles of
		  Programming Languages (POPL'98)},
  YEAR = 1998,
  PUBLISHER = {ACM Press},
  ADDRESS = {San Diego, California},
  MONTH = JAN,
  PAGES = {25--37}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)