A concern I have had all along is that there is no high-level (preferably
simple and non-operational) necessary and sufficient set of requirements for
a Java memory model. I understand this is difficult, but without such a
basis, it is difficult to determine if an “operational” model such as that
currently proposed (by Bill and Jeremy) is over-specified or
under-specified. I believe the current proposal is not (or eventually will
not be) under-specified, although someone will need to do a formal proof of
that. However, I am not sure that the model is not over-specified.
That is, I believe the model is (or will be) sufficient for correct
behavior, but is it necessary? Said another way, are there optimizations
that the model prohibits inadvertently and unnecessarily? In some of the
past iterations, we have been able to identify such optimizations, but there
is no systematic way of doing so and we cannot predict future optimizations.
Further, as the model gets more refined (and more complex), it becomes
increasingly difficult to identify such problems with ad hoc methods. I am
additionally concerned about the complexity of the model – perhaps the
complexity is inherent to the problem, but again, we do not have a formal
basis for judgment.
I therefore believe that it is important to try to formalize a set of
higher-level (program-centric, non-operational) necessary and sufficient
conditions that we expect the system to obey. Once we do that, those
conditions will themselves be a candidate for the Java memory model. It is
possible that the current proposal will be a better way of specifying those
conditions, but we will at least then have a basis to do formal proofs that
show the current specification does what we expect it to do.
I realize it is difficult to predict what is necessary and sufficient for
the future even at a high level, but I believe that it is easier to predict
that than to make predictions at the level of the current proposal. At the
least, it is a useful exercise to check correctness of the current proposal.
I have made a first attempt at formalizing such a high level necessary and
sufficient set of requirements in the following short document, and would
appreciate feedback:
http://www.cs.uiuc.edu/~sadve/java-model.pdf
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://rsim.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:39 EDT