Большинство программистов, работая с многопоточным кодом, осведомлены о примитивах синхронизации. При этом мало кто задумывается о существующей за этим сложной теории.

Привет, Хабр! Меня зовут Игорь Панасюк, я работаю в Яндекс, преподаю в ИТМО и ШАД, а также в свободное время выступаю на конференциях, делюсь опытом в соцсетях и помогаю развитию Go-сообщества, веду Telegram-канал и YouTube-канал.

В этой статье по мотивам моего доклада для Golang Conf я расскажу про Go Memory Model, понятным языком объясню отношение happens before, затрону формализм и разберу его на практических примерах.

Во второй части доклада мы поговорим про линеаризуемость, барьеры памяти, гонки и использование различных нетривиальных техник.  Поехали!

А зачем это нужно? 

Давайте разберёмся. Рассмотрим несложный код на Go. Здесь всего две функции: main и setup. 

Первая запускает горутину setup, а вторая сперва присваивает в переменную value строчку, а потом ставит флаг true — значение проинициализировано.

После этого в main мы крутимся в цикле и ждём, пока флаг станет true, то есть, пока будет присвоено значение. Далее мы печатаем это значение на экран. Давайте разберёмся, что будет на экране — «Hello, GolangConf» или что-то другое. Оказывается, что по итогу выводится пустая строка.

Хотя, казалось бы, всё хорошо — у нас есть флаг, всё отлично! Гофер покраснел, расстроился очень сильно. Запустил race-детектор и понял, что у него проблемы. 

Это ожидаемо — две конфликтующие операции (чтение и запись) без синхронизации. 

Рассмотрим следующий пример, он очень похож на предыдущий:

Здесь тоже две функции, переменная value, в которую присваивается строчка «Hello, GolangConf», после чего запускается горутина doPrint, которая печатает значение на экран. Гофер также ждёт, что будет выведено «Hello, GolangConf». 

В этом случае Гофер радостный, потому что увидел ожидаемую строчку.

Кажется, что между этими двумя примерами нет особой разницы — всё также нет никакой синхронизации, одна общая переменная, две горутины. Но почему-то в одном случае у нас всё плохо, а в другом — хорошо. Давайте разбираться. 

Формализм

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

Прописывать в каждом языке программирования, когда, какая строчка и где переставляется — это очень дорого, т.к. нужно учитывать все платформы. Разработчики не поймут, если вы напишете огромный лист бумаги, какая платформа какие гарантии предоставляет. Поэтому разработчики языков дают программистам модель Memory Model — она есть во всех языках программирования (Java, C++ и др..). Это специальный документ, который в Go описывает, когда изменения в одной горутине станут видны в другой.

Вместо того, чтобы раскрывать детали той или иной платформы, нам дают некоторую модель — по аналогии с моделью процессора. Вот есть CPU, вам никто не скажет, как он работает, ибо на деле там всё очень сложно. Поэтому, например, Intel даёт модель и говорит: «По этой модели можно судить, как работает ваш процессор». Тут то же самое: «Вот абстракция — пользуйтесь, вам не нужно думать о том, что под капотом». 

Но есть проблема. В Go, если вы начнёте читать этот документ, увидите фразу «Don’t be clever»: не надо — оно вас сожрёт.

Но давайте сегодня попробуем аккуратненько разобраться и попробовать применить эту модель на практике.

Go Memory Model описывает модель и формализм, с помощью которого можно доказывать корректность многопоточных программ. От языка к языку модели очень схожи. 

Мы хотим разобраться с этой теорией и научиться применять её на практике, чтобы:

• Писать многопоточный код без багов и уметь доказывать его корректность

Круто, когда мы можем сказать: «Всё хорошо, не разнесёт, блокировочку взяли, всё отлично». Но хочется ещё уметь более формально доказывать, что код корректный и мы при эксплуатации получим ожидаемые результаты.

• Анализировать существующий код при поиске багов

Бывает, что коллега написал многопоточный код, а потом уволился и нам приходится дебагать то, что он написал. Круто, когда есть понимание, как многопоточный код работает, и как формально доказать, работает он корректно или нет. 

Итак, мы будем использовать некоторый формализм. Как он выглядит? Во-первых, формализм строится на операциях. Во-вторых, операции в Go могут быть обычные (например, присваивание) или синхронизированные (atomic, mutex и т.д.). В-третьих, мы оперируем не программой, а её исполнением. Исполнение — это множество операций и их исходов в рамках запуска программы.

Очень важно понимать, что когда вы два раза запускаете многопоточный код, результаты могут быть совершенно разные. Исполнение отличается от запуска к запуску, потому что код многопоточный. Буквально поток немножко не так пошедулили и всё пошло по-другому. 

Операции и их обозначение:

• v.w(1) — запись 1 в v 

• v.r(1) — чтение 1 из v

Рассмотрим абстрактный пример. 

Есть две горутины: G0 пишет что-то в переменную V единицу, G1 читает из переменной V ноль, потом единичку. Это одно из исполнений. Важно понимать, что когда я запущу ещё раз этот код, всё может быть совсем иначе. 

Если я не позаботился о синхронизации, у меня могут совершенно быть другие события, потому что исполнение — не равно исходный код.

Основная идея модели памяти в том, чтобы упорядочить события. Нам, как программистам, хочется понимать, как наша многопоточная программа работает для любого исполнения. Поэтому, в Go вводятся формальные отношения:

1. Sequenced before (порядок операций внутри горутины)

Отношение применимо к событиям внутри одной горутины. Например, я вижу, что у меня в горутине G0 запись до чтения — отлично, у меня есть такая гарантия, всё корректно.

2. Synchronized before (синхронизированный порядок операций между горутинами)

Это отношение нужно, чтобы описывать порядок между синхронизированными операциями. Например, я взял mutex, отпустил, потом взял ещё раз. На основании этих синхронизированных операций могу построить порядок на общих переменных между горутинами. 

Важно понимать, что в одной горутине с помощью sequenced before мы описываем порядок операций внутри горутины, а с помощью synchronized before — порядок операций между горутинами.

Но есть более мощное отношение happens before, которое встречается во всех языках программирования.

Happens before является транзитивным замыканием объединения sequenced before и synchronized before. 

Что значат страшные слова «транзитивное замыкание»?

• Если A sequenced before B в одной горутине, то A happens before B

Если я знаю, что у меня в одной горутине событие A было до события B, то A happens before B 

• Если A synchronized before B (через механизмы синхронизации), то A happens before B

Если я, например, взял mutex, и знаю, что у меня событие A было до события B через какие-то другие механизмы другие синхронизации, то всё отлично — A happens before B.

• Если A happens before B, а B happens before C, то A happens before C (транзитивность)

Если я знаю, что у меня событие A было до события B и событие B до события C, то cобытие A было до события C — транзитивность, самое важное свойство.

Используя эти правила, мы можем описывать порядок событий в программе.

Подведём промежуточный итог.  Отношение happens before: 

• Является строгим частичным порядком (антирефлексивность, транзитивность, асимметричность)

Простыми словами, не для каждой пары операций в нашей программе есть это отношение. Например, есть присваивание в одной горутине, а есть в другой, но между этими присваиваниями я не могу применить вышеописанные отношения. Поэтому, happens before вводится именно на ограниченном подмножестве эвентов в нашей программе. 

• Это отношение используют, чтобы доказывать корректность многопоточных программ и предоставлять гарантии для thread-safe объектов в различных языках программирования.

Однако в Go все-таки чаще используют synchronized before (пример c sync.Once)

Давай разберемся, как можно на практике применять эти отношения. Сначала рассмотрим более формальные примеры, а дальше перейдём к практике. 

Практические примеры

Разбираться будем на примере той же программы, которую мы рассмотрели. 

Она была корректная. Попробуем, используя эти отношения, формально доказать, что эта программа работает. 

С виду тут никаких примитивных синхронизаций нет. Хотя, казалось бы, есть value — к нему обращаются сразу две горутины с конфликтующими операциями. Как так вышло и почему value нельзя переставить, например, после go doPrint()? 

Мы строим такой граф, такое исполнение, как ниже. Внимание, вопрос: можем ли мы упорядочить эти операции? Вот наш main.

В горутине main  я знаю, что у меня есть присваивание и запуск горутины doPrint. В рамках одной горутины я пользуюсь отношением sequenced before.

Далее, я открываю memory model, и мне говорят: если я запускаю горутину, то её запуск synchronized before кода, который начинает в ней исполняться. 

Это очень важное утверждение: оно означает, что в этом коде запуск горутины synchronized before кода, который начинает исполняться в ней. На самом деле картина у нас будет такая: событие 3 идёт после события 2.

Далее мы пользуемся транзитивностью и получаем следующее:

Выводим то, что у нас событие 1 было до события 3. То есть, мы формально через эти отношения доказали, что этот код корректный и результат будет ожидаемый при всех возможных исполнениях.

Следующий пример у нас был неудачный, давайте разберём его.

Пронумеруем операции и попробуем что-нибудь доказать.

Для этого я строю такой же граф и пользуюсь тем же самым методом. В горутине main есть порядок между этими двумя событиями, в setup тоже. Но между двумя горутинами никакого порядка нет. 

Формально здесь нет никаких отношений между событиями из разных горутин. Именно это и называется состоянием гонки с точки зрения формализма. Давайте дадим три определения.

Самое простое определение:

Состояние гонки (data race) — состояние во время исполнения программы, когда две операции над переменной происходят из разных горутин без синхронизации, при этом хотя бы одна из них является записью.

Чуть более сложное:

Состояние гонки (data race) — состояние во время исполнения программы, когда две конфликтующие операции над переменной происходят из разных горутин без синхронизации.

И самое сложное на основании формализма из Go memory model:

Состояние гонки (data race) — состояние во время исполнения программы, когда две конфликтующие операции над переменной нельзя разделить отношением happens before.

Очень многие путают data race с race condition. На деле race condition это более общее явление, когда результат зависит от многопоточного порядка событий.. Data race это частный случай с конфликтующими доступами без синхронизации.

В рамках нашего примера мы не можем разделить эти операции отношением happens before, то есть  не можем доказать — значит, может быть что угодно. Это ещё иногда называют UB. 

Давайте это пофиксим, а позже разберёмся, почему такой код решает нашу проблему. 

Заменим обычный boolean на atomic.Bool.

В Memory model Go нам говорят, что:

If the effect of an atomic operation A is observed by atomic operation B, then A is synchronized before B

Нам, как программистам, дали модель atomic операции в Go: если эффект atomic-операции A наблюдается atomic-операцией B, тогда A synchronized before B.  При этом важно, что нам ничего не нужно знать про детали реализации, ассемблерный код этого пакета и т.д. 

Теперь событие 4 будет до события 1. 

Далее, пользуясь транзитивностью, выводим то, что нам нужно:

Мы получаем, что событие 3 произошло до события 2. Мы явно знаем, что присваивание (запись в value) будет до чтения из value, чего мы и добивались.

На самом деле, в Go можно получить такой же эффект, используя, например, каналы. Для них тоже есть отношение synchronized before. 

Вариантов довольно много — например, можно взять вообще mutex:

Мы знаем, что вызов Unlock — это synchronized before вызов Lock. Написали mutex — получили ровно такой же результат. Можно точно так же доказать, что это формально корректная программа.

В следующей части статьи мы поговорим о линеаризуемости исполнения, барьерах памяти (можно ли опустить абстракцию модели памяти), гарантии Go для программ с data race и использование  продвинутых техник. Следите за обновлениями! Вторая часть будет доступна по этой ссылке через неделю!

А пока что мы приглашаем вас на конференцию развития GolangConf — «Онтико» меняет рынок IT-мероприятий! Меньше докладов с блокнотами и заметками — больше живой практики и нетворкинга, чтобы участники были не пассивными слушателями, а активными создателями решений, знаний, новых контактов и инсайтов. Приходите со своими кейсами и узнавайте первыми о ноу-хау в мире GO.

Полезные ссылки

Поизучать:

• Мой канал в Telegram, тут есть много полезных закрытых материалов

• Мой YouTube канал

• Код на Github — всё, что я тут показал

Посмотреть: 

• Видео про устройство атомиков на ассемблере и историю concurrency

• Видео про устройство оперативной и виртуальной памяти

• Видео про устройство процессора

• Видео про ошибки проектирования sync.Once

Почитать: 

• Go Memory Model