I'd like to give you an update about our effort of specifying the JMM
using our uniform memory model specification framework (UMM), a simple and
flexible system for capturing memory consistency properties.
The paper describing our approach, "Specifying Java Thread Semantics Using
a Uniform Memory Model", is going to appear in the Joint ACM Java
Grande/ISCOPE Conference in November (co-located with OOPSLA.)
Our paper is available at http://www.cs.utah.edu/~yyang/research/umm.pdf.
The executable Murphi implementation of our formal specification is
available at http://www.cs.utah.edu/~yyang/research/umm.m.
We would like to invite you to take a quick look at our paper (now it's
only 10 pages) and tell us what you like and dislike about our
approach. The final paper is going to be due around Aug 15. So it would be
especially helpful if we can hear from you soon.
***
For those of you who are not familiar with UMM, here's a quick overview:
A two-layer architecture, based on local and global instruction buffers,
is used to store thread local information and global trace information. A
bypassing table explicitly specifies how program order can be relaxed by a
memory model, which enables certain interleaving such as prescient
writes. The requirement of serialization is applied to an execution trace
following proper visibility orders to filter our illegal results. Using
this abstraction, variations between memory models can be isolated into a
few well-defined places such as the bypassing table and the visibility
ordering rules, enabling easy comparison and configuration. Semantics for
local variable operations that are related to the memory system is also
defined. This enables the source level specification of JMM and it also
helps people distinguish program semantics and memory semantics. A
guarded-command specification style is used to allow easy integration of
the model checking technique.
Compared with our earlier report of this work (available as tech report
UUCS-02-01), major changes are:
* Since the consensus of the ordering requirement for volatiles has not
been reached and it is still not clear what will eventually be used by the
future JMM, we define volatile variable operations based on Sequential
Consistency in this paper, which does not affect the presentation of our
general approach. A version supporting non-atomic volatile writes is still
implemented in the Murphi executable model.
* The bypassing table is adjusted to support our recent understanding of
Bill and Jeremy's proposed semantics for prescient writes.
* The equivalence proof is omitted due to space limitation.
* More concise presentation and a new title to better represent the nature
of our effort.
-- Jason
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:40 EDT