通过抽象解释推导逃逸分析：结果的证明
编程语言
2007-05-23 v2
摘要
面向对象语言的逃逸分析approximates 从给定上下文中不逃逸的对象集合。如果将方法作为上下文，非逃逸对象可以在其激活堆栈上分配；如果将线程作为上下文，则无需对此类对象建立 Java synchronisation locks。本文形式化了一个基本的逃逸域 e 作为具体状态的抽象解释，然后将其细化为更具体于 e 的抽象域 er，从而导致比 e 更精确的逃逸分析。我们为 e 和 er 提供了最优性结果，形式为从具体域到抽象域的 Galois 插入，以及最优抽象操作。通过限制抽象域以排除不含垃圾的元素，获得 Galois 插入属性，这通过使用抽象垃圾收集器实现。我们的 er 实现因此是对形式上正确的逃逸分析器的实现，能够检测 Java (bytecode) 应用程序中可堆栈分配的创建点。本报告包含与相同标题和作者的论文所述结果的证明，该论文将被发表于期刊 "Higher-Order Symbolic Computation"。
引用
@article{arxiv.cs/0607101,
title = {Deriving Escape Analysis by Abstract Interpretation: Proofs of results},
author = {Patricia M. Hill and Fausto Spoto},
journal= {arXiv preprint arXiv:cs/0607101},
year = {2007}
}