[Prev][Next][Index][Thread]

Paper on the Java Virtual Machine is available

The paper:

A Specification of Java Loading and Bytecode Verification

is available at

http://www.kestrel.edu/~goldberg/Bytecode.html


Abstract:

This paper gives a mathematical specification the Java Virtual Machine
(JVM) bytecode verifier. The specification is an axiomatic description
of the verifier that makes precise subtle aspects of the JVM semantics
and the verifier. We focus on the use of data flow analysis to verify
type-correctness and the use of typing contexts to insure global type
consistency in the context of an arbitrary strategy for dynamic class
loading. The specification types interfaces with sufficient accuracy
to eliminate run-time type checks. Our approach is to specify a
generic dataflow architecture and formalize the JVM verifier as an
instance of this architecture. The emphasis in this paper is on
readability of the specification and mathematical clarity. The
specification given is consistent with the descriptions in Lindholm
and Yellin, The Java Virtual Machine Specification. It less committed
to certain implementation choices than the Sun version 1.1
implementation. In particular, the specification does not commit an
implementation to any loading strategy, and detects all type errors as
early as possible.  This paper gives a mathematical specification the
Java Virtual Machine (JVM) bytecode verifier. The specification is an
axiomatic description of the verifier that makes precise subtle
aspects of the JVM semantics and the verifier. We focus on the use of
data flow analysis to verify type-correctness and the use of typing
contexts to insure global type consistency in the context of an
arbitrary strategy for dynamic class loading. The specification types
interfaces with sufficient accuracy to eliminate run-time type
checks. Our approach is to specify a generic dataflow architecture and
formalize the JVM verifier as an instance of this architecture. The
emphasis in this paper is on readability of the specification and
mathematical clarity. The specification given is consistent with the
descriptions in Lindholm and Yellin, The Java Virtual Machine
Specification. It less committed to certain implementation choices
than the Sun version 1.1 implementation. In particular, the
specification does not commit an implementation to any loading
strategy, and detects all type errors as early as possible.