顺序一致性易失性解释

Question

我正在看java jpoint会议的视频。

我对以下Alexey Shipilev报告幻灯片有疑问：

请原谅幻灯片上的非英语。实际上作者说变量集是不可能的

r1 = 1 (Y)
r2 = 0 (x)
r3 = 1 (x)
r4 = 0 (Y)

附注。

如果我理解Alexey符号正确，它尊重以下代码：

public class SequentialConsistency {
    static volatile int x;
    static volatile int y;

    public static void main(String[] args) {
        new Thread(new Runnable() {
            @Override
            public void run() {
                x = 1;
            }
        }).start();
        new Thread(new Runnable() {
            @Override
            public void run() {
                y = 1;
            }
        }).start();
        new Thread(new Runnable() {
            @Override
            public void run() {
                System.out.println("r1=" + x + ", r2=" + y);
            }
        }).start();
        new Thread(new Runnable() {
            @Override
            public void run() {
                System.out.println("r3=" + x + ", r4=" + y);
            }
        }).start();
    }
}

Answer 1

您可以为该代码构造完整的SC执行列表，并实现没有SC执行产生（1,0,1,0）。

从模型的角度来看，它很容易引起争论。同步顺序（Synchronization order,SO)一致性表示同步读取应该看到SO中的最后一个同步写入。SO-PO一致性表示SO应该与程序顺序一致。

这样就可以用矛盾来勾画证明。假设产生（1,0,1,0）的执行存在。然后，在这些执行中，读为see 0必须按照这样的顺序，由于如此一致：

(r2 = x):0 --so--> (x = 1)  [1]
(r4 = y):0 --so--> (y = 1)  [2]

...而另外两个读和写必须按照这样的顺序才能看到它们（由于如此一致）：

(x = 1) --so--> (r3 = x):1  [3]
(y = 1) --so--> (r1 = y):1  [4]

...此外，由于SO-PO的一致性：

(r1 = y):1 --po--> (r2 = x):0  [5]
(r3 = x):1 --po--> (r4 = y):0  [6]

这就产生了奇怪的传递性，所以是循环的：

(r2 = x):0 --so--> (r3 = x):1 --so--> (r4 = y):0 --so--> (r1 = y):1 --so--> (r2 = x):0
            [1,3]               [6]               [2,4]               [5]