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

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

Rq: Сначала рассмотрим случай, когда q принимает < data, true,l,w,r> при не существующем соединении (cr - false). Тогда "i < B+I : 0k(i) из (11), и w доставляется в действии. Т.к.
w = inp[B+I] из (8), присваивание Exp := I + 1 сохраняет (12).

Теперь рассмотрим случай, когда Exp увеличивается в результате принятия
< data, s,Exp,w,r> при открытом соединении. Из (12), "i < B + Exp : 0k(i) выполнялось перед принятием, и слово w = Wp[B + Exp] доставляется действием, следовательно приращение Exp сохраняет (12).

Sq: Отправление <ack, Exp, m> сохраняет (13) из (12).

Loss: Выполнение Loss может только фальсифицировать посылки предложений.

Dupl: Введение пакета m возможно только если посылка соответствующего предложения (и, следовательно, заключение) была истинна еще до введения.

Time: Таймеры не упоминались явно в (9)-(13). Выведение пакета или закрытие процессом q может только фальсифицировать посылки (11), (12) или (13).ð

Теперь может быть доказана первая часть спецификации протокола, но после дополнительного предположения. Без этого предположения отправитель может быть чрезвычайно ленивым в объявлении слов возможно потерянными; в Àëãîðèòìе 3.4 указано только, что это сообщение может и не возникнуть в промежуток времени 2m + R после окончания интервала для отправления слова, но не указано, что оно вообще должно появиться. Итак, позвольте сделать дополнительное предположение, что действие Ep на самом выполниться процессом p и в течение разумного времени, а именно прежде, чем Ut[B + Low] = —2m —R—l.

Òåîðåìà 3.12 (Нет потерь) Каждое слово inp доставляется q или объявляется p как возможно потерянное в течение U+2m+R+l после принятия слова процессом p.

Äîêàçàòåëüñòâî. После принятия слова inp[I], B+High > I начинает выполняться. Если соединение закрывается в течение указанного периода после принятия слова inp[I], то B > I, и результат следует из (9). Если соединение не закрывается в этот промежуток времени и B + Low £ I, отчет обо всех словах из промежутка B + Low..I возможен ко времени 2m + R после окончания интервала отправления inp[I]. Из этого следует, что этот отчет имел место 2m + R +l после окончания интервала отправления, ò.å., U+ 2m +R+l после принятия. Из этого также следует I < B+ Low, и, значит, слово было доставлено или объявлено (из (10)). ð

Чтобы установить второе требование корректности протокола, должно быть показано, что каждое принимаемое слово имеет больший индекс (в 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) *)

forall i do Ut[i] := Ut[i] - d ' ;

St := St - d ' ;

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

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

Rt := Rt - d " ;

if Rt < 0 then delete (Rt, Exp) ;

(* r -поле передается явно *)

forall (..,r) Î Mp, Mq do

begin r := r - d,

if r < 0 then remove packet

end

Àëãîðèòì 3.8 Измененное действие Time.

Все инвариантные предложения P2 относительно пакетов имеют форму

"m Î M : A(m)

è в самом деле легко видеть, что подобное предложение сохраняется при дублировании и потере пакетов. В дальнейших главах мы увидим инварианты в более общей форме, например

èëè

условие Þ $m Î M : A(m).

Утверждения, имеющие этй форму могут быть фальсифицированы потерей или дублированием пакетов, è следовательно не могут использоваться в дîêàçàòåëüñòâе корректности Àëãîðèòìов, которые должны допускать подобные дефекты.

Подобные же наблюдения применимы к форме инвариантов в действии Time. Уже было отмечено, что это действие сохраняет все утверждения формы Xt ³ Yt + C,

где Xt è Yt -таймеры è C -константа.

P1¢ = cs Þ St£ S (1¢)

/\ cr Þ 0 < Rt £ R (2')

/\ "i < B + High : Ut[i] < U (3')

/\ " <.., r > Î Mp, Mq : 0 < r £m (4')

/\ <data, s, i, w, r >Î M, Þ cs /\ St ³ (1+e)(r+ m+(1+e)R) (5')

/\ crÞ cs /\ St ³ (l+e)((i+e)Rt+m) (6')

/\ < ack, i, r > Î Mp Þ cs /\ St > (1 + e)´r (7')

/\ <data, s, i, w, r > ÎMq, Þ (w = inp[B + i] /\ i < High) (8')

/\ Øcs Þ \/i < B: 0k(i) (9')

/\ cs Þ \/i < B + Low : 0k(i) (10')

/\<data,true,I,w, r)Î MqÞ"i<B+I: 0k(i) (11')

/\ cr Þ "i < B + Exp : 0k(i) (12')

/\ <ack,I, r >Î MpÞ"i <B+I: Ok(i) (13')

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

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

/\ cr Þ Rt ³ (1 + e)((l + e) Ut[pr] + (1 + e)2 m) (16')

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

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

Ðèñóíîê 3.9 инвариант протокола с отклонением таймеров.

Неаккуратные таймеры. Действие Time моделирует идеальные таймеры, которые уменьшаются точно на d в течение d единиц времени, на на практике таймеры страдают неточности, называемой отклонением. Это отклонение всегда предполагается e-ограниченным, ãäå e-известная константа, что означает, что в течение d единиц времени таймер уменьшается на величину d ', которая удовлетворяет d /(l + e) £ d' £ d ´ (1 + e). (Обычно e бывает порядка 10-5 или 10-6.) Такое поведение таймеров моделируется действием Time-e, приведенном в Àëãîðèòìе 3.8.