Ëåììà 3.8 Утверждение P', определяемое как
P' º P
/\ <pack, w, i> is behind <pack, w', i'> in Qp Þ i > i' - L (4p)
/\ <pack, w, i> is behind <pack, w', i'> in Qq Þ i > i' - L (4q)
/\ <pack,w,i> ÎQp Þ i³ ap - lp (5p)
/\ <pack,w,i> ÎQq Þ i³ aq - lq (5q)
является инвариантом Àëãîðèòìа 3.1.
Äîêàçàòåëüñòâî. Т.к. уже было показано, что P - инвариант, мы можем ограничиться доказательством того, что (4p), (4q), (5p) и (5q) выполняются изначально и сохраняются при любом перемещении. Заметим, что в начальном состоянии очереди пусты, следовательно (4p), (4q), (5p) и (5q) очевидно выполняются. Сейчас покажем, что перемещения сохраняют истинность этих утверждений.
Sp: Чтобы показать, что Sp сохраняет (4p) и (5p), заметим, что Sp не добавляет пакетов в Qp и не меняет ap.
Чтобы показать, что Sp сохраняет (5q), заметим, что если Sp добавляет пакет <pack, w, i> в Qq, то i ³ ap, откуда следует, что i³ aq - lq (из Ëåììы 3.3).
Чтобы показать, что Sp сохраняет (4q), заметим, что если < pack, w', i'> в Qq, тогда из (lq) i' < sp + lp, следовательно, если Sp добавляет пакет < pack, w, i> с i ³ ap, то из Леммы 3.3 следует i' < ap+L £ i+L.
Rp: Чтобы показать, что Rp сохраняет (4p) and (4q), заметим, что Rp не добавляет пакеты в Qp или Qq.
Чтобы показать, что Rp сохраняет (5p), заметим, что когда ap увеличивается (при принятии <pack, w', i'>) до i' - lq +1, тогда для любого из оставшихся пакетов <pack, w, i> в Qp мы имеем i > i' - L (из 4р). Значит неравенство i ³ ap - lp сохраняется после увеличения ap.
Чтобы показать, что Rp сохраняет (5q), заметим, что Rp не меняет Qq и aq.
Lp: Действие Lp не добавляет пакетов в Qp или Qq, и не меняет значения ap или aq; значит оно сохраняет (4p), (4q), (5p) и (5q).
Из симметрии протокола следует, что Sq, Rq и Lq тоже сохраняет P'. ð
Ëåììà 3.9 Из P' следует, что
<pack, w,i>Î Qp Þ sp -L£ i< sp +L
и
<pack, w,i>Î Qq Þ sq -L£ i< sq +L.
Äîêàçàòåëüñòâî. Пусть <pack, w,i> Î Qp. Из (lp), i < sq + lq, и из Ëåììы 3.3 i < sp + L. Из (5p), i ³ ap— lp, и из Ëåììы 3.3 i ³ sp— L. Утверждение относительно пакетов в Qq доказывается так же. ð
Согласно Ëåììе достаточно посылать пакеты с порядковыми номерами modulo k, где k ³ 2L. В самом деле, имея sp и i mod k, p может вычислить i.
Выбор параметров. Значения констант lp и lq сильно влияют на эффективность протокола. Их влияние на пропускную способность протокола анализируется в [Sch91, Chapter 2]. Оптимальные значения зависят от числа системно зависимых параметров, таких как
время связи, т.е., время между двумя последовательными операциями процесса,
время задержки на обмен, т.е., среднее время на передачу пакета от p к q и получение ответа от q к p,
вероятность ошибки, вероятность того, что конкретный пакет потерян.
Протокол, чередующий бит. Интересный случай протокола скользящего окна получается, когда L = 1, ò.å., lp = 1 и lq= 0 (или наоборот). Переменные ap и aq, инициализируется значениями -lp и -lq, а не 0. Можно показать, что ap + lq = sp и aq + lp = sq всегда выполняется, значит только одно ap и sp (и aq и sq) нужно хранить в протоколе. Хорошо известный протокол, чередующий бит [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 между t1 and t2 не присвоено иное значение, то
Страницы: 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