Распределённый протокол нельзя покрыть юнит-тестами. Юнит-тест запускает один процесс на одной машине в одном порядке. Ваш протокол запускает десять процессов на пяти машинах в порядке, который вы не контролируете. Разрыв между этими двумя реальностями — там и обитают ваши баги.
Model checking устраняет этот разрыв. Она исследует все возможные переплетения всех возможных состояний, которых может достичь ваш протокол. Если существует способ, при котором две реплики расходятся во мнениях, способ уйти в дедлок при выборах лидера или способ возникновения сценария split-brain — model checker найдёт его. И найдёт до того, как вы напишете первый RPC handler.
Почему распределённые баги переживают традиционное тестирование
Проблема в комбинаторном взрыве состояний. Три узла, обменивающиеся сообщениями, могут породить миллиарды путей исполнения. Ручные интеграционные тесты покрывают от силы дюжину из них, обычно happy path и пару очевидных failure modes. А баг, при котором узел A падает ровно между отправкой prepare и ack? Удачи поймать это в CI.
Формальная верификация звучит как академическое упражнение, но model checking — другое. Вы не доказываете протокол корректным навеки. Вы описываете протокол на языке спецификаций, определяете интересующие вас свойства и даёте инструменту исчерпывающе перебрать пространство состояний в некоторых границах. Когда он находит нарушение, выдаёт вам минимальный trace. Вы получаете пошаговый рецепт воспроизведения бага. Никаких heisenbugs. Никакого «работает на моей машине».
Самый практичный инструмент для этого — TLA+, разработанный Лесли Лампортом. Это выглядит как математика, потому что это и есть математика. Но математика проще, чем вы ожидаете, а выгода — в нахождении багов, которые иначе всплыли бы в продакшене в два часа ночи.
Что на самом деле делает model checking
Model checker принимает три входных данных: описание вашей системы, описание её окружения и свойства, которые должны выполняться. Описание системы фиксирует логику вашего протокола. Описание окружения фиксирует всё, что вы не контролируете: сетевые задержки, потерю сообщений, падения узлов, смещение часов. Свойства обычно бывают инвариантами («зафиксированный лог никогда не перезаписывается») или условиями живучести («на каждый запрос рано или поздно придёт ответ»).
Затем checker генерирует каждое достижимое состояние и каждый допустимый переход между ними. Для конечных пространств состояний он делает это исчерпывающе, для бесконечных — с ограниченным перебором. Если инвариант нарушен, он останавливается и сообщает кратчайший путь к отказу.
Это грубая сила, а не магия. Model checker не понимает вашего замысла. Он просто перебирает всё. Именно в этом суть. Ваши интеграционные тесты необъективны из-за ваших предположений. У model checker’а предположений нет.
Спецификация простого протокола консенсуса на TLA+
Посмотрим на минимальный пример: протокол консенсуса с единственным декретом, где лидер предлагает значение, а кворум акцепторов должен принять его, прежде чем значение будет избрано. Это ключевая идея, лежащая в основе Paxos, Raft и любого другого алгоритма консенсуса, о котором вы слышали.
Вот спецификация TLA+ для системы:
------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets
CONSTANTS Values, Acceptors, Quorum
VARIABLES chosen
Init == chosen = {}
Propose(v) ==
/\\ v \\in Values
/\\ chosen = {}
/\\ chosen' = {v}
Next ==
\\E v \\in Values : Propose(v)
Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)
ChosenUniqueness ==
Cardinality(chosen) \\leq 1
=============================================================================Эта спецификация гласит: изначально ничего не избрано. Действие propose может установить chosen в единственное значение, но только если ещё ничего не избрано. Инвариант ChosenUniqueness утверждает, что избрано может быть не более одного значения.
Model checker TLA+, TLC, проверит, что ни одна execution trace не нарушает ChosenUniqueness. Если вы внесёте баг, при котором два лидера могут предлагать одновременно, не проверяя предыдущие значения, TLC найдёт контрпример за миллисекунды.
Добавляем неприятности: падения и потеря сообщений
Спецификация выше слишком чиста. Настоящие распределённые системы не бывают чистыми. Сообщения теряются. Узлы перезагружаются. Сетевые разделения изолируют группы узлов друг от друга. Модель становится полезной лишь когда вы моделируете эти сбои.
Вот более реалистичный фрагмент, моделирующий передачу сообщений с возможной потерей:
VARIABLES msgs, acceptorState
Send(m) == msgs' = msgs \\cup {m}
Deliver(m) ==
/\\ m \\in msgs
/\\ msgs' = msgs \\ {m}
/\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]
Drop(m) ==
/\\ m \\in msgs
/\\ msgs' = msgs \\ {m}
/\\ UNCHANGED acceptorState
Next ==
\\E m \\in msgs : Deliver(m) \\/ Drop(m)Drop — важное дополнение. Оно моделирует потерю сообщений, не меняя состояние акцептора. TLC будет исследовать trace’ы, в которых любое сообщение может быть доставлено, потеряно или задержано на неопределённый срок. Когда вы добавляете падение и восстановление лидера, пространство состояний растёт, но TLC всё равно исследует его систематически.
Это та часть, в которой я запутался, когда только начинал с TLA+. Я хотел моделировать только логику протокола. Но баги были не в логике. Они были во взаимодействии между логикой и режимами отказа, которые я не учёл. Нужно моделировать и то, и другое.
Компромисс: взрыв пространства состояний и абстракция
Model checking не бесплатна. Число состояний растёт экспоненциально с ростом числа процессов и размера полезной нагрузки сообщений. Спецификация с пятью значениями и тремя акцепторами может породить миллионы состояний. Добавьте четвёртого акцептора — и вы в миллиардах. Запустите это на ноутбуке, и он исчерпает память раньше, чем закончит.
Решение — абстракция. Вы не моделируете свои настоящие 64-байтные значения. Вы моделируете два значения: V1 и V2. Если протокол ведёт себя корректно для двух значений, конкретные значения не важны. Вы не моделируете лог из 10 000 записей. Вы моделируете лог глубины 2. Если safety выполняется для глубины 2, она почти всегда выполняется для произвольной глубины. Это называется small-model checking, и это стандартная практика в области.
Ключевой навык — научиться отличать важные детали от неважных. Содержимое сообщений обычно не важно для свойств safety. Порядок сообщений почти всегда важен. Идентификаторы узлов могут быть неважны, но количество узлов в каждой роли — важно.
Если пространство состояний всё ещё слишком велико, есть другие варианты. Можно использовать symmetry reduction, считая идентичные узлы взаимозаменяемыми. Можно ограничить глубину поиска. Или перейти к символьному model checker’у вроде Apalache, который использует SMT-решатели для рассуждений о состояниях, не перечисляя их все.
От спецификации к реализации: поддержание синхронизации
Верифицированная спецификация ничего не стоит, если ваша реализация расходится с ней. Спецификация — это чертёж. Код — это здание. Между ними нет автоматического моста, и именно в этом зазоре баги просачиваются обратно.
Практический подход — рассматривать спецификацию TLA+ как документ проектирования, который случайно оказывается исполняемым. Проверяйте её вместе с кодом во время pull requests. Когда реализация обрабатывает крайний случай, спросите себя, обрабатывает ли его спецификация. Когда вы находите баг в продакшене, проверьте, поймала бы его спецификация. Если нет — обновите спецификацию.
Некоторые команды идут дальше и генерируют тестовые случаи из контрпримеров, которые производит TLC. TLC trace, показывающий, как две реплики расходятся, становится сценарием интеграционного теста. Это ручная работа, но она связывает формальную модель с вашим тестовым набором.
В Sentry мы использовали этот подход для валидации распределённого протокола рейт-лимита. Спецификация поймала проблему живучести, при которой восстанавливающийся узел мог голодать в определённом сценарии разделения сети. Наши интеграционные тесты никогда не вызывали её, потому что всегда чисто устраняли разделения. Model checker не заботился о чистоте. Он попробовал грязный случай, нашёл баг и избавил нас от очень запутанного инцидента.
Начало работы: ваш первый модельный прогон
Если вы хотите попробовать, начните с TLA+ Toolbox. Это бесплатная IDE для написания и проверки спецификаций. Разберите примеры Paxos и Raft, которые идут в комплекте. Они сложнее приведённого выше фрагмента консенсуса, но показывают, как моделируются реальные протоколы.
Для вашей первой спецификации выберите что-то маленькое из своей системы. Протокол выборов лидера. Схема инвалидации распределённого кэша. Вариант two-phase commit. Запишите инварианты, в которые вы верите. А затем позвольте TLC сказать, правы ли вы. Обычно ответ — нет, и обычно он даётся в течение первого часа.
Model checking не найдёт все баги. Она не поможет с производительностью, не поймает serialization mistakes и не проверит, соответствует ли реализация спецификации. То, что она делает — находит глубокие протокольные баги, которые пропускают интеграционные тесты, и находит их на этапе проектирования, когда исправления ничего не стоят.
Это самый дешёвый фикс бага в распределённых системах. Не лучший дебаггер. Не больше мониторинга. Поймать баг до того, как код вообще существует.