Thanks. What I take away from your answer is the corrected definition of
"correctly synchronized". Hopefully it will make it into the JLS at some
point. I don't really get the message from the rest of your answer.
Thanks,-
Bart
> -----Original Message-----
> From: Bill Pugh [mailto:pugh@cs.umd.edu]
> Sent: Wednesday, August 17, 2005 4:37 PM
> To: Bart Jacobs; Jeremy Manson
> Cc: javamemorymodel-cs.umd.edu
> Subject: Re: JavaMemoryModel: JLS3 contains glitch concerning volatiles?
>
> From Jeremy's thesis:
>
> > A program is correctly
> > synchronized if and only if in all sequentially consistent
> > executions, all conflicting
> > accesses to non-volatile variables are ordered by happens-before
> > edges.
>
> This detail may have gotten left out of the JLS, but it is certain
> part of the formalism of the JMM.
> Anyway, this is only something you can deduce from the spec, not part
> of the spec. Thus,
> even if it isn't correct in the JLS, it doesn't actually effect the
> meaning of the spec.
>
> Bill
>
>
> On Aug 17, 2005, at 2:51 PM, Bart Jacobs wrote:
>
> > Hi all,
> >
> > I have a program that uses volatile variables and I am trying to
> > reason
> > about it using the
> > "A program is correctly synchronized if and only if all sequentially
> > consistent executions are free of data races." guarantee in JLS3.
> >
> > JLS3 seems to contain a glitch that prevents me from proving that
> > my program
> > is free of data races. Specifically, consider a read R of a volatile
> > variable V and a write W of V that comes after R in the
> > synchronization
> > order. JLS3 seems to consider R and W to be conflicting accesses.
> > Moreover,
> > there is no happens-before edge from R to W (and rightly so).
> > Therefore,
> > JLS3 seems to also consider R and W to constitute a data race.
> > Finally, it
> > seems therefore that I cannot apply the abovementioned guarantee.
> >
> > I assume this is an unintentional omission. I see two possible fixes:
> >
> > 1) Define "conflicting accesses" to apply only to non-volatile
> > variables.
> > or
> > 2) Define "data race" to apply only to conflicting accesses of non-
> > volatile
> > variables.
> >
> > Am I correct in this?
> >
> > Thanks,-
> > Bart Jacobs
> >
> > -------------------------------
> > 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