>рабочие заметки: Квест по внутренностям JMM: solution

15 февраля 2013 г.

Квест по внутренностям JMM: solution

Студентка Люся выучила все билеты по логике и стала мужиком.

Хорошо, давайте разберем предыдущий пост. Для доказательства нам понадобится всего ничего: ~~волос с головы Путина, менструальная кровь девственницы~~JMM в мягком переплете, и мозг со способностями к математической логике.

Замечание 0:

В JMM есть понятие частичного порядка happens-before. Немного математики: что такое вообще частичный порядок на множестве A? Неформально: частичный порядок означает, что на множестве A задан способ упорядочивания элементов a1 < a2, но упорядочить можно не все элементы множества: есть такие пары (an, am) что для них порядок не определен: не верно ни что (an < am), ни что (am < an). В противовес этому полный порядок, как можно догадаться, это когда все пары сравнимы: для любых элементов множества A всегда либо am < an, либо an < am, третьего не дано.

Замечание 1:

Если у нас есть события записи и чтения одной переменной W: sharedVar = X, R: localVar = sharedVar, то какие значения может прочитать (увидеть) чтение? Согласно JMM, варианта три:

Если W hb R, то R наверняка прочитает (увидит) X (если нет других записей в ту же переменную)
Если !(W hb R), то R может прочитать X, а может и не прочитать -- как звезды лягут (этот случай как раз называется чтением через data race)
Если R hb W, то R никак не может прочитать X (опять же, если нет других записей). Это самый важный для дальнейшего пункт

Замечание 2:

Synchronized actions (к которым принадлежат vstore и vload) образуют total synchronization order, SO. Важно здесь, что это именно полный порядок. То есть для любых двух SA1, SA2 всегда либо SA1 so SA2, либо SA2 so SA1.

Наше оружие — слово божье, и математический аппарат

Код из предыдущего примера, чуть приглаженый и пронумерованный:

(0) AI sharedRef = null; //write default value
Thread 1	Thread 2
(1) localRef = allocate(sizeOf(AI)); (2) localRef.value = 42; (3) sharedRef = localRef;	(4) localRef2 = sharedRef; (5) if(localRef2 != null ){ (6) localValue = localRef2.value; }

(0) AI sharedRef = null; //write default value

Thread 1

Thread 2

(1) localRef = allocate(sizeOf(AI));
(2) localRef.value = 42;
(3) sharedRef = localRef;

(4) localRef2 = sharedRef;
(5) if(localRef2 != null ){
(6)   localValue = localRef2.value;   
    }

Рассмотрим множество трасс над этим кодом, в которых чтение (6) происходит, и видит значение 0:

Чтобы прочитать что угодно из localRef в (6), нужно чтобы чтение (4) вернуло не null (иначе мы не попадем в эту ветку)
Поскольку 0 это не 42, то не верно, что (2) hb (6).
Раз не верно, что (2) hb (6), то не верно и что (2) sw (6), потому что synchronization order вложен в (согласован с) happens-before.
Поскольку (2) и (6) — synchronized actions, то из ![ (2) sw (6) ] => [(6) sw (2) ] => [(6) hb (2)]. Это ключевой, самый нетривиальный пункт — дальше все просто
(4) hb (6) согласно program order (который тоже вложен/согласован с hb)
(2) hb (3) аналогично
По транзитивности: [(4) hb (6)] + [(6) hb (2)] + [(2) hb (3)] => [(4) hb (3)]
Но раз [(4) hb (3)], то чтение (4) никак не может увидеть значение, записанное (3). Значит (4) может прочитать только значение, записанное в (0), то есть null.
А это противоречит первому пункту.

Получается, что предполагаемые нами трассы не могут существовать в рамках ограничений, накладываемых на исполнение кода моделью памяти java.

Dixi

P.S. Да, совсем забыл -- я могу и ошибаться :)

41 комментарий:

Vladimir Dolzhenko15 февраля 2013 г. в 10:44
Вся соль недопонимания - почему перестановка (2) и (3) не валидна и как именно она будет противоречить jmm.
ОтветитьУдалить
Ответы
Unknown15 февраля 2013 г. в 11:35
Круто. Вот только непонятно как в таких ограничениях JIT может вообще делать реордеринг вокруг ребер полного порядка. Скажем внести что-нибудь перед волатильной записью. Понятное дело, что эта логика сработает только если полный порядок ляжет вполне определенным образом, но JIT то этот порядок знать не может, будет и так и сяк падать в общем случае. Выходит реордерить ему так можно только такие вещи, которые гарантированно и другим потокам видны не будут, всякие локальные переменные итп.
ОтветитьУдалить
Ответы
Alexandr15 февраля 2013 г. в 11:44
Непонятно, почему (2) hb (3).
ОтветитьУдалить
Ответы
Alexandr15 февраля 2013 г. в 12:33
Поясню свой вопрос:
Для первого потока валидна перестановка, которая может быть выполнена компилятором:

(1) localRef = allocate(sizeOf(AI));
(3) sharedRef = localRef;
(2) localRef.value = 42;

Верно ли в этом случае доказательство?
Если перестановка не валидна, то почему?
ОтветитьУдалить
Ответы
Unknown15 февраля 2013 г. в 13:36
Кажется теперь дошло.
12.5. Creation of New Class Instances
Just before a reference to the newly created object is returned as the result, the indicated constructor is processed to initialize the new object using the following procedure:
...
5. Execute the rest of the body of this constructor.

Т.е. порядок, вроде как, JLS гарантирует. А про final я, действительно, ошибался. Там гарантируется видимость в другом потоке, аналогично volatile. Т.е. это не связано с возможной перестановкой.
Осталось тогда непонятным откуда тогда столько соплей в интернетах по поводу того что такая перестановка ((2),(3)->(3),(2)) возможна.
ОтветитьУдалить
Ответы
rx22 февраля 2013 г. в 23:03
(из JLS)
...More specifically, if two actions share a happens-before relationship, they do not
necessarily have to appear to have happened in that order to any code with which
they do not share a happens-before relationship. Writes in one thread that are in
a data race with reads in another thread may, for example, appear to occur out of
order to those reads.

Т.е. п.7 не верен, т.к.
[(2) hb (3)] - только для Thread 1
[(4) hb (6)] - только для Thread 2

Т.е. формально может быть 0.
ОтветитьУдалить
Ответы
gvsmirnov25 февраля 2013 г. в 17:48
Но подожди, разве субатомарное частичное отношение между hb 2 3 не приводит к сбросу кешей?

Вот выдержка из документации по Apache Tomcat (http://clck.ru/846):

> Given a Write W, and a Read R, such that R ha W, a Freeze F and a Synchronization Strategy S,
> such that S fml F, it is safe to assume that the caches will be flushed after F. JMM also guarantees that
> the caches being flushed will incur a FenceLoad instruction between R and S, and seven to eleven
> NOP operations being issued by each and every CPU available after W. The relevant cachelines will
> therefore be installed in the corresponding caches, which will ensure that just in time (JIT)
> for the processors to access it via R.

А ты ещё говоришь, что публикация объектов с помощью NOP race небезопасна.
ОтветитьУдалить
Ответы
Анонимный24 сентября 2013 г. в 17:37
Экскьюзмуа,
hb - это happens before, а что такое sw?
ОтветитьУдалить
Ответы
Andrey17 ноября 2013 г. в 03:53
Замечание 2:
Synchronized actions (к которым принадлежат vstore и vload) образуют total synchronization order, SO. Важно здесь, что это именно полный порядок. То есть для любых двух SA1, SA2 всегда либо SA1 so SA2, либо SA2 so SA1.

Это верно

Поскольку (2) и (6) — synchronized actions, то из ![ (2) sw (6) ] => [(6) sw (2) ] => [(6) hb (2)]. Это ключевой, самый нетривиальный пункт — дальше все просто

Нет ли здесь подмены понятий Synchronization Order на Synchronized-With? Ведь определение Synchronized-With для volatile - A write to a volatile variable v (§8.3.1.4) synchronizes-with all subsequent reads of v by any thread (where "subsequent" is defined according to the synchronization order). Но если volatile read "prior to" volatile write, то никакого отношения между этим volatile read и volatile write не будет
ОтветитьУдалить
Ответы

Добавить комментарий

15 февраля 2013 г.

Квест по внутренностям JMM: solution

Наше оружие — слово божье, и математический аппарат

41 комментарий:

15 февраля 2013 г.