Right, I see. Yes.
So the only "problem" in the JLS is that it states a theorem that is weaker
than it could be. This matters "only" for those people who are not able or
willing to expend the effort of deriving the stronger theorem from the
definitions themselves, or trust your claim, or find and check the proof in
Jeremy's thesis.
So if I wish to use the strong theorem in a paper, for now I will have to
call on the referees to perform one of the above. Fair enough.
Thanks,-
Bart
> -----Original Message-----
> From: owner-javamemorymodel@cs.umd.edu [mailto:owner-
> javamemorymodel@cs.umd.edu] On Behalf Of Bill Pugh
> Sent: Wednesday, August 17, 2005 6:11 PM
> To: Bart Jacobs
> Cc: 'Jeremy Manson'; 'javamemorymodel-cs.umd.edu'
> Subject: Re: JavaMemoryModel: JLS3 contains glitch concerning volatiles?
>
>
> On Aug 17, 2005, at 8:05 PM, Bart Jacobs wrote:
>
> > 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
>
> The point is that nothing in the semantics depend upon the definition of
> correctly synchronized.
>
> Rather, you can prove that the model provides certain properties for
> executions
> of correctly synchronized programs (appropriately defined).
>
> So if the JLS doesn't include the words "non-volatile" when it describes
> correctly synchronized programs, it doesn't effect the semantics at all.
>
> Bill
>
> -------------------------------
> 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