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

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

Музей багов

Идея простая: взять работающую реализацию, выключить в ней ровно одно правило алгоритма и потребовать, чтобы харнесс поймал это — с сидом и с именем нарушенного свойства. Не «тест покраснел», а «нарушена Leader Completeness на прогоне 2, вот трасса».

нет проверки актуальности лога  → Leader Completeness   (прогон 2)
   n2 стал лидером в терме 4 без зафиксированной записи r6

нет проверки предыдущей записи  → Log Matching          (прогон 1)
   индекс 1 терм 1 держит noop:n1:1 в одном месте и r2 на n4

конфликтующая запись остаётся   → State Machine Safety  (прогон 4)
   индекс 8: n5 применил noop:n5:6, n2 применил r7

нет пустой записи лидера        → реплики разошлись     (прогон 25)
   n1={"a":"p1.2"} против n4={"a":"p1.2","b":"p1.3"}

игнорирует более новый терм     → клиент сдался         (прогон 1)
   клиент 2 не дождался ответа на cas — безопасность цела

Figure 8                        → Leader Completeness   (прогон 1)
   n5 стал лидером в терме 4 без зафиксированной записи entry-A

голос не пережил перезапуск     → Election Safety
   n2 и n3 оказались лидерами в одном терме 1

Ни один экспонат не выдуман: у каждого в статье Ongaro и Ousterhout есть свой подраздел, объясняющий, почему очевидная версия небезопасна. Подразделы пишут не просто так — значит, очевидную версию кто-то уже отгружал.

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

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

Теперь то, ради чего всё это было

На каком-то этапе все пять свойств безопасности держались на любом расписании — и хаос-прогон всё равно упал на двадцать пятом сиде. Две реплики с разными значениями. Логи при этом совпадали. Никто не падал. Ни одно правило из Figure 3 нарушено не было.

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

Лекарство описано в статье одной фразой в §8: новый лидер сразу дописывает пустую запись своего терма. Теперь она в коде есть, а её отсутствие — четвёртый экспонат музея.

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

Как устроен харнесс

Три решения, без которых ничего не работает.

Узел не делает ввод-вывод. Он не трогает ни часы, ни сокет, ни диск: tick двигает таймеры, receive отдаёт сообщение, propose — команду, а всё, что узел хочет сделать, забирают наружу takeMessages и takeApplied. Так же устроен raft в etcd, и по той же причине: реализацию, которая сама вызывает setTimeout и пишет в сокет, можно тестировать только запуском и надеждой.

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

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

Проверяются пять свойств из Figure 3 после каждого перехода состояния (не опросом — иначе нарушение приписывается не тому месту), линеаризуемость истории клиентских операций по Вингу и Гонгу, и сходимость реплик после прекращения отказов. Линеаризуемость NP-полна, поэтому у поиска есть бюджет, и когда он кончается, честный ответ — inconclusive, а не «всё хорошо».

Чего это не доказывает

Сотни сидов — это сотни расписаний из пространства, которое астрономически больше. Очень хороший фаззинг, но не теорема: TLA±спецификации Raft доказывают то, чего симуляция доказать не может. В модель отказов входят потеря, задержка, дублирование, перестановка, разделение и падение с сохранением диска; не входят порча диска, частичная запись, расхождение часов и византийское поведение. Изменения состава кластера и снапшотов нет вовсе — а это ровно те три вещи, которые превращают корректный алгоритм в эксплуатируемую систему.

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

Код: github.com/BOTIROFF-D/bulwark, MIT, ноль зависимостей, npm run museum проходит за шесть секунд. Более длинный разбор, с ценой каждой ошибки в проде, — у меня в блоге.