Замок Петерсона: два флага, одна жертва и проверка всех состояний

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

Как думаешь, что не так

Двое хотят войти в комнату, у каждого флажок. Правило: «жди, пока у другого не опущен флажок, потом подними свой и входи». Кажется разумным: пока другой внутри, его флажок поднят, и ты ждёшь. Что может пойти не так?

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

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

Два человека у узкой двери в коридоре. Если каждый говорит «я иду» и ждёт, пока другой отступит, они стоят вечно - это LockOne. Если каждый просто смотрит, свободна ли дверь, и шагает - они сталкиваются в проёме: наивный замок. Вежливость решает: каждый говорит «я хочу пройти» и «проходите, пожалуйста». Кто сказал «проходите» последним, тот и ждёт, а другой идёт. Это Петерсон: флаг «хочу» плюс уступка, и уступает тот, кто уступил позже.

Механизм: флаги, жертва и состояние системы

У каждого потока i свой флаг f[i], у пары - общая переменная v, «жертва». Протокол Петерсона для потока i (второй поток - j):

f[i] = 1              я хочу войти
v = i                 я уступаю
ждать, пока f[j] == 1 и v == i
критическая секция
f[i] = 0              я вышел

Почему никто не войдёт вдвоём. Пусть оба в секции, и последним v записал поток A. Значит, в момент его проверки v == A, и войти он мог, только увидев f[B] == 0. Но B поднял флаг ДО того, как записал v, а запись v потоком B была раньше записи потоком A. Значит, к моменту проверки A флаг B уже поднят - противоречие. Почему никто не заклинит навсегда: v хранит одно значение, и ждать при v == i может только один из двух. Почему никто не голодает (если планировщик никого не забывает навсегда): пока поток 0 ждёт, поток 1, выйдя и захотев войти снова, сам запишет v = 1 - и теперь ждать будет он, а поток 0 войдёт.

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

Правило

Наивный замок «проверил, потом поднял флаг» не исключает: оба проходят проверку до записей. LockOne «поднял флаг, потом жду» исключает, но заклинивает, когда оба подняли флаги. Петерсон: поднять флаг, назвать себя жертвой, ждать, пока флаг другого поднят И жертва - ты; он даёт взаимоисключение, отсутствие взаимоблокировки и голодания для двух потоков. Взаимоисключение и взаимоблокировку проверяют перебором всех достижимых состояний, отсутствие голодания - рассуждением о бесконечных путях.

Разбор: перебор состояний трёх замков

Протокол записан данными: ["set", переменная, значение], ["wait", условия] - ждать, пока выполнены ВСЕ условия, ["cs"] - критическая секция. "f_i" значит «свой флаг», "f_j" - «флаг другого», значение "i" - номер потока. После последней строки поток идёт на первую: каждый хочет войти снова и снова. Перебор обходит все достижимые состояния и смотрит две вещи: бывают ли оба в секции и бывает ли, что ни один поток не может сделать шаг. Бесконечный круг без входа в секцию (живую блокировку) поиск состояний без шагов не ловит - для этого ищут циклы в графе состояний. Проверка двух условий ожидания здесь - один шаг; это упрощение, с отдельными чтениями Петерсон тоже верен, только состояний больше.

def imya(x, i):
    # "f_i" - свой флаг, "f_j" - флаг другого потока
    if x == "f_i":
        return "f" + str(i)
    if x == "f_j":
        return "f" + str(1 - i)
    return x

def znach(x, i):
    if x == "i":
        return i
    return x

def shag(prog, sost, t):
    # sost = [pc0, pc1, {память}]; шаг потока t; None - он ждёт
    pc = sost[t]
    kom = prog[pc]
    pam = dict(sost[2])
    if kom[0] == "wait":
        vse = True
        for usl in kom[1]:
            if pam[imya(usl[0], t)] != znach(usl[1], t):
                vse = False
        if vse:
            return None
    if kom[0] == "set":
        pam[imya(kom[1], t)] = znach(kom[2], t)
    novyj = [sost[0], sost[1], pam]
    novyj[t] = (pc + 1) % len(prog)
    return novyj

def v_sekcii(prog, sost, t):
    return prog[sost[t]][0] == "cs"
def proverit(prog):
    nachalo = [0, 0, {"f0": 0, "f1": 0, "v": 0}]
    vidim = {str(nachalo): True}
    stek = [nachalo]
    narushenie = False
    blokirovka = False
    while len(stek) > 0:
        s = stek.pop()
        if v_sekcii(prog, s, 0) and v_sekcii(prog, s, 1):
            narushenie = True
        dalshe = 0
        for t in [0, 1]:
            n = shag(prog, s, t)
            if n != None:
                dalshe = dalshe + 1
                if str(n) not in vidim:
                    vidim[str(n)] = True
                    stek.append(n)
        if dalshe == 0:
            blokirovka = True
    return [len(vidim), narushenie, blokirovka]

naivnyj = [["wait", [["f_j", 1]]],
           ["set", "f_i", 1],
           ["cs"],
           ["set", "f_i", 0]]
lock_one = [["set", "f_i", 1],
            ["wait", [["f_j", 1]]],
            ["cs"],
            ["set", "f_i", 0]]
peterson = [["set", "f_i", 1],
            ["set", "v", "i"],
            ["wait", [["f_j", 1], ["v", "i"]]],
            ["cs"],
            ["set", "f_i", 0]]
print("        состояний  оба в секции  все ждут")
for nazv, prog in [["наивный", naivnyj], ["LockOne", lock_one],
                   ["Петерсон", peterson]]:
    print(nazv, proverit(prog))

        состояний  оба в секции  все ждут
наивный [16, True, False]
LockOne [12, False, True]
Петерсон [26, False, False]

Наивный замок - 16 состояний, и в одном из них оба в секции. LockOne - 12 состояний, взаимоисключение соблюдено, но есть состояние, где оба подняли флаги и оба ждут: шагов больше нет никогда. Петерсон - 26 состояний, ни того, ни другого. Это не «прогнали тысячу раз и не упало», а полный обход: других состояний у этой системы нет.

Разбор: две строки местами - и замок сломан

Кажется, порядок «поднять флаг» и «назвать себя жертвой» не важен: обе записи делаются до ожидания. Поменяем их и попросим перебор найти нарушение и показать путь к нему.

def imya(x, i):
    # "f_i" - свой флаг, "f_j" - флаг другого потока
    if x == "f_i":
        return "f" + str(i)
    if x == "f_j":
        return "f" + str(1 - i)
    return x

def znach(x, i):
    if x == "i":
        return i
    return x

def shag(prog, sost, t):
    # sost = [pc0, pc1, {память}]; шаг потока t; None - он ждёт
    pc = sost[t]
    kom = prog[pc]
    pam = dict(sost[2])
    if kom[0] == "wait":
        vse = True
        for usl in kom[1]:
            if pam[imya(usl[0], t)] != znach(usl[1], t):
                vse = False
        if vse:
            return None
    if kom[0] == "set":
        pam[imya(kom[1], t)] = znach(kom[2], t)
    novyj = [sost[0], sost[1], pam]
    novyj[t] = (pc + 1) % len(prog)
    return novyj

def v_sekcii(prog, sost, t):
    return prog[sost[t]][0] == "cs"
def nayti_narushenie(prog):
    # обход в глубину; помним, откуда пришли, чтобы восстановить путь
    nachalo = [0, 0, {"f0": 0, "f1": 0, "v": 0}]
    otkuda = {str(nachalo): None}
    stek = [nachalo]
    while len(stek) > 0:
        s = stek.pop()
        if v_sekcii(prog, s, 0) and v_sekcii(prog, s, 1):
            put = []
            k = str(s)
            while otkuda[k] != None:
                put.append(otkuda[k][1])
                k = otkuda[k][0]
            put.reverse()
            return put
        for t in [0, 1]:
            n = shag(prog, s, t)
            if n != None and str(n) not in otkuda:
                otkuda[str(n)] = [str(s), t]
                stek.append(n)
    return None

# Петерсон, в котором две первые строки поменяли местами
naoborot = [["set", "v", "i"],
            ["set", "f_i", 1],
            ["wait", [["f_j", 1], ["v", "i"]]],
            ["cs"],
            ["set", "f_i", 0]]
put = nayti_narushenie(naoborot)
print("шагов до нарушения:", len(put))
s = [0, 0, {"f0": 0, "f1": 0, "v": 0}]
for t in put:
    kom = naoborot[s[t]]
    s = shag(naoborot, s, t)
    print("поток", t, kom, "->", s[2])

шагов до нарушения: 6
поток 1 ['set', 'v', 'i'] -> {'f0': 0, 'f1': 0, 'v': 1}
поток 0 ['set', 'v', 'i'] -> {'f0': 0, 'f1': 0, 'v': 0}
поток 0 ['set', 'f_i', 1] -> {'f0': 1, 'f1': 0, 'v': 0}
поток 0 ['wait', [['f_j', 1], ['v', 'i']]] -> {'f0': 1, 'f1': 0, 'v': 0}
поток 1 ['set', 'f_i', 1] -> {'f0': 1, 'f1': 1, 'v': 0}
поток 1 ['wait', [['f_j', 1], ['v', 'i']]] -> {'f0': 1, 'f1': 1, 'v': 0}

Шесть шагов. Поток 1 назвал себя жертвой, но ещё не поднял флаг. Поток 0 тоже назвал себя жертвой - теперь v = 0 - и поднял флаг. Ждёт ли он? Условие «флаг другого поднят и жертва - я» не выполнено: флаг потока 1 ещё опущен. Поток 0 входит. Поток 1 поднимает флаг и проверяет: флаг потока 0 поднят, но жертва - 0, а не 1. Поток 1 тоже входит. В правильном порядке флаг поднят раньше уступки, и тот, кто уступил последним, обязательно увидит флаг другого.

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

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

Ожидание через проверку одного условия. while v == i без флагов - это LockTwo: он исключает, но если второй поток больше не хочет входить, первый ждёт вечно - уступать некому.

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

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

Петерсона в продакшен не пишут: есть аппаратные атомарные операции (следующая глава), и они проще и быстрее. Но приём - записать протокол как систему состояний и перебрать их все - живёт в инженерной практике. TLA+ использовали в Amazon для проверки протоколов S3 и DynamoDB, проверка моделей ловит ошибки в протоколах кеш-когерентности процессоров, а SPIN десятилетиями проверяет протоколы связи. Если протокол синхронизации нельзя перебрать, его почти невозможно доказать.

Теперь сам

1. Сколько потоков может одновременно ждать в Петерсоне при v == 0, и почему это исключает взаимоблокировку?
2. В LockOne поток 0 поднял флаг и сразу вошёл (поток 1 спал). Может ли поток 1 войти, пока поток 0 в секции?
3. Почему достаточно перебрать состояния, а не все чередования?