Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 29
Текст из файла (страница 29)
Вообщето эти предикаты не задаются в явном виде булевыми переменными отправителя(или получателя); вместо этого признаком открытого сеанса связи служит существование его учетной записи. Для того чтобы выяснить, открыт ли сеанс связи,процесс проверяет, существует ли учетная запись соединения в списке записейоткрытых сеансов связи.Когда отправитель открывает сеанс связи, он начинает нумерацию поступивших к нему слов с 0.
Переменная High предназначена для подсчета количества слов, поступивших в текущем сеансе связи, а переменная Low служит дляГл. 3. Коммуникационные протоколы102Ар:(* Поступление очередного слова *)begin if not cs thenbegin)* Вначале открывается сеанс связи (соединение) *)create ( S t, H ig h , L o w ) ; (* cs := true *):= H i g h := 0 ; S t := SLowend;U t[B + H ig h ]:= U ; H i g h := H i g h + 1end§ : (* Отправить i-e слово текущего сеанса связи *){ cs A L o w < i < H i g h A U t[B + i] > 0 }begin send (data, (i = L o w ) , i, in p [B + i], p) ;S t := SendRp: (* Получить подтверждение *){ cs A (ack, i, p) € M p }begin receive (ack, i, p) ; L o w := max (L o w , i) endEp: (* Сформировать сообщение об ошибке в связи с возможной потерей слова*){ cs A U t [В + L ow ] < - 2 ц - R )beginCp:e rr o r[B+ L ow ]:= t r u e ; L o w:= L o w + 1 end(* Закрыть сеанс связи *){ cs A S t < 0 A L o w = H i g h )begin В := В + H i g h ; delete ( S t , H i g h , L o w ) end(* cs := false *)Алгоритм 3.4.
Протокол процесса-отправителяподсчета количества слов, подтвержденных в текущем сеансе связи. Тем самымпредполагается (так же как в протоколе, описанном в §3.3.1), что отправительможет пересылать пакеты, порядковые номера которых расположены в интервалемежду двумя числами Low и High — 1; однако здесь имеются некоторые особенности. Отправитель может переслать слово только в течение интервала временидлины U, начиная с момента поступления этого слова. Для этого с каждым словом itip[i\ ассоциируется таймер Ut[i\; в момент поступления слова в таймереустанавливается начальное значение — число U, и в момент отправления словатаймер должен иметь положительное значение.
Таким образом, окно передачи состоит из всех тех слов, у которых порядковые номера расположены в диапазонеLow ... High —1, и соответствующие этим словам таймеры имеют положительныезначения.Пакеты данных, которые отправляются по ходу работы рассматриваемогопротокола, состоят из особого бита (так называемого признака начала последовательности; его назначение мы обсудим позднее), порядкового номера и слова.Чтобы проводить анализ протокола, в каждом пакете выделяется четвертое поле,которое называется оставшимся сроком жизни пакета. В этом поле указывается максимальное время, на протяжении которого пакет может оставаться3.2. Протокол с таймерами103R?: (* Принять пакет данных *){ (data, s, i, w , р) 6 M q }begin receive (data, s, i, w , p) ;if c r thenif i = E x p thenbegin R t ■= R ; E x p : = i + 1 ; deliver w endelse if s = t r u e thenbegin create (R t, E x p ) ; (* cr := true *)Rt:=R; E x p := i + 1 ; deliverwendendS?: (* Отправить подтверждение *){cr }begin send (ack,E x p , pi) end(* Закрыть сеанс связи, если возник тайм-аут по таймеру R t , см.
действие Time *)Алгоритм 3.5. Протокол процесса-получателяв канале, до того как он будут доставлен по назначению или потерян в силупредположения об ограниченном времени жизни пакета. Когда пакет отправлен,оставшийся срок его жизни всегда равен pi. В пакет с подтверждением, которыйотправляется по ходу работы протокола, вкладывается только следующий порядковый номер сообщения, ожидаемого процессом q; но, как и в предыдущемслучае, для проведения анализа мы будем считать, что в пакете с подтверждениемтакже указывается оставшееся время жизни этого пакета.Закрытием сеансов связи управляют таймеры: таймер S t у отправителя и таймер Rt у получателя.
Исходя из того, что для каждого слова имеется интервал,ограничивающий время его отправления, и каждый пакет также имеет ограниченный период жизни, можно заключить, что каждое слово может быть обнаруженов канале связи только на протяжении отрезка времени длины pi + U, начинаяс момента поступления этого слова. Это позволяет получателю сбрасывать всюинформацию о том или ином слове спустя pi + U единиц времени после получения этого слова; по истечении указанного срока никакие дубликаты уже не могутпоступать и, следовательно, нет никакого риска столкнуться с повторным получением сообщения. Всякий раз, когда принимается некоторое слово, на таймереRt устанавливается время R, причем константа R выбирается так, чтобы выполнялось неравенство R > U + pi.
Если следующее слово будет получено спустяне более R единиц времени, показания таймера Rt обновляются; в противномслучае сеанс связи закрывается. Установка таймера отправителя осуществляется так, чтобы избежать ситуации, при которой подтверждение поступает призакрытом сеансе связи; для этого соединение поддерживается по меньшей мере S единиц времени после отправления очередного пакета, причем константа Sвыбирается так, чтобы выполнялось неравенство S ^ R + 2рх.
Всякий раз, когдаотправляется некоторый пакет, на таймере St устанавливается время S, и сеанссвязи закрывается только тогда, когда St < 0. Если в это время передача некоГл. 3. Коммуникационные протоколы104торых слов все еще не завершена (т. е. для некоторых отправленных слов не былополучено подтверждений), эти слова заносятся в отчет, до того как сеанс связибудет закрыт.Признак начала последовательности используется получателем в том случае,когда пакет получен при закрытом сеансе связи, для того чтобы решить, можноли открыть сеанс связи (и принять содержащееся в пакете слово). Отправительустанавливает в этом бите значение true, когда все предыдущие слова уже получили подтверждение или были занесены в отчет (как вероятно утраченные).
Еслипроцесс q получает пакет при уже открытом сеансе связи, то содержащееся впакете слово принимается в том и только том случае, когда порядковый номерпакета равен очередному номеру ожидаемого пакета (для этого используется переменная Ехр).Loss: { т 6 М }(* М — это либоbegin remove т from М endМ р,либо M q *)Dupl: { m € M }begin insertM p,либо M q *)mTime: (* 8 > 0 *)begin foralli(* M — это либоin M enddo U t [ i\ := U t [ i\ —8 ;8;R t := R t —8 ;if R t < 0 then delete ( R t, E x p ) ; (* c r := false *)forall (.., p) € M p , M q dobegin p := p —8 ;if p < 0 then remove packetendS t:= S t-endАлгоритм 3.6. Дополнительные переходы протоколаОстается обсудить, зачем нужна в протоколе отправления переменная В.
Этовспомогательная переменная, которую мы ввели только для доказательства корректности протокола. Отправитель в каждом сеансе связи проводит нумерациюслов, начиная с 0, но для того, чтобы при анализе протокола проводить различиемежду словами в разных сеансах связи, мы будем нумеровать подряд все слова.Таким образом, в том случае, когда отправитель дает некоторому слову номер г,«абсолютный» номер этого слова будет равен В + г, где В — это суммарное число пакетов, поступивших процессу р в предыдущие сеансы связи. Соответствиемежду «внутренними» и «абсолютными» номерами слов показано на рис.
3.7.При реализации протокола для переменной В памяти не отводится, и отправитель «забывает» обо всех словах inp[0..B — 1].Коммуникационная подсистема представлена двумя мультимножествами: Мрдля пакетов, адресованных процессу р, и Mq для пакетов, адресованных процессу q. Протокол отправителя задается алгоритмом 3.4, а протокол получателя3.2. Протокол с таймерами105задается алгоритмом 3.5. В системе есть также и дополнительные переходы, дляописания которых служит алгоритм 3.6.
Эти переходы не связаны с действиями протоколов процессов; с их помощью моделируются ошибки в каналах связии течение времени. В переходах Loss и Dupl буква М служит для обозначениялюбого из двух мультимножеств Мр и Mq. Действие Time приводит к уменьшению показателей всех таймеров системы на одну и ту же величину 8, и это какраз соответствует тому, что происходит, когда два дискретных события оказываются разделенными интервалом времени протяженности 8.
Как только показаниетаймера получателя оказывается равным 0, сеанс связи закрывается.3.2.2. Доказательство корректности протоколаДля обоснования всех необходимых свойств протокола воспользуемся рядомлемм и теорем. Формула Ро, приведенная ниже, выражает утверждение о том, чтосоединение отправителя остается открытым, до тех пор пока в системе остаетсяхотя бы один пакет, и порядковые номера этих пакетов в текущем сеансе связиимеют правильное значение.Р0 =cs => St ^ Sсг = > 0 < Rt^ RЛ V/ < В + High: Ut[i] ^ UЛ V(..., р)еЛ*р, Л 4 „ : 0 < р < цЛ (data, s, i, w, р) е M q =$■ cs Л St > р + pi + RЛcr =$• cs Л S t^ Rt+ у.A(ack, /, p) e M p=*- cs A S t > pA (data, s, i, w , p) e M q =$■ (w = inp[B + /] A i < High)(1)(2)Л(3)(4)(5)(6)(7)(8)Для правильного истолкования соотношения (3), мы будем предполагать, чтозначение High равно нулю во всех тех конфигурациях, в которых отправитель неимеет соединения.Лемма 3.10.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
