Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 29
Текст из файла (страница 29)
Для того чтобы выяснить, открыт ли сеанс связи,процесс проверяет, существует ли учетная запись соединения в списке записейоткрытых сеансов связи.Когда отправитель открывает сеанс связи, он начинает нумерацию поступивших к нему слов с 0. Переменная High предназначена для подсчета количества слов, поступивших в текущем сеансе связи, а переменная Low служит для102Гл.
3. Коммуникационные протоколыAp : (* Поступление очередного слова *)begin if not cs thenbegin(* Вначале открывается сеанс связи (соединение) *)create (St, High, Low) ; (* cs := true *)Low := High := 0 ; St := Send;Ut [B + High] := U ; High := High + 1endSp : (* Отправить i-е слово текущего сеанса связи *){ cs ∧ Low 6 i < High ∧ Ut [B + i] > 0 }begin send hdata, (i = Low), i, inp [B + i] , i ;St := SendRp : (* Получить подтверждение *){ cs ∧ hack, i, i ∈ Mp }begin receive hack, i, i ; Low := max (Low, i) endEp : (* Сформировать сообщение об ошибке в связи с возможной потерей слова *){ cs ∧ Ut [B + Low] 6 −2 − R }begin error [B + Low] := true ; Low := Low + 1 endCp : (* Закрыть сеанс связи *){ cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low) end(* cs := false *)Алгоритм 3.4.
Протокол процесса-отправителяподсчета количества слов, подтвержденных в текущем сеансе связи. Тем самымпредполагается (так же как в протоколе, описанном в § 3.3.1), что отправительможет пересылать пакеты, порядковые номера которых расположены в интервалемежду двумя числами Low и High − 1; однако здесь имеются некоторые особенности. Отправитель может переслать слово только в течение интервала временидлины U, начиная с момента поступления этого слова.
Для этого с каждым словом inp [i] ассоциируется таймер Ut [i] ; в момент поступления слова в таймереустанавливается начальное значение — число U, и в момент отправления словатаймер должен иметь положительное значение. Таким образом, окно передачи состоит из всех тех слов, у которых порядковые номера расположены в диапазонеLow . . . High − 1, и соответствующие этим словам таймеры имеют положительныезначения.Пакеты данных, которые отправляются по ходу работы рассматриваемогопротокола, состоят из особого бита (так называемого признака начала последовательности; его назначение мы обсудим позднее), порядкового номера и слова.Чтобы проводить анализ протокола, в каждом пакете выделяется четвертое поле,которое называется оставшимся сроком жизни пакета.
В этом поле указывается максимальное время, на протяжении которого пакет может оставаться3.2. Протокол с таймерами103Rq : (* Принять пакет данных *){ hdata, s, i, w, i ∈Mq }begin receive hdata, s, i, w, i ;if cr thenif i = Exp thenbegin Rt := R ; Exp := i + 1 ; deliver w endelse if s = true thenbegin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver wendendSq : (* Отправить подтверждение *){ cr }begin send hack, Exp, i end(* Закрыть сеанс связи, если возник тайм-аут по таймеру Rt, см.
действие Time *)Алгоритм 3.5. Протокол процесса-получателяв канале, до того как он будут доставлен по назначению или потерян в силупредположения об ограниченном времени жизни пакета. Когда пакет отправлен,оставшийся срок его жизни всегда равен . В пакет с подтверждением, которыйотправляется по ходу работы протокола, вкладывается только следующий порядковый номер сообщения, ожидаемого процессом q; но, как и в предыдущемслучае, для проведения анализа мы будем считать, что в пакете с подтверждениемтакже указывается оставшееся время жизни этого пакета.Закрытием сеансов связи управляют таймеры: таймер St у отправителя и таймер Rt у получателя.
Исходя из того, что для каждого слова имеется интервал,ограничивающий время его отправления, и каждый пакет также имеет ограниченный период жизни, можно заключить, что каждое слово может быть обнаруженов канале связи только на протяжении отрезка времени длины + U, начинаяс момента поступления этого слова. Это позволяет получателю сбрасывать всюинформацию о том или ином слове спустя + U единиц времени после получения этого слова; по истечении указанного срока никакие дубликаты уже не могутпоступать и, следовательно, нет никакого риска столкнуться с повторным получением сообщения.
Всякий раз, когда принимается некоторое слово, на таймереRt устанавливается время R, причем константа R выбирается так, чтобы выполнялось неравенство R > U + . Если следующее слово будет получено спустяне более R единиц времени, показания таймера Rt обновляются; в противномслучае сеанс связи закрывается. Установка таймера отправителя осуществляется так, чтобы избежать ситуации, при которой подтверждение поступает призакрытом сеансе связи; для этого соединение поддерживается по меньшей мере S единиц времени после отправления очередного пакета, причем константа Sвыбирается так, чтобы выполнялось неравенство S > R + 2 .
Всякий раз, когдаотправляется некоторый пакет, на таймере St устанавливается время S, и сеанссвязи закрывается только тогда, когда St < 0. Если в это время передача неко-Гл. 3. Коммуникационные протоколыАлгоритм 3.6. Дополнительные переходы протоколаОстается обсудить, зачем нужна в протоколе отправления переменная B. Этовспомогательная переменная, которую мы ввели только для доказательства корректности протокола. Отправитель в каждом сеансе связи проводит нумерациюслов, начиная с 0, но для того, чтобы при анализе протокола проводить различиемежду словами в разных сеансах связи, мы будем нумеровать подряд все слова.Таким образом, в том случае, когда отправитель дает некоторому слову номер i,«абсолютный» номер этого слова будет равен B + i, где B — это суммарное число пакетов, поступивших процессу p в предыдущие сеансы связи. Соответствиемежду «внутренними» и «абсолютными» номерами слов показано на рис.
3.7.При реализации протокола для переменной B памяти не отводится, и отправитель «забывает» обо всех словах inp [0..B − 1] .Коммуникационная подсистема представлена двумя мультимножествами: M pдля пакетов, адресованных процессу p, и Mq для пакетов, адресованных процессу q. Протокол отправителя задается алгоритмом 3.4, а протокол получателя(1)(2)(3)(4)(5)(6)(7)(8)cs =⇒ St 6 Scr =⇒ 0 < Rt 6 R∀i < B + High : Ut [i] 6 U∀h. .
. , i ∈ Mp , Mq : 0 < 6hdata, s, i, w, i ∈ Mq =⇒ cs ∧ St > + + Rcr =⇒ cs ∧ St > Rt +hack, i, i ∈ Mp =⇒ cs ∧ St >hdata, s, i, w, i ∈ Mq =⇒ (w = inp [B + i] ∧ i < High)∧∧∧∧∧∧∧P0 ≡Time: (* > 0 *)begin forall i do Ut [i] := Ut [i] − ;St := St − ;Rt := Rt − ;if Rt 6 0 then delete (Rt, Exp) ; (* cr := false *)forall h.., i ∈ Mp , Mq dobegin := − ;if 6 0 then remove packetendendДля обоснования всех необходимых свойств протокола воспользуемся рядомлемм и теорем.
Формула P0 , приведенная ниже, выражает утверждение о том, чтосоединение отправителя остается открытым, до тех пор пока в системе остаетсяхотя бы один пакет, и порядковые номера этих пакетов в текущем сеансе связиимеют правильное значение.Dupl: { m ∈ M }(* M — это либо Mp , либо Mq *)begin insert m in M end3.2.2. Доказательство корректности протоколаLoss: { m ∈ M }(* M — это либо Mp , либо Mq *)begin remove m from M end105задается алгоритмом 3.5. В системе есть также и дополнительные переходы, дляописания которых служит алгоритм 3.6.
Эти переходы не связаны с действиями протоколов процессов; с их помощью моделируются ошибки в каналах связии течение времени. В переходах Loss и Dupl буква M служит для обозначениялюбого из двух мультимножеств Mp и Mq . Действие Time приводит к уменьшению показателей всех таймеров системы на одну и ту же величину , и это какраз соответствует тому, что происходит, когда два дискретных события оказываются разделенными интервалом времени протяженности . Как только показаниетаймера получателя оказывается равным 0, сеанс связи закрывается.торых слов все еще не завершена (т. е. для некоторых отправленных слов не былополучено подтверждений), эти слова заносятся в отчет, до того как сеанс связибудет закрыт.Признак начала последовательности используется получателем в том случае,когда пакет получен при закрытом сеансе связи, для того чтобы решить, можноли открыть сеанс связи (и принять содержащееся в пакете слово).
Отправительустанавливает в этом бите значение true, когда все предыдущие слова уже получили подтверждение или были занесены в отчет (как вероятно утраченные). Еслипроцесс q получает пакет при уже открытом сеансе связи, то содержащееся впакете слово принимается в том и только том случае, когда порядковый номерпакета равен очередному номеру ожидаемого пакета (для этого используется переменная Exp).3.2. Протокол с таймерами104Для правильного истолкования соотношения (3), мы будем предполагать, чтозначение High равно нулю во всех тех конфигурациях, в которых отправитель неимеет соединения.Лемма 3.10. Формула P0 является инвариантом протокола с таймерами.Слова первого Слова второгосеанса связисеанса связи0Текущий сеанс связиB B + Low B + High? ?6 6Индексация слов в протоколе:0Рис. 3.7. Порядковые номера словLowокноотправ.?6HighГл.
3. Коммуникационные протоколы3.2. Протокол с таймерами107Time: Выполнимость соотношений (1), (2) и (3) сохраняется, поскольку значения переменных St, Rt и Ut [i] могут лишь уменьшиться и сеанс связи получателя закрывается, когда значение Rt становится равным 0. Выполнимостьсоотношения (4) сохраняется, потому что значение может лишь уменьшитьсяи пакет изымается, когда значение его поля становится равным 0.
Заметим,что действие Time приводит к уменьшению значения всех таймеров (включая те,которые содержатся в поле пакетов) на одну и ту же величину; поэтомусохраняется выполнимость всех соотношений вида Xt > Yt + C, где Xt и Yt —таймеры, а C — константа. Это означает, что соотношения (5), (6) и (7) остаютсяверными.Первое требование, которое предъявляется к рассматриваемому протоколу,состоит в том, что каждое слово должно быть рано или поздно доставлено поназначению или занесено в отчет как утраченное. Определим предикат Ok(i) следующей формулой:Ok(i) ⇐⇒ error [i] = true ∨процессу q было доставлено сообщение in p [i] .Как будет показано, протокол не теряет ни одного слова, не отметив этого факта.Рассмотрим формулу P1 следующего вида:P0¬ cs =⇒ ∀i < B : Ok(i)cs =⇒ ∀i < B + Low : Ok(i)hdata, true, I, w, i ∈ Mq =⇒ ∀i < B + I : Ok(i)cr =⇒ ∀i < B + Exp : Ok(i)hack, I, i ∈ Mp =⇒ ∀i < B + I : Ok(i)∧∧∧∧∧P1 ≡(9)(10)(11)(12)(13)Лемма 3.11.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
