Консистентность разделяемой памяти с нуля, часть 1: причинность

Первая часть серии статей на allthoughts.me от автора под псевдонимом Alloth. Основной тезис: модели памяти кажутся запутанными не из-за врождённой сложности, а потому что их плохо понимают даже эксперты. Метод автора - спроектировать виртуальный многопроцессор с ещё более слабыми гарантиями упорядочивания, чем у любой реальной архитектуры, постепенно добавлять атомарные инструкции, пока не будут исключены все классические аномалии, и на основе полученной конструкции критически разобрать модель памяти C++. В первой части рассматривается причинность (causality); операции типа read-modify-write, барьеры памяти (fences) и трансляция в машинный код компилятором обещаны во второй части.

Статья длинная, плотная и категоричная. Несколько наиболее острых утверждений о C++20 принадлежат самому автору и, по его словам, ранее нигде не публиковались. Ниже они отмечены отдельно.

Машина

Модель памяти определяет, как могут наблюдаться изменения разделяемых данных. На уровне железа это означает когерентность для одной ячейки (кэш-линии, единицы арбитража протокола когерентности кэшей) и консистентность между разными ячейками. Автор рассматривает когерентность как полосковый (striped) reader-writer lock поверх RAM, после чего задаёт вопрос, который считает главным для любой архитектуры: в какой момент запись считается завершённой и могут ли другие процессоры прочитать её раньше?

Ответ определяет атомарность записи (write-atomicity). Архитектуры x86, RISC-V, ARMv8-A и SPARC обладают атомарностью записи (MCA) либо атомарностью записи для всех чужих записей (oMCA); IBM Power, ARMv7, Itanium и GPU на NVIDIA PTX ею не обладают (nMCA). Атомарность записи превращает любое внешне видимое переупорядочивание в локальное для процессора. Без неё обязанность восстанавливать порядок ложится на читателя.

Виртуальная машина намеренно лишена этого свойства. Процессоры могут отдавать данные чтения до того, как будут инвалидированы все копии (раннее чтение, early reads). Подтверждения инвалидации попадают в буфер инвалидации и могут применяться не по порядку. Аппаратные потоки делят один store buffer и могут пересылать данные из него (forwarding). Интерконнект не даёт гарантий порядка доставки, а спекулятивные загрузки могут игнорировать зависимости по ветвлению. Заявленная цель - построить "наименее удобную для программиста архитектуру", чтобы в ней проявились все тонкости модели C++11.

Инструкции

Каждый новый суффикс инструкций вводится для устранения конкретной аномалии:

Взаимное исключение на этой машине может защищать только одну кэш-линию атомарного состояния, поэтому реальные архитектуры ограничивают размер атомарных типов несколькими байтами. В отступлении про x86 объясняется, что инструкция с префиксом LOCK, пересекающая две кэш-линии, вызывает блокировку всей шины (детектор "split lock" в Linux существует именно потому, что userspace может этим злоупотреблять), а без префикса такой доступ просто приводит к разрыву чтения/записи (tearing).

Litmus-тесты

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

Причинность "запись - чтение" (WRC, Write-to-read causality из работы Эдви и Бёма Foundations of the C++ Concurrency Memory Model): один процессор читает данные раньше времени, затем отпускает флаг через release; другой процессор захватывает флаг через acquire и читает устаревшие данные. Чтобы исключить эту аномалию, требуется внешняя кумулятивность (A-cumulativity в руководствах по Power и ARM). Автор называет этот вариант D-WRC, а непрямой вариант - I-WRC, для которого нужна внутренняя кумулятивность (B-cumulativity).

Причинность "чтение - запись" (RWC, Read-to-write causality) - именно та аномалия, на которой, по словам автора, спотыкаются опытные разработчики, и C++11 намеренно её допускает. На примере work-stealing дека Чейза - Лева это выражается в дублировании pop: единственный производитель и потребитель видят один оставшийся элемент и оба его забирают. Для исправления требуется чтение с commit у производителя и чтение с reconcile у потребителя. Вариант W+RWC проявляется при делегированной очистке с hazard pointer'ами (родственный подход к epoch-based-reclamation), когда сборщик освобождает память, которую читатель всё ещё использует.

Другие варианты добавляют упорядочивание когерентности (WRW+WR, Z6.3), независимые чтения независимых записей (IRIW, independent reads from independent writes) и пересылку из буфера записи в чтение (2+2W и SB+rfis, переименованные в SLF2 и SLF1). Каждый случай сопоставлен с результатами тестов litmus для Power из проекта herdtools Кембриджского университета, включая указание того, какие исходы действительно наблюдались на Power 6, 7 и 8.

Последовательная консистентность как ациклический граф

Формальная основа статьи: исполнение является последовательно консистентным (sequentially consistent), когда граф рёбер порядка модификаций (mo), чтения из записи (rf), чтения до записи (rb, авторское название для "from-reads" из литературы) и программного порядка (sb) ацикличен. Достаточно частичного порядка, поскольку любой DAG топологически сортируется в полный. Атомарности записи вместе с программным порядком достаточно, а доказательство сводит любой цикл исполнения к циклу между записями с помощью шаблона

W(x); mo | (rf?; sb; rb?); W(y)

который автор называет проекцией причинного чтения (causal read projection).

Такой подход может быть реализован в двух вариантах: propagate-then-commit (используется в проектируемой машине) и commit-then-propagate с центральным арбитром. На процессорах, где есть только один барьер serialize, SC-чтения и записи можно транслировать с барьером перед доступом (leading-sync) или после него (trailing-sync). В рекомендуемой для ARMv7 схеме трансляции C++11 используется по три инструкции dmb ish на каждую запись; в схеме для Power используется вариант leading-sync.

Автор считает модель SC+DRF (последовательная консистентность при отсутствии гонок данных) хорошей для языков с небольшим набором атомиков, и полагает, что именно поэтому её выбрали Java и Golang. Проблемы начинаются тогда, когда более слабые атомики сосуществуют с SC-атомиками.

Аргументы против C++

Модель C++11, которую унаследовали C, Rust, Odin, языки на базе LLVM и (косвенно) Golang, не требует атомарности записи. Лишь к 2016 году (Манеркар и др.) и 2017 году (Лахав и др., Repairing Sequential Consistency in C/C++11) исследователи показали, что схемы трансляции с trailing-sync для Power и ARMv7 нарушают её. В C++20 спецификацию исправили, но из-за этого исправления выбор инструкций на x86 стал сильно неэффективным (проблема LWG 3941), что вызвало комментарий Ханса-Ю. Бёма: аудитория этой части стандарта "практически отсутствует", а авторы компиляторов полагаются на экспертные схемы трансляции, а не на формулировки стандарта.

Диагноз автора: C++ формулирует семантику release-acquire через транзитивные правила "happens-before" вместо утверждения, что acquire гарантирует видимость только тех записей, которые причинно предшествуют прочитанному release. В качестве доказательства автор строит сценарий исполнения I-RWC, который был бы допустим на машине с динамической расстановкой точек сериализации, но запрещён в C++20, и отмечает, что, насколько ему известно, ранее этот вопрос не поднимался. Этот довод, как и утверждение о том, что отсутствие операций commit и reconcile превращает SC в слишком грубый инструмент для сложных алгоритмов, - аргументы для обсуждения, а не общепринятые выводы.

Упорядочивание для одной ячейки памяти

В последнем разделе объясняется, зачем вообще нужны relaxed-атомики, если когерентность работает как reader-writer lock. Два чтения одной и той же ячейки по разным указателям могут завершиться не по порядку, если строки с указателями заполняются в разное время, а архитектуры без буферов упорядочивания памяти (memory ordering buffers) не предотвращают это; руководство по Itanium перечисляет зависимости read-after-write, write-after-read и write-after-write, но не read-after-read. Аппаратные ошибки приводят к тому же: в статье Herding Cats 2013 года были обнаружены коллизии load-load на системах с Cortex-A9, что ARM признала как эрратум 761319 с обходным решением в виде DMB после каждого volatile-чтения. Бэкенд GCC для Itanium и Intel icc на практике трактуют volatile как relaxed-атомик, что бы ни говорил стандарт.

Статья завершается примечанием, что GPT-5.6 Sol использовалась только для поиска и составления сводок по источникам; идеи, текст и диаграммы принадлежат автору.

Связанные страницы

Трафик когерентности кэш-линий, на котором строятся эти рассуждения, со стороны софта измеряется в false-sharing-alignment-128. В threadsanitizer-limits показан софтверный аналог детектирования: определение гонки данных в C11 использует ту же терминологию "happens before", а векторные часы в TSan - один из способов её вычисления. В message-passing-vs-shared-memory задан общий контекст дискуссии о моделях памяти, а art-of-multiprocessor-programming - классический учебник по алгоритмам для разделяемой памяти, которые моделируются litmus-тестами. В itanium-too-few-parameters разбирается ещё один пример того, как Itanium обеспечивал корректность на уровне железа там, где другие архитектуры перекладывали её на софт. Спецификация cobaltc использует тот же словарь упорядочивания для потоков, определяя happens-before как транзитивное замыкание sequenced-before и synchronizes-with (именно такие транзитивные правила критикуются в статье применительно к C++), и оставляет за каждым режимом атомарного упорядочивания документирование собственных гарантий.