2016 Алгоритм Раны_ инвариант и корректность (подробное решение), страница 2

При этом tok от любой другой волны в процессе s будет в пункте 5.3.3 иметь меньшую метку, и потому волна будет прерываться (не произойдёт события решения и пересылки токена (нарушение 2-го пункта из свойств волнового алгоритма, а значит волновой алгоритм не завершится))

Всё это строилось на допущении, что алгоритм посылки tok - это волновой алгоритм, однако это

1. сказано, согласно формулировке алгоритма Раны.

2. можно доказать по сформулированным процедурам, процедуры идентичны (за исключением строки 5.3.3? прокомментированной выше, а часы Лемпорта в процедуре на условие посылки токена не влияют (они просто обновляются и посылаются)) процедурам кольцевого алгоритма, его формулировка и доказательство см. лекция 7.

Таким образом, волновой алгоритм с максимальным по времени токеном завершится, т.к. он начнётся через конечное число шагов, после выполнения условия term (это доказано выше) + конечное число шагов выполнения волнового алгоритма (согласно его 1-му свойству), т.е. decide (Announce) - произойдёт обязательно и через конечное число шагов.

(A)

Если выполнен term (т.е. базовый алгоритм таки завершился, то согласно доказательству (B) Announce обязательно произойдёт, причём через конечное число шагов).

Осталось доказать, что Announce переводит все процессы в конечное состояние, для этого докажем, что в каждом процессе произойдёт событие решения halt этого алгоритма.

Начальный процесс s выполняет процедуру Announce, это приводит к тому, что он посылает сообщение stop всем своим соседям, каждый сосед получив это сообщение повторяет эту процедуру и посылает сообщение stop всем своим соседям. Так как граф связный, то найдётся путь от начальной вершины s до любой другой вершины p, и по этому пути будут посланы сообщения stop от одного процесса к другому процессу, однако если у одной из вершин q на этом пути произошло выполнение halt, то она больше не обрабатывает приходящие сообщения и следовательно не перешлёт stop, тем самым цепочка s -1-> q -> p нарушена, однако если в процессе q произошёл halt, то это значит, что она хоть раз приняла сообщение stop и сразу после этого, но перед halt выполнила Announce разослав stop своим соседям, таким образом существовала цепочка s -2-> q по которой распространилось сообщение stop а значит есть цепочка s -2-> q -> p от исходной вершины s до любой другой вершины p.

(рассуждения приведены для случая, если halt в цепочке случился только в одной вершине, однако аналогичным образом они распространяются и на k вершин (если в цепочке у k вершин случился halt, то есть пусть распространения stop до последней вершины, в которой случился halt, а оттуда путь до p))

Итак stop распространится по всем вершинам, это значит, что для любой вершины p все её соседи рано или поздно получат stop и выполнят Announce прислав вершине p сообщения stop, но тогда переменная RecStop из алгоритма будет после последнего stop == #In, а значит будет выполнена операция halt.

Таким образом, если Выполнен term, то через конечное количество шагов выполнится Announce, а Announce за конечное количество шагов (потому что каждый процесс может принять не более #In сообщений, после чего он выключится через halt) переведёт каждый процесс в конечное состояние.

(С)

Announce - является событием decide для волнового алгоритма используемого в алгоритме Раны в процессе s (причём в конкретно нашем случае - циклического волнового алгоритма). Это означает, что согласно пункту 3 волновых алгоритмов, в каждом процессе, ему предшествовало хотя бы одно событие связанное с этим алгоритмом (5.3.3.1), т.е. это процедура I (для процесса инициатора это ещё могла быть процедура A), т.е. для каждого процесса было выполнено условие 5.3.3 и 5.3, т.е. каждый процесс находился в состоянии quiet в момент передачи tok.

Пойдём от противного - допустим term не выполнен, в момент decide волнового алгоритма, это значит, что либо один из процессов active, либо было послано mes в канал, но mes послал кто-то - это процесс, который выполнил процедуру S, т.е. был active, причём это случилось в момент decide - т.е. после передачи tok этой волны, возьмём первый процесс из тех, которые передали tok, а после этого стали active, т.е. перестали удовлетворять quiet, этот процесс p - мог стать active только в результате получения сообщения mes в процедуру R (нету другого кода, меняющего состояние на active), однако это сообщение послал другой процесс q, и он ещё не передавал tok (т.к. если он уже передал tok, а после этого послал сообщение, т.е. стал active, то вместе с сообщением он послал своё времечко, => θp >= θq +1 => p - не самый первый процесс, который стал active после передачи tok, противоречие).

Таким образом p - первый процесс нарушитель передал tok процесса инициатора s с временем qt_s потом получил сообщение mes от процесса q с временем θq > θ, и отправил ему ack с временем θ > θq и θ > qt_s,процесс q, получив ack обновит своё время на новое θ+1, и т.к. он не находился в состоянии quiet, рано или поздно перейдёт в состояние quiet (ведь только в этом состоянии можно передать tok, который согласно утверждению, что decide случился и волновой алгоритм завершился, - должен быть передан по свойству волнового алгоритма), однако при переходе в quiet qt_q >= θ+1 > qt_s, что приводит к невыполнению условия 5.3.3 и глушит волну.

Это противоречит тому, что волна закончилась => исходное предположение ложь, и term выполнен в момент decide волнового алгоритма.

всё, что нужно было доказать - доказали

ч.т.д.

8/8