Модели памяти: почему Петерсон ломается на x86 и что чинит барьер

Если ты знаешь, чем последовательная согласованность отличается от TSO, что делает буфер записи и где ставить барьер в Петерсоне, листай до «Теперь сам».

Как думаешь, возможно ли

Два потока, в начале x = y = 0. Поток 0: x = 1, потом читает y в r0. Поток 1: y = 1, потом читает x в r1. Может ли оказаться r0 = 0 и r1 = 0?

Ответь себе до чтения. Перебери чередования: кто-то записал первым, значит, второй поток, читая после своей записи, увидит эту первую запись - хотя бы одно из чисел равно 1. На бумаге 0, 0 невозможно. На x86 это наблюдается в настоящих программах, и разбор покажет почему.

На что это похоже

Сотрудник отправляет письмо и сразу идёт проверять общую доску объявлений. Письмо ещё лежит в исходящих почтового клиента - он «отправил», но адресат его пока не видит. Коллега в соседнем кабинете делает то же самое. Оба смотрят на доску, не видят писем друг друга и решают, что второй ещё ничего не сделал. Каждый видит своё письмо отправленным, а чужое - нет.

Буфер записи и есть такая папка «исходящие»: своё ядро читает из неё, чужие ядра - только то, что уже ушло в общую память.

Механизм: буфер записи и барьер

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

TSO (total store order, модель x86): у каждого ядра очередь записей. Запись встаёт в конец очереди, чтение сначала ищет адрес в своей очереди и только потом идёт в память, а в фоне самые старые записи уходят в память по одной. Порядок записей сохраняется, но чтение может обогнать собственную более раннюю запись в другую ячейку. В ARM и POWER модели ещё слабее: там переставляются и записи между собой.

Барьер памяти (mfence в x86, std::atomic_thread_fence в C++) - операция «жди, пока моя очередь записей не опустеет». В модели TSO после него всё, что поток записал, уже в памяти, и следующее чтение уже не обгонит. В C++ барьер работает только вместе с атомарными переменными: обычные флаги без std::atomic остаются гонкой данных, что бы ни стояло рядом.

Правило

Последовательная согласованность: исполнение равно какому-то чередованию с сохранением порядка каждого потока. В x86 (TSO) запись идёт через буфер, и чтение другой ячейки может её обогнать - исход r0 = r1 = 0 возможен. Протоколы вроде Петерсона, где «записал флаг, потом прочитал чужой», ломаются без барьера между записью и чтением. В языке барьер дают атомарные переменные с последовательно согласованным порядком (std::atomic по умолчанию, volatile в Java).

Разбор: все исходы теста «запись, потом чтение»

Программа перебирает все исполнения двух потоков в двух моделях. В TSO у каждого потока очередь записей, и «слить самую старую запись в память» - отдельный шаг, который может случиться когда угодно. Барьер - команда, которая не выполняется, пока очередь своего потока не пуста.

# поток 0: x = 1; r0 = y        поток 1: y = 1; r1 = x
# операция: ["st", адрес] - записать 1, ["ld", адрес, регистр],
# ["fence"] - ждать, пока свой буфер записи не опустеет
def ishody(progi, tso):
    nachalo = [[0, 0], {"x": 0, "y": 0}, [[], []], {}]
    stek = [nachalo]
    vidim = {}
    ishod = {}
    while len(stek) > 0:
        s = stek.pop()
        if str(s) in vidim:
            continue
        vidim[str(s)] = True
        pc, pam, buf, reg = s
        if (pc[0] == len(progi[0]) and pc[1] == len(progi[1])
                and len(buf[0]) == 0 and len(buf[1]) == 0):
            ishod[str([reg["r0"], reg["r1"]])] = True
            continue
        for t in [0, 1]:
            # слив самой старой записи из буфера в память - отдельный шаг
            if len(buf[t]) > 0:
                nb = [buf[0][:], buf[1][:]]
                adr = nb[t].pop(0)
                np = dict(pam)
                np[adr] = 1
                stek.append([pc[:], np, nb, dict(reg)])
            if pc[t] == len(progi[t]):
                continue
            kom = progi[t][pc[t]]
            npc = pc[:]
            npc[t] = pc[t] + 1
            np = dict(pam)
            nb = [buf[0][:], buf[1][:]]
            nr = dict(reg)
            if kom[0] == "st":
                if tso:
                    nb[t].append(kom[1])
                else:
                    np[kom[1]] = 1
            elif kom[0] == "ld":
                if kom[1] in nb[t]:
                    nr[kom[2]] = 1
                else:
                    nr[kom[2]] = np[kom[1]]
            elif len(nb[t]) > 0:
                continue
            stek.append([npc, np, nb, nr])
    return sorted(ishod)

sb = [[["st", "x"], ["ld", "y", "r0"]], [["st", "y"], ["ld", "x", "r1"]]]
s_bar = [[["st", "x"], ["fence"], ["ld", "y", "r0"]],
         [["st", "y"], ["fence"], ["ld", "x", "r1"]]]
print("согласованная:", ishody(sb, False))
print("TSO:          ", ishody(sb, True))
print("TSO + барьер: ", ishody(s_bar, True))

согласованная: ['[0, 1]', '[1, 0]', '[1, 1]']
TSO:           ['[0, 0]', '[0, 1]', '[1, 0]', '[1, 1]']
TSO + барьер:  ['[0, 1]', '[1, 0]', '[1, 1]']

При последовательной согласованности три исхода - [0, 0] нет. В TSO появляется четвёртый, [0, 0]: оба потока положили запись в буфер, оба прочитали чужую ячейку из памяти, где ещё ноль, и только потом буферы слились. Барьер между записью и чтением возвращает три исхода: прочитать можно только после того, как своя запись видна всем.

Разбор: Петерсон на TSO

Тот же перебор состояний, что в уроке про Петерсона, но теперь с буферами записи. У каждого ядра в очереди помещается две записи - настоящий буфер тоже конечен, а без предела состояний стало бы бесконечно много.

def imya(x, i):
    if x == "f_i":
        return "f" + str(i)
    if x == "f_j":
        return "f" + str(1 - i)
    return x

def prochitat(pam, buf, adr):
    # свой поток видит свою последнюю запись из буфера, иначе - память
    znach = pam[adr]
    for z in buf:
        if z[0] == adr:
            znach = z[1]
    return znach

def proverit(prog, tso):
    # буфер записи каждого потока вмещает не больше двух записей
    nachalo = [[0, 0], {"f0": 0, "f1": 0, "v": 0}, [[], []]]
    vidim = {str(nachalo): True}
    stek = [nachalo]
    oba = False
    while len(stek) > 0:
        pc, pam, buf = stek.pop()
        if prog[pc[0]][0] == "cs" and prog[pc[1]][0] == "cs":
            oba = True
        dalshe = []
        for t in [0, 1]:
            if len(buf[t]) > 0:
                nb = [buf[0][:], buf[1][:]]
                z = nb[t].pop(0)
                np = dict(pam)
                np[z[0]] = z[1]
                dalshe.append([pc[:], np, nb])
            kom = prog[pc[t]]
            np = dict(pam)
            nb = [buf[0][:], buf[1][:]]
            if kom[0] == "set":
                znach = kom[2]
                if znach == "i":
                    znach = t
                if not tso:
                    np[imya(kom[1], t)] = znach
                elif len(nb[t]) < 2:
                    nb[t].append([imya(kom[1], t), znach])
                else:
                    continue
            elif kom[0] == "wait":
                vse = True
                for usl in kom[1]:
                    nuzhno = usl[1]
                    if nuzhno == "i":
                        nuzhno = t
                    if prochitat(pam, buf[t], imya(usl[0], t)) != nuzhno:
                        vse = False
                if vse:
                    continue
            elif kom[0] == "fence" and len(nb[t]) > 0:
                continue
            npc = pc[:]
            npc[t] = (pc[t] + 1) % len(prog)
            dalshe.append([npc, np, nb])
        for s in dalshe:
            if str(s) not in vidim:
                vidim[str(s)] = True
                stek.append(s)
    return [len(vidim), oba]

peterson = [["set", "f_i", 1],
            ["set", "v", "i"],
            ["wait", [["f_j", 1], ["v", "i"]]],
            ["cs"],
            ["set", "f_i", 0]]
s_bar = [["set", "f_i", 1],
         ["set", "v", "i"],
         ["fence"],
         ["wait", [["f_j", 1], ["v", "i"]]],
         ["cs"],
         ["set", "f_i", 0]]
print("Петерсон, согласованная память:", proverit(peterson, False))
print("Петерсон на TSO:               ", proverit(peterson, True))
print("Петерсон на TSO с барьером:    ", proverit(s_bar, True))

Петерсон, согласованная память: [26, False]
Петерсон на TSO:                [400, True]
Петерсон на TSO с барьером:     [134, False]

На согласованной памяти - знакомые 26 состояний и никакого нарушения. На TSO - 400 состояний, и среди них есть оба потока в секции. Сценарий тот же, что в тесте выше: каждый поток записал свой флаг и жертву в буфер, прочитал флаг другого из памяти - там ноль - и вошёл. Барьер после записи жертвы, перед ожиданием, сливает буфер, и нарушение исчезает: 134 состояния, всё чисто. Херлихи и Шавит прямо пишут, что флаги и жертва в таких замках должны быть объявлены volatile - иначе код работает только на бумаге.

Что ломается без этого

Двойная проверка без атомарности. Классическая ленивая инициализация «если объект ещё не создан - захвати замок, проверь снова, создай» ломалась в Java до 2004 года (новая модель памяти, JSR-133): другой поток мог увидеть ссылку на объект раньше, чем записи полей самого объекта.

Флаг готовности обычной переменной. Поток пишет данные, потом ready = True; другой ждёт ready и читает данные. В C++ без атомарности это гонка данных и неопределённое поведение, а на ARM второй поток реально видит ready раньше данных.

Барьеры «на всякий случай» везде. mfence стоит десятки тактов. Ставить его в каждую строку - значит потерять производительность; ставят там, где «запись, потом чтение другой ячейки» решает корректность.

Зачем это в работе

Пишешь ли ты на Java, Go, Rust или C++, модель памяти языка определяет, что гарантировано без синхронизации. Правило «нет гонок данных - получаешь последовательную согласованность» есть в моделях Java, C++ и Go (в C++ - если атомарные операции идут с порядком по умолчанию, seq_cst): программу, где все общие переменные защищены замками или атомарны, можно продумывать как чередование. Всё остальное - экспертная территория с memory_order_acquire и release, куда заходят ради скорости и с перебором состояний в руках.

Следующая глава поднимается на уровень выше: вместо отдельных ячеек - целые объекты (счётчик, очередь), и вопрос «что значит, что объект работает правильно при одновременных вызовах» получает точный ответ.

Теперь сам

1. Поток 0: x = 1; y = 1. Поток 1: читает y, потом x. Может ли в TSO оказаться y = 1, x = 0?
2. В каком месте Петерсона нужен барьер и почему не после f[i] = 1?
3. Чем последовательная согласованность отличается от «каждая операция мгновенна»?