Тестирование распределённых систем: chaos engineering, Jepsen, симуляция

Есть тест, который проходит зелёным четыре тысячи раз подряд, а на четыре тысячи первый падает — и больше никогда не падает. Есть баг, который воспроизводится только в проде, только по вторникам, только когда деплой совпал с ротацией TLS-сертификатов. Есть инцидент, разбор которого заканчивается фразой «мы не смогли восстановить последовательность событий».

Это не признаки слабой дисциплины. Это признак того, что к распределённой системе применяют инструменты, рассчитанные на детерминированную программу. Обычный тест проверяет «на вход X — на выходе Y». Распределённая система не является функцией от входа. Её поведение — функция от входа и от порядка, в котором сложились миллионы событий, которые вы не контролируете: доставки пакетов, тики планировщика, паузы сборщика мусора, задержки fsync, шаги NTP.

Предыдущие двенадцать статей трека объясняли, что ломается: модели отказов, время, согласованность, консенсус, идемпотентность. Эта статья — про то, как убедиться, что система ведёт себя так, как вы утверждаете. Не «мы верим, что она согласованна», а «мы прогнали 200 000 сценариев отказа, вот вердикт чекера и вот seed, по которому падение воспроизводится за девять секунд».

Главная мысль: в распределённой системе тест — это не сравнение результата с ожидаемым. Тест — это порождение враждебного расписания событий и проверка полученной истории на существование допустимого объяснения. Всё остальное — детали реализации этой идеи.

Почему обычные тесты здесь бессильны

Четыре причины, и каждая диктует свой инструмент.

1. Пространство расписаний комбинаторно взрывается. Пять узлов, у каждого десяток внутренних состояний, плюс сеть, в которой в полёте до двадцати сообщений в произвольном порядке — счёт достижимых состояний идёт на астрономические величины. Юнит-тест проверяет одну траекторию. Вероятность попасть в опасную близка к нулю: опасные траектории редки, но не невозможны — а при миллионе запросов в час «редкое» происходит ежедневно.

2. Наблюдаемое — не то, что произошло. Клиент видит тайм-аут. Тайм-аут не означает «не выполнено». Он означает «не знаю». Тест вида assert response.status == 200 в распределённом мире некорректен по построению: он предполагает, что отсутствие ответа равно отсутствию эффекта. Именно на этом ломается большинство самописных «тестов на надёжность».

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

4. Отказ не воспроизводится по требованию. Чтобы отладить, нужно повторить. Чтобы повторить, нужно контролировать порядок событий. В обычном стеке порядок определяют восемь независимых источников случайности, и ни один из них вам не подчиняется.

Полезная эмпирика: исследование Ding Yuan и соавторов «Simple Testing Can Prevent Most Critical Failures» (OSDI 2014) разобрало 198 критичных отказов в Cassandra, HBase, HDFS, MapReduce и Redis. 92 % катастрофических отказов вызваны неправильной обработкой уже обнаруженных ошибок, а 58 % из них поймал бы линтер или три строчки теста: пустой catch, TODO вместо обработки, abort() на восстановимой ошибке. И одновременно: 77 % отказов требуют более одного события, а треть — специфического порядка. Отсюда двойная мораль — сначала закройте тривиальное, потом стройте машинерию для поиска порядков.

Что вообще считать багом

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

• Safety («ничего плохого не случится») — нарушается конкретным конечным префиксом истории. Прочитанное значение, которого никто не писал; подтверждённая запись, исчезнувшая после перевыборов; два держателя одной блокировки. Такое нарушение можно предъявить.
• Liveness («что-то хорошее в конце концов случится») — нарушается только бесконечной историей, поэтому в тестах его превращают в safety с дедлайном: «после прекращения отказов кластер обязан принять запись за 30 секунд». Формально это уже другое свойство, зато проверяемое.

Ключевая деталь всей дисциплины — статус операции. Их три, а не два:

:fail — операция гарантированно не применилась (сервер ответил «отклонено», соединение не установилось). :info — неизвестно. Разница принципиальна: :fail можно выкинуть из истории, :info — нет, чекер обязан перебрать обе возможности. Система, в которой клиент не может отличить :fail от :info, непроверяема в принципе: любая история объяснима, потому что любую операцию можно объявить не случившейся. Отсюда же требование к API, которое обычно всплывает поздно: без стабильного идентификатора запроса (см. идемпотентность) вы не сможете ни дедуплицировать ретрай в проде, ни разрешить :info в тесте.

Карта методов: реалистичность против воспроизводимости

Инструментов много, и они не конкурируют, а покрывают разные квадранты. Ось X — насколько дёшево повторить найденное падение, ось Y — насколько похоже на прод.

Стоимость находки растёт примерно на порядок с каждым шагом вправо-вверх: баг, пойманный симуляцией, — это полчаса разработчика; тот же баг в Jepsen — день; в проде — инцидент, постмортем и потерянные деньги. Отсюда стратегия: всё, что можно сдвинуть влево, сдвигайте влево, а chaos в проде оставьте для того, что принципиально не воспроизводится в лаборатории — реальных объёмов трафика, реального железа, реальных зависимостей и реальных людей на дежурстве.

Историческая канва короткая: 1990 — формализация линеаризуемости у Herlihy и Wing; 2011 — Netflix открывает Chaos Monkey и вводит термин chaos engineering; 2012 — FoundationDB строит движок вокруг детерминированной симуляции; 2013 — Kyle Kingsbury запускает Jepsen и создаёт жанр публичного аудита БД; 2014 — Amazon публикует опыт TLA+; 2015 — lineage-driven fault injection выводит инъекции из следов; 2020 — Elle находит аномалии изоляции без перебора; 2020-е — детерминизм переносят на уровень гипервизора (Antithesis, VOPR в TigerBeetle).

Что можно ломать: таксономия инъекций

Инъекция отказа должна соответствовать модели отказов, а не фантазии автора теста. Практический список, отсортированный по злобности:

Два наблюдения из практики. Первое: kill -9 — самый добрый вид отказа. Он однозначен, быстро обнаруживается, и обработка его обычно отлажена. Настоящие проблемы дают паузы и серые отказы, когда узел не умер, а стал медленным или частично связным. Второе: разделения сети редко бывают симметричными. Работа «An Analysis of Network-Partitioning Failures in Cloud Systems» (OSDI 2018) показала, что 69 % отказов из-за разделений приводят к катастрофическим последствиям, при этом 80 % из них воспроизводятся на кластере из трёх узлов, а 90 % — детерминированно. То есть барьер входа низкий: три контейнера и iptables уже дают доступ к большинству реальных сценариев.

Детерминированная симуляция: свести весь недетерминизм к одному числу

Идея, к которой независимо пришли FoundationDB, TigerBeetle и Antithesis: если весь недетерминизм проходит через ваши абстракции, его можно параметризовать одним seed. Тогда отчёт о баге — восемь байт.

Требования к коду жёсткие, и их проще заложить сразу, чем внедрять потом:

• никаких прямых системных вызовов — время, сеть, диск, случайность только через интерфейсы; никаких потоков и блокировок — одна кооперативная петля событий, иначе планировщик ОС снова становится источником недетерминизма;
• никаких зависимостей от порядка обхода хеш-таблиц (в Go порядок map намеренно рандомизирован, в Python — стабилен для строк только внутри процесса);
• виртуальные часы: время двигают события, а не процессор. Поэтому сутки жизни кластера прогоняются за секунды — между событиями нечего ждать.

Минимальный, но настоящий каркас симулятора:

import heapq
import random
from dataclasses import dataclass, field

@dataclass(order=True)
class Event:
    at: float                       # виртуальное время срабатывания
    seq: int                        # тай-брейк: полный порядок при равном времени
    node: str = field(compare=False)
    msg: dict = field(compare=False)

class Sim:
    """Однопоточная петля событий. Единственный источник случайности — self.rnd."""

    def __init__(self, seed: int, nodes: list[str]):
        self.rnd = random.Random(seed)
        self.now = 0.0
        self.seq = 0
        self.queue: list[Event] = []
        self.state = {n: {"log": [], "term": 0, "alive": True} for n in nodes}
        self.cut: set[tuple[str, str]] = set()   # односторонние разрывы (src, dst)

    def schedule(self, at: float, node: str, msg: dict) -> None:
        self.seq += 1
        heapq.heappush(self.queue, Event(at, self.seq, node, msg))

    def send(self, src: str, dst: str, msg: dict) -> None:
        # Разрыв: сообщение исчезает молча — отправитель об этом не узнает никогда.
        if (src, dst) in self.cut or not self.state[dst]["alive"]:
            return
        if self.rnd.random() < 0.02:                     # 2 % потерь
            return
        delay = self.rnd.uniform(0.001, 0.050)           # задержка канала
        self.schedule(self.now + delay, dst, msg)
        if self.rnd.random() < 0.01:                     # 1 % дублей: сеть ретранслировала
            self.schedule(self.now + delay + self.rnd.uniform(0, 0.2), dst, msg)

    def buggify(self, p: float = 0.25) -> bool:
        """Точка редкого поведения: включается только в симуляции.
        Приём из FoundationDB — заставить редкую ветку срабатывать часто."""
        return self.rnd.random() < p

    def run(self, until: float, handle, invariants) -> None:
        while self.queue and self.queue[0].at <= until:
            ev = heapq.heappop(self.queue)
            self.now = ev.at             # часы двигают события, а не процессор
            if self.buggify(0.001):      # редкий отказ узла в произвольный момент
                self.state[ev.node]["alive"] = False
                self.schedule(self.now + self.rnd.uniform(1, 10), ev.node,
                              {"type": "restart"})
                continue
            handle(self, ev)
            for check in invariants:     # safety проверяем после КАЖДОГО шага
                check(self)

Сложность: O(E log E) по времени на E обработанных событий (каждое проходит через кучу дважды) и O(N + Q) по памяти, где Q — максимальный размер очереди в полёте. Проверка инвариантов добавляет свою цену: если она O(N) на шаг, суммарно получится O(E · N) — за этим надо следить, иначе прогон замедляется в разы и вы прогоните не 200 000 сценариев, а 2 000.

buggify — самое недооценённое место. В FoundationDB эти маркеры расставлены по всему коду: они увеличивают вероятность редких веток (переполнение буфера, повторная отправка, срабатывание таймера ровно в момент переключения роли). Без них симуляция честно воспроизводит распределение реального мира, где интересные ветки не встречаются никогда. Подробности — в статье «FoundationDB: A Distributed Unbundled Transactional Key Value Store» (SIGMOD 2021) и в докладе Will Wilson «Testing Distributed Systems w/ Deterministic Simulation» (Strange Loop 2014).

Как выглядит падение — и в этом вся ценность подхода:

[sim] seed=0x4f2a9c31 commit=a91f3d7 steps=118374 vtime=86412.118s
[sim] FAIL invariant=committed_entry_survives node=n3
[sim]   entry idx=4412 term=7 acked_to_client=true present_on={n1} quorum=3
[sim] replay: SEED=0x4f2a9c31 cargo test --test sim -- --nocapture

Отчёт о баге — одна строка: через год на чужом ноутбуке тот же seed воспроизведёт тот же прогон байт в байт, включая момент падения. Сравните с «иногда падает в ночном прогоне на CI».

Практический ориентир по эффективности: у алгоритма случайного планирования PCT (Burckhardt и др., ASPLOS 2010) есть доказанная нижняя граница вероятности найти баг глубины d за один прогон: 1 / (n · k^(d-1)), где n — число потоков, k — число шагов. Смысл: баги малой глубины (2–3 «неудачных» решения планировщика) находятся быстро, и именно они составляют большинство. Поэтому тысяча коротких прогонов с разными seed эффективнее одного длинного. Чего симуляция не даёт: она проверяет вашу модель мира — если реальный диск теряет данные способом, которого нет в SimDisk, симуляция будет вечно зелёной. Поэтому её дополняют проверкой на настоящем кластере.

Проверка историй: линеаризуемость и изоляция

Допустим, история собрана. Как решить, законна ли она? Для регистра и линеаризуемости (см. модели согласованности) вопрос ставится так: существует ли линейный порядок операций, который (а) согласован с последовательной спецификацией объекта и (б) уважает реальное время — если операция A завершилась до начала B, то A стоит раньше B.

Классический алгоритм Wing–Gong: перебирать, какая из «свободных» операций линеаризуется следующей.

def linearizable(pending: list[dict], state, apply_op) -> bool:
    """pending: операции с полями call, ret, op, value.
    apply_op(state, op) -> (совместимо?, новое состояние)."""
    if not pending:
        return True
    for i, op in enumerate(pending):
        # Операцию нельзя ставить первой, если какая-то другая завершилась
        # ДО её вызова: реальный порядок это запрещает.
        if any(other["ret"] < op["call"] for other in pending):
            continue
        ok, new_state = apply_op(state, op)
        if not ok:
            continue
        rest = pending[:i] + pending[i + 1:]
        if linearizable(rest, new_state, apply_op):
            return True
    return False

В худшем случае это O(c!) по числу одновременно висящих операций c; с мемоизацией по паре «состояние + множество оставшихся» — примерно O(2^c · c). Это не лень реализации: проверка линеаризуемости NP-полна (Gibbons и Korach, Testing Shared Memories, SIAM J. Comput. 1997). Практический вывод жёсткий и часто игнорируемый: держите конкурентность 5–10 клиентов и короткие истории. Знаменитый Knossos на 200 параллельных клиентах будет считать сутки и не закончит; Porcupine (Go) быстрее на порядок, но природу задачи не меняет.

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

Для транзакционных БД перебор безнадёжен, и здесь работает другой приём. Elle (Kingsbury и Alvaro, VLDB 2020) использует значения, из которых можно вывести зависимости: списки, к которым операции только дописывают (append). Если транзакция прочитала [1 2 5], то порядок записей известен точно — не нужно ничего перебирать. Дальше строится граф зависимостей (ww, wr, rw) и ищутся циклы: любой цикл — аномалия из формализма Adya, с точным именем.

Поиск циклов — O(V + E) через Тарьяна, то есть на порядки дешевле перебора. Вывод чекера выглядит так:

{:valid? false
 :anomaly-types (:G-single-item :cyclic-versions)
 :not #{:repeatable-read}
 :also-not #{:strict-serializable :serializable :snapshot-isolation}}

Эту же логику стоит применять к своему коду: если тест не может назвать нарушенное свойство по имени из формальной иерархии, он проверяет не гарантию, а ощущение. Набор запросов Hermitage даёт готовые сценарии для проверки уровней изоляции конкретной СУБД — полезное дополнение к транзакциям и изоляции.

Jepsen: как устроен и что он нашёл

Jepsen — фреймворк Kyle Kingsbury на Clojure, породивший целый жанр публичных аудитов баз данных. Его архитектура — образец того, как вообще строится такой тест.

Пять частей с чёткими ответственностями:

• Generator — чистый поток операций без побочных эффектов (отделение «что делать» от «как делать» и даёт воспроизводимость); Client — по одному на узел, превращает операцию в вызов к БД и возвращает :ok / :fail / :info.
• Nemesis — отдельный «клиент», операции которого суть отказы: разделить сеть, сдвинуть часы, послать SIGSTOP, убить процесс.
• History — журнал всех вызовов и завершений, включая немезиду; Checker — превращает историю в вердикт: линеаризуемость (Knossos), изоляция (Elle), потеря множеств, монотонность offset-ов.

Обратите внимание на финальный вопрос. Если write 9 со статусом :info всё-таки применился, а последующее чтение вернуло 7 — это потерянная подтверждённая запись? Нет: :info не был подтверждён клиенту, поэтому чекер вправе линеаризовать его после чтения или не линеаризовать вовсе. А вот если бы write 9 вернул :ok, а чтение после схождения кластера дало 7 — это нарушение, и его надо предъявлять.

Минимальный клиент выглядит так (Clojure, потому что таков Jepsen) — вся суть в двух catch:

(defrecord Client [conn]
  client/Client
  (invoke! [this test op]
    (case (:f op)
      :read  (assoc op :type :ok :value (kv/get conn "x"))
      :write (try (kv/put! conn "x" (:value op))
                  (assoc op :type :ok)
                  ;; Сервер явно отклонил: эффекта нет — законно писать :fail.
                  (catch RejectedException _ (assoc op :type :fail))
                  ;; Тайм-аут: НЕ :fail. Мы не знаем, применилось ли.
                  (catch TimeoutException _ (assoc op :type :info))))))

Реальные находки

Ценность жанра не в громких заголовках, а в том, что он превратил маркетинговые обещания в проверяемые утверждения:

• MongoDB годами показывала потерю подтверждённых записей при разделениях; серия отчётов привела к переработке протокола репликации и к тому, что уровни записи по умолчанию стали безопаснее.
• etcd (реализация Raft) проверку прошёл, но обнаружилось, что чтения без linearizable-флага возвращают устаревшие данные — гарантия зависела от опции клиента, а не от системы.
• Cassandra: облегчённые транзакции (LWT, Paxos поверх кворумов) при определённых сочетаниях отказов давали потерю обновлений; часть проблем упиралась в разрешение конфликтов по времени записи — прямое следствие того, о чём говорилось в статье про время.
• Kafka: анализ транзакций показал сценарии, где заявленные гарантии не выполнялись при определённых конфигурациях; разбор изменил и документацию, и код — см. очереди и потоки.
• PostgreSQL 12.3: при исполнении на уровне serializable через сетевой драйвер обнаружилось нарушение, которое многие считали невозможным для «зрелой РСУБД».

Общая мораль: гарантия, которую никто не проверял, — это гарантия из README. Полные отчёты — на jepsen.io/analyses; читать их полезно даже без намерения писать тесты, как сборник анти-паттернов.

Chaos engineering: эксперимент, а не хулиганство

Chaos engineering часто понимают как «убить случайный под и посмотреть». Это не так. Согласно Principles of Chaos Engineering, это эксперимент с гипотезой о поведении системы в стационарном состоянии.

Элементы, без которых это не эксперимент, а авария:

1. Стационарное состояние измеряется бизнес-метрикой, а не загрузкой CPU. Netflix использует число запусков воспроизведения в секунду: метрика чувствительная, шумная предсказуемо и понятна всем.
2. Радиус поражения ограничен и растёт постепенно. Платформа ChAP в Netflix (ICSE-SEIP 2019) направляет на эксперимент малую долю трафика и сравнивает канареечную группу с контрольной — статистически, а не «на глаз».
3. Автоматическая остановка — условия отката определены до старта и исполняются автоматикой, а не человеком, который «сейчас посмотрит»; и наблюдаемость сначала, chaos потом: эксперимент, результат которого нельзя измерить, бесполезен — вы устроили отказ и не узнали ничего.

Чем инжектировать

# Задержка 150 мс с джиттером 30 мс и 1 % потерь на исходящем интерфейсе.
sudo tc qdisc add dev eth0 root netem delay 150ms 30ms loss 1%

# Асимметричное разделение: n1 не принимает от n4, а n4 продолжает "видеть" n1.
# Самый коварный класс отказов: heartbeat идёт в одну сторону, кворум разваливается.
sudo iptables -A INPUT -s 10.0.0.4 -j DROP

# Пауза процесса на 25 секунд — эмуляция stop-the-world паузы GC.
kill -STOP "$PID"; sleep 25; kill -CONT "$PID"

# Сдвиг часов на 12 минут вперёд — проверка логики лиз и TTL.
sudo date -s "+12 minutes"

# Chaos Mesh: разделение платёжного сервиса и его базы на 90 секунд.
# Злее, чем убить под: kubelet не перезапустит его, трафик продолжит идти,
# health-check останется зелёным — классический серый отказ.
apiVersion: chaos-mesh.org/v1alpha1
kind: NetworkChaos
metadata: {name: payment-db-partition, namespace: staging}
spec:
  action: partition
  mode: all
  direction: both
  duration: 90s
  selector:                                   # кого отрезаем
    namespaces: [staging]
    labelSelectors: {app: payment-api}
  target:                                     # от кого отрезаем
    mode: all
    selector:
      namespaces: [staging]
      labelSelectors: {app: postgres-primary}

Полезные инструменты: Toxiproxy (управляемый прокси, отказы включаются по HTTP прямо из теста — идеален для интеграционных тестов), Chaos Mesh и LitmusChaos для Kubernetes, Pumba для контейнеров без прав на хост-сеть, AWS Fault Injection Service для отказов зон и API облака. Про площадку для всего этого — Kubernetes.

Умный chaos вместо случайного

Случайное убийство подов быстро выходит на плато: девяносто процентов инъекций попадают в места, которые уже отлажены. Дальше есть два пути.

Lineage-driven fault injection (Peter Alvaro, Molly, SIGMOD 2015): взять след успешного выполнения, построить дерево причин («почему результат получился»), решателем SAT найти минимальный набор отказов, который обрубает все пути к успеху, и внедрить именно его. В промышленной версии на данных Netflix это сократило пространство поиска на порядки: вместо миллионов комбинаций — десятки осмысленных.

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

Как тестами убить миф про exactly-once

Обещание «exactly-once delivery» — самое частое утверждение, которое разваливается при первом же честном тесте. Причина фундаментальная: канал ненадёжен, отправитель не может отличить «сообщение потеряно» от «потерян ответ». Ретрай обязателен, значит дубликат возможен. Единственное, что достижимо, — at-least-once доставка плюс идемпотентная обработка, что даёт наблюдаемый эффект «ровно один раз» (это и называют effectively-once). Механику разбирала статья про гарантии доставки; здесь — как это проверять.

Так выглядит нарушение в логах платёжного шлюза, где ключ идемпотентности заявлен, но проверяется не транзакционно:

14:02:11.884 gw   POST /v1/charge idem=8f2c1a order=A-77 -> upstream timeout after 3000ms
14:02:11.902 psp  charge 8f2c1a authorized amount=4990 auth=P-91120
14:02:14.910 gw   retry=1 POST /v1/charge idem=8f2c1a order=A-77 -> 201 auth=P-91121
14:02:14.913 db   INSERT payments(order=A-77) x2   -- ключ уникален по auth, не по idem
14:47:02.310 ops  клиент видит два списания по 49.90

Всё решили 18 миллисекунд между тайм-аутом шлюза и успешной авторизацией на стороне PSP; никакой тест на «счастливый путь» этого не покажет. Проверяемый тест выглядит так:

1. Генератор отправляет N логических операций, каждая с устойчивым ключом; повторы делает сам тест, имитируя ретраи клиента.
2. Немезида во время нагрузки бьёт: разделение между продюсером и брокером, перезапуск консьюмера в момент коммита offset, пауза координатора транзакций.
3. Инвариант проверяется не по числу сообщений, а по эффекту: сумма в БД равна сумме логических операций; множество применённых ключей равно множеству отправленных; ни один ключ не применён дважды.
4. Отдельный инвариант на окно дедупликации: тест должен послать дубликат позже, чем живёт таблица ключей (например, через 8 дней при TTL 7 дней) и убедиться, что система либо отклоняет такой запрос, либо это осознанно принятый риск, записанный в решении.

Что этот тест обычно находит:

• дедупликация в кеше, а не в той же транзакции, что и эффект: кеш очистился при рестарте — дубликат прошёл; либо ключ, включающий timestamp или UUID, сгенерированный на каждом ретрае, то есть не работающий вообще;
• транзакции Kafka (KIP-98), работающие «ровно один раз» внутри Kafka, но теряющие свойство на границе с внешней БД: exactly-once заканчивается там, где начинается сторонний side-effect;
• «идемпотентный» обработчик, идемпотентный по первичному эффекту (списание), но не по вторичным (письмо клиенту, событие в аналитику, метрика).

Формулировка, которую стоит записать в требования буквально: «мы гарантируем at-least-once доставку и идемпотентную обработку по ключу X с окном Y дней; наблюдаемый эффект — ровно один раз в пределах окна». Такое утверждение можно проверить тестом. «Exactly-once» — нельзя.

Формальные методы: проверять дизайн, а не код

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

TLA+ (Leslie Lamport) описывает систему как множество допустимых поведений и проверяет инварианты полным перебором пространства состояний в модели. Amazon описал опыт в CACM 2015: в DynamoDB нашли ошибку глубины 35 шагов — последовательность, которую не породил бы ни один тест; в S3 и EBS TLA+ ловил дефекты дизайна до написания кода. Позже команда S3 применила «облегчённые формальные методы» (SOSP 2021): исполняемая эталонная модель на том же языке, что и продукт, плюс property-based тесты, сверяющие реализацию с моделью в CI.

Более мягкие ступени, доступные обычной команде:

• Property-based тесты (Hypothesis, QuickCheck, testing/quick) с автоматическим сокращением контрпримера — половина пользы формальных методов за день работы; в паре с ними модель-оракул: простая однопоточная эталонная реализация, с которой сравнивают ответы настоящей системы под нагрузкой и отказами.
• Язык P (p-org.github.io/P) — модель-чекинг для событийных систем; применялся в AWS для протоколов хранилищ.

Формальные методы и тесты ловят непересекающиеся множества ошибок, поэтому «у нас есть TLA+, тесты не нужны» — такая же ошибка, как обратная.

Минимальный набор для обычного сервиса

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

1. Тест на дубликат. Отправить одну и ту же операцию дважды с одним ключом (последовательно и параллельно) — эффект обязан быть один. Пять строк, ловит целый класс инцидентов.
2. Тест на тайм-аут зависимости. Toxiproxy между сервисом и БД: задержка выше таймаута. Проверить, что сервис отвечает деградацией, а не виснет и не исчерпывает пул соединений.
3. Тест на рестарт в середине. Убить процесс между записью в БД и публикацией события. Проверить, что запись и событие в итоге сходятся (это и есть проверка outbox из распределённых транзакций).
4. Тест на порядок. Доставить события в обратном порядке и с дублем. Проверить, что состояние сходится (версии, номера последовательности или CRDT — см. репликацию).
5. Тест на потерю кворума. Разделить кластер БД так, чтобы приложение оказалось в меньшинстве. Убедиться, что оно возвращает ошибку, а не «успешно» записывает в никуда — это прямая проверка позиции по CAP и PACELC.
6. Тест на сдвиг часов. Сдвинуть время на минуту вперёд и назад: проверяется логика TTL, лиз и координации — лизы, завязанные на абсолютное время, ломаются первыми. Системы уровня Spanner потому и делают неопределённость часов явной (интервал TrueTime и commit-wait), что иначе такой тест не пройти.
7. Тест на горячий ключ. Направить 80 % нагрузки в один ключ и убедиться, что партиционирование и backpressure не превращают это в отказ всего сервиса.

Встраивание в CI: быстрые тесты (1–4) — на каждый коммит, они укладываются в минуты. Прогон с немезидой на 5–10 минут — на merge в основную ветку. Длинный ночной прогон симуляции или Jepsen — по расписанию. Отдельный бюджет времени и отдельная очередь: тест, который занимает 40 минут в общем пайплайне, отключат через две недели (организационная сторона — в стратегии автоматизации). И обязательное правило: падение с известным seed превращается в детерминированный регресс-тест, иначе одна и та же ошибка будет находиться заново каждые полгода.

Типичные ошибки

1. Считать тайм-аут отказом. Тест, который на :info пишет assert failed, проверяет не систему, а предположения автора.
2. Ронять только процессы. kill -9 — добрый отказ. Реальные проблемы дают паузы, асимметричные разделения и медленные ответы.
3. Проверять только после восстановления. Многие нарушения существуют лишь в окне отказа: два лидера живут восемь секунд и успевают навредить, а к моменту проверки система выглядит здоровой.
4. Chaos без наблюдаемости. Эксперимент, результат которого нельзя измерить, — просто авария, устроенная своими руками.
5. Гонять симуляцию с одним seed. Один seed — одна траектория. Ценность даёт число прогонов, а не наличие симулятора.
6. Не минимизировать контрпример. Падение из 4000 событий бесполезно; автоматическое сокращение до трёх необходимых инъекций превращает отчёт в задачу на полчаса.
7. Ставить 200 клиентов в чекер линеаризуемости. Задача NP-полна: чекер будет считать сутки и не закончит. Держите 5–10.
8. Тестировать в топологии, отличной от продовой, и верить документации вендора. Три узла в одной зоне не воспроизводят межрегиональные задержки и коррелированные отказы зоны; а привычка верить README на слово и породила жанр Jepsen — проверяйте гарантии на своей версии и своей конфигурации.
9. Останавливаться на «тест прошёл». Прошедший тест означает лишь то, что этот набор сценариев не нашёл нарушений. Отсутствие доказательства ошибки — не доказательство отсутствия ошибок.

Мини-итог

• Обычные тесты проверяют одну траекторию из астрономического пространства. Распределённые баги живут в редких порядках событий, поэтому порождать надо расписания, а не входы.
• Баг здесь — нарушение safety на истории целиком (liveness проверяется превращением в safety с дедлайном), а статус :info — центральное понятие: система, где :fail неотличим от тайм-аута, непроверяема в принципе.
• Детерминированная симуляция сводит весь недетерминизм к одному seed: сутки жизни кластера за секунды, отчёт о баге — восемь байт. Цена — дисциплина: весь I/O через абстракции, никаких потоков и глобальных часов.
• Проверка линеаризуемости NP-полна — держите конкурентность низкой; для транзакционных БД используйте Elle с поиском циклов за O(V + E).
• Chaos engineering — эксперимент с гипотезой о бизнес-метрике, минимальным радиусом поражения и автоматической остановкой, а не убийство подов ради адреналина.
• Формальные методы проверяют дизайн, тесты — реализацию; это разные множества ошибок. А «exactly-once» и «наш кластер не теряет данные» — гипотезы: пока чекер не прошёл по истории с инъекциями, это утверждения веры.

Источники

• Kyle Kingsbury. Jepsen: analyses — отчёты по MongoDB, etcd, Cassandra, Kafka, PostgreSQL и десяткам других систем.
• Kyle Kingsbury, Peter Alvaro. Elle: Inferring Isolation Anomalies from Experimental Observations, VLDB 2020.
• Maurice Herlihy, Jeannette Wing. Linearizability: A Correctness Condition for Concurrent Objects, TOPLAS 1990; Phillip Gibbons, Ephraim Korach. Testing Shared Memories, SIAM J. Comput. 1997 — NP-полнота проверки.
• Ding Yuan et al. Simple Testing Can Prevent Most Critical Failures, OSDI 2014.
• Ahmed Alquraan et al. An Analysis of Network-Partitioning Failures in Cloud Systems, OSDI 2018.
• Jingyu Zhou et al. FoundationDB: A Distributed Unbundled Transactional Key Value Store, SIGMOD 2021 — симуляция и BUGGIFY.
• Sebastian Burckhardt et al. A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs, ASPLOS 2010.
• Peter Alvaro et al. Lineage-driven Fault Injection, SIGMOD 2015; Automating Failure Testing Research at Internet Scale, SoCC 2016.
• Ali Basiri et al. Automating Chaos Experiments in Production, ICSE-SEIP 2019; Principles of Chaos Engineering.
• Chris Newcombe et al. Use of Formal Methods at Amazon Web Services, CACM 2015; James Bornholt et al. Lightweight Formal Methods for a Key-Value Node in S3, SOSP 2021.
• Первоисточники, гарантии которых проверяют перечисленные инструменты: Leslie Lamport. Time, Clocks, and the Ordering of Events (1978); Diego Ongaro, John Ousterhout. In Search of an Understandable Consensus Algorithm (Raft) (2014); Giuseppe DeCandia et al. Dynamo (SOSP 2007); James Corbett et al. Spanner (OSDI 2012).
• Инструменты: Toxiproxy, Chaos Mesh, LitmusChaos, AWS FIS, Pumba, Porcupine, madsim, turmoil, Hermitage, TLA+, P.

Что дальше

Это последняя статья трека «Распределённые системы», и круг замыкается. Модели отказов объяснили, что именно ломается; время, CAP и PACELC и модели согласованности дали язык для описания компромиссов; репликация, партиционирование и консенсус — механизмы; транзакции, идемпотентность, координация и очереди — прикладные приёмы; наблюдаемость и эта статья — способы узнать правду о собственной системе. Общая картина трека — в карте.

Куда двигаться дальше, в зависимости от вашей роли:

• Проектируете системы. System design — как из этих кирпичей собирают целое, и паттерны устойчивости — таймауты, ретраи, circuit breaker и bulkhead в прикладном виде.
• Работаете с данными. Транзакции и уровни изоляции и распределённые БД и NewSQL показывают, как теория выглядит внутри конкретных движков.
• Отвечаете за эксплуатацию. Kubernetes как площадка для инъекций и наблюдаемость и дежурства — организационная половина надёжности.
• Занимаетесь качеством. Трек тестирования даёт базу: дизайн тестов, стратегия автоматизации, тесты в CI. Отдельно интересен поиск тестов эволюционными методами — прямое развитие идеи «искать враждебные сценарии автоматически».
• Хотите теории. NP-полнота и приближённые алгоритмы объяснят, почему проверка линеаризуемости так дорога, а параллельные и распределённые алгоритмы добавят вычислительный взгляд на те же задачи.

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