java - 为什么我们不能应用 JLS 中包含的保证？

Question

我收到一封来自 mailing list 的邮件其中表示，如果对 volatile 变量的操作包含数据竞争，则无法应用保证(“当且仅当所有顺序一致的执行都没有数据竞争时，程序才能正确同步。” JLS )。

为了方便，我只放了orginal content的一部分在这里:

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.

所以这是我的问题:如果对 volatile 变量的操作包含数据竞争，为什么我们不能应用 JLS 中包含的保证？

Answer 1

顺序一致的执行包含在写入 volatile 之前读取 volatile

=>

执行包含数据竞争

=>

程序未“正确同步”

=>

JLS 不提供适用于正确同步程序的保证。