Сейчас будет продемонстрировано, что Алгоритм 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 не уменьшаются.

Протокол удовлетворяет требованию «окончательной доставки», если удовлетворяются два следующих справедливых предположения.

Fl. Если посылка пакета возможна в течение бесконечно долгого временно, пакет посылается бесконечно часто.

F2. Если один и тот же пакет посылается бесконечно часто, то он принимается бесконечно часто.

Предположение Fl гарантирует, что пакет посылается снова и снова, если не получено подтверждение; F2 исключает вычисления, подобные описанному выше, когда повторная передача никогда не принимается.

Ни один из двух процессов не может быть намного впереди другого: разница между sp и sq остается ограниченной. Поэтому протокол называется сбалансированным, а также из этого следует, что если требование окончательной доставки удовлетворяется для sp, тогда оно также удовлетворяется для sq, и наоборот. Понятно, что протокол не следует использовать в ситуации, когда один процесс имеет намного больше слов для пересылки, чем другой.

Ëåììà 3.3 Из P следует sp— lq £ ap £ sq £ aq+ lp £ sp + lp.

Äîêàçàòåëüñòâî. Из (0p) и (2p) следует sp— lq£ ap, из (3p) следует  ap£ sp . Из (0q) и (2q)       следует sp £ ap + lp . Из (3q) следует ap + lp £ sp + lp .ð

Òåîðåìà 3.4  Àëãîðèòì 3.1 удовлетворяет требованию окончательной доставки.

Äîêàçàòåëüñòâî. Сначала будет продемонстрировано, что в протоколе невозможны тупики. Из инварианта следует, что один из двух процессов может послать пакет, содержащий слово с номером, меньшим, чем ожидается другим процессом.

Утверждение 3.5 Из P следует, что посылка < pack, in[sq], sq> процессом p или посылка
< pack, inq[sp], sp ) процессом  q возможна.

Äîêàçàòåëüñòâî. Т.к. lp + lq > 0, хотя бы одно из неравенств Ëåììы 3.3 строгое, т.е.,

sq < sp + lp   \/   sp < sq+lq.

Из P также следует ap £ sq (3p) и aq £ sp (3q), а также следует, что

(ap £ sq<sp+lp) \/ (aq £ sp<sq+lq)

это значит, что Sp применим с i = sq или Sq применим с i = sp.       ð

Теперь мы можем показать, что в каждом из вычислений sp и sq увеличиваются бесконечно часто. Согласно Утверждению 3.5 протокол не имеет терминальных конфигураций, следовательно каждое вычисление неограниченно. Пусть C - вычисление, в котором sp и sq увеличиваются ограниченное число раз, и пусть sp and sq - максимальные значения, которые эти переменные принимают в C. Согласно утверждению, посылка <pack, inp[sq], sq> процессом p или посылка <pack, in q[sp], sp > процессом q применима всегда после того, как sp, sq, ap и aq достигли своих окончательных значений. Таким образом, согласно Fl, один из этих пакетов посылается бесконечно часто, и согласно F2, он принимается бесконечно часто. Но, т.к. принятие пакета с порядковым номером sp процессом p приводит к увеличению sp (и наоборот для q), это противоречит допущению, что ни sp, ни sq  не увеличиваются более. Таким образом Òåîðåìà 3.4 доказана.                                                              ð

Мы завершаем этот подраздел кратким обсуждением предположений Fl и F2. F2-ìèíèìàëüíîå требование, которому должен удовлетворять канал, соединяющий p и q, для того, чтобы он мог передавать данные. Очевидно, если некоторое слово inp[i] никогда не проходит через канал, то невозможно достичь окончательной доставки слова. Предположение Fl обычно реализуется в протоколе с помощью условия превышения времени: если ap не увеличилось в течение определенного промежутка времени, inp[ap] передается опять. Как уже было отмечено во введении в эту главу, для этого протокола безопасная доставка может быть доказана без принятия во внимания проблем времени (тайминга).

3.1.3 Обсуждение протокола

Ограничение памяти в процессах. Àëãîðèòì 3.1 не годится для реализации в компьютерной сети, т.к. в каждом процессе хранится бесконечное количество информации (массивы in и out) и т.к. он использует неограниченные порядковые номера. Сейчас будет показано, что достаточно хранить только ограниченное число слов в каждый момент времени. Пусть L = lp + lq.

Ëåììà 3.6 Из P следует, что отправление < pack, w,i> процессом p применимо только для i < ap+L.

Äîêàçàòåëüñòâî. Сторож Sp требует i < sp+lp, значит согласно Ëåììе 3.3 i < ap+L.   ð                                                     

Ëåììà 3.7 Из P следует, что если outp[i]¹ udef, то i < sp + L.

Äîêàçàòåëüñòâî. Из (2p), ap > i— lq, значит i < ap + lq, и i < sp + L (из Ëåììы 3.3). ð 

Ðèñóíîê 3.2 Скользящие окна протокола.

Последствия этих двух лемм отображены на Ðèñóíêе 3.2. Процессу p необходимо хранить только слова inp[ap..sp + lp — 1] потому, что это слова, которые p может послать. Назовем их как  посылаемое окно  p (представлено как S на Ðèñóíêе 3.2). Каждый раз, когда ap увеличивается, p отбрасывает слова, которые больше не попадают в посылаемое окно (они представлены как A на Ðèñóíêе 3.2). Каждый раз, когда sp увеличивается, p считывает следующее слово из посылаемого окна от источника, который производит слова. Согласно Ëåììе 3.6, посылаемое окно процесса p содержит не более L слов.

Подобным же образом можно ограничить память для хранения процессом p массива outp. Т.к. outp[i] не меняется для i < sp, можно предположить, что p выводит эти слова окончательно и более не хранит их (они представлены как W на Ðèñóíêе 3.2). Т.к. outp[i] = udef для всех i ³ sp + L, эти значения outp[i] также не нужно хранить. Подмассив outp[sp..sp +L—1] назовем принимаемое окно p. Принимаемое окно представлено на Ðèñóíêе 3.2 как u для неозначенных слов и R для слов, которые были приняты. Только слова, которые попадают в это окно, хранятся процессом. Леммы 3.6 и 3.7 показывают, что не более 2L слов хранятся процессом в любой момент времени.

Ограничение чисел последовательности. В заключение будет показано, что числа последовательности могут быть ограничены, если используются fifo-каналы. При использовании fifo предположения можно показать, что номер порядковый номер пакета, который получен процессом p  всегда внутри 2L-окрестности sp. Обратите внимание, что fifo предположение используется первый раз.

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