Гарантии для 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 моделью памяти джавы разрешен.