To study the properties of the Java Virtual Machine(JVM)
and Java programs, our research group has produced a
series of JVM models written in a functional subset of
Common Lisp. In this paper, we present our most complete
JVM model from this series, namely, M6, which is derived
from a careful study of the J2ME KVM implementation.
On the one hand, our JVM model is a conventional machine
emulator. M6 models accurately almost all aspects of the KVM
implementation, including the dynamic class loading, class
initialization and synchronization via monitors. It executes
most J2ME Java programs that do not use any I/O or floating
point operations. Engineers may consider M6 an
implementation of the JVM. It is implemented with around 10K
lines in 20+ modules. Source code is online:
http://www.cs.utexas.edu/users/hbl/pub/M6/ivme03/
On the other hand, M6 is a novel model that allows for
analytical reasoning besides conventional testing. M6 is
written in an applicative (side-effect free) subset of
Common Lisp, for which we have given precise meaning in
terms of axioms and inference rules. A property of M6 can
be expressed as a formula. Rules of interference can be
used analytically to derive properties of M6 and the Java
programs that run on the model, using a mechanical theorem
prover.
We argue that our approach of building an executable model
of the system with an axiomatically described functional
language can bring benefits from both the testing and the
formal reasoning worlds.
