Последовательное непротиворечивое объяснение

Question

Я смотрю видео с конференции java jpoint.

У меня вопрос о следующем слайде из доклада Aleksey Shipilev:

Извините за не английский на слайде. На самом деле автор говорит, что невозможно, чтобы набор переменных был

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

По видео он подразумевает, что это очевидно.

Может кто-нибудь уточнить, почему этот набор значений невозможен в соответствии с JMM?

PS

Если я правильно понимаю обозначения Алексея, это соответствует следующему коду:

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) нет.

По поводу модели очень легко спорить. Согласованность порядка синхронизации (SO) говорит о том, что синхронизированные чтения должны видеть последнюю синхронизированную запись в SO. Согласованность SO-PO говорит о том, что SO должен соответствовать порядку программы.

Это позволяет набросать доказательство от противного. Предположим, что выполнение, которое дает (1, 0, 1, 0), существует. Затем в этих выполнениях читайте, что нули должны быть в этом порядке из-за согласованности SO:

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

... и два других чтения должны быть в этом порядке с записями, чтобы увидеть их (из-за согласованности SO):

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

Это дает странный переходный SO, который является циклическим:

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

Обратите внимание, что для любой пары действий A!= B в приведенном выше выполнении мы можем сказать, (A --so--> B) а также (B --so--> A) - это называется симметрией. По определению, SO является полным порядком, а общий порядок антисимметричным, и здесь мы имеем симметричный. Мы пришли к противоречию, и поэтому такой казни не существует. QED

Answer 2

Вы можете думать об этом в несколько более простой форме (хотя точнее, чем Алексей, вы не найдете). volatile в предложениях Java sequential consistency, что означает, что операции выполняются как в глобальном, так и в атомарном порядке. Если вы напишете в поле (x = 1), все увидят, что пишут. Чтобы было правильнее по вашему примеру, если есть ThreadA это делает x = 1, и то и другое ThreadB (что делает r2 = x) и ThreadC (что делает r3 = x), буду читать x быть 1. Это то, что гарантирует последовательная согласованность.

На слайдах видно, что в SC (последовательное последовательное) выполнение: 1, 0, 1, 0невозможно. Потому что это будет означать следующее:

ThreadA wrote to x value of 1
ThreadB observed that value to be 1 (via r2 = x)
ThreadC observed that value to be 0 (via r3 = x)

Но в мире SC, как только происходит запись (и мы знаем, что это произошло, потому что ThreadBнаблюдал это), это должны соблюдать все остальные. Здесь не так: ThreadC видит x быть 0. Таким образом, это нарушает SC.

Вы должны вспомнить, что его точка зрения - "Можем ли мы заменить каждую изменчивую версию на выпуск / приобретение? (В конце концов, это дешевле)". И ответ - нет, потому что SC запрещает 1, 0, 1, 0, в то время как release/acquire позволяет это.

Answer 3

Поверьте, что я понял.

Допустим, у нас есть 4 потока. t1-t4(слева направо согласно рисунку)

T3 читает у, а затем х, и мы видим результат

y=1
x=0

Это означает, что последовательность была следующей:

1. Т1 пишет у
2. т3 читает у
3. т3 читает х
4. Т2 пишет х

Это единственная возможная последовательность.

Давайте проверим это для t4 чтений:

x=1
y=0

Согласно рассуждениям относительно t3 это означает, что

t2 write происходит раньше t1 write но это противоречит выводу t3, таким образом, это невозможно