Оптимальность интервальной маршрутизации: специальные топологии. 1 глава

End

 

L p: {< pack,w,i>ÎQ _p }

begin Q_p:= Q_p \ {< pack, w,i > } end

 

Алгоритм 3.1 Протокол скользящего окна (для p).

Инвариант протокола. Подсистема связи представляется двумя очередями, Q_p для пакетов с адресатом p и Q_q, для пакетов с адресатом q. Заметим, что перевычисление s_p в R _p никогда не дает значение меньше предыдущего, поэтому s_p никогда не уменьшается. Чтобы показать, что этот алгоритм удовлетворяет данным ранее требованиям, сначала покажем, что утверждение P - инвариант. (В этом и других утверждениях i - натуральное число.)

P º " i < s _p: out_p[i] ¹ udef                           (0p)

/\ " i < s _q,: out_q[i] ¹ udef                                 (0q)

/\ < pack, w, i > Î Q_p Þ   w = in_q[i] /\ (i < s_q + l_q)       (lp)

/\ < pack, w, i > Î Q_q Þ   w = in_p[i] /\ (i < s_p + l_p)       (lq)

/\ out_p[i] ¹ udef Þ out_p[i] = in_q[i] /\ (a_p > i— l_q) (2p)

/\ out_q[i] ¹ udef Þ out_q[i] = in_p[i] /\ (a_q > i— l_p) (2q)

/\ a_p £ s_q,                                              (3p)

/\ a_q £ s_p                                                            (3q)

 

Лемма 3.1 P - инвариант Алгоритма 3.1.

Доказательство. В любой начальной конфигурации Q_p и Q_q - пустые, для всех i, out_p[i] и out_q[i] равны udef, и a_p,a_p, s_p и s_q равны нулю 0; из этого следует, что P=true. Перемещения протокола рассмотрим с точки зрения сохранения значения P. Во-первых, заметим, что значения in_p и in_q, никогда не меняются.

S _p: Чтобы показать, что S _p сохраняет (0p), заметим, что S _p не увеличивает s_p и не делает ни один из out_p[i] равным udef.

Чтобы показать, что S _p сохраняет (0q), заметим, что S _p не увеличивает s_q, и не  делает ни один из out_q[i] равным udef.

Чтобы показать, что S _p сохраняет (1p), заметим, что S _p не добавляет пакеты в Q_p и не уменьшает s_p.

Чтобы показать, что S _p сохраняет (lq), заметим S _p добавляет < pack, w, i > в Q_p с w = in_p[i] и i < s_p + l_p, и не изменяет значение s_p.

Чтобы показать, что S _p сохраняет (2p) и (2q), заметим, что S _p не изменяет значения out_p, out_q, a_p, или a_q.

Чтобы показать, что S _p сохраняет (3p) и (3q), заметим, что S _p не меняет значения a_p , a_p , s_q , или s_p.

R p: Чтобы показать, что R _p сохраняет (0p), заметим, что R _p не делает ни одно out_p[i] равным udef, и если он перевычисляет s_p, то оно впоследствии также удовлетворяет (0p).

Чтобы показать, что R _p сохраняет (0q), заметим, что R _p не меняет out_q или s_q.

Чтобы показать, что R _p сохраняет (lp), заметим, что R _p не добавляет пакеты в Q_p и не уменьшает s_q.

Чтобы показать, что R _p сохраняет (lq), заметим, что R _p не добавляет пакеты в Q_q и не уменьшает s_p.

Чтобы показать, что R _p сохраняет (2p), заметим, что R _p изменяет значение out_p[i] на w при принятии < pack, w,i>. Т.к. Q_p содержала этот пакет до того, как выполнился R _p, из (1p) следует, что w = in_p[i]. Присваивание a_p:= max (a_p, i— l_q+1) гарантирует, что a_p > i— l_q сохраняется после выполнения. Чтобы показать, что R _p сохраняет (2q), заметим, что R _p не меняет значения out_q или a_q.

Чтобы показать, что R _p сохраняет (3p), заметим, что когда R _p присваивает
a_p:= max(a_p, i— l_q+1) (при принятии <pack, w,i>), из (lp) следует, что i < s_q+l_q, следовательно a_p £ s_q сохраняется после присваивания. R _p не меняет s_q. Чтобы показать, что R _p сохраняет (3q), заметим, что s_p может быть увеличен только при выполнении R _p.

L _p: Чтобы показать, что L _p сохраняет (0p), (0q), (2p), (2q), (3p), и (3q), достаточно заметить, что L _p не меняет состояния процессов. (lp) и (lq) сохраняются потому, что L _p только удаляет пакеты (а не порождает или искажает их).

Процессы S _q, R _q, и L _q сохраняют P, что следует из симметрии.                 ð

3.1.2 Доказательство правильности протокола

Сейчас будет продемонстрировано, что Алгоритм 3.1 гарантирует безопасную и окончательную доставку. Безопасность следует из инварианта, как показано в Теореме 3.2, а живость продемонстрировать труднее.

Теорема 3.2 Алгоритм 3.1 удовлетворяет требованию безопасной доставки.

 

Доказательство. Из (0p) и (2p) следует, что out_p[0..s_p —1] =in_q[0..s_p—1], а из (0q) и (2q) следует out_p[0..Sq -1] = in_p[0..Sq -1].ð

 

Чтобы доказать живость протокола, необходимо сделать справедливых предположений и предположение относительно l _p и l _q. Без этих предположений протокол не удовлетворяет свойству живости, что может быть показано следующим образом. Неотрицательные константы l _p и l _q еще не определены; если их выбрать равными нулю, начальная конфигурация протокола окажется тупиковой. Поэтому предполагается, что l _p + l _q > 0.

Конфигурация протокола может быть обозначена g = (c _p, c _q, Q _p, Q _q), где c _p и c _q - состояния p и q. Пусть g будет конфигурацией, в которой применим S _p (для некоторого i). Пусть

d = S _p (g) = (c _p, c _q, Q _p, (Q _q È { m } )),
и отметим, что действие L _q применимо в d. Если L _q удаляет m, L _q (d) = g. Отношение L _q (S _p (g)) = g äàåò íà÷àëî íåîãðàíè÷åííûì âû÷èñëåíèÿì, â êîòîðûõ íè s _p, ни s _q не уменьшаются.

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

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

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

 

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

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

Ëåììà 3.3 Из P следует s _p— l _q £ a _p £ s _q £ a _q + l _p £ s _p + l _p.

Äîêàçàòåëüñòâî. Из (0p) и (2p) следует s _p — l _q £ a _p, из (3p) следует   a _p £ s _p. Из (0q) и (2q)  следует s _p £ a _p + l _p. Из (3q) следует a _p + l _p £ s _p + l _p. ð

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

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

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

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

s q < s p + l p \/ s p < s q+l q.

Из P также следует a p £ s q (3p) и a q £ s p (3q), а также следует, что

(a p £ s q<s p+l p) \/ (a q £ s p<s q+l q)

это значит, что S p применим с i = s q или S q применим с i = s p.   ð

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

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

 

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

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

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

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

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

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

 

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

                                  

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

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

 

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

 

Ëåììà 3.8 Утверждение P', определяемое как

P' º P

/\ < pack, w, i> is behind < pack, w', i'> in Q p Þ i > i' - L (4p)

/\ < pack, w, i> is behind < pack, w', i'> in Q q Þ i > i' - L (4q)

/\ < pack ,w,i> Î Q p Þ i ³ a p - l p                                        (5p)

/\ < pack ,w,i> Î Q q Þ i ³ a q - l q                                        (5q)

 

является инвариантом Àëãîðèòìа 3.1.

Äîêàçàòåëüñòâî. Т.к. уже было показано, что P - инвариант, мы можем ограничиться доказательством того, что (4p), (4q), (5p) и (5q) выполняются изначально и сохраняются при любом перемещении. Заметим, что в начальном состоянии очереди пусты, следовательно (4p), (4q), (5p) и (5q) очевидно выполняются. Сейчас покажем, что перемещения сохраняют истинность этих утверждений.

S p: Чтобы показать, что S _p сохраняет (4p) и (5p), заметим, что S _p не добавляет пакетов в Q p и не меняет a p.

Чтобы показать, что S _p сохраняет (5q), заметим, что если S _p добавляет пакет < pack, w, i> в Q_q, то i ³ a p, откуда следует, что i ³   a q - l q (из Ëåììы 3.3).

Чтобы показать, что S _p сохраняет (4q), заметим, что если < pack, w', i'> в Q_q,тогда из (lq)
i' < s p + l p, следовательно, если S _p добавляет пакет < pack, w, i> с i ³ a p, то из Леммы 3.3 следует i' < a p+L £ i+L.

R p: Чтобы показать, что R _p сохраняет (4p) and (4q), заметим, что Rp не добавляет пакеты в Q p или Q q.

 Чтобы показать, что R _p сохраняет (5p), заметим, что когда a p увеличивается (при принятии < pack, w', i'>) до i' - l q + 1, тогда для любого из оставшихся пакетов < pack, w, i> в Q p мы имеем i > i' - L (из 4р). Значит неравенство i ³ a p - l p сохраняется после увеличения a p.

Чтобы показать, что R _p сохраняет (5q), заметим, что  R p не меняет Q q  и a q.

L p: Действие L p не добавляет пакетов в Q p или Q q, и не меняет значения a p или a q; значит оно сохраняет (4p), (4q), (5p) и (5q).

Из симметрии протокола следует, что S q, R q и L q тоже сохраняет P'. ð

                                                      

Ëåììà 3.9 Из P' следует, что

<pack, w,i> Î Q p Þ s p -L £ i< s p +L

и

  <pack, w,i> Î Q q Þ s q -L £ i< s q +L.

Äîêàçàòåëüñòâî. Пусть <pack, w,i > Î Q p. Из (lp), i < s q + l q, и из Ëåììы 3.3 i < s p + L. Из (5p), i ³ a p — l p, и из Ëåììы 3.3 i ³ s p— L. Утверждение относительно пакетов в Q q доказывается так же. ð

Согласно Ëåììе достаточно посылать пакеты с порядковыми номерами modulo k, где
k ³ 2L. В самом деле, имея s p и i mod k, p может вычислить i.

Выбор параметров. Значения констант l p и l q сильно влияют на эффективность протокола. Их влияние на пропускную способность протокола анализируется в [Sch91, Chapter 2]. Оптимальные значения зависят от числа системно зависимых параметров, таких как

время связи, т.е., время между двумя последовательными операциями процесса,

время задержки на обмен, т.е., среднее время на передачу пакета от p к q и получение ответа от q к p,

вероятность ошибки, вероятность того, что конкретный пакет потерян.

 

Протокол, чередующий бит. Интересный случай протокола скользящего окна получается, когда L = 1, ò.å., l p = 1 и l q = 0 (или наоборот). Переменные a p и a q, инициализируется значениями -l p и -l q, а не 0. Можно показать, что a p + l q = s p и a q + l p = s q всегда выполняется, значит только одно a p и s p (и a q и s q) нужно хранить в протоколе. Хорошо известный протокол, чередующий бит [Lyn68] получается, если использование таймеров дополнительно ограничивается, чтобы гарантировать, что станции посылают сообщения в ответ.

 

3.2 Протокол, основанный на таймере

Теперь мы изучим роль таймеров в проектировании и проверке протоколов связи, анализируя упрощенную форму Dt-протокола Флэтчера и Уотсона (Fletcher и Watson) для сквозной передачи сообщений. Этот протокол был предложен в [FW78], но (несколько упрощенный) подход этого раздела взят из [Tel91b, Раздел 3.2]. Этот протокол обеспечивает не только механизм для передачи данных (как сбалансированный протокол скользящего окна Раздела 3.1), но также открытие и закрытие соединений. Он устойчив к потерям, дублированию и переупорядочению сообщений.

Информация о состоянии (передачи данных) протокола хранится в структуре данных, называемой запись соединения. (В Подразделе 3.2.1 будет показано, какая информация хранится в записи соединения). Запись соединения может быть создана и удалена для открытия и открытия соединения. Òàêèì îáðàçîì, ãîâîðÿò, ÷òî ñîåäèíåíèå îòêðûòî (на одной из станций), если существует запись соединения.

Чтобы сконцентрироваться на релевантных аспектах протокола (а именно, на механизме управления соединением и роли таймеров в этом механизме), будем рассматривать упрощенную версию протокола. Более практические и эффективные расширения протокола могут быть найдены [FW78] и [Tel91b, Раздел 3.2]. В протоколе, описанном здесь, сделаны следующие упрощения.

One direction. Подразумевается, что данные передаются в одном направлении, скажем от p к q. Иногда будем называть p отправителем, а q - адресатом (приемником). Однако, следует отметить, что протокол использует сообщения подтверждения, которые посылаются в обратном направлении, т.е. от q к p.

Обычно данные нужно передавать в двух направлениях. Чтобы предусмотреть подобную ситуацию, дополнительно выполняется второй протокол, в котором p и q поменяны ролями. Тогда можно ввести комбинированные data/ack (данные/подтверждения) сообщения, содержащие как данные (с соответствующим порядковым номером), так и информацию, содержащуюся в пакете подтверждения протокола, основанного на таймере.

Окно приема из одного слова. Приемник не хранит пакеты данных с номером, более высоким, чем тот, который он ожидает. Только если следующий пакет, который прибудет - ожидаемый, он принимается во внимание и немедленно принимается. Более интеллектуальные версии протокола хранили бы прибывающие пакеты с более высоким порядковым номером и принимали бы их после того, как прибыли и были приняты пакеты с меньшими порядковыми номерами.

Предположения, упрощающие синхронизацию. Протокол рассмотрен с использованием минимального числа таймеров. Например, предполагается, что подтверждение может быть послано процессом-получателем в любое время, пока соединение открыто со стороны приемника. Также возможен случай, когда подтверждение может быть послано только в течение определенного интервала времени, но это сделало бы протокол более сложным.

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

Однословные пакеты. Отправитель может помещать только одиночное слово в каждый пакет данных. Протокол был бы более эффективным, если бы пакеты данных могли содержать блоки последовательных слов.

Протокол основан на таймере, то есть процессы имеют доступ к физическим часовым устройствам. По отношению ко времени и таймерам в системе сделаны следующие предположения.

Глобальное время. Глобальная мера времени простирается над всеми процессами системы, то есть каждое событие происходит в некоторое время. Предполагается, что каждое событие имеет продолжительность 0, и время, в которое происходит событие, не доступно процессам.

Ограниченное время жизни пакета. Время жизни пакета ограничено константой m (максимальное время жизни пакета). Òàêèì îáðàçîì, если пакет посылается во время s и принимается во время t, то

s < t < s + m.

Если пакет дублируется в канале, каждая копия должна быть принята в течение промежутка времени m после отправления оригинала (или стать потерянной).

Таймеры. Процессы не могут наблюдать абсолютное время своих действий, но они имеют доступ к таймерам. Таймер - действительная переменная процесса, чье значение непрерывно уменьшается со временем (если только ей явно не присваивают значение). Точнее, если Xt - таймер, мы обозначаем его значение в момент времени t как Xt(t) и если Xt между t₁ and t₂ не присвоено иное значение, то

Xt^{(t 1)}-Xt^{(t 2)}=t₂-t₁.

Заметим, что эти таймеры работают так: в течение времени d они уменьшаются точно на d. В Подразделе 3.2.3 мы обсудим случай, когда таймеры страдают отклонением.

Входные слова для отправителя моделируются, как в Разделе 3.1, неограниченным массивом in_p. Снова этот массив не полностью хранится в p; p в каждый момент времени имеет доступ только к его части. Часть in_p, к которой p имеет доступ расширяется (в сторону увеличения индексов), êîãäà p получает следующее слово от процесса, который их генерирует. Эту операцию будем называть как принятие слова отправителем.

Предыдущая12345678910111213141516Следующая

Поделиться:

Воспользуйтесь поиском по сайту: