Article

Free access

Towards array bound check elimination in Java ^TM virtual machine language

Authors:

Songtao XiaAuthors Info & Claims

CASCON '99: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research

Page 14

Published: 08 November 1999 Publication History

Abstract

In a standard Java implementation, a Java program is compiled into Java bytecode, which is then interpreted by Java virtual machine (JVM). We refer to the bytecode language as Java virtual machine language in this paper. for safety concerns, JVM performs run-time array bounds checking to detect out-of-bounds array access. Unfortunately, this practice can be prohibitively expensive in cases involving numerical computation.We propose a type-theoretic approach to eliminating run-time array bound checks in JVML and demonstrate that the property of safe array access can be readily captured with a restricted form of dependent type system and therefore enforced through type-checking. We focus on a language JVMLa, which is basically a subset of JVML with array access instructions, and prove that the execution of a well-typed JVMLa program can never cause memory violations.

References

[1]

{1} David Detlefs. An overview of the extended static checking system. In Workshop in formal Methods in Software Practice, 1996.]]

[2]

{2} Stephen N. Freund and John C. Mitchell. A Type System for Object Initialization in the JavaTM Bytecode Language. In Proceedings of ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Application, pages 310-327, Vancouver, 1998.]]

[3]

{3} R. Gupta. Optimizing array bound checks using flow analysis. ACM Letters on Programming Languages and Systems, 2(1-4):135-150, 1994.]]

Digital Library

[4]

{4} Ishizaki et al. Design, Implementation and Evaluation of Optimizations in Just-in-time Compiler. In Proceedings of ACM Java Grande, 1999.]]

Digital Library

[5]

{5} Pryadarshan Kolte and Michael Wolfe. Elimination of redundant array subscript checks. In ACM SIGPLAN '95 Conference on Programming Language Design and Implementation . ACM Press, June 1995.]]

Digital Library

[6]

{6} S. P. Midkiff, J. E. Moreira, and M. Snir. Optimizing array reference checking in Java programs, 1998. Available as http://www.almaden.ibm.com/journal/sj /373/midkiff.txt]]

Digital Library

[7]

{7} Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In Proceedings of Workshop on Types in Compilation, March 1998.]]

Digital Library

[8]

{8} Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From system F to typed assembly language. In Proceedings of ACM Symposium on Principles of Programming Languages, pages 85-97, January 1998.]]

Digital Library

[9]

{9} G. Necula and P. Lee. The design and implementation of a certifying compiler. In ACM SIGPLAN '98 Conference on Programming Language Design and Implementation, pages 333-344. ACM press, June 1998.]]

Digital Library

[10]

{10} George Necula. Proof-carrying code. In Conference Record of 24th Annual ACM Symposium on Principles of Programming Languages, pages 106-119. ACM press, 1997.]]

Digital Library

[11]

{11} Robert O'Callahan. A simple, Comprehensive type system for Java bytecode subrontines. In Proceedings of ACM SIGPLAN Symposium on Principles of Programming Languages, pages 70-78, San Antonio, January 1999.]]

Digital Library

[12]

{12} Zhenyu Qian. A formal specification of Java Virtual Machine instructions for objects, methods and subroutines. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java. Springer-Verlag, 1998.]]

Digital Library

[13]

{13} Raymie Stata and Martín Abadi. A type system for java bytecode subroutines. In Proceedings of the 25th ACM Symposium on Principles of Programming Languages, pages 149-160, January 1998.]]

Digital Library

[14]

{14} Sun Microsystems. The Java language specification, 1995. Available as ftp://ftp.javasoft.com/docs/ javaspec.ps.zip]]

[15]

{15} Tim Lindholm and Frank Yellin. The Java virtual machine specification. Andison-Wesley, 1996.]]

Digital Library

[16]

{16} Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 249-257, Montreal, June 1998.]]

Digital Library

[17]

{17} Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proceedings of ACM SIGPLAN Symposium on Principles of programming Languages, pages 214-227, San Antonio, January 1999.]]

Digital Library

[18]

{18} Hongwei Xi and Robert Harper. A Dependently Typed Assembly Language. Technical Report CSE-99-008, Oregon Graduate Institute, July 1999.]]

Digital Library

[19]

{19} Hongwei Xi and Songtao Xia. Some examples in JVMLa, 1999. Available as http://www.cse.ogi.edu/~hongwei/JVMLa]]

[20]

{20} Hongwei Xi and Songtao Xia. Towards array bound check elimination in JavaTM virtual machine language, 1999. Available as http://www.cse.ogi.edu/~hongwei/ academic/papers/JVMLa.ps]]

Cited By

Demange DJensen TPichardie D(2010)A provably correct stackless intermediate representation for Java bytecodeProceedings of the 8th Asian conference on Programming languages and systems10.5555/1947873.1947884(97-113)Online publication date: 28-Nov-2010
https://dl.acm.org/doi/10.5555/1947873.1947884
Besson FJensen TPichardie DTurpin T(2010)Certified result checking for polyhedral analysis of bytecode programsProceedings of the 5th international conference on Trustworthly global computing10.5555/1893701.1893722(253-267)Online publication date: 24-Feb-2010
https://dl.acm.org/doi/10.5555/1893701.1893722
Chiueh T(2008)Fast bounds checking using debug registerProceedings of the 3rd international conference on High performance embedded architectures and compilers10.5555/1786054.1786066(99-113)Online publication date: 27-Jan-2008
https://dl.acm.org/doi/10.5555/1786054.1786066
Show More Cited By

Index Terms

Towards array bound check elimination in Java ^TM virtual machine language
1. Software and its engineering
  1. Software notations and tools
    1. Compilers
      1. Interpreters
      2. Source code generation
    2. General programming languages
      1. Language types

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image DL Hosted proceedings

CASCON '99: Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research

November 1999

186 pages

Sponsors

IBM Canada: IBM Canada
NRC: National Research Council - Canada

Publisher

IBM Press

Publication History

Published: 08 November 1999

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 24 of 90 submissions, 27%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
841
Total Downloads

Downloads (Last 12 months)523
Downloads (Last 6 weeks)42

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Demange DJensen TPichardie D(2010)A provably correct stackless intermediate representation for Java bytecodeProceedings of the 8th Asian conference on Programming languages and systems10.5555/1947873.1947884(97-113)Online publication date: 28-Nov-2010
https://dl.acm.org/doi/10.5555/1947873.1947884
Besson FJensen TPichardie DTurpin T(2010)Certified result checking for polyhedral analysis of bytecode programsProceedings of the 5th international conference on Trustworthly global computing10.5555/1893701.1893722(253-267)Online publication date: 24-Feb-2010
https://dl.acm.org/doi/10.5555/1893701.1893722
Chiueh T(2008)Fast bounds checking using debug registerProceedings of the 3rd international conference on High performance embedded architectures and compilers10.5555/1786054.1786066(99-113)Online publication date: 27-Jan-2008
https://dl.acm.org/doi/10.5555/1786054.1786066
Würthinger TWimmer CMössenböck HAmaral V(2007)Array bounds check elimination for the Java HotSpot™ client compilerProceedings of the 5th international symposium on Principles and practice of programming in Java10.1145/1294325.1294343(125-133)Online publication date: 5-Sep-2007
https://dl.acm.org/doi/10.1145/1294325.1294343
Barthe GDufay G(2005)Formal methods for smartcard securityFoundations of Security Analysis and Design III10.5555/2137760.2137767(133-177)Online publication date: 1-Jan-2005
https://dl.acm.org/doi/10.5555/2137760.2137767
Bentley CWatterson SLowenthal DRountree BFeautrier PGoodman JSeznec A(2004)Implicit java array bounds checking on 64-bit architectureProceedings of the 18th annual international conference on Supercomputing10.1145/1006209.1006242(227-236)Online publication date: 26-Jun-2004
https://dl.acm.org/doi/10.1145/1006209.1006242

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents