Re: JavaMemoryModel: JLS3 contains glitch concerning volatiles?

From: Victor.Luchangco@sun.com
Date: Wed Aug 17 2005 - 23:13:08 EDT


> So if the JLS doesn't include the words "non-volatile" when it
> describescorrectly synchronized programs, it doesn't effect the
> semantics at all.

While this is true, I think it misses Bart's point. We said from the
beginning that most programmers (and all programmers most
of the time) should be able to reason about their programs
using only the "correctly synchronized programs are guaranteed
sequential consistency" property. To do this, they need to know
when their programs are correctly synchronized. JLS3 defines
"correctly synchronized" as the lack of data races in SC executions
(in 17.4.5), which would be fine, except that the definition of a
data race is "conflicting accesses not ordered by happens-before",
which would include the R and W in Bart's initial email (which are
respectively a read and a write to the same volatile, where R
precedes W in the synchronization order). This means that there
are programs that we want "most programmers" to be able to
argue get sequentially consistent results (because they are
correctly synchronized by the definition in Jeremy's thesis) for
which the programmer needs to understand more of the JMM
than that "correctly synchronized programs get sequential
consistency" (because they are not correctly synchronized by
the definition given in JLS3). For example, I think we would
like all programmers to be able to reason that programs in
which all sharing of data is done through volatile variables are
guaranteed sequential consistency. Since "most programmers"
can only reason that they are guaranteed SC for correctly
synchronized programs, they would not be able to do so using
the definition in JLS3.

I think it is the definition of data race that needs fixing: accesses
to volatile variables should never be considered data races. And
JLS should be updated to reflect this. So I would say this is a
bug in JLS: it gives the wrong definition for data race. It may not
affect the semantics (though I worry about what else might have
slipped by, and if any of those affect the semantics), but it will
foster confusion, as if there wasn't enough of that already.

I'm sorry this is so verbose. I'm just trying to spell out in detail
what I understood Bart to be saying, and to echo his concern.

- Victor

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



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