RE: JavaMemoryModel: JLS3 contains glitch concerning volatiles?

From: Sarita Adve (sadve@cs.uiuc.edu)
Date: Thu Aug 18 2005 - 00:09:49 EDT


Yes, this is a bad mistake in JLS3 that I hope will be fixed (i.e., a data
race should be defined as conflicting actions on *non-volatile* variables
that are not ordered by happens-before).

Sarita

> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu
> [mailto:owner-javamemorymodel@cs.umd.edu] On Behalf Of
> Victor.Luchangco@sun.com
> Sent: Wednesday, August 17, 2005 10:13 PM
> To: Bill Pugh
> Cc: Bart Jacobs; 'Jeremy Manson'; 'javamemorymodel-cs.umd.edu'
> Subject: Re: JavaMemoryModel: JLS3 contains glitch concerning
> volatiles?
>
>
>
> > 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
>

-------------------------------
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