JavaMemoryModel: A new JMM specification framework

From: Yue Yang (yyang@cs.utah.edu)
Date: Wed Apr 24 2002 - 13:53:24 EDT


Hello everyone,

We would like to announce that at University of Utah, we have
developed a new specification framework called Uniform Memory
Model (UMM).

UMM is a generic framework for specifying and verifying both
architectural level and language level memory consistency requirements.
In particular, the Java Memory Model (JMM), primarily based on
the semantics proposed by Jeremy and Bill, has been formally specified
and analyzed in UMM. Subtle mistakes from the original proposal have
been revealed using this approach.

This work is summarized in our recent paper "Formalizing the Java
Memory Model for Multithreaded Program Correctness and Optimization",
which is submitted for publication and also available as Technical
Report UUCS-02-011. The paper can be found at
http://www.cs.utah.edu/~yyang/research.

*** An Overview of UMM ***

UMM defines a memory model using a transition system based on thread
local instruction buffers and a global instruction buffer. It specifies
all memory operations as events. The conditions and actions of these
memory events can be easily configured to capture different shared
memory semantics into a formal executable specification. The UMM
prototype has been implemented in Murphi, a description language and
model checking tool, to facilitate verification.

There are three major characteristics for UMM:

1) UMM provides strong built-in support for formal verification and
program analysis.

Our previous analysis of the CRF JMM, which can also be found at
http://www.cs.utah.edu/~yyang/research, has demonstrated that formal
methods such as model checking are feasible and effective techniques for
understanding a language level memory model specified in an executable
style. Following the same methodology, UMM uses an operational
specification format based on guarded commands that allows it to be
easily integrated with a model checking utility.

UMM also addresses the special need from the JMM by including local
variable state information into the global transition system.
This reduces the gap between memory semantics and program semantics and
allows one to specify the JMM at Java byte code level as well as the
source program level. In addition, thread local data dependency is
explicitly defined as precise mathematical rules, which enables one to
study the memory model implications in the context of data flow analysis.

2) UMM is very flexible.

The architecture of UMM is not restricted by any architectural or memory
model specific designs. Therefore, it is generic enough to describe
different memory model requirements.

3) UMM is simple and intuitive.

The data structures applied in UMM, such as instruction buffers and
arrays, are standard devices that are easy for one to understand.
Similar notations have been used in processor memory model
descriptions, making this framework intuitive to most hardware designers.

Although the details of UMM might still require some fine-tuning, we
hope this framework can bring positive contributions to the Java
Community process of revising the JMM.

Your comments and suggestions will be very appreciated!

Jason Yang

School of Computing
University of Utah

-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel



This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:39 EDT