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, варианта три:
  1. Если W hb R, то R наверняка прочитает (увидит) X (если нет других записей в ту же переменную)
  2. Если !(W hb R), то R может прочитать X, а может и не прочитать -- как звезды лягут (этот случай как раз называется чтением через data race)
  3. Если 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;   
    }

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

Dixi


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

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

  1. Вся соль недопонимания - почему перестановка (2) и (3) не валидна и как именно она будет противоречить jmm.

    ОтветитьУдалить
    Ответы
    1. Вся соль этого непонимания в том, что JMM это инструмент доказательства корректности/некорректности целой конкретной трассы -- а не отдельных перестановок. Я не знаю, возможно ли переставить именно (2) и (3) -- я доказываю, что любой набор перестановок, который приведет к значению 0 в localValue -- противоречит JMM.

      Чтобы было понятнее -- есть ведь такие трассы, где (2) и (3) переставлены, но localValue все равно 42. Такие трассы, вообще говоря, валидны

      Удалить
    2. Понятнее не стало. Доказательство опирается на (2) hb (3) согласно program order. Но откуда этот program order вытекает?
      JMM гарантирует только видимость default value и значений final полей. Никаких гарантий (2) hb (3) нет. Меняем (2),(3) местами, получаем новый program order и 0 значение.

      Удалить
    3. Program order -- это тот порядок, в котором инструкции идут в коде программы. Можно просто открыть страницу с JMM, и поиском по странице найти определение :)

      Удалить
  2. Круто. Вот только непонятно как в таких ограничениях JIT может вообще делать реордеринг вокруг ребер полного порядка. Скажем внести что-нибудь перед волатильной записью. Понятное дело, что эта логика сработает только если полный порядок ляжет вполне определенным образом, но JIT то этот порядок знать не может, будет и так и сяк падать в общем случае. Выходит реордерить ему так можно только такие вещи, которые гарантированно и другим потокам видны не будут, всякие локальные переменные итп.

    ОтветитьУдалить
    Ответы
    1. Вполне можно реордерить любые записи/чтения разделяемых переменных, если этот реордеринг не пересекает какой-нибудь SA. Насчет реордерингов "через" SA -- да, почти наверняка там очень консервативная политика.

      Удалить
    2. Так новизна данного конкретного поста, именно в том, что реордеринг "через" SA даже если это разрешено JMM на уровне JIT невозможен практически. Это можно делать только в рантайме, то есть остается процессор или интерпретатор. Это я к тому, чтобы попытатся сконструировать реально воспроизводимый пример такого реордеринга врядли возможно даже на АРМ архитектуре. Я очень сомневаюсь, что интерпретатор будет заморачиваться такими оптимизациями.

      Удалить
    3. @andrey
      Вы удивитесь, но вопрос возник вовсе не из воздуха. Один из портов openJDK на архитектуру со слабой моделью памяти падал на этом (ну, аналогичном) тесте -- возвращал 0. И надо было понять, это правда допустимое поведение, которое на остальных платформах просто не случается, или это баг, который нужно исправлять.

      Удалить
  3. Ответы
    1. 17.4.5 http://docs.oracle.com/javase/specs/jls/se7/jls7.pdf
      If we have two actions x and y, we write hb(x, y) to indicate that x happens-before y.
      • If x and y are actions of the same thread and x comes before y in program order,
      then hb(x, y).

      Удалить
    2. В JMM гарантия hb((2), (3)) для инициализации значения поля в конструкторе и присвоении ссылки на создаваемый объект, есть только для final полей. Наше value не final. Поэтому никакой hb((2), (3)) там нет.

      Удалить
    3. Я не первый раз сталкиваюсь с тем, что люди даже давно работающие с JMM совершенно не замечают иезуитскую хитрость понятия partial happens-before order. Мне это всегда было странно, потому что я как-то сразу, как прочитал, ощутил что здесь огромное поле для неочевидных фокусов

      Далее -- вам выше привели четкую цитату -- там ясно сказано, что program order вложен в happens-before order. Я в посте совершенно явно написал про это же.

      В завершение: то, что вы пишете про final поля -- это ерунда. Гарантии, которые для final-полей -- они совершенно не такие, что вы написали. Вот здесь можете прочитать перевод на русский.

      Удалить
    4. An object is considered to be completely initialized when its constructor finishes. A
      thread that can only see a reference to an object after that object has been completely
      initialized is guaranteed to see the correctly initialized values for that object's final
      fields.

      Я так понимаю на момент (3) объект полностью проинициализирован и следовательно гарантируется что в рамках этого потока он увидит все значения корректно. Можно ли это трактовать как hb я не вполне уверен, но как я понимаю, можно.

      Удалить
    5. @andrey
      Да тут нет никакой специфичной для конструктора магии. Внутри каждого потока все его инструкции связаны HB в том порядке, в котором они выполняются. Но поскольку HB -- частичный порядок, то эти последовательности из разных потоков никак не связаны -- инструкции из разных потоков просто не сравнимы в смысле HB. Чтобы сделать их "сравнимыми" (а это нужно, чтобы получить гарантии видимости/не видимости каких-то записей) нужны _межпоточные_ ребра HB. Такие ребра это, в основном SW. (Есть еще final-induced HB, и lazySet HB -- но с ними все сложнее, надо разбираться отдельно). Как только вы создаете через SW порядок между двумя инструкциями в разных потоках -- вы через транзитивность делаете сравнимыми сразу целое множество (но не все!) инструкций из этих потоков. Тем и живем...

      Удалить
    6. Как я понял вопрос Ростислава, тут у нас один поток и вопрос даже не о hb, а о programming order. Это уже конечно занудство, но можно ли воспринимать публикацию ссылки (шаг (3)) как отдельный action не очень понятно из JMM.
      Например если мы публикуем объект эксепшена инструкцией athrow, является ли это отдельным action? И где это написано в JMM?

      Если посмотреть во что скомпилируется наша программа, то очевидно, что (3) это экшен связанный программинг ордером, но в рамках нескомпилированной ява программы это уже не так очевидно и если мы говорим о мат модели, насколько корректные такие аппеляции? Скорее всего это я глупости пишу и ответ гдето прописан, но навскидку не нашел.

      Удалить
    7. Даже так, если говорить о строгой мат модели, насколько корректно аппелировать к байт коду сгенеренным данным конкретным компилятором. Допустимы ли другие варианты компиляции нашей ява программы, при которых публикация не будет отдельным action. Думаю Блох бы ответил просто "не допустимы", но я вот навскидку не готов.

      Удалить
    8. @andrey

      Частью на ваши вопросы можно ответить. Модель памяти оперирует действиями с памятью (сюрприз!). Более конкретно -- с разделяемой памятью, т.е локальные переменные и параметры методов ей не интересны. В рамках модели есть "действия с (разделяемой) памятью", есть некоторые "внешние действия" (external action), типа ввода-вывода, и есть синтетические действия, типа старт-завершение потока (они ограничивают начало-конец множества инструкций). Поэтому throw модель памяти не интересует -- это не действие с разделяемой памятью.

      Что касается вопроса, как именно транслируется ява-код в набор таких вот "действий с памятью" -- я думаю, что многое прописано в спецификации явы в целом. Например я знаю, что там есть спецификация порядка вычисления выражений -- т.е. как должно быть вычислено a = new B(f(x)). Я сильно подозреваю, что JMM привязывается именно к этому порядку вычислений, а не к инструкциям байт-кода (хотя возможно, что это одно и то же)

      Удалить
  4. Поясню свой вопрос:
    Для первого потока валидна перестановка, которая может быть выполнена компилятором:

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

    Верно ли в этом случае доказательство?
    Если перестановка не валидна, то почему?

    ОтветитьУдалить
    Ответы
    1. Ваш вопрос уже задал первый комментатор, и я на него уже и ответил ему же. Встречный вопрос -- как вы определяете, что какая-то перестановка валидна?

      Удалить
    2. 2 и 3 не зависит по данным - поэтому теоретически могут быть переставлены.
      Правильно ли я понимаю, что пользуясь вашим доказательством, в следующем примере будет истина:

      volatile int i = 0;
      int j = 0;
      // thread 1
      i = 1;
      j = 1;
      // thread 2
      if (j == 1) {
      int k = i;
      // we know that k = 1
      }

      Удалить
    3. hb не гарантирует что на практике они будут выполнены именно в таком порядке. Но гарантируется, что на исполнении програмы эти перестановки не скажутся. Даже из другого потока эта разница не будет видна. А вы сами показываете, что разница видна будет, следовательна такая перестановка недопустима.

      Удалить
    4. @alexandr
      А зависимые по данным инструкции не могут быть переставлены? Почему?

      Удалить
    5. @Ruslan
      Я ничего не говорил про зависимые по данным инструкции

      Интересно, что тут http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.112.1790&rep=rep1&type=pdf
      утверждается, что перестановка независимых инструкций в текущем виде JMM невалидна.

      Удалить
  5. Кажется теперь дошло.
    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)) возможна.

    ОтветитьУдалить
    Ответы
    1. Соплей много как раз потому, что такая перестановка чаще всего таки возможна. Если вы уберете volatile с value -- она станет возможна. Даже если вы оставите volatile, но добавите в класс других полей -- все станет не так просто. Если value будет меняться несколько раз -- все опять же будет не так просто...

      Удалить
  6. (из 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.

    ОтветитьУдалить
    Ответы
    1. Если вы еще раз внимательно прочитаете пункт 7, то вы сможете увидеть, что этот пункт как раз и показывает, каким образом два потока начинают share happens-before relationship. А именно: их частичные порядки сливаются ("замыкаются") через свойство транзитивности соотношения HB, с помощью того факта, что [(6) hb (2)].

      У абсолютного большинства программистов в голове из JMM остаются отдельные куски. Как эти куски складываются в общую картинку, какое место каждый кусочек в ней занимает -- мало кто, увы, понимает. Я собираюсь как раз про это рассказывать на javapoint -- правда мне пока самому не понятно, уложусь ли я в 50 минут с такой темой

      Удалить
  7. Но подожди, разве субатомарное частичное отношение между 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 небезопасна.

    ОтветитьУдалить
  8. Экскьюзмуа,
    hb - это happens before, а что такое sw?

    ОтветитьУдалить
  9. Замечание 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 не будет

    ОтветитьУдалить
    Ответы
    1. Точнее будет отношение SO, но не SW

      Удалить
    2. Ага, доказательство ошибочно. То, что 6 so 2 не допускает быть 3 hb 5, но вполне позволяет 3 и 5 быть никак не упорядоченными по hb. И поэтому не мешает 5 прочитать результат 3, хотя бы и "против" so.

      Поскольку код очевидно содержит data race, то его надо анализировать анализировать с позиций "большой" модели памяти, с commitment procedure и сопутствующим адом. Я обнаружил ошибку когда готовил презентацию по JMM, и понадеялся, что в ближайшее время найду нормальное доказательство -- но времени-то и не оказалось. Насколько я понимаю, вы просто не сможете построить такую commitment sequence, где это самое чтение 5-3 идет против so.

      Удалить
    3. Руслан, а Вы не написали в комментариях про ошибочность доказательства, чтобы развлечь читатателей вашего блога?:)

      Удалить
    4. Ну во-первых пост писался в ходе подготовки к докладу про JMM -- и цель была в том числе понять, насколько люди вообще понимают модель рассуждений, которую предлагает JMM. И когда я обнаружил ошибку, то решил оставить как есть -- насколько быстро кто-нибудь найдет ошибку? Вы, собственно, первый.

      А во-вторых -- ну неловко было, конечно, так громко размотать, а потом облажаться. Поначалу горело все-таки засесть за commitment procedure, доказать (собственно, известно, что утверждение-то правильное, за это сам Даг Ли поручился), но так и не сраслось. А позже уже не до того стало.

      Удалить
    5. А я тоже перечитывал с месяц-полтора назад и смутился. Но как-то застремался отрепортить.

      Удалить
    6. Доказательство через comittment procedure от Алексея Шипилева читаем на concurrency interest

      Удалить
    7. Только судя по обсуждению там в доказательства такая же ошибка

      Удалить