DOC PREVIEW
Type-Preserving Compilation of Featherweight Java

This preview shows page 1-2-3-18-19-37-38-39 out of 39 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 39 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

Type-Preserving Compilation of Featherweight JavaCHRISTOPHER LEAGUE, ZHONG SHAO, and VALERY TRIFONOVYale UniversityWe present an efficient encoding of core Java constructs in a simple, implementable typed in-termediate language. The encoding, after type erasure, has the same operational behavior as astandard implementation using vtables and self-application for method invocation. Classes inheritsuper-class methods with no overhead. We support mutually recursive classes while preservingseparate compilation. Our strategy extends naturally to a significant subset of Java, includinginterfaces and privacy. The formal translation using Featherweight Java allows comprehensi-ble type-preservation proofs and serves as a starting point for extending the translation to newfeatures. Our work provides a foundation for supporting certifying compilation of Java-like class-based 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-OrientedConstructsGeneral Terms: Languages, VerificationAdditional Key Words and Phrases: Java, object encodings, type systems, typed intermediatelanguages1. INTRODUCTIONMany compilation techniques for functional languages focus on type-directed com-pilation [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 guideand justify advanced optimizations. More generally, types preserved throughoutcompilation can be used to reason about the safety and security of object code [Nec-ula 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 compilingthem to machine code [Morrisett et al. 1999], and about implementing the Fωtypesystem efficiently in a production compiler [Shao et al. 1998].Recently, several researchers have attempted to apply these techniques to object-oriented languages [Wright et al. 1998; Crary 1999; League et al. 1999; Vanderwaart1999; Glew 2000a; League et al. 2001b]. While there is significant precedent forThis work was sponsored in part by DARPA OASIS grant F30602-99-1-0519, NSF grant CCR-9901011, and NSF ITR grant CCR-0081590. Any opinions, findings, and conclusions containedin 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, CT06511 USA; email: {league, shao, trifonov}@cs.yale.edu.Permission to make digital/hard copy of all or part of this material without fee for personalor classroom use provided that the copies are not made or distributed for profit or commercialadvantage, the ACM copyright/server notice, the title of the publication, and its date appear, andnotice 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; Bruce1994; Eifrig et al. 1995; Abadi et al. 1996; Bruce et al. 1999], type-preservingcompilation alters the requirements in some fundamental ways. The intermediatelanguage must provide simple, orthogonal primitives that are amenable to opti-mization. If method invocation is an atomic primitive, for example, then we cannotsafely optimize a sequence of calls on the same object. Furthermore, we must avoidintroducing any dynamic overhead solely to achieve static typing. One can often,for example, simplify a type system by adding coercion functions or extra indirec-tions, but these techniques have associated run-time penalties. The machinery usedto achieve static typing should be erasable, meaning that it can be discarded afterverification without affecting execution.Given these constraints, the type system for the intermediate language should beas simple as possible. Type checking must be not only decidable, but efficient inpractice. Typed compilation generally places greater demands on the implementa-tion of a type system than does a simple type checker for a source language. Onthe other hand, at the level of the intermediate language, we can add more detailedand explicit type annotations than a source-level programmer might accept. Withrespect 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-levelabstractions. Source language type systems enforce certain abstractions (such asprivate fields and restricted interfaces) which could be eliminated in a translationwithout compromising type safety. This is dangerous if the translated code will belinked with other code, perhaps translated from a different source language. Link-time type checking will not prevent, for example, one module from accessing theprivate 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 sim-ple and efficient typed intermediate language [League et al. 1999; 2001b]. Methodinvocation, after type erasure, has the same operational behavior as a standard im-plementation of self application using vtables (per-class tables of functions). Classesinherit or override methods from super classes with no overhead. By pairing an ob-ject with a particular view whenever it is cast to an interface type, interface callsare no more expensive than ordinary method calls. We support mutually recursiveclasses (at the type and term level) while still maintaining separate compilation.Dynamic casts and instance-of queries are implemented as polymorphic methodsusing tags generated at link-time. Private fields can be hidden from outsiders usingexistential types.Ours is the first efficient encoding of a class-based language into Fωwithoutsubtyping or bounded quantification. Glew [2000a] compiles a simple class-basedcalculus using F-bounded quantification. It is not known whether this feature


Type-Preserving Compilation of Featherweight Java

Download Type-Preserving Compilation of Featherweight Java
Our administrator received your request to download this document. We will send you the file to your email shortly.
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 2 2 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?