Method Inlining, Dynamic Class Loading, and Type Soundness
Method Inlining, Dynamic Class Loading, and Type Soundness
复制标题
方法内联、动态类加载和类型健全性
DOI：
10.5381/jot.2005.4.8.a2
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
J. Palsberg
中科院分区：
文献类型：
--
作者：
Neal Glew;J. Palsberg
方法内联是一种优化，可以在以后的类加载中使其失效。基于当前加载的类的程序分析可能会确定方法调用具有唯一的目标，但以后的类加载可能会添加目标。如果编译器根据当前信息推测性地内联方法，那么当后面的类使假设无效时，它将不得不撤销内联。撤消内联的问题在于，优化后的代码可能在撤消时正在执行，因此需要对程序状态进行复杂的即时更新。以前的工作提供了处理无效的技术，包括堆栈上替换、预先存在分析、现有分析和代码修补。到目前为止，这类操作是否可以以类型安全的方式完成一直是一个悬而未决的问题，而且在文献中也没有正式的正确性证明。在本文中，我们提出了一个关于方法内联、动态类加载和类型可靠性的推理框架。我们的示例语言既有非优化语义，也有优化语义。在动态加载类时，优化语义执行整个程序分析，内联新加载的代码中的调用，并修补所有先前加载的代码中无效的内联。打补丁是基于一种新的构造，该构造模拟机器代码的就地更新--这是一些虚拟机用来进行推测性方法内联的技术。这两种语义是等价的，都具有类型健壮性属性--证明优化的正确性和类型安全性。我们的框架可以形成以类型化低级语言表示优化代码的虚拟机的基础。
Method inlining is an optimisation that can be invalidated by later class loading. A program analysis based on the current loaded classes might determine that a method call has a unique target, but later class loading could add targets. If a compiler speculatively inlines methods based on current information, then it will have to undo the inlining when later classes invalidate the assumptions. The problem with undoing inlining is that the optimised code might be executing at the time of undo and therefore require a complicated, on-the-fly update of the program state. Previous work presented techniques for dealing with invalidation including on-stack replacement, preexistence analysis, extant analysis, and code patching. Until now, it has been an open question whether such operations can be done in a type-safe manner, and no formal proof of correctness exists in the literature. In this paper we present a framework for reasoning about method inlining, dynamic class loading, and type soundness. Our example language has both a nonoptimising and an optimising semantics. At the point of dynamically loading a class, the optimising semantics does a whole-program analysis, inlines calls in the newly loaded code, and patches the invalidated inlinings in all previously loaded code. The patching is based on a new construct that models in-place update of machine code—a technique used by some virtual machines to do speculative method inlining. The two semantics are equivalent and both have a type soundness property—proving correctness and type safety of the optimisation. Our framework can form the basis of virtual machines that represent optimised code in a typed low-level language.