Введение: Четыре строки кода против интуиции ── Лакмусовый тест Store Buffering (SB)

Рассмотрим следующую многопоточную программу на C из четырёх инструкций. Две общие переменные x и y инициализированы нулями (0). Два потока на двух разных ядрах процессора выполняют по одной записи (Store) и одному чтению (Load):

1
2
3
4
5
6
7
8
9

// Initial state in shared memory:
int x = 0, y = 0;
int r1 = 0, r2 = 0;

// Thread 1 (Core 0)          // Thread 2 (Core 1)
void thread1(void) {          void thread2(void) {
    x = 1;      // (S1)           y = 1;      // (S2)
    r1 = y;     // (L1)           r2 = x;     // (L2)
}                             }

Какие значения (r1, r2) возможны после завершения обоих потоков? Согласно здравому смыслу:

• Если Поток 1 выполнится раньше Потока 2, получим r1 = 0, r2 = 1.
• Если Поток 2 выполнится раньше Потока 1, получим r1 = 1, r2 = 0.
• Если оба сначала выполнят первую строку (x = 1 и y = 1), а затем вторую, получим r1 = 1, r2 = 1.

При любом мыслимом чередовании хотя бы одна запись единицы должна произойти раньше чтения другого потока, поэтому исход r1 == 0 && r2 == 0 кажется математически невозможным. Однако при запуске этого кода на современном процессоре Intel/AMD x86-64, чипе Apple Silicon (ARMv8) или с оптимизирующим компилятором C/C++/Rust (-O2) «невозможный» результат r1 == 0 && r2 == 0 возникает тысячи раз в секунду! Это не ошибка оборудования, а следствие переупорядочивания инструкций (Instruction Reordering) в рамках однопоточного правила «As-If» (как если бы).

Глава 1: Иллюзия последовательной консистентности (Sequential Consistency)

В 1979 году лауреат премии Тьюринга Лесли Лампорт (Leslie Lamport) формализовал интуитивную модель многопоточности как последовательную консистентность (Sequential Consistency, SC): результат любого выполнения должен быть таким же, как если бы операции всех процессоров выполнялись в некотором едином глобальном линейном порядке ($\prec_m$), причём операции каждого отдельного процессора шли бы в нём строго в порядке программы (Program Order, $\prec_p$).

В модели SC невозможность r1 == 0 && r2 == 0 доказывается в три строки:

Чтобы получилось $r_1 = 0$, чтение $L_1$ должно произойти раньше записи $S_2$ ($L_1 \prec_m S_2$). Аналогично $r_2 = 0$ требует $L_2 \prec_m S_1$. Объединяя это с порядком программы $S_1 \prec_p L_1$ и $S_2 \prec_p L_2$, получаем замкнутый цикл во времени $S_1 \prec L_1 \prec S_2 \prec L_2 \prec S_1$! Но поскольку x и y — разные адреса без зависимости по данным внутри одного потока, процессор и компилятор нарушают глобальный порядок ради скрытия задержек памяти.

Глава 2: Аппаратные модели памяти ── Буферы записи (Store Buffers), протокол MESI и очереди инвалидации

2.1 Кэш-когерентность MESI и переупорядочивание Store-Load из-за Store Buffer

На современном процессоре с частотой 4 ГГц обращение к регистру занимает $0{,}25\text{ нс}$ (1 такт), попадание в L1-кэш — около $1\text{ нс}$, тогда как межъядерная синхронизация кэшей или доступ к DRAM требует $50\text{–}100\text{ нс}$ (до 300 тактов). Ядра поддерживают когерентность кэш-линий по протоколу MESI (Modified, Exclusive, Shared, Invalid). Чтобы Ядро 0 могло изменить кэш-линию x, находящуюся в состоянии Shared, оно обязано разослать остальным ядрам сообщение Invalidate (Read-For-Ownership, RFO) и дождаться подтверждения (Ack).

Чтобы не останавливать конвейер на десятки тактов при каждой записи, все современные CPU (включая x86-64!) помещают между исполнительным блоком и L1-кэшем приватную очередь Store Buffer (буфер записи):

  flowchart TD
    subgraph Core0 ["Ядро CPU 0 (Поток 1: x = 1; r1 = y;)"]
        Exec0["Исполнительный блок (Core 0)"]
        SB0["Приватный Store Buffer Ядра 0<br/>[В очереди: x = 1] (Невидимо для Ядра 1!)"]
        L1_0["Кэш данных L1 (Core 0)<br/>y = 0 (Shared)"]
        Exec0 -- "1. Помещает x = 1 в Store Buffer и сразу идёт дальше" --> SB0
        Exec0 -- "2. Мгновенно читает r1 = y из L1 (r1 = 0!)" --> L1_0
        SB0 -. "3. Сбрасывает x = 1 в L1 только после MESI Ack" .-> L1_0
    end
    subgraph Core1 ["Ядро CPU 1 (Поток 2: y = 1; r2 = x;)"]
        Exec1["Исполнительный блок (Core 1)"]
        SB1["Приватный Store Buffer Ядра 1<br/>[В очереди: y = 1] (Невидимо для Ядра 0!)"]
        L1_1["Кэш данных L1 (Core 1)<br/>x = 0 (Shared)"]
        Exec1 -- "1. Помещает y = 1 в Store Buffer и сразу идёт дальше" --> SB1
        Exec1 -- "2. Мгновенно читает r2 = x из L1 (r2 = 0!)" --> L1_1
        SB1 -. "3. Сбрасывает y = 1 в L1 только после MESI Ack" .-> L1_1
    end
    L1_0 <== "Шина когерентности кэша MESI (Invalidate / RFO)" ==> L1_1

Ядро 0 кладёт x = 1 в свой приватный Store Buffer (невидимый для Ядра 1!) и тут же читает r1 = y (0) из своего L1-кэша. Одновременно Ядро 1 кладёт y = 1 в свой Store Buffer и читает r2 = x (0) из своего L1-кэша. Чтение (Load) обгоняет предшествующую запись (Store) в глобальной видимости — это переупорядочивание Store-Load! (Если же Ядро 0 читает собственную переменную x, механизм Store Buffer Forwarding напрямую возвращает x = 1 из локального буфера, сохраняя однопоточную семантику.)

2.2 Строгая модель x86-TSO против слабых моделей памяти (ARMv8, RISC-V, PowerPC)

Модель x86-TSO (Total Store Order) от Intel и AMD использует строгий FIFO Store Buffer: она никогда не меняет местами Load-Load, Load-Store и Store-Store, допуская только переупорядочивание Store -> Load. Напротив, ARMv8-A (AArch64 / Apple Silicon), RISC-V (RVWMO) и IBM PowerPC используют слабо упорядоченные модели памяти (Weakly Ordered): из-за не-FIFO слияния записей, спекулятивных чтений и очередей инвалидации (Invalidate Queues) все четыре комбинации (Load-Load, Load-Store, Store-Store, Store-Load) могут переупорядочиваться аппаратно!

Глава 3: Переупорядочивание компилятором и теорема DRF-SC ── Почему гонки данных являются неопределённым поведением (UB)

Даже на процессоре x86 передача сообщений без синхронизации data = 42; ready = 1; не работает, так как оптимизирующий компилятор (gcc, clang, rustc) свободно меняет местами все четыре типа обращений к памяти. Более того, за счёт продвижения в регистры (Register Promotion) и выноса инвариантов цикла (LICM) компилятор превращает цикл ожидания while (!ready) в однократное чтение в регистр и бесконечный цикл! А ключевое слово volatile в C/C++ предназначено только для регистров MMIO и не генерирует аппаратных барьеров памяти.

В 1990 году Сарита Адве и Марк Хилл доказали фундаментальную теорему DRF-SC (Data-Race-Free Sequential Consistency):

• Гонка данных (Data Race): Одновременный доступ двух потоков к одной ячейке памяти, где хотя бы один доступ — запись, хотя бы один — неатомарный, и между ними нет отношения Happens-Before ($\xrightarrow{hb}$).
• Контракт DRF-SC: Если в программе нет гонок данных (DRF), компилятор и процессор гарантируют, что любое выполнение неотличимо от последовательно консистентного (SC). Наличие же хотя бы одной гонки данных в C/C++ или Unsafe Rust приводит к неопределённому поведению (Undefined Behavior, UB).

Глава 4: Отношение Happens-Before ($\xrightarrow{hb}$) и синхронизация Acquire-Release

В формальной модели памяти C++11 / C11 / Rust, когда Поток 1 выполняет атомарную запись Release $W_{\text{rel}}(x, v)$, а Поток 2 выполняет атомарное чтение Acquire $R_{\text{acq}}(x, v)$ и считывает это значение ($W_{\text{rel}} \xrightarrow{rf} R_{\text{acq}}$), между потоками возникает связь Synchronizes-With ($\xrightarrow{sw}$). Транзитивное замыкание внутрипоточного порядка (Sequenced-Before, $\xrightarrow{sb}$) и $\xrightarrow{sw}$ образует отношение Happens-Before ($\xrightarrow{hb}$):

С помощью memory_order_release и memory_order_acquire передача сообщения становится математически надёжной:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

#include <atomic>
#include <cassert>

int data = 0;                        // Non-atomic payload
std::atomic<int> flag{0};            // Atomic synchronization variable

void producer_thread() {
    data = 42;                                           // (1) Sequenced-before (2)
    flag.store(1, std::memory_order_release);            // (2) Release store
}

void consumer_thread() {
    while (flag.load(std::memory_order_acquire) == 0) {  // (3) Acquire load
        // spin until flag == 1
    }
    assert(data == 42);                                  // (4) Guaranteed never to fail!
}

  flowchart TD
    subgraph Thread1 ["Поток-производитель (Core 0)"]
        W_data["(1) data = 42 (Неатомарная запись)"]
        W_flag["(2) flag.store(1, release) (Атомарная запись Release)"]
        W_data -- "Sequenced-Before (sb)<br/>[Барьер Release запрещает опускать (1) ниже (2)!]" --> W_flag
    end
    subgraph Thread2 ["Поток-потребитель (Core 1)"]
        R_flag["(3) flag.load(acquire) == 1 (Атомарное чтение Acquire)"]
        R_data["(4) assert(data == 42) (Неатомарное чтение)"]
        R_flag -- "Sequenced-Before (sb)<br/>[Барьер Acquire запрещает поднимать (4) выше (3)!]" --> R_data
    end
    W_flag == "Reads-From (rf) ⟹ Synchronizes-With (sw) установлено!" ==> R_flag
    W_data -. "По транзитивности: Happens-Before (hb) гарантировано!" .-> R_data

Строгое доказательство:

Глава 5: Спектр порядков памяти и инструкции CPU (MFENCE, DMB, LDAR/STLR)

C++ и Rust предоставляют три основных уровня упорядочивания:

1. Relaxed: Гарантирует только неделимость и порядок модификации ($\xrightarrow{mo}$) одной переменной без синхронизации $\xrightarrow{sw}$ (для простых счётчиков).
2. Acquire / Release / AcqRel: Односторонние барьеры (семантика Roach Motel), создающие связь $\xrightarrow{sw}$, но НЕ предотвращающие переупорядочивание Store -> Load между предшествующим store(release) и последующим load(acquire)!
3. SeqCst (по умолчанию): Дополнительно устанавливает единый глобальный линейный порядок $\xrightarrow{S}$ для всех SeqCst-операций и запрещает переупорядочивание Store -> Load (единственный способ исключить r1 == 0 && r2 == 0 в тесте SB).

На x86-64 Acquire и Release компилируются в обычные инструкции mov без аппаратных затрат, тогда как store(seq_cst) использует xchg (с неявным префиксом LOCK) или mfence для принудительного сброса Store Buffer. На ARMv8-A специальные инструкции LDAR и STLR элегантно реализуют Acquire-Release и SeqCst без тяжёлого барьера DMB ISH.