Действия 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.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)2m) (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)2Yt + 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.1 Покажите, что сбалансированный протокол скользящего окна не удовлетворяет требованию окончательной доставки, если из предположений Fl è FS, выполняется только F2.