23 апреля 2012 г.

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

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

  1. Я вот как раз хотел у тебя спросить, не пробовал ли ты доказать корректность работы смазнаешьчего при использовании lazySet. Думаешь, Disruptor guys отправляли код Дагу Ли? :)

    ОтветитьУдалить
  2. Не знаю, отправляли ли они, но я -- отправлял :) Даг ответил, что конкретно в этом use case есть гарантии корректности, хотя для доказательства прогресса нужны дополнительные предположения

    ОтветитьУдалить
  3. А доказательства он не приводит? Вышел бы интересный матан-псто :)

    ОтветитьУдалить
  4. Ну в принципе, формальных доказательств тут быть не может -- я ж пишу, что lazySet находится вне текущей редакции JMM, поэтому как его включать в построения на ее основе -- непонятно. Т.е. не только мне непонятно -- вообще непонятно, потому что это будет второй всего случай, когда у нас в JMM есть инструкции, порождающие между-поточные HB, и при этом эти инструкции не являются SA, и не участвуют в TSO.

    Для примера: первый случай -- это final поля :) И ты можешь оценить объем работы, который потребовался чтобы их вписать в JMM :) И сложность правильного понимания их семантики ;)

    ОтветитьУдалить
  5. Мда, веселье с осознанием final помню :)

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

    ОтветитьУдалить
  7. Пробовал померять способности наиболее популярных библиотек акторов:
    https://github.com/plokhotnyuk/actors

    Но по ходу попалась на глаза MPSC очередь на сайте у Дмитрия Вьюкова:
    http://www.1024cores.net/home/lock-free-algorithms/queues/non-intrusive-mpsc-node-based-queue

    Было сделано несколько попыток допилить существующие (как раз за счет рискованного использования lazySet):
    https://github.com/plokhotnyuk/actors/blob/master/src/main/scala/com/github/plokhotnyuk/actors/Actor2.scala
    https://github.com/plokhotnyuk/actors/blob/master/src/main/scala/com/github/plokhotnyuk/actors/UnboundedMailbox2.scala
    ...и запилить собственный базирующийся на выделенном потоке:
    https://github.com/plokhotnyuk/actors/blob/master/src/main/scala/com/github/plokhotnyuk/actors/ThreadBasedActor.scala

    В итоге последний на максимальных нагрузках разгоняется к скоростям сравнимым с Distruptor (100M сообщений в сек. для теста OnePublisherToOneProcessorUniCastThroughputTest.java на аналогичной аппаратуре и конфигурации):
    https://github.com/plokhotnyuk/actors/blob/master/out1.txt#L328

    Осталось только доказать что там везде ошибки чтобы никто не заюзал...

    ОтветитьУдалить
  8. Я посмотрю код чуть позже -- скала не мой родной язык :) Но навскидку 100М/с кажется очень высокой цифрой. Как бы там не было косяков с бенчмарками...

    ОтветитьУдалить
  9. Для сравнения результаты тестов distruptor на той же конфигурации и настройках JVM как у out1.txt:

    OnePublisherToOneProcessorUniCastThroughputTest run 0: BlockingQueue=5 349 596 Disruptor=73 855 243 ops/sec
    OnePublisherToOneProcessorUniCastThroughputTest run 1: BlockingQueue=5 220 296 Disruptor=77 700 077 ops/sec
    OnePublisherToOneProcessorUniCastThroughputTest run 2: BlockingQueue=5 313 778 Disruptor=73 800 738 ops/sec


    ThreePublisherToOneProcessorSequencedThroughputTest run 0: BlockingQueue=6 808 742 Disruptor=19 319 938 ops/sec
    ThreePublisherToOneProcessorSequencedThroughputTest run 1: BlockingQueue=6 945 409 Disruptor=19 065 776 ops/sec
    ThreePublisherToOneProcessorSequencedThroughputTest run 2: BlockingQueue=6 301 594 Disruptor=19 940 179 ops/sec

    ОтветитьУдалить
  10. @andriy

    Я тут добрался посмотреть на MPSC-queue. Месяц провисела открытая страница в браузере :)

    Ничего особо нового там нет: если взять j.u.c.CLQ, и оптимизировать ее под единственного dequeuer-а, как раз что-то в таком духе и получится. Что эта штука может быть достаточно быстрой -- в этом сомнений нет, та же CLQ у меня давала ~10M/s. Но что она может быть быстрее D -- крайне сомнительно.

    И там, и там 1 CAS на арбитрацию в enqueue. D немного проигрывает за счет того, что он bounded -- ему при записи нужно проверять, что он свой хвост не кусает. Но при этом он на порядок лучше по кэш-локальности. Плюс к тому, если мы предположим, что Node занимает ~30 байт, то 100М/с означает аллокацию 3Гб/с только на внутреннюю механику в MPSC. У меня есть сомнения, что GC способен справиться с такой нагрузкой, и не замедлить при этом существенно приложение в целом.

    Вы не замеряли установившийся размер очереди в ваших тестах?

    ОтветитьУдалить
  11. Правильно ли я понимаю, что lazySet в Atomic это оно и есть? Но верно ли, что при вызове get мы получим актуальное значение переменной? Ведь то, что вы описываете - это store load barrier для двух разных волатильных переменных. А что есть мы сделаем lazySet в переменную, а потом ее же и прочтем?

    ОтветитьУдалить
  12. Да, это и есть AtomicXXX.lazySet()

    А какое значение переменной вы считаете "актуальным"?

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

    ОтветитьУдалить
  13. Актуальное в смысле последнее установленное... Я имел ввиду связаны ли lazySet и get happens before? Видимо из за отсутствия StoreLoad ответ нет, то есть видимость lazySet не обеспечивается читающему потоку. Или я ошибаюсь?

    ОтветитьУдалить
  14. lazySet образует HB с get, вернувшим то значение, которое было записано lazySet. То есть здесь все как для обычных volatile store/load.

    ОтветитьУдалить
  15. А именно с тем get, который вернул значение записанное lazySet? То есть из за отсутствия StoreLoad get вызванный после lazySet может вернуть устаревшее значение? Тут мы правда опять приходим к тому, что хронология событий на многопроцессорных машинах это некорректное понятие

    ОтветитьУдалить
  16. >А именно с тем get, который вернул значение записанное lazySet?

    А попробуйте объяснить, что означает HB между a.lazySet(4) и a.get()->5 ?

    "Устаревшее значение" это очень расплывчатое понятие. Лучше с ним не связываться, оно только запутывает.

    Если вы в одном потоке записали в а=1, и в другом прочитали из а единицу -- значит чтение произошло как-бы-после записи. Из-за различных источников переупорядочиваний это как-бы-после ничем вам особо не помогает -- например, вы вовсе не можете утверждать, что записи, выполненные в первом потоке до а=1 будут видны во втором потоке после чтения единицы из а. А вот если запись и чтение в а волатильные -- это как-бы-после становится практически нормальным строгим "после". Его можно скомбинировать с отношением до/после внутри каждого потока, и таким образом установить порядок между целым множеством инструкций в разных потоках. В этом -- в транзитивности -- смысл нотации HB. И в этом смысле lazySet делает то же самое, что и volatile store.

    Но пользуясь только отношениями между двумя потоками вы можете получить глобально противоречивое отношение порядка инструкций. Точнее -- нет возможности доказать, что такие парные межпоточные взаимодействия дадут в конце непротиворечивый глобальный порядок. Без этого порядка в принципе можно жить -- но поведение программы становится сильно сложнее анализировать, возможны довольно сложные и неочевидные ситуации. Чтобы не взорвать мозг обычным программистам (ха-ха) -- авторы JMM ввели TSO -- его наличие позволяет доказать, что глобальный порядок всегда получится если в программе нет гонок.

    ОтветитьУдалить
  17. Я правильно понимаю что все что определять jmm, это вещи вроде, если один поток увидел какое то действие второго, то все предыдущие действия первого так же видны второму. А вот момент когда второй поток это увидит не определяется. Иными словами есть ли вообще для каких либо конструкций гарантия прогресса? Вроде как jsr 133 cookbook предлагает вставлять memory barriers, которые могли бы стать гарантией прогресса, но ведь никто не обязан реализовывать jmm именно так.

    ОтветитьУдалить
  18. Да, большинство гарантий, даваемых JMM они именно такие: если "нечто" уже случилось, то вот "это" и вот "то" тоже должно уже случиться. Другими словами, если ты (компилятор/процессор) откладываешь A -- будь добр заодно отложить и (Б, В...). Насколько долго ты можешь отложить А -- здесь не определяется, покуда ты откладываешь и все, что еще должен отложить.

    Даже поваренная книга вам здесь не поможет, потому что барьеры памяти в ее терминологии -- это тоже довольно абстрактная штука, они точно так же задают порядок, не гарантируя прогресса. Конкретный барьер на конкретной архитектуре _может_ задавать и какие-то гарантии прогресса (т.е. это может быть описано в спеке), но это уже слишком низкоуровневые детали.

    Задание явных гарантий прогресса находится в очевидном конфликте с доступным потенциалом для оптимизаций. Поэтому на это мало кто идет. Попробуйте найти гарантии прогресса хоть в каком-нибудь высокоуровневом ЯП.

    ОтветитьУдалить
  19. "Обычные ребра HB этого не запрещают: записи идущие после volatile write можно переставлять до нее" - JMM ничего про перестановки не говорит, а отношение HB применимо только при наличии SAs, замкнутых на PO.

    Я правильно понимаю, что это выведено из знаменитого Roach Motel, где разрешается расширять границы критической секции с учетом того, что по факту ( с точки зрения release/acquire семантики ) volatile - это (захват/освобождение монитора)^-1 ?

    ОтветитьУдалить
    Ответы
    1. Я не рискну сказать, что откуда выведено: формальная спецификация описывает поведение volatile read/volatile write/lock enter/lock exit в терминах HB/SA, то есть, в этом смысле, никакая из этих операций не является более фундаментальной, и блокировки и волатильные операции в одинаковом приоритете.

      Исторически, наверное, семантика roach motel влияла на формулировку модели памяти, и в этом, историческом, смысле -- вероятно да, семантика volatile была формализована под влиянием желательной семантики RM.

      volatile в джаве имеют более строгую семантику, чем acquire-release. Acquire/release это как раз lazySet/get

      Удалить