Why we cannot apply the guarantee included in JLS?

Question

I got a mail from mailing list which says that if actions on volatile vars contain data race then guarantee("A program is correctly synchronized if and only if all sequentially consistent executions are free of data races." in JLS) can not be applied.

For convenience, I just put part of orginal content at here:

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 above mentioned guarantee.

So this is my question: Why we cannot apply the guarantee included in JLS if actions on volatile vars contain data race?

Answer 1

A sequentially consistent execution contains a read of volatile preceding a write to a volatile

=>

the execution contains a data race

=>

the program is not "correctly synchronized"

=>

the JLS does not give the guarantees that apply to correctly synchronized programs.