Кратко

  • Фишер, Линч и Патерсон доказали: для любого детерминированного частично корректного протокола консенсуса в их асинхронной модели с не более чем одним отказом существует допустимое выполнение, которое никогда не принимает решение.
  • Бивалентная конфигурация сохраняет доступными оба значения. Перестановка независимых событий позволяет откладывать критический шаг, оставаясь честным к процессам и доставке сообщений.
  • Частичная синхронность, детекторы отказов и случайность меняют предпосылки. Тайм-аут может запускать действие, но не доказывает отказ удалённого процесса.

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

Эту неопределённость Майкл Фишер, Нэнси Линч и Майкл Патерсон оформили в теорему 1985 года. Их статья Impossibility of Distributed Consensus with One Faulty Process не говорит, что любой запуск обречён. Она говорит, что в выбранной модели у безопасного детерминированного протокола всегда найдётся хотя бы одно допустимое выполнение без решения.

Надёжность без срока

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

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

Отвергается даже слабое условие завершения: в каждом допустимом выполнении когда-нибудь решает хотя бы один процесс. Если нельзя гарантировать это, нельзя гарантировать и более сильное завершение.

Бивалентность хранит две возможности

Конфигурация включает локальные состояния и буфер сообщений. Она 0-валентна, если все решающие продолжения дают 0, 1-валентна для 1 и бивалентна, если достижимы оба исхода.

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

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

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

Не диагноз для любого инцидента

Существование одного плохого выполнения не означает, что оно обычно. Практические системы решают, потому что конкретная сеть ведёт себя лучше худшего случая или архитектура вводит дополнительные предпосылки. FLP отменяет безусловную гарантию, а не успешную работу.

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

Цена прогресса — явная предпосылка

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

Детекторы отказов Чандры и Туэга добавляют источник сведений с заданными полнотой и точностью. Они не выводят смерть из тишины. Рандомизированные протоколы, включая раннюю работу Бен-Ора, меняют детерминированность и дают вероятностную формулировку завершения.

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

Совместный результат и метод Линч

Линч вспоминала, что они с Фишером начали работу в 1982 году, а затем к доказательству присоединился Патерсон. Сохранение тройного авторства важно для точности: известный результат возник из совместной работы.

Зрелая система публикует предел отказов, свойства часов и детектора, приоритет безопасности и условия ожидаемой живости. FLP не запрещает строить консенсус. Он запрещает скрывать зависимость гарантии от мира, в котором она обещана.

Источники