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

Константы протокола:

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, соединение закрывается.

[pic]

Рисунок 3.7 Порядковые номера протокола.

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

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

Утверждение P0, которое определено ниже, показывает, что соединение

отправителя остается открытым пока в системе еще есть пакеты, и что

порядковые номера этих пакетов имеют корректное значение в текущем

соединении.

P0 ( cs ( St ( S

(1)

cr ( 0 < Rt( R (2)

(i < B+ High : Ut[i] ( U (3)

(( Mp, Mq : 0 ( Mq ( cs (St( ( +(+R (5)

cr( cs /\ St ( Rt + ( (6)

(Mp ( cs /\ St>( (7)

(Mq ( (w = inp[B + i] /\ i < High) (8)

Объяснение к (3): значение High предполагается равным нулю во всех

конфигурациях, в которых со стороны приемника нет соединения.

Лемма 3.10 P0 - инвариант протокола, основанного на таймере.

Доказательство. Первоначально не соединения, нет пакетов, и B = 0, из чего

следует, что P0 - true.

Ap: (1) сохраняется, т.к. St всегда присваивается значения S (St = S).

(3) сохраняется, т.к. перед увеличением High, Ut[B + High]

присваивается значение U. (5), (6) и (7) сохраняются, т.к. St может

только увеличиваться. (8) сохраняется, т.к. High может только

увеличиваться.

Sp: (1) сохраняется, т.к. St всегда присваивается значения S. (4)

сохраняется, т.к. каждый пакет посылается с оставшимся временем жизни

равным ?. (5) сохраняется, т.к. пакет посылается и St

устанавливается в S, и S = R + 2?. (6) и (7) сохраняется, т.к. St

может только увеличиться в этом действии. (8) сохраняется, т.к. новый

пакет удовлетворяет w = inp[B + i] и i < High.

Rp: Действие Rp не меняет никаких переменных из P0, и удаление пакета

сохраняет (4) и (7).

Ep: Действие Ep не меняет никаких переменных из P0.

Cp: Действие Cp делает равным false заключения (5), (6) и (7), но

((2), (5), (6) и (7)) применимы только когда их посылки ложны. Cp

также меняет значение B, но, т.к. пакетов для передачи нет, (по (5) и

(7)), (8) сохраняется.

Rq: (2) сохраняется, т.к. Rt всегда присваивается значение R (если

присваивается). (6) сохраняется, т.к. Rt устанавливается только в R

только при принятии пакета , и из (4) и (5) следует

cs ? St ( R + ? когда это происходит.

Sq: (4) сохраняется, т.к. каждый пакет посылается с оставшимся

временем жизни, равным ?. (7) сохраняется, т.к. пакет < ack,i,( >

посылается с ( = ? когда cr истинно, так что из (2) и (6) St > ?.

Loss: (4), (5), (7) и (8) сохраняются, т.к. удаление пакета может

фальсифицировать только их посылку.

Dupl: (4), (5), (7) и (8) сохраняются, т.к. ввод пакета m применимо

только если m уже был в канале, из чего следует, что заключение

данного предложения было истинным и перед введением.

Time: (1), (2) и (3) сохраняются, т.к. St, Rt, и Ut[i] может только

уменьшаться, и соединение приемника закрывается, когда Rt становится

равным 0. (4) сохраняются, т.к. ( может только уменьшиться, и пакет

удаляется, когда его (-поле достигает значения 0. Заметим, что Time

уменьшает все таймеры (включая (-поле пакета) на одну и ту же

величину, значит сохраняет все утверждения вида Xt > Yt +C, где Xt и

Yt -таймеры, и C - константа. Это показывает, что (5), (6) и (7)

сохраняются. (

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

доставляется или объявляется потерянным. Определим предикат 0k(i) как

0k(i) ( error [i] = true \/ q доставил inp [i].

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

объявляя об этом. Определим утверждение P1 как

P1( P0

/\ (cs (( i < B: 0k(i) (9)

/\ cs (( i < B + Low : 0k(i) (10)

/\ (Mq((i( Mp (( i, но т.к. s

истинно только при I = Low, то это сохраняет (11) из (10).

Rp: Значение Low может быть увеличено, если принят пакет < ack, I, (

>. Тем не менее, (10) сохраняется, т.к. из (13) (i < B + I : 0k(i)

выполняется, если получено это подтверждение.

Ep: Значение Low может быть увеличено, когда применяется действие Ep,

но генерация сообщения об ошибке гарантирует, что (10) сохраняется.

Cp: Действие Cp обращает cs в false, но оно применимо только если St <

0 и Low == High. Из (10) следует, что (i < B+ High : 0k(i)

выполняется прежде выполнения Cp, следовательно (9) сохраняется.

Посылка (10) обращается в false в этом действии, и из (5), (6) и (7)

следует, что посылки (11), (12) и (13) ложны; следовательно (10),

(11), (12) и (13) сохраняются.

Rq: Сначала рассмотрим случай, когда q принимает < data, true,l,w,(>

при не существующем соединении (cr - false). Тогда (i < B+I : 0k(i)

из (11), и w доставляется в действии. Т.к.

w = inp[B+I] из (8), присваивание Exp := I + 1 сохраняет (12).

Теперь рассмотрим случай, когда Exp увеличивается в результате

принятия

< data, s,Exp,w,(> при открытом соединении. Из (12), (i < B + Exp :

0k(i) выполнялось перед принятием, и слово w = Wp[B + Exp]

доставляется действием, следовательно приращение Exp сохраняет (12).

Sq: Отправление сохраняет (13) из (12).

Loss: Выполнение Loss может только фальсифицировать посылки

предложений.

Dupl: Введение пакета m возможно только если посылка соответствующего

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

введения.

Time: Таймеры не упоминались явно в (9)-(13). Выведение пакета или

закрытие процессом q может только фальсифицировать посылки (11), (12)

или (13).(

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

дополнительного предположения. Без этого предположения отправитель может

быть чрезвычайно ленивым в объявлении слов возможно потерянными; в

Алгоритме 3.4 указано только, что это сообщение может и не возникнуть в

промежуток времени 2( + R после окончания интервала для отправления слова,

но не указано, что оно вообще должно появиться. Итак, позвольте сделать

дополнительное предположение, что действие Ep на самом выполниться

процессом p и в течение разумного времени, а именно прежде, чем Ut[B + Low]

= —2( —R—(.

Теорема 3.12 (Нет потерь) Каждое слово inp доставляется q или объявляется p

как возможно потерянное в течение U+2(+R+( после принятия слова процессом

p.

Доказательство. После принятия слова inp[I], B+High > I начинает

выполняться. Если соединение закрывается в течение указанного периода после

принятия слова inp[I], то B > I, и результат следует из (9). Если

соединение не закрывается в этот промежуток времени и B + Low ( I, отчет

обо всех словах из промежутка B + Low..I возможен ко времени 2( + R после

окончания интервала отправления inp[I]. Из этого следует, что этот отчет

имел место 2( + R +( после окончания интервала отправления, т.е., U+ 2(

+R+( после принятия. Из этого также следует I < B+ Low, и, значит, слово

было доставлено или объявлено (из (10)). (

Чтобы установить второе требование корректности протокола, должно быть

показано, что каждое принимаемое слово имеет больший индекс (в inp), чем

ранее принятое слово. Обозначим индекс самого последнего доставленного

слова через pr (для удобства запишем, что изначально

pr =-1 and Ut[-1] = -( ). Определим утверждение P2 как:

P2( P1

/\ ( Mq ( Ut[B+i] > ( -( (14)

/\ i1 ( i2 < B + High ( Ut[i1] ( Ut[i2] (15)

/\ cr ( Rt ( Ut[pr] + ( (16)

/\ pr < B + High /\ ( Ut[pr] > -( ( cr) (17)

/\ cr ( B + Exp = pr + 1 (18)

Лемма 3.13 P2 - инвариант протокола, основанного на таймере.

Доказательство. Изначально Mq пусто, B + High равно нулю, (cr выполняется,

и

Ut[pr] < -(, откуда следуют (14)-(18).

Ap: (15) сохраняется, т.к. каждое новое принятое слово получает

значение таймера U, что из (3) по крайней мере равно значениям

таймеров ранее принятых слов.

Sp: (14) сохраняется, т.к. Ut[B +i] > 0 и пакет отправляется с ((( .

Cp: (14), (16) и (18) сохраняются, т.к. из (5) и (6) их посылки ложны,

когда Cp применимо. (15) сохраняется, т.к. B принимает значение B +

High и таймеры не меняются. (17) сохраняется, т.к. B присваивается

значение B + High и pr и cr не меняются.

Rq: (16) сохраняется, т.к. когда Rt устанавливается в R (при принятии

слова) Ut[pr] ( U из (3), и R( 2(+U. (17) сохраняется, т.к. pr

< B+High, что следует из (8), и cr становится true. (18) сохраняется,

т.к. Exp устанавливается в i +1 и pr в B + i, откуда следует, что

(18) становится true.

Time: (14) сохраняется, т.к. Ut[B + i] и ( уменьшаются на одно и то же

число (и выведение пакета только делает ложной посылку). (15)

сохраняется, т.к. Ut[i1] и Ut[i2] уменьшаются на одну и туже

величину. (16) сохраняется, т.к. cr не становится истинным в этом

действии, и Rt и Ut[pr] уменьшаются на одну и ту же величину. (17)

сохраняется, т.к. его заключение становится ложным только, если Rt

становится ( 0, откуда следует (по (16)), что Ut[pr] становится < -(.

(18) сохраняется, т.к., если cr не обратился в false, B, Exp и pr не

меняются.

Действия Rp, Ep, и Sq, не меняют никакие переменные в (14)-(18). Loss и

Dupl сохраняют (14)-(18) исходя из тех же соображений, что и в предыдущих

доказательствах. (

Лемма 3.14 Из P2 следует, что

< data, s,i1,w,(> ( Mq ( (cr \/ B+i1 > pr).

Доказательство. По (14), из ( Mq следует Ut[B+i1] >( -( >

-(.

Если B +i1 ( pr то, т.к. pr < B + High из (15), Ut[pr] > -(, так что из

(17) cr true. (

Теорема 3.15 (Упорядочение) Слова, доставляемые q появляются в строго

возрастающем порядке в массиве inp.

Доказательство. Предположим q получает пакет и доставляет

w. Если перед получением не было соединения, B + i1 > pr (по Лемме 3.14),

так что слова w располагается в inp после позиции pr. Если соединение было,

i1 = Exp, значит B+i1 = B+Exp = pr+1 из (18), откуда следует, что w =

inp[pr+1]. (

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

Некоторые расширения протокола уже обсуждались во введении в этот раздел. И

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

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

Качество протокола. Требования Нет потерь и Упорядочение являются

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

решение, а именно протокол, который не посылает или получает никакие

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

такой протокол, который не дает никакой транспортировки данных от

отправителя к приемнику, не является очень "хорошим" решением.

Хорошие решения проблемы не только удовлетворяют требованиям Нет потерь и

Страницы: 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