Sequential consistency volatile explanation

Question

I am watching video from java jpoint conference.

I have question about following slide from Alexey Shipilev report:

Excuse me for non-english on slide. Actually author says that it is impossible that variable set will be

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

According the video he implies that it is obviously.

Can someone clarify why this value set impossible according JMM?

P.S.

If I understand Alexey notation correct it respects the following code:

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

You can construct exhaustive list of SC executions for this code, and realize no SC execution yields (1, 0, 1, 0).

Model-wise, it is very easy to argue about. Synchronization order (SO) consistency says that synchronized reads should see the last synchronized write in SO. SO-PO consistency says SO should be consistent with program order.

This allows to sketch the proof by contradiction. Suppose the execution that yields (1, 0, 1, 0) exists. Then, in those executions read that see zeroes must be in this order, due to SO consistency:

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

...and the other two reads must be in this order with writes to see them (due to SO consistency):

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

...and further, due to SO-PO consistency:

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

This yields weird transitive SO that is cyclic:

(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]

Notice that for any pair of actions A != B in the execution above, we can say (A --so--> B) and (B --so--> A) -- this is called symmetry. By definition, SO is total order, and total order is antisymmetric, and here we have the symmetric one. We have arrived to contradiction, and therefore such execution does not exist. Q.E.D.