Изменения

== Доказательство ==Из презентации Р. Елизарова. От противного: пусть есть такой алгоритм, тогда мы проанализируем варианты его исполнения, подстроим порядок доставки сообщений (без откладывания сообщений бесконечно далеко) и получим противоречие с нетривиальностью консенсуса. === Модель ==={{Определение|definition='''Процесс''' — это детерминированный автомат, который может выполнять три операции:* TODO<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