|
JVM 2001 Abstract
An Executable Formal Java Virtual Machine Thread Model
J Strother Moore and George M. Porter, University of Texas at Austin
Abstract
We discuss an axiomatic description of a simple abstract machine similar to
the Java Virtual Machine (JVM). Our model supports classes,
with fields and bytecoded methods, and a representative sampling of
JVM bytecodes for basic operations for both data and control. The
GETFIELD and PUTFIELD instructions accurately model
inheritance, as does the INVOKEVIRTUAL instruction. Our model
supports multiple threads, synchronized methods, and monitors. Our
current model is inadequate or inaccurate in many respects (e.g., we
do not formalize the JVM's finite arithmetic nor do we describe class
loading and initialization). But the model is a useful tool for
studying the application of formal reasoning to the JVM and to Java
programs.
We demonstrate two useful aspects of an operational formal semantics. First,
the model is executable: bytecoded methods can be run on the model. Second,
the model allows us to prove theorems about those methods or, more generally,
about the model. Because the JVM provides a relatively clean semantics for
Java, our model can be thought of as a step towards Java software
verification. We illustrate these points. We cite some
theorems proved about our model, including a theorem involving unbounded
multi-threading and mutual exclusion with MONITORENTER and
MONITOREXIT. Our proofs are carried out with the ACL2 theorem
prover.
- View the full text of this paper in
HTML form, and
PDF form.
- If you need the latest Adobe Acrobat Reader, you can download it from Adobe's site.
- To become a USENIX Member, please see our Membership Information.
|
Need help? Use our Contacts page.
