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

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

Чтобы установить второе требование корректности протокола, должно быть показано, что каждое принимаемое слово имеет больший индекс (в inp), чем ранее принятое слово. Обозначим индекс самого последнего доставленного слова через pr (для удобства запишем, что изначально
pr =-1 and Ut[-1] = -¥ ). Определим утверждение P2 как:

P2º P1

/\ <data,s,i,w,r> Î Mq Þ Ut[B+i] > r -m (14)

/\ i1 £ i2 < B + High Þ Ut[i1] £ Ut[i2] (15)

/\ cr Þ Rt ³ Ut[pr] + m (16)

/\ pr < B + High /\ ( Ut[pr] > -m Þ cr) (17)

/\ cr Þ B + Exp = pr + 1 (18)

Ëåììà 3.13 P2 - инвариант протокола, основанного на таймере.

Äîêàçàòåëüñòâî. Изначально Mq пусто, B + High равно нулю, Øcr выполняется, и
Ut[pr] < -m, откуда следуют (14)-(18).

Ap: (15) сохраняется, т.к. каждое новое принятое слово получает значение таймера U, что из (3) по крайней мере равно значениям таймеров ранее принятых слов.

Sp: (14) сохраняется, т.к. Ut[B +i] > 0 и пакет отправляется с r=m .

Cp: (14), (16) и (18) сохраняются, т.к. из (5) è (6) их посылки ложны, когда Cp применимо. (15) сохраняется, т.к. B принимает значение B + High è таймеры не меняются. (17) сохраняется, т.к. B присваивается значение B + High è pr è cr не меняются.

Rq: (16) сохраняется, т.к. когда Rt устанавливается в R (при принятии слова) Ut[pr] £ U из (3), è R³ 2m+U. (17) сохраняется, т.к. pr < B+High, что следует из (8), è cr становится true. (18) сохраняется, т.к. Exp устанавливается в i +1 è pr в B + i, откуда следует, что (18) становится true.

Time: (14) сохраняется, т.к. Ut[B + i] è r уменьшаются на одно и то же число (è выведение пакета только делает ложной посылку). (15) сохраняется, т.к. Ut[i1] è Ut[i2] уменьшаются на одну и туже величину. (16) сохраняется, т.к. cr не становится истинным в этом действии, è Rt è Ut[pr] уменьшаются на одну и ту же величину. (17) сохраняется, т.к. его заключение становится ложным только, если Rt становится £ 0, откуда следует (по (16)), что Ut[pr] становится < -m. (18) сохраняется, т.к., если cr не обратился в false, B, Exp è pr не меняются.

Действия Rp, Ep, è Sq, не меняют никакие переменные в (14)-(18). Loss è Dupl сохраняют (14)-(18) исходя из тех же соображений, что и в предыдущих доказательствах. ð

Ëåììà 3.14 Из P2 следует, что

< data, s,i1,w,r> Î Mq Þ (cr \/ B+i1 > pr).

Äîêàçàòåëüñòâî. По (14), из <data,s,i1,w, r> Î Mq следует Ut[B+i1] >r -m > -m.

Если B +i1 £ pr то, т.к. pr < B + High из (15), Ut[pr] > -m, так что из (17) cr true. ð

Òåîðåìà 3.15 (Упорядочение) Слова, доставляемые q появляются в строго возрастающем порядке в массиве inp.

Äîêàçàòåëüñòâî. Предположим q получает пакет <data, s,i1,w,r > è доставляет w. Если перед получением не было соединения, B + i1 > pr (по Ëåììе 3.14), так что слова w располагается в inp после позиции pr. Если соединение было, i1 = Exp, значит B+i1 = B+Exp = pr+1 из (18), откуда следует, что w = inp[pr+1]. ð

3.2.3 Обсуждение протокола

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

Качество протокола. Требования Нет потерь è Упорядочение являются свойствами безопасности, è они позволяют получить чрезвычайно простое решение, а именно протокол, который не посылает или получает никакие пакеты, и объявляет каждое слово потерянным. Само собой разумеется, что такой протокол, который не дает никакой транспортировки данных от отправителя к приемнику, не является очень "хорошим" решением.

Хорошие решения проблемы не только удовлетворяют требованиям Нет потерь и Упорядочение, но также объявляют потерянными как можно меньше слов. Для этой цели, протокол этого раздела может быть расширен механизмом, который посылает каждое слово неоднократно (пока не конец посылки интервала), пока не получит подтверждение. Интервал посылки должен быть достаточно длинным, чтобы можно было повторить передачу некоторого слова несколько раз, и чтобы вероятность, что слово потеряется, стала очень маленькой.

На стороне приемника предусмотрен механизм, который вызывает посылку подтверждения всякий раз, когда пакет доставлен или получен при открытом соединении.

Ограниченные порядковые номера. Порядковые номера, используемые в протоколе, могут быть ограничены, если получить для протокола результат, аналогичный Ëåììе 3.9 для сбалансированного протокола скользящего окна [Tel91b, Section 3.2]. Для этого нужно предположить, что скорость принятия слов (процессом p) ограничена следующим образом: слово может быть принято только если первое из предыдущих слов имеет возраст по крайней мере U + 2m+ R единиц времени. Для этого нужно к действию Ap добавить сторож

{(High < L) V ( Ut[B + High - L] <-R -2m)}.

Учитывая это предположение, можно показать, что порядковые номера принимаемых пакетов лежат в 2L-окрестности вокруг Exp, è порядковые номера подтверждений - в L-окрестности вокруг High. Следовательно, можно передавать порядковые номера modulo 2L.

Форма действий и инвариант. Благодаря использованию утверждений, рассуждения относительно протокола связи уменьшены до (большого) манипулирования формулами. Манипулирование формулами - "безопасная" методика потому, что каждый шаг может быть проверен в очень подробно, так что возможность сделать ошибку в рассуждениях мала. Но есть риск, что читатель может потеряет идею протокола и его отношение к рассматриваемым формулам. Проблемы проектирования протокола могут быть поняты и с прагматической, и с формальной точки зрения. Fletcher и Watson [FW78] утверждают, что упрафляющая информация должна быть "защищена" в том смысле, что ее значение не должно измененяться потерей или дублированием пакетов; это - прагматическая точка зрения. При использовании в проверке утверждений, "значение" информации управления отражено в выборе специфических утверждений в качестве инвариантов. Выбор этих инвариантов и проектирование переходов, сохраняющих их, составляет формальную точку зрения. Действительно, как будет показано, наблюдение Fletcher и Watson может быть вновь показано в терминах "формы" формул, которые могут или не могут быть выбран как инварианты протокола, устойчивые к потере и дублированию пакетов.

Time-e: { d > 0}

begin (* Таймеры в p уменьшаются на d ' *)

d ' := ... ; (* £ d ' £ d ´ (1 + e) *)