通过抽象解释推导逃逸分析：结果的证明
摘要：对象导向语言的逃逸分析近似计算给定上下文中不逃逸的对象集合。如果我们将一个方法作为上下文，那么非逃逸对象可以分配在其活动栈上；如果我们将一个线程作为上下文，那么Java同步锁对于这些对象是不需要的。在本文中，我们将一个基本的逃逸域e形式化为具体状态的抽象解释，并将其进一步细化为比e更具体的抽象域er，从而比e提供更精确的逃逸分析。我们提供了e和er的优化结果，即从具体域到抽象域的Galois插入和最优抽象操作。通过使用抽象垃圾收集器将抽象域限制为不包含垃圾的元素，我们获得了Galois插入属性。因此，我们的er的实现是一个正式正确的逃逸分析器的实现，能够检测Java（字节码）应用程序的堆栈可分配的创建点。 《Higher-Order Symbolic Computation》杂志将发表同名且同作者的论文的证明。
作者：Patricia M. Hill, Fausto Spoto
论文ID：cs/0607101
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23