292
правки
Изменения
→Шаг 3: разбор случаев
==== Шаг 3: разбор случаев ====
Теперь у нас, помимо конфигурации $C$ и события $e$, есть некоторое событие $e'$ и конфигурации $C_0$ и $C_1$, причём:
* $e(C_0)=D_0$ является 0-валентной, а $e(C_1)=D_1$ является 1-валентной (или наоборот, повторим доказательство)
* $e'(C_0)=C_1$
Разберём два случая, в зависимости от того, одному процессу приходят $e$ и $e'$ или разным.
===== Разным =====
Пусть $proc(e)\neq proc(e')$ (т.е. эти события в разных процессах).
Тогда нам всё равно, в каком порядке их обрабатывать, т.е. $e'(e(C_0))=e(e'(C_0))=e(C_1)=D_1$:
[[Файл:Distributed-flp-proof-case1.png|300px]]
Мы знаем, что $D_1$ является 1-валентной. Но так как они достижима из $D_0$, то она также является и 0-валентной, противоречие.
===== Одному =====
Пусть $proc(e) = proc(e') = p$ (т.е. это два сообщения одному и тому же процессу).
Тогда рассмотрим цепочку шагов $\sigma$ от состояния $C_0$, в которой процесс $p$ вообще отказал вместо обработки сообщений.
Тогда остальные процессы в этой цепочке пришли к какому-то решению в конфигурации $A=\sigma(C_0)$.
Тогда эта конфигурация должна быть либо 0-, либо 1-валентной (в ней уже принято решение).
[[Файл:Distributed-flp-proof-case2.png|400px]]
Но теперь мы можем сказать, что процесс $p$ не отказал, а просто очень долго работал и теперь получает событие $e$.
Так как $\sigma$ не обращается к $p$, то $E_0=e(\sigma(C_0)=\sigma(e(C_0))=\sigma(D_0)$ — конфигурация, достижимая из 0-валентной, т.е. тоже 0-валентная.
С другой стороны, можно аналогично сказать, что процесс $p$ теперь получает сообщение $e'$, а за ним — сообщение $e$.
Тогда получается $E_1=e(e'(\sigma(C_0))$.
Из-за коммутативности получаем $E_1=\sigma(e(e'(C_0)))=\sigma(e(C_1))=\sigma(D_1)$ — конфигурация, достижимая из 1-валентной, т.е. тоже 1-валентная.
Таким образом получаем, что из $A$ достижимы и 0-валентная, и 1-валентная конфигурация, противоречие.
== Ссылки ==
* http://bailonga.es/tpmtp/lecture09.pdf
* https://github.com/volhovm/study-notes/blob/master/parallel_programming/parallel_programming.org
