Xt(t1)-Xt(t2)=t2-t1.
Заметим, что эти таймеры работают так: в течение времени d они уменьшаются точно на d. В Подразделе 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, для которых ассоциированный с ними таймер положителен.
Сетевые константы:
m : real ; (* Максимальное время жизни пакета *)
Константы протокола:
U : real ; (* Длина интервала отправки *)
R : real ; (* Значение тийм-аута приемника: R³ U+m *)
S : real ; (* Значение тайм-аута отправителя: S ³ R + 2m *)
Запись соединения отправителя:
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 Переменные протокола, основанного на таймере.
Протокол посылает пакеты данных, состоящие из: бита (бит начала-последовательности; его значение будет обсуждаться позже), порядкового номера и слова. Для анализа протокола каждый пакет данных содержит четвертое поле, называемое оставшееся время жизни пакета. Оно показывает максимальное время, в течение которого пакет еще может находиться в канале до того, как он должен быть принят или стать потерянным согласно предположению об ограниченном времени жизни. В момент отправления оставшееся время жизни пакета всегда равно m. Пакеты подтверждения протокола состоят только из порядкового номера, ожидаемого процессом 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 <data, (i = Low),i, inp[B + i],m > ;
St:=S
Rp: (* Принятие подтверждения *)
{ cs /\ <ack, i, r >Î Mp }
begin receive <ack, i, r > ; Low := max (Low, i) end
Ep: (* Генерация сообщения об ошибке для возможно потерянного слова *)
{cs /\ Ut[B + Low] £ -2m -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 для приемника. Ограниченный интервал посылки каждого слова и ограниченное время жизни пакета приводят к тому, что каждое слово может быть найдено в каналах только лишь в течение интервала времени длиной m + U, начиная с момента принятия слова. Это позволяет приемнику отбрасывать информацию о конкретном слове через m + U единиц времени после принятия слова; после этого не могут появиться дубликаты, следовательно не возможна повторная доставка. Таймер Rt устанавливается в R каждый раз, когда слово доставляется, константа R выбирается так, чтобы удовлетворять неравенству R ³ U + m. Если следующее слово принимается в течение R единиц времени, то таймер Rt обновляется, иначе соединение закрывается. Значение таймера отправители выбирается так, чтобы невозможно было принять подтверждение при закрытом соединении; для этого, соединение поддерживается в течение по крайней мере S единиц времени после отправления пакета, где S - константа, выбираемая так, чтобы удовлетворять S ³ R+2m. Таймер St устанавливается в S каждый раз, когда посылается пакет, и соединение может быть закрыто только если St < 0. Если к этому времени еще остались незавершенные слова (ò.å. слова, для которых не было получено подтверждение), эти слова объявляются потерянными до закрытия соединения.
Rq: (* Принимаем пакет данных *)
{ <data, s, i,w,r > Î Mq }
begin receive <data, s, i,w,r > ;
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
Sq: (* Посылаем подтверждение *)
{cr}
begin send <ack, Exp, m > end
(* Закрытие соединения по истечении времени Rt, см. В действии Time *)
Àëãîðèòì 3.5 Протокол приемника
Бит начало-последовательности используется приемником, если пакет получен при закрытом соединении, чтобы решить, может ли быть открыто соединение (и доставлено слово в пакете ). Отправитель устанавливает бит в true, если все предыдущие слова были подтверждены или объявлены (как возможно потерянные). Когда q получает пакет при уже открытом соединении, содержащееся слово доставляется тогда и только тогда, когда порядковый номер пакета равен ожидаемому порядковому номеру (хранится в Exp).
Страницы: 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
