Распределенные алгоритмы

отсюда еq применимо в (р. Запишем (pq = eq((р), и запомним, что

(рq = (..., dp, ..., dq, ..., ((M \ xp ( ур ) \ xq ) ( уq ).

С помощью симметричного аргумента может быть показано, что ер

применимо в (q = eq((). Запишем (qp = ep((q), и запомним, что

(qp = (..., dp, ..., dq, ..., ((M \ xq ( уq ) \ xp ) ( уp ).

Так как M – мультимножество сообщений, xp ( M, и xq ( M,

((M \ xp ( ур ) \ хq ( уq ) = ((M \ xq ( уq ) \ xp ( ур ),

и отсюда (pq = (qp .

(

Пусть ер и еq будут двумя событиями, которые появляются последовательно

в исполнении, т.е. исполнение содержит подпоследовательность

..., (, ер((), еq(ер(()), ...

для некоторых (. Посылка теоремы 2.19 применима к этим событиям за

исключением следующих двух случаев.

1) p = q; или

2) ер – событие отправки, и еq - соответствующее событие получения.

В самом деле, теорема явно утверждает, что p и q должны быть

различными, и если еq получает сообщение, посланное в ер, событие отправки

не применимо в начальной конфигурации события ep, как требуется. Таким

образом, если одно из этих двух утверждений истина, события не могут

появляться в обратном порядке, иначе они могут встречаться в обратном

порядке и кроме того иметь результат в одной конфигурации. Запомните, что с

глобальной точки зрения переходы не могут быть обменены, потому что (в

нотации теоремы 2.19) переход из (р в (pq отличается от перехода из ( в (q.

Однако, с точки зрения процесса эти события неразличимы.

Тот факт, что конкретная пара событий не может быть обменена,

выражается тем, что существует каузальное отношение между этими двумя

событиями. Это отношение может быть расширено до частичного порядка на

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

Определение 2.20 Пусть Е – исполнение. Отношение (, называемое

каузальным порядком, на событиях исполнения есть самое малое отношение,

которое удовлетворяет

1) Если е и f – различные события одного процесса и е появляется перед

f, то е ( f.

2) Если s – событие отправки и r – соответствующее событие получения,

то s ( r.

3) Отношение ( транзитивно.

Мы пишем а (= b, чтобы обозначить (а ( b ( а = b). Так как (= есть

частичный порядок, могут существовать события а и b, для которых ни а (= b

ни b (= а не выполняется. Говорят такие события конкурирующие, в нотации а

|| b. На рисунке 2.1, b || f, d || i, и т.д.

Каузальный порядок был впервые определен Лампортом [Lam78] и играет

важную роль в рассуждениях, относящихся к распределенным алгоритмам.

Определение ( подразумевает существование каузальной цепочки между

каузально связанными событиями. Этим мы подразумеваем, что а ( b включает

существование последовательности а = е0 , е1 , ..., ек = b такой, что

каждая пара последовательных событий в цепочке удовлетворяет либо (1), либо

(2) в определении 2.20. Каузальная цепочка может быть даже выбрана так, что

каждая пара, удовлетворяющая (1), есть последовательная пара событий в

процессе, где они встречаются, т.е., нет событий между ними. На рисунке 2.1

каузальная цепочка между событием а и событием l есть последовательность а,

f, g, h, j, k, l.

2.3.2 Эквивалентность исполнений: вычисления

В этом подразделе показывается, что события исполнения могут быть

переупорядочены в любом порядке, согласующимся с каузальным порядком, без

воздействия на результат исполнения. Это переупорядочивание событий

вызывает другую последовательность конфигураций, но это исполнение будет

рассматриваться как эквивалент исходного исполнения.

Пусть f = (f0 , f1 , f2 ,...) будет последовательностью событий. Эта

последовательность - последовательность событий относящихся к исполнению F

= ((0, (1, (2, ...), если для каждого i, fi применимо в (i и fi ((i) =

(i+1. В этом случае F называется включенным исполнением последовательности

f. Мы хотели бы, чтобы F уникально определялась последовательностью f, но

это не всегда так. Если для некоторого процесса p нет события в p,

включенного в f, то состояние процесса p может быть произвольным начальным

состоянием. Однако, если f содержит по крайней мере одно событие из р, то

первое событие в р, скажем (с, х, у, d), определяет, что начальное

состояние процесса р будет с. Поэтому, если f содержит по крайней мере одно

событие в каждом процессе, (0 уникально определено, и это определяет целое

исполнение уникально.

Теперь пусть Е = ((0, (1, (2, ... ) будет исполнением с ассоциированной

последовательностью событий Е’ = (е0 , е1 , е2 , ...) и положим, что f

–перестановка из Е’. Это означает, что существует перестановка (

натуральных чисел (или множества {0, ..., k-1}, если Е – конечное

исполнение с k событиями) таких, что fi = е((i). Перестановка (f0 , f1 , f2

, ...) событий из Е согласующаяся с каузальным порядком, если fi (= fj

подразумевает i ( j, т.е., если нет события, которому предшествует в

последовательности событие, которому оно само каузально предшествует.

Теорема 2.21 Пусть f = (f0 , f1 , f2 , ...) – перестановка событий из

Е, которая согласуется с каузальным порядком исполнения Е. Тогда f

определяет уникальное исполнение F, начинающееся в начальной конфигурации

из Е. F имеет столько же событий сколько и Е, и если Е конечно, то

последняя конфигурация из F такая же как и последняя конфигурация из Е.

Доказательство. Конфигурации из F строятся одна за другой, и чтобы

построить (i+1 достаточно показать, что fi применимо в (i. Возьмем (0 = (0.

Предположим, что для всех j < i, fj применимо в конфигурации (j и (j+1

= fj ((j ). Пусть (i = (cp1 , ..., cpN , M) и пусть fi =(c, x, y, d) будет

событие в процессе р, тогда событие fi применимо в (i, если сp = c и х (

М.

Чтобы показать, что сp = c нужно различать два случая. В обоих случаях

мы должны помнить, что каузальный порядок исполнения Е абсолютно

упорядочивает события в процессе р. Это подразумевает, что события в

процессе р появляются в точно таком же порядке и в f и в Е’.

Случай 1: fi - первое событие в р из f, тогда ср – это начальное

состояние р. Но тогда fi – также первое событие в р из Е’, что

подразумевает, что с – это начальное состояние р. Следовательно, с = ср.

Случай 2: fi – не первое событие в р из f. Пусть последнее событие в р

из f перед fi будет fi' = (c’, x’, y’, d’), тогда ср = d’. Но тогда fi'

также последнее событие в р перед fi из Е’, что подразумевает, что с = d’.

Следовательно, с = ср.

Чтобы показать, что х ( М мы должны помнить, что соответствующие

события приема и посылки встречаются в одном порядке и в f и в Е’. Если fi

не событие посылки, то х = ( и х ( М выполняется тривиально. Если fi – это

событие посылки, пусть fi будет соответствующим событием посылки. Так как

fj ( fi , j < i выполняется, т.е., событие посылки предваряет fi в f,

следовательно, х ( М.

Мы сейчас показали, что для каждого i, fi применимо в (i, и (i+1 может

быть взято как fi((i). Мы должны, наконец, показать, что последние

конфигурации из F и Е совпадают, если Е конечно. Пусть (k будет последней

конфигурацией из Е. Если Е’ не содержит события в р, то состояние р в (k

равно его начальному состоянию. Так как f также не содержит события в р, то

состояние р в (k также равно начальному состоянию, отсюда состояние р в (k

равняется его состоянию в (k. Иначе, состояние р в (k есть состояние после

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

это также состояние р в (k.

Сообщения в процессе передачи в (k есть такие сообщения, для которых

событию посылки нет соответствующего события получения в Е’. Но так как Е’

и f содержат один и тот же набор событий, те же сообщения в процессе

передачи в последней конфигурации из F. (

Рис. 2.2 Пространственно-временная диаграмма эквивалентная рис. 2.1

Исполнения F и Е имеют один набор событий, и каузальный порядок этих

событий – один и тот же для Е и F. Поэтому, также, в этом случае Е – это

перестановка событий из F, которая согласуется с каузальным порядком

исполнения F. Если применить условие теоремы 2.21, мы можем сказать, что Е

и F – эквивалентные исполнения, что обозначается как E ~ F.

Рис. 2.2 показывает временную диаграмму исполнения, эквивалентного

исполнению, изображенному на рис. 2.1. Эквивалентные временные диаграммы

могут быть получены с помощью «трансформаций резиновой ленты» [Mat89c].

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

стрелки сообщений продолжают указывать направо, рис. 2.1 может быть

деформирован до рис. 2.2.

Хотя изображенные исполнения эквивалентны и содержат одинаковый набор

событий, они не могут содержать одинаковый набор конфигураций. Рис. 2.1

содержит конфигурацию ((”), в которой сообщение, посланное в событии е и

сообщение, посланное в событии l, передаются одновременно . Рис. 2.2 не

содержит такой конфигурации, потому что сообщение, посланное в событии l,

получено перед свершением события е.

Глобальный наблюдатель, кто имеет доступ к действительной

последовательности событий, может различать два эквивалентных исполнения,

т.е. может наблюдать либо одно, либо другое исполнение. Однако, процессы не

могут различать две эквивалентных исполнения, т.к. для них невозможно

решить, какое из двух исполнений имеет место. Это иллюстрируется следующим.

Предположим, что мы должны решить будут ли посылаться сообщения в событии е

и будут в передаче одновременно. Существует булевская переменная sim в

одном из процессов, которая должна установлена в истину, если сообщения

были в передаче одновременно, и ложь иначе. Таким образом, в последней

конфигурации рис. 2.1 значение sim – истина, и в последней конфигурации на

рис 2.2 значение – ложь. По теореме 2.21, конфигурации равны, что

показывает, что требуемое присваивание sim невозможно.

Класс эквивалентности при отношении ~ полностью характеризуется набором

событий и каузальным порядком на этих событиях. Классы эквивалентности

называются вычислениями алгоритма.

Определение 2.22 Вычисление распределенного алгоритма – это класс

эквивалентности (при ~) исполнений алгоритма.

Не имеет смысла говорить о конфигурациях вычисления, потому что

различные исполнения вычисления могут не иметь одних и тех же конфигураций.

Имеет смысл говорить о наборе событий вычисления, потому что все исполнения

вычисления состоят из одного и того же набора событий. Также, каузальный

порядок событий определен для вычисления. Мы будем называть вычисление

конечным, если его исполнения конечны. Все исполнения вычисления начинаются

в одной конфигурации и, если вычисление конечно, завершаются в одной

конфигурации (теорема 2.21). Эти конфигурации называются начальными и

конечными конфигурациями вычисления. Мы будем определять вычисление с

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

Результат из теории частичных порядков подразумевает, что каждый

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

Факт 2.23 Пусть (Х, , где w - слово данных, а i - натуральное число (называемое

порядковым номером пакета). Этот пакет, посылаемый процессом p (к q),

передает слово = inp[i] для q, но также, как было отмечено, подтверждает

получение некоторого количества пакетов от q. Процесс p может быть

«впереди» q не более, чем на lp пакетов, если мы потребуем, что пакет

данных < pack, w, i >, посланный p, подтверждает получение слов с номерами

0.. i— lp от q. (q посылает аналогичные пакеты.) Константы lp и lq

неотрицательны и известны обоим процессам p и q. Использование пакета

данных в качестве подтверждения имеет два последствия для протокола:

1) Процесс p может послать слово inp[i] (в виде пакета < pack, inp[i], i

>) только после того, как запишет все слова от outp[0] до outp[i — lp],

т. е. , если i < sp + lp.

2) Когда p принимает < pack, w,i>, повторная передача слов с inp[0] до

inp[i — lq] уже не нужна.

Объяснение псевдокода. После выбора модели нетрудно разработать код

протокола; см. Алгоритм 3.1. Для процесса p введена переменная ap (и aq для

q), в которой хранится самое первое слово, для которого p (или q,

соответственно) еще не получил подтверждение..

В Алгоритме 3.1 действие Sp - посылка i-го слова процессом p, действие Rp -

принятие слова процессом p, и действие Lp - потеря пакета с местом

назначения p. Процесс p может послать любое слово, индекс которого попадает

в указанные ранее границы. Когда сообщение принято, в первую очередь

делается проверка - было ли идентичное сообщение принято ранее (на случай

повторной передачи). Если нет, слово, содержащееся в нем, записывается в

выход, и ap и sp корректируются. Также вводятся действия Sq, Rq и Lq , где

p и q поменяны ролями.

var sp, ap : integer init 0, 0 ;

inp : array of word (* Посылаемые данные *) ;

outp : array of word init udef, udef, ...',

Sp: {ap ( i < Sp+lp}

begin send < pack,inp[i],i> to q end

Rp: { < pack, w, i > (Qp }

begin receive ;

if outp[i] = udef then

begin outp[i] := w ;

ap := max(ap,i-lp+1) ;

Sp := minj

end

(* else игнорируем, пакет передавался повторно *)

end

Lp: {(Qp}

begin Qp := Qp\ {} end

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

Инвариант протокола. Подсистема связи представляется двумя очередями, Qp

для пакетов с адресатом p и Qq, для пакетов с адресатом q. Заметим, что

перевычисление sp в Rp никогда не дает значение меньше предыдущего, поэтому

sp никогда не уменьшается. Чтобы показать, что этот алгоритм удовлетворяет

данным ранее требованиям, сначала покажем, что утверждение P - инвариант.

(В этом и других утверждениях i - натуральное число.)

P ( (i < sp : outp[i]( udef (0p)

/\ (i < sq, : outq[i] ( udef (0q)

/\ < pack, w, i > ( Qp ( w = inq[i] /\ (i < sq + lq) (lp)

/\ < pack, w, i > ( Qq ( w = inp[i] /\ (i < sp + lp) (lq)

/\ outp[i]( udef ( outp[i] = inq[i] /\ (ap > i— lq) (2p)

/\ outq[i]( udef ( outq[i] = inp[i] /\ (aq > i— lp) (2q)

/\ ap ( sq, (3p)

/\ aq ( sp (3q)

удотооyоонґн4пїозс›п…снчнTж

к?Ю|и6ЫMкЛЭщо2в6цrе}юўз_єи©[pic]иш?еpрУгШпёе8х№й?ь|н;[1]8пL›михнжСйвСбGЯЯ†Эў

а-

Ю]жгб…н=зУт4мхх™р‹щ_х“ющУ[pic]іш+я”уЩфDмeжЩжЫЩжбУaилЦUмщбЈсYо?чёууыЎря‘лXЖзЄ

xбї[pic]LЩ“щОФ?тЧ…оЯhмЁйЬлHт(нЬцІручсхнхы?пъь•жxъЯ7хѕЬFр2а†нЛемма 3.1 P -

инвариант Алгоритма 3.1.

Доказательство. В любой начальной конфигурации Qp и Qq - пустые, для всех

i, outp[i] и outq[i] равны udef, и ap,ap, sp и sq равны нулю 0; из этого

следует, что P=true. Перемещения протокола рассмотрим с точки зрения

сохранения значения P. Во-первых, заметим, что значения inp и inq, никогда

не меняются.

Sp: Чтобы показать, что Sp сохраняет (0p), заметим, что Sp не увеличивает

sp и не делает ни один из outp[i] равным udef.

Чтобы показать, что Sp сохраняет (0q), заметим, что Sp не увеличивает

sq, и не делает ни один из outq[i] равным udef.

Чтобы показать, что Sp сохраняет (1p), заметим, что Sp не добавляет

пакеты в Qp и не уменьшает sp.

Чтобы показать, что Sp сохраняет (lq), заметим Sp добавляет < pack, w,

i > в Qp с w = inp[i] и i < sp + lp, и не изменяет значение sp.

Чтобы показать, что Sp сохраняет (2p) и (2q), заметим, что Sp не

изменяет значения outp, outq, ap, или aq.

Чтобы показать, что Sp сохраняет (3p) и (3q), заметим, что Sp не меняет

значения ap , ap , sq , или sp.

Rp: Чтобы показать, что Rp сохраняет (0p), заметим, что Rp не делает ни

одно outp[i] равным udef, и если он перевычисляет sp, то оно

впоследствии также удовлетворяет (0p).

Чтобы показать, что Rp сохраняет (0q), заметим, что Rp не меняет outq

или sq.

Чтобы показать, что Rp сохраняет (lp), заметим, что Rp не добавляет

пакеты в Qp и не уменьшает sq.

Чтобы показать, что Rp сохраняет (lq), заметим, что Rp не добавляет

пакеты в Qq и не уменьшает sp.

Чтобы показать, что Rp сохраняет (2p), заметим, что Rp изменяет

значение outp[i] на w при принятии < pack, w,i>. Т.к. Qp содержала этот

пакет до того, как выполнился Rp, из (1p) следует, что w = inp[i].

Присваивание ap:= max (ap, i— lq+1) гарантирует, что ap > i— lq

сохраняется после выполнения. Чтобы показать, что Rp сохраняет (2q),

заметим, что Rp не меняет значения outq или aq.

Чтобы показать, что Rp сохраняет (3p), заметим, что когда Rp

присваивает

ap:= max(ap, i— lq+1) (при принятии ), из (lp) следует, что

i < sq+lq, следовательно ap ( sq сохраняется после присваивания. Rp не

меняет sq. Чтобы показать, что Rp сохраняет (3q), заметим, что sp может

быть увеличен только при выполнении Rp.

Lp : Чтобы показать, что Lp сохраняет (0p), (0q), (2p), (2q), (3p), и

(3q), достаточно заметить, что Lp не меняет состояния процессов. (lp) и

(lq) сохраняются потому, что Lp только удаляет пакеты (а не порождает

или искажает их).

Процессы Sq, Rq, и Lq сохраняют P , что следует из симметрии.

(

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

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

Конфигурация протокола может быть обозначена ( = (cp, cq, Qp, Qq), где cp и

cq - состояния p и q. Пусть ( будет конфигурацией, в которой применим Sp

(для некоторого i). Пусть

( = 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 процессом p или посылка

процессом 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). (

[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' < ap+L ( i+L.

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 в момент принятия, и должен быть положительным для

Страницы: 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18