Method Inlining, Dynamic Class Loading, and Type Soundness

Neal Glew, Intel Corporation
Jens Palsberg, UCLA Computer Science Department

REFEREED
ARTICLE

Abstract

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.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

		Neal Glew received a PhD in Computer Science from Cornell University in 2000 before working for InterTrust Technologies Corporation, and now Intel Corparation. He is currently a member of the Programming Systems Lab working on Managed Runtime Environments. He can be reached at aglew@acm.org.
		Jens Palsberg is a Professor of Computer Science at UCLA. His research interests span the areas of compilers, embedded systems, programming languages, software engineering, and information security. He can be reached at palsberg@ucla.edu.

Cite this article as follows: Neal Glew and Jens Palsberg: “Method Inlining, Dynamic Class Loading, and Type Soundness", in Journal of Object Technology, vol. 4, no. 8, Special Issue: ECOOP 2004 Workshop FTfJP, October 2005, pp. 33-53, http://www.jot.fm/issues/issue_2005_10/article2