Два процесса связи обозначаются как p и q. Предположения, требования и протокол абсолютно симметричны. Вход p состоит из информации, которую он должен послать q, и моделируется неограниченным массивом слов inp. Выход p состоит из информации, которую он получает от q, и также моделируется неограниченным массивом слов, outp. Предполагается, что p имеет случайный доступ по чтению к inp и случайный доступ по записи к outp. Первоначально значение outp[i] не определено и представлено как udef для всех i. Вход и выход процесса q моделируется массивами inq и outq соответственно. Эти массивы нумеруются натуральными числами, т.е. они начинаются со слова с номером 0. В подразделе 3.1.3 будет показано, что произвольный доступ может быть ограничен доступом к "окну" конечной длины, передвигающемуся вдоль массива. Поэтому протокол называется протоколом «скользящего окна».
Процесс p содержит переменную sp, показывающую наименьшее нумерованное слово, которое p все еще ожидает от q. Таким образом, в любой момент времени, p уже записал слова от outp[0] до outp[sp - 1]. Значение sp никогда не уменьшается. Аналогично q содержит переменную sq. Теперь могут быть установлены требуемые свойства протокола. Свойство безопасности говорит о том, что каждый процесс передает только корректные данные; свойство живости говорит о том, что все данные когда-либо будут доставлены.
(1) Свойство безопасности. В каждой достижимой конфигурации протокола
outp[0..sp — 1] = inq[0..Sp — 1] и outq[0..sq — 1] = inp [0...sq — 1].
(2) Окончательная доставка. Для каждого целого k ³ 0, конфигурации с sp ³ k и sq ³ k когда-либо достигаются.
3.1.1 Представление протокола
Протоколы передачи обычно полагаются на использование сообщений подтверждения. Сообщение подтверждения посылается процессом получения, чтобы сообщить отправителю о данных, которые он получил корректно. Если отправитель данных не получает подтверждение, то он предполагает, что данные (или подтверждение) потеряно, и повторно передает те же самые данные. В протоколе этого раздела, однако, не используются явные сообщения подтверждения. В этом протоколе обе станции имеют сообщения, которые нужно послать другой станции; сообщения станции служат также подтверждениями для сообщений другой станции.
Сообщения, которыми обмениваются процессы, называют пакетами, и они имеют форму < 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 := minoutp[j]= udef
end
(* else игнорируем, пакет передавался повторно *)
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 Доказательство правильности протокола
Страницы: 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, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90
