Check out the new USENIX Web site.

Home About USENIX Events Membership Publications Students
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.

Last changed: 3 Jan. 2002 ml
Technical Program
JVM 2001 Home
USENIX home