9 декабря 2011 г.

Гарантии для final-полей

На днях была интересная переписка с Глебом Смирновым, автором статьи про модель памяти на Хабре. Мы обсуждали тонкости спецификации final-полей. Камнем преткновения был такой пример:
public class A {
    public int value;
    public final int finalValue;

    public A(final int value, final int finalValue) {
        this.value = value;
        this.finalValue = finalValue;
    }
    ....
}

//где-то в коде Thread1:
public A sharedReference = new A();

//где-то в коде Thread2:
if( sharedReference != null ){
    //
    final int finalValue = sharedReference.finalValue;
    final int value = sharedReference.value;
}
Довольно общеизвестно, что спецификация final-полей в JMM гарантирует, что доступ к .finalValue корректный (== запись значения в .finalValue внутри конструктора происходит до чтения .finalValue через общедоступную ссылку, присвоенную после завершения конструктора). Вопрос в том, является ли корректным в том же смысле чтение поля .value? Т.е. можно ли сесть на хвост (piggyback) той магии, которая приводит к корректной передаче значений final-полей между потоками?

На первый взгляд кажется, что можно -- ведь обычные ребра happens-before транзитивны: A hb B, B hb C => A hb C. При этом дано, что действия, идущие до А в program order идут до А и в happens-before order -- т.е. в рамках одного потока частичный порядок HB совпадает с порядком инструкций в коде программы. Значит, поскольку присвоение значения полю .value в конструкторе происходит до присвоения .finalValue, а присвоение .finalValue происходит до чтения в потоке 2, а оно, в свою очередь, происходит до чтения .value в потоке 2 -- то по транзитивности получается, что присвоение .value в конструкторе happens-before чтения .value в потоке 2.

Однако©, на самом деле© -- это неправда. Ну, мне так кажется :)



Во-первых, определение отношения порядка в случае операций с final-полями содержит такое уточнение (Евангелие от ИоанаJMM, 17.5.1): Given a write w, a freeze f, action a (that is not a read of a final field), a read r1 of the final field frozen by f and a read r2 such that hb(w, f), hb(f, a), mc(a, r1) and dereferences(r1 , r2), then when determining which values can be seen by r2, we consider hb(w, r2) (but these orderings do not transitively close with other happens-before orderings). (выделение мое)

То есть то отношение порядка, порождаемое семантикой final-полей -- это такое особое happens-before. Оно почти как обычное happens-before, но не транзитивно с ним.

Во-вторых, чтобы быть совсем строгим, я попытаюсь продраться через формальное определение семантики в 17.5.1. Читать такое на русском я когда-то очень неплохо умел, но буржуйский -- другое дело, так что прошу ногами пианиста не бить, он играет как умеет. Лучше в комментариях предлагайте свои варианты трактовки. Итак, поехали:



Чтобы определить семантику final-полей нам понадобится несколько новых терминов. А именно:

Заморозка (freeze) -- это специальное действие, которое происходит в момент завершения (нормального, или с выбросом исключения) конструктора объекта, содержащего final-поле.

Помимо заморозки нам понадобятся еще два специальных частичных порядка (кроме уже всем знакомого happens-before):
  • порядок разыменования (dereference chain, обозначается далее как dereferences(a,b))
  • порядок доступа к памяти (memory chain, обозначается далее как mc(a,b))
Оба этих порядка считаются частью сценария выполнения (трассы над кодом, execution), и поэтому, для конкретного сценария, считаются фиксированными. Эти два частичных порядка должны удовлетворять определенным ограничениям (но решение, удовлетворяющее этим ограничениям, не обязано быть единственным)


То, что идет дальше, лично мне кажется смесью определений самих порядков ("что такое MC/DC"), и условий (которые формулируются, в том числе, в терминах только что введенных MC/DC), которым должны удовлетворять допустимые по JMM сценарии исполнения. Мне это кажется очень неудобным для восприятия, но я оставляю эту часть как она есть

Порядок разыменования, dereferences: Если A -- чтение/запись поля объекта О, причем О инициализирован не текущим потоком, тогда в текущем потоке должна существовать операция чтения R, которая видит адрес объекта О, и такая, что dereferences(R, A). Другими словами: операция чтения адреса объекта должна происходить до (в смысле порядка разыменования) любой операции чтения/записи полей объекта.

Порядок доступа к памяти, mc:
  1. Если чтение R видит результат записи W, то mc(W,R) (запись происходит до чтения в смысле частичного порядка доступа к памяти)
  2. Если dereferences(А,Б) (А происходит до Б в смысле порядка разыменования), то и mc(А, Б) (А происходит до Б и в смысле порядка доступа к памяти) Т.е dereferences является "подмножеством" mc.
  3. Если W -- запись адреса объекта О, производимая не тем потоком, который О инициализировал, то, в этом же потоке должно существовать некоторое чтение R, которое видит адрес объекта О, и такое, что mc(R,W) (R происходит до W в смысле порядка доступа к памяти)


Теперь само определение семантики final-полей:
Дано:
  1. Некоторая запись W
  2. Заморозка F
  3. Произвольное действие с памятью (кроме чтения final-поля) A
  4. Чтение R1 финального поля, замороженного F
  5. Чтение R2
Пусть между собой эти действия связаны такими соотношениями: hb(W,F), hb(F, A), mc(A, R1), dereferences(R1, R2).

Тогда: определяя, какие значения могут быть прочитаны R2, мы можем полагать, что W и R2 связаны порядком happens-before: hb(W, R2). Но: это отношение порядка не транзитивно с другими отношениями порядка HB.

Отдельно заметим, что отношение порядка разыменования (dereferences) рефлексивно -- т.е. dereferences(a,a) всегда верно. Поэтому в определении выше R2 может совпадать с R1.

Только те записи, что подходят под определение семантики final-полей -- гарантированно упорядочены до чтения final-поля. (Я понимаю этот пункт просто как еще одно напоминание, что гарантии, даваемые для final-полей распространяются ровно настолько, насколько указывает данное определение, и не дальше)



Теперь попробую изложить то же самое на простом языке и более развернуто.

hb(W,F): Наша "некоторая запись" происходит до завершения конструктора, или до "заморозки", что то же самое в данном случае.

hb(F, A): "некоторое действие с памятью" происходит после завершения конструктора ("заморозки").

mc(A, R1): Чтение final-поля видит результат "некоторого действия с памятью"

dereferences(R1, R2): R2 это либо само чтение значения поля (т.е. R2==R1), либо это чтение поля/элемента какого-то объекта, доступного по цепочке ссылок, начинающейся в final-поле.

Что это за загадочное "некоторое действие А"? Насколько я понимаю смысл -- это должна быть публикация ссылки на объект. Но точнее описать не могу -- для меня пока загадка, почему же это действие описано настолько абстрактно -- может ли А быть чем-то кроме публикации ссылки?



Уф. Выдыхаем...

Что можно видеть из этого определения? Во-первых, возможности "сесть на хвост" -- по крайней мере, в том смысле, в котором был пример в начале статьи -- нельзя. Семантика final-полей гарантирует видимость записей, идущих до freeze только для тех чтений, что идут через цепь разыменований, начиная с самого final-поля. Поскольку увидеть .value через эту цепь нельзя, то видимость значения, записанного в это поле в конструкторе не гарантируется.

В этом определении мне интересны еще несколько вещей (помимо его зубодробительности, конечно).

Во-первых, оно идет в некотором смысле в обратном направлении по отношению к обычным определениям JMM. В "обычном" определении логика такая: мы сначала определяем упорядоченность действий (через набор правил порождения ребер happens-before + транзитивность), а потом говорим, что если hb(А,Б) => то Б гарантированно видит результат действия А. Здесь же ситуация обратная: мы говорим, что если Б видит результат А => то определенные действия происходящие до А происходят до определенных действий, происходящих после Б.

Во-вторых здесь необычная ситуация с определением того, для каких операций чтения/записи пригодно это определение. Формально все начинается с любой операции записи, идущей до заморозки. Но в конце оказывается, что ребро HB можно установить по этому определению начиная с любой записи -- да не к любому чтению. А поскольку ребро это еще и не транзитивно -- то получается, что ограничивая спектр операций чтения, на которых ребро может заканчиваться -- мы тем самым ограничиваем и спектр операций записи, на которых оно может начинаться. А именно: ребро может начинаться только на таких операциях записи, результаты которых могут увидеть чтения из того самого ограниченного списка. Для других операций записи эффект ребра HB просто не наблюдаем :) Причем если бы нам оставили транзитивность -- мы бы могли по транзитивности продлить ребро HB с "разрешенного" чтения до следующей в program order операции, которая уже могла бы быть любым (в том числе и "не разрешенным") чтением. Но у нас транзитивность отобрали. И поэтому вместо любой операции записи это определение позволяет проводить ребра HB только от таких записей, которые а) происходят до завершения конструктора б) результаты которых видны по цепочке ссылок начиная с final-поля, инициализированного в этом конструкторе.

В третьих, обратите внимание, что от записей W не требуется, чтобы они происходили внутри конструктора. Они могут происходить где угодно, только бы была возможность показать, что они происходят до завершения конструктора (до заморозки). Это как раз и означает, что мы можем передать в конструктор объекта сколь угодно сложный объектный граф, заполненный где-то на стороне (но гарантированно до окончания конструктора), присвоить в конструкторе ссылку на него final-полю, и далее мы можем быть уверены, что всё его содержимое будет видимо любому потоку, читающему граф через разыменование final-поля. Это тоже своеобразный piggybacking, и вот такой piggybacking моделью памяти джавы разрешен.

17 комментариев:

  1. public Data(final int value, final int finalValue) {
    this.value = value;
    this.finalValue = finalValue;
    }

    Это конструктор?

    ОтветитьУдалить
  2. Этот комментарий был удален автором.

    ОтветитьУдалить
    Ответы
    1. Руслан, учитывая, что в статье не приводится конкретный пример с указанием действий {w, f, a, r1, r2} и доказательством существования hb(w, r2), я думаю, что предлагаемый пример добавит полезность статье.

      Дано:
      Класс A содержит только одно поле final fx; thread1 создаёт объект new A(), после чего сохраняет ссылку на объект в общее поле A.o; thread2 читает значение общего поля A.o и по счастливой случайности видит там !null, т.е. ссылку на объект, созданный thread1, после этого thread2 читает поле A.o.fx.
      Доказать:
      Что при указанном исполнении существует hb(запись fx в конструкторе A, чтение A.o.fx в thread2).
      Замечание:
      Конкуррентный доступ к A.o происходит через гонку, т.к. иначе мы и без семантики final обошлись бы для доказательства.

      Код:
      class A {
      static A o;
      final int fx;
      A() {
      fx = 1;
      }
      }

      thread1
      A.o = new A();

      thread2
      A o = A.o;
      if (o != null) {
      int result = o.fx;
      }

      Нас интересуют следующие действия в нитях (в квадратных скобках указаны обозначения действия):
      thread1
      [w] write fx
      [f] freeze
      [a] write A.o
      thread2
      [ro] read A.o
      write o
      [r1, r2] read o.f

      Формальная семантика final говорит что если:
      w - некоторая запись
      r1 - чтение final поля (в нашем лучае чтение o.fx)
      a - некоторое действие не являющееся чтением final поля (в нашем случае запись A.o, т.е. публикация ссылки на сконструированны в thread1 объект)
      f - фриз (в нашем случае случился при завершении конструктора)
      r2 - некоторое чтение, в котором нас интересует возможный результат
      и выполняются отношения
      (1) hb(w, f)
      (2) hb(f, a)
      (3) mc(a, r1)
      (4) dereferences(r1, r2)
      то r2 видит w и существует отношение hb(w, r2), которое хотя и обозначается зачем-то привычным hb, но является совсем другим отношением, т.к. не транзитивно с частичным порядком hb.

      Покажем, что необходимые нам отношения (1) - (4) действительно существуют в рассматриваемом исполнении:
      (1) po(w, f) ⇒ hb(w, f) - т.к. в well formed исполнении hb являтся транзитивным замыканием po и sw, а другие исполнения JMM не рассматривает, т.е. JVM их произвести не может
      (2) po(f, a) ⇒ hb(f, a) - аналогично предыдущему
      ro видит a ⇒ mc(a, ro) - по определению частичного порядка mc
      (thread2 не конструировал объект o) ∧ (r1 является чтением поля объекта o в thread2) ∧ (ro является единственным чтением адреса объекта o в thread2) ⇒ defererences(ro, r1) - по определению частичного порядка dereferences
      defererences(ro, r1) ⇒ mc(ro, r1) - по определению частичного порядка mc
      (3) mc(a, ro) ∧ mc(ro, r1) ⇒ mc(a, r1) - частичный порядок транзитивен по определению, а mc является частичным порядком
      (4) r1 = r2 ⇒ dereferences(r1, r2) - частичный порядок рефлексивен по определению, а dereferences является частичным порядком

      Итак, мы показали существование отношений (1) - (4), следовательно в соответствии с Java 7 JLS 17.5.1 выполняется hb(w, r2).

      Удалить
    2. Валентин, только не hb(w, r2) - а точечный freeze hb(w, r2), я бы обозначал его как fhb(w,r2).

      Удалить
    3. Вообще недостает модификатора folatile. Это такая штука которая будет и freeze обеспечивать при конструировании и обычный hb при дальнейшем видоизменении. Хотя конечно и обычный volatile можно безопасно опубликовать просто для этого лишний напряг извилин нужен.

      Удалить
    4. >>недостает модификатора folatile
      Скорее просто volatile'у недостаёт той части семантики final, которая про точечный hb. Из-за этого, например, в случае передачи ссылки на объект new AtomicInteger(42) через data race, get() может вернуть значение по умолчанию, т.е. 0.

      Удалить
    5. Учитывая, что по утверждению Дага Ли, ему не известны реализаций JVM, в которых бы описанная ситуация могла случиться (http://cs.oswego.edu/pipermail/concurrency-interest/2013-November/011966.html), и утверждение Лёши Шипилёва о том, что не осталось железа, на котором упомянутая ситуация возможна (https://www.youtube.com/watch?v=iB2N8aqwtxc#t=5990), легкопонятно, что добавление части семантики final к volatile никак бы не отразилось на производительности.

      Удалить
    6. Коллеги, очень хорошо, что вы здесь без меня разобрались :)

      Насчет добавления семантики final к volatile -- меня лично больше волнует не производительность, а сложность формальной семантики. Т.е. сейчас-то JMM состоит из HBMM (которой в обед 100 лет, которая общий знаменатель всех не-SC моделей, в которой много нетривиальных вещей для новичков, но эти вещи не-новичкам уже давно известны) + finality (которая вполне себе отдельная штука, с конкретной узкой целью и областью применимости) и causality procedure, которая в нормальной работе никому нафиг не сдалась. А вот как будет выглядеть формализм с усиленными volatile -- для меня пока вопрос. Есть небольшие старческие опасения, что в угоду упрощению жизни для новичков будет усложнение формализма для остальных.

      Удалить
    7. вот и Даг Ли пишет, что он не знает простых способов сделать такое изменение в JMM.
      Посмотрим, что принесёт нам JMM9

      Удалить
    8. Этот комментарий был удален автором.

      Удалить
    9. >>не знает простых способов сделать такое изменение в JMM.
      Гм... Ну есть же механизм обеспечения freeze - ну натравили бы его на первичную инициализацию volatile из конструктора.
      ИМХО: это не делают по политическим соображениям

      Удалить
    10. Механизм реализации конечно есть. Речь идет о механизме _формализации_. Представьте на секунду, что в описание семантики volatile просто "вклеено" описание final -- со всеми этими memory ordering chains, reference ordeing chains, freeze, tainted, etc... Можно ли это формализовать проще -- это и есть вопрос, который меня волнует (и Дага, видимо, тоже). Обычную семантику volatile и то один из 10 нормально понимает.

      Удалить
    11. Этот комментарий был удален автором.

      Удалить
    12. http://cr.openjdk.java.net/~jrose/draft/lazy-final.html
      Дождались

      Удалить
  3. >>po(w, f) ⇒ hb(w, f) - т.к. в well formed исполнении hb являтся транзитивным замыканием po и sw, а другие исполнения JMM не рассматривает, т.е. JVM их произвести не может<<

    должен поправить себя:
    po(w, f) ⇒ hb(w, f) - т.к. в well-formed исполнении hb являтся транзитивным замыканием po и sw, а JVM обязана производить результаты, предсказуемые с помощью JMM, которая предсказывает только well-formed исполнения.

    Т.е. на самом деле JVM может какое угодно исполнение программы осуществить, если оно приводит к результатам, которые можно объяснить каким-нибудь well-formed исполнением разрешённым JMM.

    ОтветитьУдалить
  4. Этот комментарий был удален автором.

    ОтветитьУдалить