lazySet: тайные страницы JMM

Подолжая раскрывать темы, недостаточно раскрытые на докладе -- сейчас про lazySet. Тема это непростая, и не потому, что там все сложно, а потому, что нужно повторить основы JMM. У меня уже давно бродит мысль написать цикл статей "Скрытые главы JMM", но все руки не доходят -- это ж надо будет advanced JMM перечитать внимательно и пристально, все теоремы разбирая... Вот, может, в старости...

Так что сейчас будет краткое введение, голопом по европам.

Дисклаймер: все что идет дальше -- это мое личное понимание JMM. Оно может быть неполным, неправильным, и вообще полной херней. Я вас предупреждал!

...Когда пишут про JMM -- почти всегда пишут про частичный порядок "происходит до" (partial happens before order). Это действительно самая ходовая часть JMM -- в большинстве практических случаев достаточно знать правила формирования ребер HB, и счастье будет уже здесь, и моментально.

Но JMM гораздо более сложная конструкция, чем только HB. JMM -- это такой набор ограничений на исполнение java кода. Эти ограничения позволяют сделать одно очень сильное утверждение относительно возможных сценариев его исполнения. А именно: если у нас в коде нет гонок (data race), то любой сценарий исполнения будет sequentially consistent.

По пунктам: что такое гонки (data race)? Пусть у нас в программе есть разделяемая (т.е используемая из >1 потока) переменная, и хоть один поток в нее пишет. Почему важна запись понятно: если никто не пишет, а все только читают, то это не интересно, никаких конфликтов. А вот если есть запись и чтение(-я) -- тогда все любопытнее. Если запись и чтение не упорядочены (через HB) то говорят, что этот набор инструкций (запись и чтения) образует гонку. Код без гонок называется data race free, DRF

В чем проблема с гонками? В том, что в них становятся заметными весь тот треш, угар и содомия (для наших читателей из Питера: здесь нет пропаганды гомосексуализма, я гарантирую это!), которую творят с вашим кодом современные оптимизирующие компиляторы и (в большей степени) современные CPU и контроллеры памяти. Все эти instruction reordering, out-of-order execution, speculative branch prediction, write combining, и прочие ужасы царизма. Это то, что, по-идее, программисту видно быть не должно -- ибо он поседеет, если это увидит. Другими словами: в коде с гонками начинают течь широко используемые абстракции -- что код исполняется так, как вы его написали, что память у нас общая и однородная, и т.п. Вы начинаете видеть грязную кухню реального мира :)

Вернемся к баранам. Что такое sequentially consistent (SC) execution? Неформально: SC для многопоточной программы -- это когда ваш код исполняется так, как будто он исполняется на единственном устройстве выполнения, безо всяких буферов, кэшей и внеочередного выполнения операций. Т.е. каждая инструкция атомарна, и ее результат сразу же доступен (виден) всем остальным потокам. Инструкции выполняются строго в том порядке, как они идут в коде. Переход от исполнения кода одного потока к коду другого возможен только в промежутке между двумя инструкциями. Еще проще -- это back to i386. Разумеется, реально ваш код может исполняться как угодно -- но результат в любой точке должен быть только такой, какой возможен при каком-нибудь SC сценарии.

Итак, еще раз, что нам дает JMM: утверждается, что если у нас в коде нет гонок (т.е. все конфликтующие доступы к разделяемым данным упорядочены с помощью нужных ребер HB), то код будет вести себя так, как если бы мы исполняли его на i386. Никакая черная магия которую современные компиляторы, процессоры и контроллеры памяти делают с вашим кодом -- вам заметна не будет. Нам возвращают довольно простой и понятный мир, где компьютер не умничает -- он делает строго то, что написано в вашей программе, именно так, как это написано, в том порядке, как написано, и строго не более того.

Это вовсе не означает, что в SC программе нельзя сделать ошибки. Это лишь означает, что имея гарантию sequentially consistency можно хоть иногда писать правильный код -- потому что список возможных сценариев выполнения становится хотя бы более-менее обозримым


Теперь, когда мы прониклись величием решаемой JMM задачи, можно уже отметить одну мелочь: для того, чтобы доказать свойство (DRF -> SC) одного частичного порядка HB недостаточно. Нужны еще две важных вещи.

Во-первых это причинность (causality). Неформально: что у любого события есть первопричина. Не допускаются циклы причинности: когда А является причиной для Б, а Б -- является причиной для А. Причинность, в частности, запрещает в яве значениям переменных возникать из воздуха ("out of thin air") -- для любого прочитанного из переменной значения должна существовать в коде программы операция записи, которая это значение туда записала (и она не должна происходить после этого чтения). Для явы это архиважно, потому что если бы значение ссылки могло возникнуть из ниоткуда -- вся безопасность языка и среды накрылась бы медным тазом.

Во-вторых, это Total Synchronization Order. В JMM некоторые операции (захват/освобождение монитора, чтение/запись волатильной переменной, и всякая эзотерика, типа условных "первое/последнее действие в потоке", операция запускающая поток, операция обнаруживающая завершение потока... см подробнее JLS 17.4.2) объявлены как Synchronized Actions. Особенность этих SA в том, что они образуют Total Synchronization Order. Ключевое здесь именно total -- полный порядок, в отличие от partial happens-before order, который частичный порядок.

Частичный порядок означает, что между некоторыми операциями есть точно определенный порядок -- А всегда (во всех сценариях исполнения) идет до Б. А между некоторыми операциями такого однозначного порядка нет -- в одних сценариях исполнения В может идти до Г, в других -- Г до В. И более того -- в одном и том же сценарии исполнения один поток может видеть сначала результат Г, а потом результат В, а другой поток -- сначала результат В, а потом Г. Т.е. порядок В и Г не определен в обоих смыслах: и поскольку он в разных сценариях (запусках) может быть разным, и поскольку даже в одном сценарии он может видиться разным с разных точек зрения.

А вот полный порядок означает, что между любыми двумя операциями всегда есть какой-то порядок. Либо А до Б, либо Б до А -- третьего не дано. И этот порядок всеми виден одинаково.

То есть тот факт, что synchronization actions образуют полный порядок означает (в переводе с математического на русский), что любая пара synchronization actions всегда упорядочена, и этот порядок виден всеми потоками программы одинаково.

Получается, что synchronization actions -- они уже sequentially consistent. И чтобы получить SC для всей программы нам осталось только как-то "растянуть" эту sequentially consistency на все остальные инструкции в коде. И мы это делаем с помощью частичного порядка happens-before -- присоединяя по транзитивности к уже существующим и всегда упорядоченным synchronization actions обычные инструкции. И если нам удастся по транзитивности присоединить все инструкции в программе (а это удастся если в программе нет гонок) -- то мы и получим SC для всей программы в целом!

То есть, если очень кратко -- мы создаем в программе становый хребет из synchronization actions, которые по-определению sequentially consistent. И ребрами HB присоединяем к нему то, что можно присоединить. Если в программе нет гонок -- то нам удастся присоединить все инструкции, и вся программа окажется доказуемо SC.


Зачем вся эта длительная история? Нужно понимать, что обеспечение для целого множества инструкций полного порядка, который одинаково виден всем потокам -- это несколько более сложная штука, чем просто упорядочить пару инструкций в двух конкретных потоках. Вот например:

volatile va = 0;
volatile vb = 1;
a = 0;

//Thread 1:
va = 1;
a = vb;

//Thread 2: 
print( "va=" + va + ", a=" + a ); 
//может ли вывести "va=0, a=1"?

Может этот код вывести "va=1, a=0"? Т.е. может ли быть a = vb переставлено до va = 1?

Обычные ребра HB этого не запрещают: записи идущие после volatile write можно переставлять до нее, а волатильное чтение образует HB только с волатильной записью той же переменной -- чего здесь нет.

Однако если допустить, что такая перестановка возможна и допустима, то мы получаем ситуацию, когда Thread 1 видит (в соответствии со своей внутри-поточной семантикой) сначала волатильную запись va=1, а потом волатильное чтение a=vb. А Thread 2 видит другой порядок -- сначала чтение vb, потом запись va. А это означает, что у нас нет единого, согласованного между всеми потоками порядка SA-операций. То есть такая перестановка недопустима, ее нужно запрещать.

Вот здесь мы подходим (наконец-то! вы там еще не уснули?) различию между volatile write и lazySet.

Для того, чтобы обеспечить обычное ребро HB между volatile write и read одной и той же переменной достаточно всего двух барьеров -- store-store до записи:

membar(store&load|store)
store va

и load-load после чтения:

load va
membar(load|store&load)

Этого достаточно, чтобы все, что было записано до store va было гарантированно видно после load va. Но этого не достаточно, чтобы обеспечить TSO -- нужно еще запретить реордеринг для synchronized actions. И вот для этого нужен дополнительный StoreLoad после записи:

membar( store&load | store )
store va
membar( store | load )

Именно отсутствием этого store-load и отличается lazySet. lazySet не является sychronized action, он не участвует в total synchronization order, и обходится без соответствующего барьера. А store-load -- единственный необходимый явный барьер на x86 (остальные выполняются неявно, в силу довольно большой строгости аппаратной модели памяти x86). Реализуется он как lock add %esp, 0x00 -- и это довольно дорогая операция. Поэтому если вы можете доказать корректность своей программы без того, чтобы какая-то конкретная волатильная запись была частью TSO -- можно на нем сэкономить. Правда, доказать это весьма непросто. Единственный известный мне метод -- это прислать код в concurrency-interest на ревизию Дагу Ли лично :)

[*] JSR-133 Cookbook for compile writers