My recent experience in trying to formalize the Java memory model has
led me to the same conclusion as Bill Pugh---that is, there need to be
rules governing the relative order of volatile and non-volatile
operations.
A quick background: I'm attempting to formalize a memory semantics
for Java by extending Arvind and Xiaowei Shen's CRF memory model. I
took the following as my starting point:
1) Final fields need be read at most once by any thread. We thus
must reconcile at the first read but need not do so again.
2) Data read through a final field should be up-to-date with respect
to the time when the final field was written. Thus, we must commit
data pointed to by the final field before the field itself is written.
This solves the "strings-must-be-constant" problem without locking.
3) Volatile fields are sequentially consistent---all reads and writes
are strongly globally ordered.
4) It should always be possible to change a variable to "volatile"
without changing program semantics.
5) Regular fields require monitor synchronization in order to
guarantee coherence, except when accessed through a final field
(condition 2) or through a volatile field (condition 2 via condition
4).
My impression is that condition 4) requires the same synchronization
constraints between regular fields and volatile fields that Bill seems
to be advocating. I believe (admittedly without proof) that condition
(4) will prove useful from the point of view of code maintainence.
The barriers our model use are considerably finer-grain---we only
require a barrier between a regular write and a volatile write if the
regular field becomes accessible through the volatile field. We then
hope to use the compiler to merge as many barriers as possible
together, and to eliminate barriers with no observable effect. The
latter is far easier when the scope of the barriers is limited (even if
remaining memory barriers are heavyweight).
Note that to ensure transitivity of constraint (2) (as with an array
of objects we would now like to consider constant), we need to use a
heavier-weight barrier based on reachability, or lighter-weight
barriers before writes of regular fields. This choice should have no
effect on its own---reads of regular fields can still see stale data
unless explicitly synchronized (by a monitor or by fetching their
contents through volatile or final fields). However, it involves a
tradeoff between a potentially much larger number of very fine-grained
memory barriers and a few much coarser-grained barriers. I'm at the
moment attempting to verify that these two approaches really are
equivalent.
-Jan-Willem Maessen
MIT LCS CSG
-------------------------------
JavaMemoryModel mailing list - http://www.cs.umd.edu/~pugh/java/memoryModel
This archive was generated by hypermail 2b29 : Thu Oct 13 2005 - 07:00:21 EDT