Теория языков программирования

Модели памяти и порядок выполнения

Программа работает правильно при компиляции без оптимизаций, но падает с -O2. Или работает на x86, но даёт неверные результаты на ARM. Это не баг компилятора - это модели памяти в действии.

  • **Linux kernel**: spinlock использует `smp_store_release` / `smp_load_acquire` - без них DEC Alpha мог читать устаревшие данные под локом
  • **Java Double-Checked Locking**: до Java 5 классический паттерн DCL был сломан из-за отсутствия volatile - JMM 1.5 исправил, добавив happens-before для volatile
  • **Disruptor (LMAX)**: high-performance очередь для 6 млн транзакций/сек использует Relaxed reads и точечные Release/Acquire вместо volatile для каждого поля
  • **Go race detector**: встроен в `go test -race`, обнаруживает нарушения happens-before через shadow memory - находит реальные баги в продакшен коде

Sequential Consistency

**Sequential Consistency (SC)** - это интуитивная модель, где все операции с памятью выполняются в том порядке, в котором их написал программист, и все потоки видят единую глобальную последовательность операций. Лесли Лэмпорт сформулировал это в 1979 году.

SC - самая строгая (и медленная) модель. На x86 она почти бесплатна из-за аппаратной TSO, но на ARM/POWER требует дорогих барьеров памяти.

Проблема SC: современные процессоры и компиляторы агрессивно оптимизируют - переставляют инструкции, кешируют записи в store buffer, делают prefetch. SC запрещает все такие оптимизации между потоками.

Что гарантирует Sequential Consistency в многопоточной программе?

Acquire-Release семантика

**Acquire-Release** - это асимметричная пара барьеров. **Acquire** (чтение с флагом) гарантирует, что никакие последующие операции не будут перемещены до него. **Release** (запись с флагом) гарантирует, что никакие предыдущие операции не будут перемещены после него.

Acquire-Release дешевле SC на ARM: Release компилируется в `stlr`, Acquire в `ldar`. На x86 store/load уже имеют TSO-семантику, поэтому компилятор добавляет только `lock` для seq_cst.

Классический use case - spinlock: `lock()` делает Acquire, `unlock()` делает Release. Всё, что произошло под локом у одного потока, будет видно другому потоку после его Acquire.

Что гарантирует `store(Release)` в отношении предыдущих операций?

Happens-Before

**Happens-before** - это частичный порядок на операциях в программе. Операция A happens-before B, если: A и B в одном потоке и A стоит раньше, ИЛИ A синхронизируется с B через acquire-release пару, ИЛИ транзитивно через цепочку.

Если между двумя операциями нет happens-before отношения - это **data race**. Data race = undefined behavior в C++, и непредсказуемое поведение в Java/Go. Именно HB является формальной основой для рассуждений о корректности любой многопоточной программы.

Два потока обращаются к общей переменной без синхронизации. Что происходит по happens-before?

Relaxed Ordering

**Relaxed** - самый слабый ordering в C++11. Гарантирует только атомарность самой операции, но не даёт никаких гарантий относительно порядка других операций. Единственная гарантия - modification order: для одной переменной все потоки согласны, в каком порядке менялись её значения.

На x86 Relaxed для loads/stores почти бесплатен - аппаратная TSO уже запрещает многое. На ARM Relaxed даёт реальный прирост скорости: нет ldar/stlr, только обычные load/store.

Relaxed атомики всё равно медленные - раз атомарные, значит есть барьер

Атомарность и барьеры памяти - разные вещи. Relaxed атомик атомарен (нет torn reads), но без барьера

На x86 атомарность одиночного aligned word обеспечивается аппаратно без барьера. Барьер нужен только для упорядочивания относительно других операций

Для чего Relaxed ordering подходит лучше всего?

Ключевые идеи

  • **SC** - строжайшая модель: единая глобальная история. Дорого на слабых архитектурах (ARM, POWER)
  • **Acquire-Release** - асимметричные барьеры для publish-subscribe паттернов. Дешевле SC, достаточно для большинства задач
  • **Happens-before** - формальная основа: нет HB между конфликтующими доступами = data race = UB
  • **Relaxed** - только атомарность, без упорядочивания. Для счётчиков и флагов без зависимостей

Связанные темы

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

  • Алгоритмы lock-free структур данных — Lock-free алгоритмы строятся именно на acquire-release гарантиях
  • GC и управление памятью — Concurrent GC должен учитывать модель памяти при трассировке живых объектов

Вопросы для размышления

  • Почему программа может работать корректно тысячи раз и потом упасть из-за модели памяти - в чём недетерминизм?
  • Как бы вы объяснили разницу между атомарностью и барьером памяти коллеге, который только слышал про `volatile`?
  • Если acquire-release дешевле SC, почему не использовать его везде вместо SC?

Связанные уроки

  • dist-03-fallacies
Модели памяти и порядок выполнения

0

1

Войти