Реферат: Распределенные алгоритмы
Ù VF ¹ Æ Þ F is a forest (4)
Ù (statep = passive A scp = 0) Þ p Ï Vp (5)
Ù emptyp Û Tp is empty (6)
Lemma 8.6 Q - инвариант Shavit-Francez алгоритма.
Доказательство. Первоначально statep = passive для каждого не-инициатора p, и fatherp = p для каждого инициатора p, что доказывает (1). Также, Ep = Æ, что доказывает (2). Так как scp = 0 для каждого p, (3) удовлетворяется. VF = {p : p -инициатор} и EF = Æ, так что F - лес, состоящий из деревьев, содержащих один узел для каждого инициатора, что доказывает (4). Процессы в VF - инициаторы, которые являются активными; это доказывает (5). Первоначально emptyp равны (p - не-инициатор) и Tp действительно пуст, тогда и только тогда, когда p - не инициатор, что доказывает (6).
Sp: Никакой процесс не становится активным в Sp, и никакой процесс не удаляется из VF, таким образом (1) сохраняется.
Применимость действия означает, что p, отец нового узла, находится в VF, таким образом (2) сохраняется.
В результате действия, VF пополняется вершиной (mes, p) и EF ребром ((mes, p), p), что означает, что F остается лесом, и scp правильно увеличивается на единицу, чтобы представить наличие нового сына процесса p, таким образом (3) и (4) сохраняются.
Никакой процесс не становится пассивным листом, и никакой процесс не вставляется в VF, таким образом (5) сохраняется.
Поскольку новый лист добавлен в не-пустое дерево, никакое дерево не становится непустым, и поскольку ни одна переменная empty не изменяется, (6) сохраняется.
Rp: p уже был в VF (fatherp ¹ udef) или p вставлен после действия, таким образом (1) сохраняется.
Если значение fatherp определено, его новое значение - q, и если послан сигнал, его отец также q, и q находится в VT , таким образом (2) сохраняется.
Число сыновей процесса q не изменяется, потому что сын (mes, q) процесса q заменяется сыном p или сыном (sig, q), таким образом scq оставляет правильным (3).
Структура графа не изменяется, таким образом (4) сохраняется. Никакой процесс не становится пассивным листом, и никакой процесс не вставляется в VF, таким образом (5) сохраняется.
Никакое дерево не становится пустым, следовательно (6) сохраняется.
Ip: Перевод p в пассивное состояние сохраняет (1), (2), (3), и (4). То, что p прежде был активен означает, что p был в VF. Если scp = 0, p удаляется из VF, таким образом (5) сохраняется.
Затем мы рассмотрим что случится, если p удалить из F, то есть если p окажется, пассивным листом F. Если послан сигнал, отец сигнала - последний отец процесса p, который находится в VF, следовательно (2) сохраняется. В этом случае, сигнал заменяет p на сына процесса fatherp , следовательно scfather p остается правильным, и (3) сохраняется. Структура графа не изменилась, следовательно (4) сохраняется. Никакое дерево не становится пустым, таким образом (6) сохраняется. Иначе, то есть, если fatherp = p, p был корнем и то, что p является листом означает, что p единственная иуршина в Tp ,таким образом ее удаление делает Tp пустым и присваивание emptyp сохраняет (6).
var statep : (active, passive) init if p is initiator then active else passive ;
scp : integer init 0 ;
fatherp : P init if p is initiator then p else udef ;
emptyp : boolean init if p is initiator then false else true ;
begin send (mes, p) ; scp := scp + 1 end
Rp: { Сообщение (mes, q) пришло в p }
begin receive (mes, q) ; statep := active ;
if fatherp = udef then fatherp := q else send ( sig, q ) to q
end
if scp = 0 then (* Delete p from F *)
begin if fatherp = p then emptyp := true else send ( sig, fatherp } to fatherp ;
fatherp := udef
end
end
Ap: { Сигнал (sig,p) пришел в p }
begin receive (sig,p) ; scp := scp - 1;
if scp = 0 and statep = passive then
begin if fatherp = p then emptyp := true else send ( sig, fatherp ) to fatherp ;
fatherp := udef
end
end
Процессы одновременно выполняют волновой алгоритм, в котором посылка или принятие решения процессом p разрешается только, если emptyp истина и тогда decide вызывает алгоритм объявления .
Алгоритм 8.4 shavit-francez алгоритм.
Ap: получение сигнала уменьшает число сыновей процесса p на единицу, и присваивание scp гарантирует, что (3) сохраняется. То, что p был отцом сигнала означает, что p был в VF. Если statep=passive и после получение сигнала scp = 0, p удаляется, таким образом (5) сохраняется.
Если p удаляется из VF, инвариант сохраняется по тем же причинам, что и при действии Ip.
Теорема 8.7 Алгоритм Shavit-Francez (Алгоритм 8.4) - правильный алгоритм обнаружения завершения и использует М + W управляющих сообщени.
Доказательство. Также как в Теореме 8.5 можно показано, что число сигналов не превышает число основных сообщений. Помимо сигналов, управляющий алгоритм только посылает сообщения для одной волны. Из этого следует, что послано не более М + W управляющих сообщений.
Чтобы доказать живость алгоритма предположим, что основное вычисление закончилось. За конечное число шагов алгоритм обнаружения завершения достигает конечной конфигурации, и можно показать, как это было сделано в Теореме 8.5, что в этой конфигурации F пуст. Следовательно, все события волны возможны в каждом процессе, и то, что конфигурация является конечной теперь означает, что все события волны были выполнены, включая по крайней мере одно принятие решения, при котором был вызван алгоритм объявления.
Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105
