用抽象解释推导逃逸分析：结果证明
Deriving Escape Analysis by Abstract Interpretation: Proofs of results
摘要：
面向对象语言的逃逸分析近似于不从给定上下文逃逸的对象集。如果我们把一个方法作为上下文，非转义对象可以在它的激活堆栈上分配;如果我们把一个线程作为上下文，那么就不需要在这些对象上使用Java同步锁。在本文中，我们形式化的基本逃逸域E作为一个抽象的解释具体的国家，我们然后细化到一个抽象的域ER比E更具体，因此，导致更精确的逃逸分析比E。我们提供的最优性结果为E和ER，在形式的伽罗瓦插入从具体的抽象域和最佳的抽象操作。伽罗瓦插入属性是通过使用抽象垃圾收集器将抽象域限制为不包含垃圾的那些元素而获得的。因此，我们实现的er是一个正式正确的转义分析器的实现，能够检测Java（字节码）应用程序的堆栈可分配创建点。这份报告包含了一篇论文的结果的证明，该论文具有相同的标题和作者，并将发表在《高阶符号计算》杂志上。
英文摘要：
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. This report contains the proofs of results of a paper with the same title and authors and to be published in the Journal "Higher-Order Symbolic Computation".
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
