Быстрый поиск

Реферат: Распределенные алгоритмы

P º "i < sp : outp[i]¹ udef (0p)

/\ "i < sq, : outq[i] ¹ udef (0q)

/\ < pack, w, i > Î Qp Þ w = inq[i] /\ (i < sq + lq) (lp)

/\ < pack, w, i > Î Qq Þ w = inp[i] /\ (i < sp + lp) (lq)

/\ outp[i]¹ udef Þ outp[i] = inq[i] /\ (ap > i— lq) (2p)

/\ outq[i]¹ udef Þ outq[i] = inp[i] /\ (aq > i— lp) (2q)

/\ ap £ sq, (3p)

/\ aq £ sp (3q)

Лемма 3.1 P - инвариант Алгоритма 3.1.

Доказательство. В любой начальной конфигурации Qp и Qq - пустые, для всех i, outp[i] и outq[i] равны udef, и ap,ap, sp и sq равны нулю 0; из этого следует, что P=true. Перемещения протокола рассмотрим с точки зрения сохранения значения P. Во-первых, заметим, что значения inp и inq, никогда не меняются.

Sp: Чтобы показать, что Sp сохраняет (0p), заметим, что Sp не увеличивает sp и не делает ни один из outp[i] равным udef.

Чтобы показать, что Sp сохраняет (0q), заметим, что Sp не увеличивает sq, и не делает ни один из outq[i] равным udef.

Чтобы показать, что Sp сохраняет (1p), заметим, что Sp не добавляет пакеты в Qp и не уменьшает sp.

Чтобы показать, что Sp сохраняет (lq), заметим Sp добавляет < pack, w, i > в Qp с w = inp[i] и i < sp + lp, и не изменяет значение sp.

Чтобы показать, что Sp сохраняет (2p) и (2q), заметим, что Sp не изменяет значения outp, outq, ap, или aq.

Чтобы показать, что Sp сохраняет (3p) и (3q), заметим, что Sp не меняет значения ap , ap , sq , или sp.

Rp: Чтобы показать, что Rp сохраняет (0p), заметим, что Rp не делает ни одно outp[i] равным udef, и если он перевычисляет sp, то оно впоследствии также удовлетворяет (0p).

Чтобы показать, что Rp сохраняет (0q), заметим, что Rp не меняет outq или sq.

Чтобы показать, что Rp сохраняет (lp), заметим, что Rp не добавляет пакеты в Qp и не уменьшает sq.

Чтобы показать, что Rp сохраняет (lq), заметим, что Rp не добавляет пакеты в Qq и не уменьшает sp.

Чтобы показать, что Rp сохраняет (2p), заметим, что Rp изменяет значение outp[i] на w при принятии < pack, w,i>. Т.к. Qp содержала этот пакет до того, как выполнился Rp, из (1p) следует, что w = inp[i]. Присваивание ap:= max (ap, i— lq+1) гарантирует, что ap > i— lq сохраняется после выполнения. Чтобы показать, что Rp сохраняет (2q), заметим, что Rp не меняет значения outq или aq.

Чтобы показать, что Rp сохраняет (3p), заметим, что когда Rp присваивает
ap:= max(ap, i— lq+1) (при принятии <pack, w,i>), из (lp) следует, что i < sq+lq, следовательно ap £ sq сохраняется после присваивания. Rp не меняет sq. Чтобы показать, что Rp сохраняет (3q), заметим, что sp может быть увеличен только при выполнении Rp.

Lp : Чтобы показать, что Lp сохраняет (0p), (0q), (2p), (2q), (3p), и (3q), достаточно заметить, что Lp не меняет состояния процессов. (lp) и (lq) сохраняются потому, что Lp только удаляет пакеты (а не порождает или искажает их).

Процессы Sq, Rq, и Lq сохраняют P , что следует из симметрии. ð

3.1.2 Доказательство правильности протокола

Сейчас будет продемонстрировано, что Алгоритм 3.1 гарантирует безопасную и окончательную доставку. Безопасность следует из инварианта, как показано в Теореме 3.2, а живость продемонстрировать труднее.

Теорема 3.2 Алгоритм 3.1 удовлетворяет требованию безопасной доставки.

Доказательство. Из (0p) и (2p) следует, что outp[0..sp —1] =inq[0..sp—1], а из (0q) и (2q) следует outp[0..Sq -1] = inp[0..Sq -1].ð

Чтобы доказать живость протокола, необходимо сделать справедливых предположений и предположение относительно lp и lq. Без этих предположений протокол не удовлетворяет свойству живости, что может быть показано следующим образом. Неотрицательные константы lp и lq еще не определены; если их выбрать равными нулю, начальная конфигурация протокола окажется тупиковой. Поэтому предполагается, что lp + lq > 0.

Конфигурация протокола может быть обозначена g = (cp, cq, Qp, Qq), где cp и cq - состояния p и q. Пусть g будет конфигурацией, в которой применим Sp (для некоторого i). Пусть

d = Sp(g) = (cp, cq, Qp, (Qq È {m})),
и отметим, что действие Lq применимо в d. Если Lq удаляет m, Lq(d) = g. Отношение Lq(Sp(g)) = g äàåò íà÷àëî íåîãðàíè÷åííûì âû÷èñëåíèÿì, â êîòîðûõ íè sp , ни sq не уменьшаются.

Протокол удовлетворяет требованию «окончательной доставки», если удовлетворяются два следующих справедливых предположения.

Fl. Если посылка пакета возможна в течение бесконечно долгого временно, пакет посылается бесконечно часто.

F2. Если один и тот же пакет посылается бесконечно часто, то он принимается бесконечно часто.

Предположение Fl гарантирует, что пакет посылается снова и снова, если не получено подтверждение; F2 исключает вычисления, подобные описанному выше, когда повторная передача никогда не принимается.

Ни один из двух процессов не может быть намного впереди другого: разница между sp и sq остается ограниченной. Поэтому протокол называется сбалансированным, а также из этого следует, что если требование окончательной доставки удовлетворяется для sp, тогда оно также удовлетворяется для sq, и наоборот. Понятно, что протокол не следует использовать в ситуации, когда один процесс имеет намного больше слов для пересылки, чем другой.

Ëåììà 3.3 Из P следует sp— lq £ ap £ sq £ aq+ lp £ sp + lp.

Äîêàçàòåëüñòâî. Из (0p) и (2p) следует sp— lq£ ap, из (3p) следует ap£ sp . Из (0q) и (2q) следует sp £ ap + lp . Из (3q) следует ap + lp £ sp + lp .ð

Òåîðåìà 3.4 Àëãîðèòì 3.1 удовлетворяет требованию окончательной доставки.

Äîêàçàòåëüñòâî. Сначала будет продемонстрировано, что в протоколе невозможны тупики. Из инварианта следует, что один из двух процессов может послать пакет, содержащий слово с номером, меньшим, чем ожидается другим процессом.

Утверждение 3.5 Из P следует, что посылка < pack, in[sq], sq> процессом p или посылка
< pack, inq[sp], sp ) процессом q возможна.

Äîêàçàòåëüñòâî. Т.к. lp + lq > 0, хотя бы одно из неравенств Ëåììы 3.3 строгое, т.е.,

sq < sp + lp \/ sp < sq+lq.

Из P также следует ap £ sq (3p) и aq £ sp (3q), а также следует, что

(ap £ sq<sp+lp) \/ (aq £ sp<sq+lq)

это значит, что Sp применим с i = sq или Sq применим с i = sp. ð

Теперь мы можем показать, что в каждом из вычислений sp и sq увеличиваются бесконечно часто. Согласно Утверждению 3.5 протокол не имеет терминальных конфигураций, следовательно каждое вычисление неограниченно. Пусть C - вычисление, в котором sp и sq увеличиваются ограниченное число раз, и пусть sp and sq - максимальные значения, которые эти переменные принимают в C. Согласно утверждению, посылка <pack, inp[sq], sq> процессом p или посылка <pack, in q[sp], sp > процессом q применима всегда после того, как sp, sq, ap и aq достигли своих окончательных значений. Таким образом, согласно Fl, один из этих пакетов посылается бесконечно часто, и согласно F2, он принимается бесконечно часто. Но, т.к. принятие пакета с порядковым номером sp процессом p приводит к увеличению sp (и наоборот для q), это противоречит допущению, что ни sp, ни sq не увеличиваются более. Таким образом Òåîðåìà 3.4 доказана. ð