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

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

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

К этому моменту сеть уже была склеена, ничего не падало, логи у реплик совпадали. И все пять safety-свойств из Figure 3 статьи Онгаро и Оустерхаута — Election Safety, Leader Append-Only, Log Matching, Leader Completeness, State Machine Safety — держались на каждом переходе состояния, включая тот, что был непосредственно перед проверкой.

Правила алгоритма выполнялись. Система была неправа.

Что это было

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

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

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

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

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

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

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

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

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

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

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

Набор тестов, который никогда не краснел, одинаково хорошо описывает две ситуации. Либо код правильный, либо никто не смотрит. Различить их по цвету нельзя, и годами он будет докладывать вторую как первую.

Проверить чекер, запустив его и увидев зелёное, невозможно. Зелёное — ровно то, что выдаёт сломанный чекер.

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

Музей багов

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

нет проверки актуальности лога → Leader Completeness: n2 стал лидером в терме 4 без
                                 закоммиченной записи r6 на индексе 8 (терм 1)   (прогон 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","b":"p0.2"},
                                 n4={"a":"p1.2","b":"p1.3"}                      (прогон 25)
игнорирует более новый терм    → клиент 2 сдался на cas                          (прогон 1)

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

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

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

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

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

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

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

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

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

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

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

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

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

Два экспоната случайный поиск не достанет

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

Надеяться, что сидированный поиск туда забредёт, — не план. Оба строятся руками, отдельным файлом.

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

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

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

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

Эта проверка не доказывает почти ничего.

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

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

read-uncommitted     чисто на 150 расписаниях   допускает G1b на сиде 0
read-committed       чисто на 150 расписаниях   допускает G-single на сиде 1
snapshot-isolation   чисто на 150 расписаниях   допускает G2-item на сиде 25
serializable         чисто на 150 расписаниях   не допускает ничего, коммитит 51%

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

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

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

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

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

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

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

Направленный сценарий, две транзакции, каждая читает то, что другая собирается писать:

Уровень PostgreSQL	Что вышло	Вердикт чекера
`READ COMMITTED`	обе закоммитились	G2-item, `T2 —rw→ T1 —rw→ T2`
`REPEATABLE READ`	обе закоммитились	G2-item
`SERIALIZABLE`	одна отменена	ничего

Случайная выборка, 25 раундов по три конкурентные транзакции:

Уровень PostgreSQL	Отмены	Найдено аномалий
`READ COMMITTED`	0 / 100	G-single × 24
`REPEATABLE READ`	32 / 100	нет
`SERIALIZABLE`	32 / 100	нет

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

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

Сценарии лежат в against-postgres/ и запускаются на любой локальной базе: npm run test:postgres, ADYA_PG=postgres://... если она не там, где по умолчанию. Числа в таблицах сняты на 18-й версии; на других я их не перепроверял, так что если у кого-то выйдет иначе — интересно услышать.

Редукция, которая врёт теми же словами

Дальше картина становится неприятно общей.

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

Две классические редукции:

спецификация     без    симметрия   обе   выигрыш
workers(4)       625        70       17     37×
workers(6)     15625       210       25    625×

Симметрия — потому что шесть взаимозаменяемых воркеров в пяти фазах дают 5⁶ = 15 625 назначений, но всего 210 мультимножеств. Редукция частичных порядков — потому что два действия, не пересекающихся ни по одной переменной, коммутируют, и обход обоих порядков не показывает ничего сверх обхода одного.

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

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

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

И ещё одна строка, которая лежит в тестах как утверждение:

peterson          20        20       20      1×

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

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

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

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

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

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

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

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

Оформление этого баг-репорта стоило бы мейнтейнеру вечера из-за одной миллисекунды. Дисциплина, которая в таком инструменте что-то значит, — это не умение находить. Это умение не оформить то, что очень хотелось бы найти.

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

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

Свойство	Выборкой	Доказано
Election Safety, 3 узла, термы ≤ 3	сотни расписаний	2 428 состояний, исчерпывающе
Election Safety, 5 узлов, термы ≤ 2	сотни расписаний	148 318 состояний, исчерпывающе
Election Safety, 5 узлов, термы ≤ 3	сотни расписаний	6 801 084 состояния, исчерпывающе
Write skew под snapshot isolation	найден на сиде 25 из 300	достижим за 5 шагов, кратчайших

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

✗ выборы в 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

Шесть шагов, кратчайшие по построению, никакого сида.

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

А баг в начале этой статьи был в коде, не в алгоритме.

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

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

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

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

И это дорого. Не в деньгах, в объёме. У model checker’а 944 строки исходников — и 1767 строк того, что эти 944 строки проверяет. Почти вдвое больше кода, чем кода.

Не потому, что я аккуратный. Потому что у model checker’а нет способа сообщить, что он ошибся. Единственный способ это узнать — держать рядом второй поиск, который ошибиться не может, и требовать совпадения.

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

Что я бы отсюда вынес

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

Неочевидным для меня было другое, мельче и скучнее:

Зелёный набор тестов не несёт информации, пока его не заставили покраснеть намеренно.

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

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

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

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

Код

Если интереснее читать его, а не мой пересказ. Всё на TypeScript, MIT, без рантайм-зависимостей.

unflake — детерминированная симуляция: один сид, один и тот же прогон побайтово
bulwark — Raft, сидированные отказы и музей багов
adya — MVCC-движок, лестница изоляции и чекер аномалий
pnueli — model checker, его редукции и поиск, который их проверяет

Об авторе

Дониёр Ботиров, основатель dbit.one. Пятый год в разработке, архитектуру пишу сам и остаюсь на проекте до релиза — по складу тимлид, а не менеджер.

Из того, что строил: система управления парком тяжёлой техники для мирового производителя, контур национальной системы здравоохранения, ИИ-ассистент врача для университетского госпиталя, аналитический контур розничного банка, CRM сети учебных заведений. Заказчики под NDA, поэтому имён не будет — зато есть открытый код выше, который можно прочитать и запустить.