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

Rp: Действие Rp не меняет никаких переменных из P0, и удаление пакета сохраняет (4) и (7).

Ep: Действие Ep не меняет никаких переменных из P0.

Cp: Действие Cp делает равным false заключения (5), (6) и (7), но ((2), (5), (6) и (7)) применимы только когда их посылки ложны. Cp также меняет значение B, но, т.к. пакетов для передачи нет, (по (5) и (7)), (8) сохраняется.

Rq: (2) сохраняется, т.к. Rt всегда присваивается значение R (если присваивается). (6) сохраняется, т.к. Rt устанавливается только в R только при принятии пакета <data, s,i,w,r>, è из (4) и (5) следует  cs Ù St ³ R + m когда это происходит.

Sq: (4) сохраняется, т.к. каждый пакет посылается с оставшимся временем жизни, равным m. (7) сохраняется, т.к. пакет < ack,i,r > посылается с r = m когда cr истинно, так что из (2) и (6)   St > m.

Loss: (4), (5), (7) и (8) сохраняются, т.к. удаление пакета может фальсифицировать только их посылку.

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

Time: (1), (2) и (3) сохраняются, т.к. St, Rt, и Ut[i] может только уменьшаться, и соединение приемника закрывается, когда Rt становится равным 0. (4) сохраняются, т.к. r может только уменьшиться, и пакет удаляется, когда его r-поле достигает значения 0. Заметим, что Time уменьшает все таймеры (включая r-поле пакета) на одну и ту же величину, значит сохраняет все утверждения вида Xt > Yt +C, где Xt и Yt -таймеры, и C - константа. Это показывает, что (5), (6) и (7) сохраняются.           ð

Первое требование к протоколу в том, что каждое слово в конце концов доставляется или объявляется потерянным. Определим предикат 0k(i) как

0k(i) ó error [i] = true \/ q доставил inp [i].

Сейчас может быть показано, что протокол не теряет никаких слов, не объявляя об этом. Определим утверждение P1 как

P1º   P0

/\ Ø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: 0k(i)                  (13)

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

Äîêàçàòåëüñòâî. Сначала заметим, что как только 0k(i) стало true для некоторого i, он никогда больше не становится false. Сначала нет соединения, нет пакетов, и B = 0, откуда следует, что P1 выполняется.

Ap: Действие Ap может открыть соединение, но при этом сохраняется (10), т.к. соединение открывается с Low = 0 и "i < B : 0k(i) выполняется из (9).

Sp: Действие Sp может послать пакет < data, s, I, w, r >, но т.к. s истинно только при I = Low, то это сохраняет (11) из (10).

Rp: Значение Low может быть увеличено, если принят пакет < ack, I, r >. Тем не менее, (10) сохраняется, т.к. из (13) "i < B + I : 0k(i) выполняется, если получено это подтверждение.

Ep: Значение Low может быть увеличено, когда применяется действие Ep, но генерация сообщения об ошибке гарантирует, что (10) сохраняется.

Cp: Действие Cp обращает cs в false, но оно применимо только если St < 0 и Low == High. Из (10) следует, что "i < B+ High : 0k(i) выполняется прежде выполнения Cp, следовательно (9) сохраняется. Посылка (10) обращается в false в этом действии, и из (5), (6) и (7) следует, что посылки (11), (12) и (13) ложны; следовательно (10), (11), (12) и (13) сохраняются.

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

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.

Было замечено, что Time сохраняет утверждения специальной формы Xt ³ Yt + C потому, что таймеры обеих частей неравенства уменьшаются на в точности одинаковую величину, è из
Xt ³ Yt + C следует (Xt - d) ³ ( Yt - d) + C. Такое жн наблюдение может быть сделано для Time-e. Для действительных чисел Xt, Yt, d, d ', d", r, è c, удовлетворяющих d > 0 è r > 1, из

(Xt ³ r2 Yt + c) /\ ( £ d '£ d ´ r) /\  ( £ d ''£ d ´ r)

следует

(Xt-d ')³ r2(Yt- d") + c.

Следовательно, Time-e сохраняет утверждение формы

Xt ³ (1 + e)2 Yt + c.

Теперь протокол может быть адаптирован к работе с отклоняющимися таймерами, если соответствующим образом изменить инварианты. Для того, чтобы другие действия тоже сохраняли измененные инварианты, константы R è S протокола должны удовлетворять

R ³ (1 + e)((1 + e)U + (I + e)2) è S ³ (1 + e)(2m + (1 + e)R).

Исключая измененные константы, протокол остается таким же. Его инвариант приведен на Ðèñóíêе 3.9.

Òåîðåìà 3.16 P2'- инвариант протокола, основанного на таймере с e-ограниченным отклонением таймера. Протокол удовлетворяет требованиям Нет потерь и Упорядочение.

Упражнения к главе 3

Раздел 3.1

Óïðàæíåíèå 3.1 Покажите, что сбалансированный протокол скользящего окна не удовлетворяет требованию окончательной доставки, если из предположений Fl è FS, выполняется только F2.

Óïðàæíåíèå 3.2 Докажите, что если L = 1 в сбалансированном протоколе скользящего окна è ap è aq, инициализируются значениями -lq è -lp, то всегда верно ap+lq = sp è aq+lp = sq.

Страницы: 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