Предыдущая страница реферата | 16  17  18  19  20  21  22  23  24  25  26 | Следующая страница реферата

( = Sp(() = (cp, cq, Qp, (Qq ( {m})),

и отметим, что действие Lq применимо в (. Если Lq удаляет m, Lq(() = (.
Отношение Lq(Sp(()) = ( дает начало неограниченным вычислениям, в которых ни 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 i— lq, значит i Леммы 3.3). (

[pic]
Рисунок 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 предположение используется первый раз.

Лемма 3.8 Утверждение P', определяемое как
P' ( P
/ is behind in Qp ( i > i' - L (4p)
/ is behind in Qq ( i > i' - L (4q)
/ (Qp ( i( ap - lp (5p)
/ (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 добавляет пакет в 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' Rp: Чтобы показать, что Rp сохраняет (4p) and (4q), заметим, что Rp не добавляет пакеты в Qp или Qq.

Чтобы показать, что Rp сохраняет (5p), заметим, что когда ap увеличивается (при принятии ) до i' - lq +1, тогда для любого из оставшихся пакетов в 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' следует, что
( Qp ( sp -L( i< sp +L и
( Qq ( sq -L( i< sq +L.

Доказательство. Пусть ( 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 Протокол, основанный на таймере

Теперь мы изучим роль таймеров в проектировании и проверке протоколов связи, анализируя упрощенную форму (t-протокола Флэтчера и Уотсона
(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, и время, в которое происходит событие, не доступно процессам.
Ограниченное время жизни пакета. Время жизни пакета ограничено константой (
(максимальное время жизни пакета). Таким образом, если пакет посылается во время ( и принимается во время (, то

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

Xt(t1)-Xt(t2)=t2-t1.
Заметим, что эти таймеры работают так: в течение времени ( они уменьшаются точно на (. В Подразделе 3.2.3 мы обсудим случай, когда таймеры страдают отклонением.
Входные слова для отправителя моделируются, как в Разделе 3.1, неограниченным массивом inp. Снова этот массив не полностью хранится в p; p в каждый момент времени имеет доступ только к его части. Часть inp, к которой p имеет доступ расширяется (в сторону увеличения индексов), когда p получает следующее слово от процесса, который их генерирует. Эту операцию будем называть как принятие слова отправителем.
В этом разделе моделирование слов, принятых приемником, отлично от Раздела
3.1. Вместо того, чтобы записывать (бесконечный) массив, приемник передает слова процессу потребления операцией, называемой доставка слова. В идеале, каждое слово inp должно быть доставлено точно один раз, и слова должны быть доставлены в правильном порядке.
Спецификация протокола, однако, слабее, и причина в том, что протокол позволяется обрабатывать каждое слово inp только в течение ограниченного интервала времени. Не каждый протокол может гарантировать, что слово принимается за ограниченное время потому, что возможно, что все пакеты в это время потеряются. Следовательно, спецификация протокола учитывает возможность сообщенной потери, когда протокол отправителя генерирует отчет об ошибке, указывающий, что слово возможно потеряно. (Если после этого протокол более высокого уровня предлагает это слово p снова, то возможно дублирование; но мы не будем касаться этой проблемы здесь.) Свойства протокола, который будет доказан в Подразделе 3.2.2:
Нет потерь. Каждое слово inp доставляется процессом q или посылается отчет процессом p ("возможно потеряно" ) в течение ограниченного времени после принятия слова процессом p.
Упорядочение. Слова, доставляемые q принимаются в строго возрастающем порядке (так же, как они появляются в inp).

3.2.1 Представление Протокола

Соединение в протоколе открыто, если прежде не существовало никакого соединения и если (для отправителя) принято следующее слово или (для приемника) прибывает пакет, который может быть доставлен. Таким образом, в этом протоколе, чтобы открыть соединение нет необходимости обмениваться какими-либо сообщениями управления прежде, чем могут быть посланы пакеты данных. Это делает протокол относительно эффективным для прикладных программ, где в каждом соединении передаются только несколько слов
(маленькие пакеты связи). Предикат cs (или cr, соответственно) истинен, когда отправитель (или приемник, соответственно) имеет открытое соединение.
Это, обычно, не явная булева переменная отправителя (или приемника, соответственно); вместо этого открытое соединение определяется существованием записи соединения. Процесс проверяет, открыто ли соединение, пытаясь найти запись соединения в списке открытых соединений.
Когда отправитель открывает новое соединение, он начинает нумеровать принятые слова с 0. Количество уже принятых слов в данном соединении обозначается High, и количество слов, для которых уже было получено подтверждение обозначается через Low. Это подразумевает (аналогично протоколу Раздела 3.1), что отправитель может передавать пакеты с порядковыми номерами в диапазоне от Low до High —1, но есть здесь и своя особенность. Отправитель может посылать слово только в течение промежутка времени длиной U, начиная с того момента, когда отправитель принял слово.
Для этого с каждым словом inp[i] ассоциируется таймер Ut[i], он устанавливается в U в момент принятия, и должен быть положительным для передаваемого слова. Таким образом, посылаемое окно p состоит из тех слов с индексами Low ...High - 1, для которых ассоциированный с ними таймер положителен.
Сетевые константы:
( : real ; (* Максимальное время жизни пакета *)
Константы протокола:
U : real ; (* Длина интервала отправки *)
R : real ; (* Значение тийм-аута приемника: R( U+( *)
S : real ; (* Значение тайм-аута отправителя: S ( R + 2( *)
Запись соединения отправителя:
Low : integer ; (* Подтвержденные слова текущего соединения *)
High : integer ; (* Принятые слова текущего соединения *)
St : timer ; (* Таймер соединения *)
Запись соединения приемника:
Exp : integer ; (* Ожидаемый порядковый номер *)
Rt : timer ; (* Таймер соединения *)
Подсистема связи:
Mq : channel ; (* Пакеты данных для q *)
Mp : channel ; (* Пакеты подтверждения для p *)
Вспомогательные переменные:
B : integer init 0 ; (* Слова в предыдущем соединении *) cr : boolean init false ; (* Существование соединения для приемника
*) cs : boolean init false ; (*Существование соединения для отправителя *)

Рисунок 3.3 Переменные протокола, основанного на таймере.

Протокол посылает пакеты данных, состоящие из: бита (бит начала- последовательности; его значение будет обсуждаться позже), порядкового номера и слова. Для анализа протокола каждый пакет данных содержит четвертое поле, называемое оставшееся время жизни пакета. Оно показывает максимальное время, в течение которого пакет еще может находиться в канале до того, как он должен быть принят или стать потерянным согласно предположению об ограниченном времени жизни. В момент отправления оставшееся время жизни пакета всегда равно (. Пакеты подтверждения протокола состоят только из порядкового номера, ожидаемого процессом q, но опять для целей анализа каждое подтверждение содержит оставшееся время жизни пакета.

Ap: (* Принятие следующего слова *) begin if not cs then begin (* Сначала соединение открывается *) create (St, High, Low) ; (* cs := true *)
Low := High := 0 ; St := S end;
Ut[B + High] := U, High := High + 1 end

Sp: (* Отправление i-го слова текущего соединения *)
{ cs / Low ( i < High / Ut[B + i] > 0} begin send ;
St:=S end

Rp: (* Принятие подтверждения *)
{ cs / ( Mp } begin receive ; Low := max (Low, i) end

Ep: (* Генерация сообщения об ошибке для возможно потерянного слова *)
{cs / Ut[B + Low] ( -2( -R} begin error [B + Low] := true ; Low := Low + 1 end

Cp: (* Закрытие соединения *)
{cs / St < 0 / Low = High } begin B := B + High , delete (St, High, Low) end
(* cs := false *)

Алгоритм 3.4 Протокол отправителя.

Закрытие соединения контролируется таймерами, таймером St для отправителя и таймером Rt для приемника. Ограниченный интервал посылки каждого слова и ограниченное время жизни пакета приводят к тому, что каждое слово может быть найдено в каналах только лишь в течение интервала времени длиной ( +
U, начиная с момента принятия слова. Это позволяет приемнику отбрасывать информацию о конкретном слове через ( + U единиц времени после принятия слова; после этого не могут появиться дубликаты, следовательно не возможна повторная доставка. Таймер Rt устанавливается в R каждый раз, когда слово доставляется, константа R выбирается так, чтобы удовлетворять неравенству R
( U + (. Если следующее слово принимается в течение R единиц времени, то таймер Rt обновляется, иначе соединение закрывается. Значение таймера отправители выбирается так, чтобы невозможно было принять подтверждение при закрытом соединении; для этого, соединение поддерживается в течение по крайней мере S единиц времени после отправления пакета, где S - константа, выбираемая так, чтобы удовлетворять S ( R+2(. Таймер St устанавливается в S каждый раз, когда посылается пакет, и соединение может быть закрыто только если St < 0. Если к этому времени еще остались незавершенные слова (т.е. слова, для которых не было получено подтверждение), эти слова объявляются потерянными до закрытия соединения.

Rq: (* Принимаем пакет данных *)
{ ( Mq } begin receive ; if cr then if i = Exp then begin Rt := R ; Exp := i + 1 ; deliver w end else if s = true then begin create (Rt, Exp) ; (* cr := true *)
Rt := R ; Exp := i +1 ; deliver w end end

Sq: (* Посылаем подтверждение *)

{cr} begin send end
(* Закрытие соединения по истечении времени Rt, см. В действии Time *)

Алгоритм 3.5 Протокол приемника

Бит начало-последовательности используется приемником, если пакет получен при закрытом соединении, чтобы решить, может ли быть открыто соединение (и доставлено слово в пакете ). Отправитель устанавливает бит в true, если все предыдущие слова были подтверждены или объявлены (как возможно потерянные).
Когда q получает пакет при уже открытом соединении, содержащееся слово доставляется тогда и только тогда, когда порядковый номер пакета равен ожидаемому порядковому номеру (хранится в Exp).
Остается обсудить значение переменной B в протоколе отправителя. Это вспомогательная переменная, введенная только с целью доказательства правильности протокола. Отправитель нумерует слова в каждом соединении, начиная с 0, но, чтобы различать слова в различных соединениях, все слова индексируются последовательно по возрастанию для анализа протокола. Таким образом, там, где отправитель индексирует слово как i, "абсолютный" номер указанного слова B + i, где B - общее количество пакетов, принятых p в предыдущих соединениях. Соответствие между "внутренними" и "абсолютными" номерами слов показывается на Рисунке 3.7. В реализации протокола B не хранится, и отправитель "забывает" все слова inp [0 .. B-1].
Loss: { m ( M } (* M - либо Mp, либо Mq *) begin remove m from M end
Dupl: { m (M } (*M - либо Mp, либо Mq *) begin insert m in M end
Time: (* ( > 0 *) begin forall i do Ut[i] := Ut[i] -( ,
St := St -( ; Rt := Rt - ( ; if Rt ( 0 then delete (Rt, Exp) ; (* cr := false *) forall ( Mp, Mq do begin ( := (— ( ; if ( ( 0 then remove packet end end
Алгоритм 3.6 Дополнительные переходы Протокола.

Подсистема связи представляется двумя мультимножествами, Mp для пакетов с адресатом p и Mq для пакетов с адресатом q. Протокол отправителя - Алгоритм
3.4, протокол приемника - Алгоритм 3.5. Имеются дополнительные переходы системы, представленные Алгоритмом 3.6, которые не соответствуют шагам в протоколе процессов. Эти переходы представляют собой отказы канала и изменение времени. В переходах Loss и Dupl M означает или Mp, или Mq.
Действие Time уменьшает все таймеры в системе на величину (, это случается между двумя дискретными событиями, которые отличаются на ( единиц времени.
Когда таймер приемника достигает значения 0, соединение закрывается.

Рекомендуем скачать другие рефераты по теме: педагогические рефераты, реферат машини.





Предыдущая страница реферата | 16  17  18  19  20  21  22  23  24  25  26 | Следующая страница реферата