View Full Document

Type-Preserving Compilation of Featherweight Java



View the full content.
View Full Document
View Full Document

8 views

Unformatted text preview:

Type Preserving Compilation of Featherweight Java CHRISTOPHER LEAGUE ZHONG SHAO and VALERY TRIFONOV Yale University We present an efficient encoding of core Java constructs in a simple implementable typed intermediate language The encoding after type erasure has the same operational behavior as a standard implementation using vtables and self application for method invocation Classes inherit super class methods with no overhead We support mutually recursive classes while preserving separate compilation Our strategy extends naturally to a significant subset of Java including interfaces and privacy The formal translation using Featherweight Java allows comprehensible type preservation proofs and serves as a starting point for extending the translation to new features Our work provides a foundation for supporting certifying compilation of Java like classbased languages in a type theoretic framework Categories and Subject Descriptors D 3 4 Programming Languages Processors Compilers F 3 3 Logic and Meanings of Programs Studies of Program Constructs Object Oriented Constructs General Terms Languages Verification Additional Key Words and Phrases Java object encodings type systems typed intermediate languages 1 INTRODUCTION Many compilation techniques for functional languages focus on type directed compilation Peyton Jones et al 1992 Shao and Appel 1995 Morrisett et al 1996 Source level types are transformed along with the program and then used to guide and justify advanced optimizations More generally types preserved throughout compilation can be used to reason about the safety and security of object code Necula and Lee 1996 Necula 1997 Morrisett et al 1999 Type preserving compilers typically use variants of the polymorphic typed calculus F Girard 1972 Reynolds 1974 as their intermediate representations Much is known about optimizing F programs Tarditi et al 1996 about compiling them to machine code Morrisett et al 1999 and about implementing the F type system efficiently in a production compiler Shao et al 1998 Recently several researchers have attempted to apply these techniques to objectoriented languages Wright et al 1998 Crary 1999 League et al 1999 Vanderwaart 1999 Glew 2000a League et al 2001b While there is significant precedent for This work was sponsored in part by DARPA OASIS grant F30602 99 1 0519 NSF grant CCR9901011 and NSF ITR grant CCR 0081590 Any opinions findings and conclusions contained in this document are those of the authors and do not reflect the views of these agencies Authors addresses Department of Computer Science Yale University P O Box 208285 New Haven CT 06511 USA email league shao trifonov cs yale edu Permission to make digital hard copy of all or part of this material without fee for personal or classroom use provided that the copies are not made or distributed for profit or commercial advantage the ACM copyright server notice the title of the publication and its date appear and notice is given that copying is by permission of the ACM Inc To copy otherwise to republish to post on servers or to redistribute to lists requires prior specific permission and or a fee ACM Transactions on Programming Languages and Systems Vol TBD No TDB Month Year Pages 1 39 2 Christopher League et al encoding object oriented languages in typed calculi Canning et al 1989 Bruce 1994 Eifrig et al 1995 Abadi et al 1996 Bruce et al 1999 type preserving compilation alters the requirements in some fundamental ways The intermediate language must provide simple orthogonal primitives that are amenable to optimization If method invocation is an atomic primitive for example then we cannot safely optimize a sequence of calls on the same object Furthermore we must avoid introducing any dynamic overhead solely to achieve static typing One can often for example simplify a type system by adding coercion functions or extra indirections but these techniques have associated run time penalties The machinery used to achieve static typing should be erasable meaning that it can be discarded after verification without affecting execution Given these constraints the type system for the intermediate language should be as simple as possible Type checking must be not only decidable but efficient in practice Typed compilation generally places greater demands on the implementation of a type system than does a simple type checker for a source language On the other hand at the level of the intermediate language we can add more detailed and explicit type annotations than a source level programmer might accept With respect to object encodings for example subsumption is not necessarily required it can be replaced with explicit coercions as long as their run time cost is nil Finally a type preserving compiler should where possible maintain source level abstractions Source language type systems enforce certain abstractions such as private fields and restricted interfaces which could be eliminated in a translation without compromising type safety This is dangerous if the translated code will be linked with other code perhaps translated from a different source language Linktime type checking will not prevent for example one module from accessing the private fields of another unless the abstractions are preserved in the object code We have developed techniques for compiling a significant subset of Java into a simple and efficient typed intermediate language League et al 1999 2001b Method invocation after type erasure has the same operational behavior as a standard implementation of self application using vtables per class tables of functions Classes inherit or override methods from super classes with no overhead By pairing an object with a particular view whenever it is cast to an interface type interface calls are no more expensive than ordinary method calls We support mutually recursive classes at the type and term level while still maintaining separate compilation Dynamic casts and instance of queries are implemented as polymorphic methods using tags generated at link time Private fields can be hidden from outsiders using existential types Ours is the first efficient encoding of a class based language into F without subtyping or bounded quantification Glew 2000a compiles a simple class based calculus using F bounded quantification It is not known whether this feature is practical in a production compiler since the type checker must infer derivations of the subtyping judgments Fisher and Mitchell 1998 use


Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Type-Preserving Compilation of Featherweight Java and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Type-Preserving Compilation of Featherweight Java and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?