(1) Свойство безопасности. В каждой достижимой конфигурации протокола
outp[0..sp — 1] = inq[0..Sp — 1] и outq[0..sq — 1] = inp [0...sq — 1].
(2) Окончательная доставка. Для каждого целого k ³ 0, конфигурации с sp ³ k и
sq³ k когда-либо достигаются.
Протоколы передачи обычно полагаются на использование сообщений подтверждения. Сообщение подтверждения посылается процессом получения, чтобы сообщить отправителю о данных, которые он получил корректно. Если отправитель данных не получает подтверждение, то он предполагает, что данные (или подтверждение) потеряно, и повторно передает те же самые данные. В протоколе этого раздела, однако, не используются явные сообщения подтверждения. В этом протоколе обе станции имеют сообщения, которые нужно послать другой станции; сообщения станции служат также подтверждениями для сообщений другой станции.
Сообщения, которыми обмениваются процессы, называют пакетами, и они имеют форму
< pack, w, i >, где w - слово данных, а i - натуральное число (называемое порядковым номером пакета). Этот пакет, посылаемый процессом p (к q), передает слово = inp[i] для q, но также, как было отмечено, подтверждает получение некоторого количества пакетов от q. Процесс p может быть «впереди» q не более, чем на lp пакетов, если мы потребуем, что пакет данных < pack, w, i >, посланный p, подтверждает получение слов с номерами 0.. i— lp от q. (q посылает аналогичные пакеты.) Константы lp и lq неотрицательны и известны обоим процессам p и q. Использование пакета данных в качестве подтверждения имеет два последствия для протокола:
(1) Процесс p может послать слово inp[i] (в виде пакета < pack, inp[i], i >) только после того, как запишет все слова от outp[0] до outp[i — lp], т. е. , если i < sp + lp.
(2) Когда p принимает < pack, w,i>, повторная передача слов с inp[0] до inp[i — lq] уже не нужна.
Объяснение псевдокода. После выбора модели нетрудно разработать код протокола; см. Алгоритм 3.1. Для процесса p введена переменная ap (и aq для q), в которой хранится самое первое слово, для которого p (или q, соответственно) еще не получил подтверждение..
В Алгоритме 3.1 действие Sp - посылка i-го слова процессом p, действие Rp - принятие слова процессом p, и действие Lp - потеря пакета с местом назначения p. Процесс p может послать любое слово, индекс которого попадает в указанные ранее границы. Когда сообщение принято, в первую очередь делается проверка - было ли идентичное сообщение принято ранее (на случай повторной передачи). Если нет, слово, содержащееся в нем, записывается в выход, и ap и sp корректируются. Также вводятся действия Sq, Rq и Lq , где p и q поменяны ролями.
var sp, ap : integer init 0, 0 ;
inp : array of word (* Посылаемые данные *) ;
outp: array of word init udef, udef, ...',
Sp: {ap £ i < Sp+lp}
begin send < pack,inp[i],i> to q end
Rp: { < pack, w, i > ÎQp }
begin receive <pack, w, i> ;
if outp[i] = udef then
begin outp[i] := w ;
ap := max(ap,i-lp+1) ;
Sp := min{j|outp[j]= udef}
end
(* else игнорируем, пакет передавался повторно *)
end
Lp: {<pack,w,i>ÎQp}
begin Qp:= Qp\ {<pack,w,i>} end
Алгоритм 3.1 Протокол скользящего окна (для p).
Инвариант протокола. Подсистема связи представляется двумя очередями, Qp для пакетов с адресатом p и Qq, для пакетов с адресатом q. Заметим, что перевычисление sp в Rp никогда не дает значение меньше предыдущего, поэтому sp никогда не уменьшается. Чтобы показать, что этот алгоритм удовлетворяет данным ранее требованиям, сначала покажем, что утверждение P - инвариант. (В этом и других утверждениях i - натуральное число.)
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 не уменьшаются.