Towards Array Bound Check Elimination in Java Virtual Machine Language

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. 1 Introduction Java is an object-oriented programming language designed to support multiple host architectures and allow..