Теорема Фишера-Линча-Патерсона (FLP) — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 9: Строка 9:
 
Если разрешаем недетерминизм, то есть [[алгоритм Бен-Ора]].
 
Если разрешаем недетерминизм, то есть [[алгоритм Бен-Ора]].
  
−
* TODO: доказательство из презентации Елизарова.
+
== Доказательство ==
−
* Инфо: http://bailonga.es/tpmtp/lecture09.pdf + презентация Р.Елизарова
+
Из презентации Р. Елизарова.
−
* Инфо: https://github.com/volhovm/study-notes/blob/master/parallel_programming/parallel_programming.org
+
 
 +
От противного: пусть есть такой алгоритм, тогда мы проанализируем варианты его исполнения, подстроим порядок доставки сообщений (без откладывания сообщений бесконечно далеко) и получим противоречие с нетривиальностью консенсуса.
 +
 
 +
=== Модель ===
 +
{{Определение
 +
|definition=
 +
'''Процесс''' — это детерминированный автомат, который может выполнять три операции:
 +
* <code>receive() : msg</code> — бесконечная блокировка до получения ближайшего сообщения. Так как система асинхронна, возможности "посмотреть следующее сообщение" или ''таймаутов нет''.
 +
* <code>send(msg)</code> — отправка сообщения другому процессу. Гарантируется, что сообщение дойдёт получателю за конечное время, но это время может быть сколь угодно большим.
 +
* <code>decided(value)</code> — процесс принял решение <code>value</code>. Решение процесс может принять только один раз, но после этого он ''может продолжить выполняться'' и помогать остальным процессам.
 +
Заметим, что так как нет "времени", можно считать все переходы в процессе мгновенными.
 +
}}
 +
Для доказательства от противного у нас есть такой алгоритм для процессов, что все они вызывают <code>decided(value)</code> с одинаковым значением через конечное время, независимо от того, как система задерживает сообщения.
 +
{{Определение
 +
|definition=
 +
'''Конфигурация''' — это состояния всех процессов плюс все сообщения в пути (которые отправили, но ещё не доставили).
 +
}}
 +
В начальной конфигурация у каждого процесса может быть сколько угодно входных данных и даже своя программа.
 +
{{Определение
 +
|definition=
 +
'''Шаг''' из одной конфигурации в другую — это либо приём какого-то сообщения процессом (событие), либо внутренние действия процесса между соседними <code>receive()</code>. Эти действия ''однозначно'' определяются предыдущей конфигурацией и событием.
 +
}}
 +
{{Определение
 +
|definition=
 +
'''Исполнение''' — это ''бесконечная'' цепочка шагов из начальной конфигурации. Бесконечная, потому что процессы могут выполняться и после принятия решений.
 +
}}
 +
{{Определение
 +
|definition=
 +
'''Отказавший процесс''' — это процесс, который делает только конечное количество шагов в исполнении. Такой в системе может быть максимум один (это более сильное условие, чем если может много процессов отказывать).
 +
}}
 +
 
 +
Также гарантируется, что в любом исполнении любое сообщение, предназначенное не отказавшему процессу, обрабатывается через конечное число шагов.
 +
Другими словами, ''сообщения не теряются''.
 +
 
 +
== Ссылки ==
 +
* http://bailonga.es/tpmtp/lecture09.pdf  
 +
* https://github.com/volhovm/study-notes/blob/master/parallel_programming/parallel_programming.org

Версия 16:03, 3 июня 2019

Теорема Фишера, Линча и Патерсона (FLP, 1985 год) невозможно достичь даже необоснованного консенсуса $N>2$ процессами даже на одном бите при следующих условиях:

  • Алгоритм должен завершиться за конечное время.
  • Один из узлов может отказать
  • Система асинхронна
  • Алгоритм должен быть детерминирован.

Если отказов нет, есть простой алгоритм. Если система синхронна, то есть консенсус в синхронных системах. Если разрешаем недетерминизм, то есть алгоритм Бен-Ора.

Доказательство

Из презентации Р. Елизарова.

От противного: пусть есть такой алгоритм, тогда мы проанализируем варианты его исполнения, подстроим порядок доставки сообщений (без откладывания сообщений бесконечно далеко) и получим противоречие с нетривиальностью консенсуса.

Модель

Определение:
Процесс — это детерминированный автомат, который может выполнять три операции:
  • receive() : msg — бесконечная блокировка до получения ближайшего сообщения. Так как система асинхронна, возможности "посмотреть следующее сообщение" или таймаутов нет.
  • send(msg) — отправка сообщения другому процессу. Гарантируется, что сообщение дойдёт получателю за конечное время, но это время может быть сколь угодно большим.
  • decided(value) — процесс принял решение value. Решение процесс может принять только один раз, но после этого он может продолжить выполняться и помогать остальным процессам.
Заметим, что так как нет "времени", можно считать все переходы в процессе мгновенными.

Для доказательства от противного у нас есть такой алгоритм для процессов, что все они вызывают decided(value) с одинаковым значением через конечное время, независимо от того, как система задерживает сообщения.

Определение:
Конфигурация — это состояния всех процессов плюс все сообщения в пути (которые отправили, но ещё не доставили).

В начальной конфигурация у каждого процесса может быть сколько угодно входных данных и даже своя программа.

Определение:
Шаг из одной конфигурации в другую — это либо приём какого-то сообщения процессом (событие), либо внутренние действия процесса между соседними receive(). Эти действия однозначно определяются предыдущей конфигурацией и событием.


Определение:
Исполнение — это бесконечная цепочка шагов из начальной конфигурации. Бесконечная, потому что процессы могут выполняться и после принятия решений.


Определение:
Отказавший процесс — это процесс, который делает только конечное количество шагов в исполнении. Такой в системе может быть максимум один (это более сильное условие, чем если может много процессов отказывать).


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

Ссылки

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Теорема_Фишера-Линча-Патерсона_(FLP)&oldid=71469»