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