JavaMemoryModel: My approach

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Thu Aug 08 2002 - 00:33:22 EDT


I have a revised proposal for a Java memory model, for reasons explained
below. It is similar to my previous proposal, but the revisions make it
simpler to understand. The model itself is one page long at
http://www.cs.uiuc.edu/~sadve/jmm.pdf. An accompanying document contains
the intuition and rationale behind the model and discussion on the
necessary proofs: http://www.cs.uiuc.edu/~sadve/jmm-appendix.pdf

The new Manson/Pugh (M/P) approach has many similarities with this, but
there is still a significant difference. Here are the reasons why the
new M/P approach isn't good enough yet:

(1) The new M/P approach essentially gives up on trying to precisely
prohibit "causal loops." Instead, it claims without proof that the
formalism prohibits most of the important cases, and the rest will be
prohibited with an informal statement that "the JVM should not allow
causal loops." If we cannot formalize what we mean by causal loops, I am
not sure what good the informal statement does. Programmers can't assume
anything, and JVM implementors will have to assume their most
conservative interpretation of a causal loop. That's unacceptable in my
opinion, and should only be considered as an absolutely last resort.

(2) This one is a subjective point, but I think important. The
approaches used by M/P have seemed somewhat ad hoc to me. The last one
is definitely much better, but still not grounded in solid intuition.
What is the rationale for the choices made in this model? For example,
what's the rationale for using prescient reads vs. prescient writes?
What's the rationale for using program ordered thread interleavings for
execution traces when trying to validate PURs? Etc. It's hard to argue
about the correctness (necessity or sufficiency) of an ad hoc approach.

I have tried to define the memory model starting from the intuitive
requirements that are necessary and sufficient to meet. These
requirements were determined from several discussions with Bill. The
requirements and how they lead to the formal model are covered in the
appendix document above.

Finally, I would like to add that Bill shares credit for this as well
since it has benefitted significantly from discussions with him; in
fact, the initial intuitive requirements came directly from him.

Sarita

-----------------------------------------------------------------------
Sarita Adve
Associate Professor
University of Illinois at Urbana-Champaign Email: sadve@cs.uiuc.edu

Department of Computer Science Office: 3302 DCL
1304 West Springfield Avenue Phone: 217-333-8461
Urbana, IL 61801 Fax: 217-333-3501
                     WWW URL: http://www.cs.uiuc.edu/~sadve
-----------------------------------------------------------------------

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



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