Все пять safety-свойств Raft прошли. Две реплики разошлись

Причина: одно предложение в §8

§5.4.2 запрещает лидеру коммитить запись, унаследованную от предыдущего терма, простым подсчётом реплик: большинство, держащее старую запись, ещё не делает её безопасной — более поздний лидер всё ещё может её затереть. Правило такое: лидер коммитит запись своего терма, а унаследованные едут следом за ней.

Правило верное. И оно тихо зависит от того, что запись текущего терма вообще когда-нибудь появится.

В моём прогоне клиенты замолчали сразу после смены лидера. Такая запись не появилась. Унаследованные записи остались незакоммиченными навсегда — а реплики, которые успели применить их при прошлом лидере, остались навсегда впереди тех, кто сигнала о коммите так и не получил.

Лекарство в статье занимает одно предложение, §8: при вступлении в должность лидер дописывает пустую запись своего терма. Она текущего терма, значит её можно закоммитить подсчётом, и она тянет за собой всё, что было раньше. Восемь строк кода.

Я бы это чтением не нашёл. §8 я читал. Оно там на одно предложение, выглядит как оптимизация, и я его не реализовал.

Какая проверка это поймала

Интересен не баг. Интересно, какая именно проверка сработала.

Не проверка свойств. Все пять держались — я потом прошёл трассу руками, они действительно держатся. Тест, проверяющий правила самого Raft, прошёл бы. Тест, проверяющий, что итоговые значения правильные, тоже прошёл бы: на тех репликах, которые их получили, значения были правильные.

Сработало сравнение, дописанное почти между делом: когда отказы прекратились и кластеру дали время устояться — все ли реплики сошлись. Это не свойство Raft. Это то, ради чего Raft существует, и оказалось, что это разные утверждения.

И прогон двадцать пятый. Не второй. Не первый. Двадцать пять случайных расписаний должны были пройти мимо, прежде чем клиенты замолчали ровно в том окне, где это имело значение.

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

Работает только одно: дать чекеру то, про что заранее известно, что оно неправильное, и потребовать, чтобы он это сказал. И сказал правильным именем.

Музей багов

У реализации есть переключатели. Каждый выключает ровно одно правило алгоритма, и обвязка обязана поймать каждый.

нет проверки актуальности лога → Leader Completeness: n2 стал лидером в терме 4
                                 без закоммиченной записи r6        (прогон 2)
нет проверки prevLog           → Log Matching: индекс 1 терм 1 держит
                                 noop:n1:1, но r2 на n4             (прогон 1)
конфликтующая запись остаётся  → State Machine Safety: индекс 8: n5 применил
                                 noop:n5:6, n2 применил r7          (прогон 4)
нет no-op лидера               → реплики разошлись: n1={"a":"p1.2"},
                                 n4={"a":"p1.2","b":"p1.3"}         (прогон 25)
игнорирует более новый терм    → клиент 2 сдался на cas             (прогон 1)

Соломенных чучел здесь нет. У каждого из этих правил в статье есть свой подраздел, объясняющий, почему очевидная реализация небезопасна, — и этих подразделов в статье бы не было, если бы очевидную реализацию никто никогда не выкатил.

Четвёртая строка — тот самый баг, теперь приколотый как постоянный экспонат. Если рефакторинг когда-нибудь снова уберёт no-op, красное загорится намеренно.

Да, это мутационное тестирование

Притворяться, что здесь придумано что-то новое, было бы глупо. Разница одна, и она практическая.

Инструменты вроде Stryker мутируют операторы языка: меняют > на >=, выкидывают вызов, инвертируют условие. А выключить нужно правило протокола, и правило протокола не живёт в одном операторе.

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

upToDateCheck         // §5.4.1 — кандидат должен быть не отстающим
prevLogCheck          // §5.3   — согласование логов при репликации
truncateConflicting   // §5.3   — конфликтующий хвост срезается
leaderNoop            // §8     — пустая запись своего терма при вступлении
stepDownOnHigherTerm  // §5.1   — увидел больший терм, сложил полномочия
persistBeforeReply    // §5.1   — голос на диск до ответа
currentTermCommitOnly // §5.4.2 — коммитить только запись своего терма

Автоматически такое не сгенерируешь. Список — это конспект статьи, записанный так, что его можно исполнить.

Устроено оно скучно: набор правил — обычный объект, приезжает в конструктор узла, по умолчанию всё включено, а тест музея создаёт кластер с одним выставленным в false. Никакой инструментации байт-кода, никакой подмены модулей. Из-за этого ветки остаются в рабочем пути — семь условий, которые в нормальной жизни всегда идут в одну сторону. Мне это не нравится, но альтернатива — держать вторую копию реализации, а вторая копия разъезжается с первой на третьем рефакторинге.

Ловится разное, и в этом смысл

Три экспоната из пяти ломают названное safety-свойство. Один оставляет все пять свойств целыми и просто перестаёт сводить кластер — это no-op. Один не стоит безопасности вообще, только прогресса: клиент в какой-то момент сдаётся.

Если сплющить это в «тест покраснел», выбрасывается самое полезное, что дало упражнение, — карта того, какая строчка статьи держит какую гарантию.

Два экспоната случайный поиск не достанет вообще. Figure 8 — сценарий, ради которого §5.4.2 и написан, — требует четырёх смен лидера в предписанном порядке с предписанными разделениями сети. Непереживший перезапуск голос требует, чтобы узел упал внутри окна в один тик между «проголосовал» и «записал голос на диск». Надеяться, что сидированный поиск туда забредёт, — не план, поэтому оба строятся руками.

Оправдание, которое ничего не стоит

Та же проблема в более резкой форме вылезла в соседнем проекте: MVCC-движок с четырьмя уровнями изоляции и чекер, который ищет циклы зависимостей в наблюдённых историях — G0, G1a, G1b, G1c, G-single, G2-item. Имена взяты у Адьи, чтобы читатель мог сверить реализацию с диссертацией, а не с моим пересказом.

Очевидная проверка здесь — на корректность уровня: на уровне L, на сотнях сидированных расписаний, движок ни разу не выдаёт аномалию, которую L обязан предотвращать.

Эта проверка не доказывает почти ничего. Движок, который отменяет каждую транзакцию, корректен на всех уровнях сразу. Чекер, который никогда ничего не находит, с ним восторженно согласится. Оба пройдут, и вдвоём они будут очень дорогим способом печатать слово «готово».

Поэтому от каждой ступени требуется второе, в противоположную сторону: должно существовать расписание, на котором она выдаёт аномалию, запрещённую уже следующей ступенью.

Read committed обязан показать read skew. Snapshot isolation обязан показать write skew. Теперь уровень стоит там, где его ставит литература, а не оказывается более строгим уровнем под чужим именем. Но полезнее другое: это требование проверяет чекер. Чекер, который не умеет найти write skew под snapshot isolation, ничем не подкреплял и своё оправдание serializable.

Последняя строка несёт вторую половину. Serializable не допускает ничего — и коммитит 51% транзакций на конкурентной нагрузке. Это число не отчёт, а утверждение в тесте: оправдание, купленное отменой всех транзакций, — вырожденный случай сверху, и единственный способ его не пустить — включить пропускную способность в саму формулировку.

Ни одной стороне не веришь отдельно. Каждая уличает другую.

Спросить того, кому на вас плевать

Всё это по-прежнему замкнуто. Мой движок, мой чекер, мои сиды. Если обе стороны разделяют одно и то же заблуждение — например, я последовательно неправильно прочитал Адью, — набор тестов этого не заметит. Все внутренние проверки согласятся друг с другом, и согласятся по неправильной причине.

Поэтому чекер наводится на PostgreSQL 18, поведение которого задокументировано не мной и ответы которого известны до начала прогона. Repeatable read у Postgres — это snapshot isolation; так написано в руководстве, и там же написано, что write skew там возможен. Serializable — это SSI Кэхилла, Рёма и Фекете.

Это та же лестница. Read committed допускает read skew и никогда не отменяет транзакции ради изоляции. Repeatable read read skew предотвращает, платит за это отменами и всё равно пропускает write skew, если сценарий построен под него. Serializable не допускает ничего и платит ту же цену.

PostgreSQL воспроизвёл мою лестницу, и он для этого со мной не советовался. Из всего раздела работает только это предложение.

Сокращение, которое врёт теми же словами

Дальше картина становится неприятно общей. Перебор расписаний находит баги и никогда не может доказать их отсутствие: двести расписаний из комбинаторного пространства — это хороший фаззинг, а не теорема. Доказать отсутствие значит обойти все достижимые состояния, а это экспонента — и поэтому вся инженерия в проверке моделей не про сам поиск, а про то, как его избежать.

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

Это тот же зелёный набор тестов, этажом ниже. И хуже, потому что сокращение — ровно та часть, которую дописывают ради скорости, а значит та, которую с наименьшей вероятностью станут выводить заново.

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

Результат, который не хотелось публиковать

Планировщик, на котором всё это стоит, навели на семь популярных async-пакетов: p-limit, p-queue, async-mutex, async-sema, generic-pool, p-retry и bottleneck. Девятнадцать задокументированных контрактов, сотни сидированных расписаний на каждый.

Все контракты выполнились. Ни одного бага.

Это честный заголовок, и я его чуть не выкинул, потому что «новый инструмент ничего не нашёл» — не та история, которую хочется рассказывать. Но нулевой результат здесь и есть калибровка. Это зрелые пакеты, чьи основные контракты каждый пользователь трогает ежедневно. Инструмент, объявивший, что в первый же вечер сломал ограничение конкурентности в p-limit, сообщил бы что-то о себе, а не о p-limit.

Что прогон действительно показывает: симулятор ведёт семь чужих пакетов — их таймеры, их промисы, их вытеснение — и ни один из них не знает о его существовании.

Один случай выглядел настоящим. Bottleneck запускал две задачи с разрывом 9 мс при минимальном интервале 10 мс. Оно воспроизвелось вне симулятора — обычно на этом вопрос закрывается. А потом выяснилось, что разрыв ровно 1 мс на всех 400 расписаниях. Не распределение, а константа. Это стоимость старта, а не дефект планирования.

Где кончается выборка

Когда в одном наборе лежат и сэмплер, и проверка моделей, появляется сравнение, которое я не ожидал увидеть настолько перекошенным. Одно и то же свойство, двумя способами.

И режимы отказа совпали с теми, которые пришлось строить руками. Экспонат с непережившим перезапуск голосом — тот, которому нужно падение внутри окна в один тик, тот, в который случайный поиск не попадает, — в модели оказывается просто достижимым состоянием.

✗ выборы в raft (3 узла, термы ≤ 2, один-голос-на-терм ВЫКЛ)
  инвариант «не более одного лидера в терме» не держится

  трасса
    (начало)                  n0:f0 n1:f0 n2:f0
    n0: выдвигается           n0:c1→0 n1:f0   n2:f0
    n1: выдвигается           n0:c1→0 n1:c1→1 n2:f0
    n0: голосует за n1        n0:c1→1 n1:c1→1 n2:f0
    n1: вступает в должность  n0:c1→1 n1:l1→1 n2:f0
    n1: голосует за n0        n0:c1→1 n1:l1→0 n2:f0
    n0: вступает в должность  n0:l1→1 n1:l1→0 n2:f0

Поэтому существуют оба. Ни одного не хватает, и отказ каждого закрывается ровно другим. Про вторую половину этой пары — отказ мастера и консенсус.

Чего это не даёт и чего стоит

Про TypeScript спросят, поэтому отвечу сразу. Он выбран не потому, что подходит для распределённых систем лучше Go или Rust, — он для этого подходит хуже. Он выбран потому, что детерминированной симуляции в JavaScript не было, а готовые поддельные таймеры управляют временем, но не тем, какой из нескольких готовых колбэков пойдёт первым, — а баг живёт именно там. В Rust это делает loom, и делает лучше: код под тестом использует примитивы самого loom, поэтому он видит каждое обращение к общему состоянию и умеет сокращать перебор. В JavaScript так не выйдет, не попросив пользователя объявлять разделяемые ресурсы руками. Это открытый вопрос, и хорошего ответа у меня нет.

Реального параллелизма здесь тоже нет: Node однопоточный, и симулятор тоже. Это про конкурентность, не про параллелизм. Гонки между воркерами и внутри нативных модулей — вне области.

И это дорого — не в деньгах, в объёме. У проверки моделей 944 строки исходников и 1767 строк того, что эти 944 строки проверяет. Почти вдвое больше кода, чем кода. Не потому, что я аккуратный: у неё нет способа сообщить, что она ошиблась. Единственный способ это узнать — держать рядом второй поиск, который ошибиться не может, и требовать совпадения.

Большинству кода всё это не нужно. В линейном коде путей конечное число и покрытие их закрывает. Смысл появляется ровно там, где порядок шагов выбирает не программист: два запроса на один счёт, платёж, повторённый после таймаута, очередь и её потребитель, блокировка и ожидание на ней. Там пространство поведений комбинаторное, и набор тестов достаёт из него горсть.

Что из этого забрать

Почти ничего из перечисленного не ново. Мутационному тестированию десятки лет, Jepsen занимается тем же снаружи много лет, TLC и SPIN — инструменты лучше того, что я когда-либо напишу, а FoundationDB выкатила базу, у которой вся история про корректность сводится к «мы это отсимулировали». Алгоритмы все лежат в книжках.

Вопрос к своему набору тестов стоит задавать не «проходит ли он». А: что должно сломаться, чтобы он покраснел, и проверял ли я хоть раз, что он краснеет.