Введение в распределённые алгоритмы. Ж. Тель (2009) (не распознанно) (1185664), страница 39
Текст из файла (страница 39)
Когда связь в каналевосстанавливается (или в сети появляется новый канал связи), в конфигурациивозникают две новые пустые очереди, а узлы по обе стороны этого канала связиполучают сообщение типа repair. Если между узлами u 1 и u2 образуется каналсвязи, то процесс u1 получает сообщение hrepair, u2 i, а процесс u2 — сообщениеhrepair, u1 i.Алгоритм предусматривает следующую реакцию на сообщения о разрыве иливосстановлении канала связи. Когда выходит из строя канал связи между узламиu и w, вершина w удаляется из списка Neighu , и наоборот. Проводится перевычисление оценок расстояний до каждой вершины, и в случае изменения оценки,об этом узнают все оставшиеся соседи. Это происходит, если неисправный канал ранее был одним из звеньев наилучшего маршрута и не осталось ни одногососеда w0 , для которого верно равенство ndisu [w0 , v] = ndisu [w, v] .
Когда каналсвязи восстанавливается (или добавляется новый канал), вершина w добавляетсяк списку вершин Neighu , но в памяти узла u еще нет никаких оценок расстояния d(w, v) (и наоборот). Новому соседу w немедленно сообщаются оценки D u [v]расстояний от узла u до всех возможных вершин-адресатов v (путем отправлениясообщений hmydist, v, Du [v] i. До тех пор пока узел u не получит такого сообщения от узла w, величина N будет использоваться в нем для оценки расстоянияd(w, v), т. е. значение переменной ndisu [w, v] полагается равным N.P(u, w, v) ≡up(u, w) ⇐⇒ w ∈ Neighu∧ up(u, w) ∧ Qwu содержит сообщение hmydist, v, di=⇒ последнее сообщение в очередиудовлетворяет равенству d = Dw [v]∧ up(u, w) ∧ Qwu не содержит сообщений hmydist, v, di=⇒ ndisu [w, v] = Dw [v]L(u, v) ≡u = v =⇒ (Du [v] = 0 ∧ Nbu [v] = local)∧ (u 6= v ∧ ∃w ∈ Neighu : ndisu [w, v] < N − 1)=⇒ (Du [v] = 1 + min ndisu [w, v] = 1 + ndisu [Nbu [v] , v])w∈Neighu∧ (u 6= v ∧ ∀w ∈ Neighu : ndisu [w, v] > N − 1)=⇒ (Du [v] = N ∧ Nbu [v] = udef)Рис.
4.10. Инварианты P(u, w, v) и L(u, v)(1)(2)(3)(4)(5)(6)141Инварианты алгоритма Netchange. Мы установим, что утверждения, приведенные на рис. 4.10, являются инвариантами. Формула P(u, w, v) выражаетутверждение о том, что если процесс u завершил обработку сообщений типа mydist, полученных от процесса w, то оценка расстояния d(w, v) в узле u совпадаетс оценкой расстояния d(w, v) в узле w. Мы будем считать, что предикат up(u, w)принимает значение true тогда и только тогда, когда между узлами u и w есть(двунаправленный) исправный канал связи. Формула L(u, v) гласит, что оценки расстояний d(u, v) и содержимое списка Nbu [v] в узле u всегда согласованос теми данными, которые хранятся в локальной памяти узла u.Вычисление алгоритма завершается, когда в каналах связи не остается ни одного сообщения, находящегося на этапе пересылки.
Конфигурации такого вида неявляются заключительными конфигурациями для всей системы в целом, потомучто вычисление системы может быть продолжено, после того как какой-нибудьканал выйдет из строя или восстановит свою работоспособность (что потребуетреакции со стороны алгоритма). Конфигурацию, не имеющую в каналах связи ниодного сообщения, мы будем называть стабильной; предикат stable определяется следующим соотношением:stable ≡ ∀ u, w : up(u, w) =⇒ Qwu не содержит сообщений типа mydist.Необходимо принять во внимание, что первоначально каждый список Neigh uправильно отражает наличие и работоспособность каналов связи между узлами,т.
е. первоначально соотношение (1) считается верным. Чтобы доказать инвариантность приведенных утверждений, мы должны рассмотреть три типа переходов.1. Прием сообщения типа mydist. Все выполнение соответствующего фрагмента кода проводится автоматически и укладывается в один переход. В этом переходе происходит прием одного сообщения и (возможно) отправление нескольких сообщений.2. Обрыв канала и обработка сообщения типа fail в узлах по обе стороныканала.3. Восстановление канала и обработка сообщения типа repair в обоих узлах,соединенных этим каналом.Лемма 4.14.
Для любой тройки вершин u0 , w0 и v0 формула P(u0 , w0 , v0)является инвариантом.Д о к а з а т е л ь с т в о. В самом начале после выполнения процедуры инициализации в каждом узле соотношение (1) выполняется согласно сделанномудопущению. Если первоначально выполняется условие ¬up(u 0 , w0), то соотношения (2) и (3), очевидно, выполняются. Если же вначале выполняется условие up(u0 , w0), то имеет место равенство ndisu0 [w0 , v0 ] = N. Если w0 = v0 , тоDw0 [w0 ] = 0, но при этом в очереди Qw0 u0 содержится сообщение hmydist, v0 , 0i,и поэтому верны соотношения (2) и (3).
Если w0 6= v0 , то Dw0 [v0 ] = N и в очередиканала нет сообщений, поэтому соотношения (2) и (3) также будут верны. Теперьрассмотрим поочередно три типа переходов, которые были упомянуты выше.142Гл. 4. Алгоритмы маршрутизацииТип 1. Предположим, что узел u получает сообщение hmydist, v, di от узлаw. Это не влечет за собой никаких изменений топологии сети, и поэтому спискивершин-соседей Neigh не изменяются, и соотношение (1) остается верным. Еслиv 6= v0 , то с получением этого сообщения в формуле P(u0 , w0 , v0) ничего неизменяется.Если v = v0 , u = u0 и w = w0 , то значение ndisu0 [w0 , v0 ] может измениться.
Однако если в канале связи есть еще одно сообщение типа mydist, тозначения, содержащиеся в этом сообщении, удовлетворяют соотношению (2), ипоэтому выполнимость соотношения (2) сохраняется. Выполнимость соотношения (3) также сохраняется, поскольку его предпосылка ложна. Если полученноесообщение было последним сообщением в очереди сообщений этого канала, тосогласно соотношению (2) имеет место равенство d = D w0 [v0 ] . Отсюда следует,что заключение формулы (3) становится истинным, и, значит, соотношение (3)остается верным. Поскольку предпосылка утверждения (2) становится ложной,выполнимость соотношения (2) сохраняется.Если v = v0 , u = w0 (и u0 является соседом вершины u), то заключения утверждений (2) или (3) могут стать ложными в том случае, когда значение D w0 [v0 ]изменяется в результате выполнения процедуры Перевычислить(v) в узле w 0 .Однако в этом случае сообщение hmydist, v0 , .
. . i с новым значением отправляется узлу u0 , и это приводит к тому, что предпосылка утверждения (3) становитсяложной, а заключение утверждения (2) становится истинным; поэтому оба утверждения (2) и (3) остаются верными. Это единственно возможный случай, когдасообщение hmydist, v0 , . . . i становится в очередь Qw0 u0 , и в этом случае имеетместо равенство d = Dw0 [v0 ] .Если v = v0 и u 6= u0 , w0 , то в формуле P(u0 , w0 , v0) ничего не изменяется.Тип 2. Предположим, что канал uw выходит из строя.Если u = u0 и w = w0 , то возникшая неисправность канала приводит ктому, что предпосылки утверждений (2) и (3) становятся ложными, и поэтомувыполнимость этих утверждений сохраняется.
Выполнимость утверждения (1)сохраняется, ввиду того что w0 удаляется из списка Neighu0 . То же самое имеетместо и в случае u = w0 и w = u0 .Если u = w0 , но w 6= u0 , то заключения утверждений (2) и (3) могут статьложными, поскольку может измениться значение D w0 [v0 ] . Однако в этом случаепосле отправления узлом w0 сообщения hmydist, v0 , ..i предпосылка утверждения (3) становится ложной, а заключение утверждения (2) становится истинным,и поэтому выполнимость утверждений (2) и (3) сохранется.Во всех остальных случаях в формуле P(u0 , w0 , v0) не происходит никакихизменений.Тип 3. Предположим, что в сети появился канал uw.Если u = u0 и w = w0 , то предикат up(u0 , w0) принимает значение true,но ввиду того что вершина w0 добавляется в список Neighu0 (а вершина u0 —в список Neighw0), выполнимость утверждения (1) сохраняется.После отправления узлом w0 сообщения hmydist, v0 , Dw0 [v0 ] i заключениеутверждения (2) становится истинным, а предпосылка утверждения (3) становится ложной, и поэтому выполнимость формулы P(u 0 , w0 , v0) сохраняется.4.3.
Алгоритм Netchange143Во всех остальных случаях в формуле P(u0 , w0 , v0) не происходит никакихизменений.Лемма 4.15. Для любой пары вершин u0 и v0 формула L(u0 , v0) являетсяинвариантом.Д о к а з а т е л ь с т в о. Первоначально Du0 [u0 ] = 0 и Nbu0 [u0 ] = local.Если v0 6= u0 , то в самом начале ndisu0 [w, v0 ] = N для всех w ∈ Neighu , Du0 [v0 ] == N и Nbu0 [v0 ] = udef.Тип 1.
Предположим, что узел u получает сообщение hmydist, v, di от узла w.Если u 6= u0 или v 6= v0 , то ни одна переменная, фигурирующая в формулеL(u0 , v0), не изменяет значения. Если u = u0 и v = v0 , то значение переменной ndisu0 [w, v0 ] изменяется, но при этом Du0 [v0 ] и Nbu0 [v0 ] перевычисляютсяв точности так, чтобы выполнялось утверждение L(u 0 , v0).Тип 2. Предположим, что канал uw оказывается неисправным.Если u = u0 или w = u0 , то список Neighu0 изменяется, но при этом значенияDu0 [v0 ] и Nbu0 [v0 ] вновь перевычисляются в точности так, чтобы выполнялосьутверждение L(u0 , v0).Тип 3. Предположим, что в сети образуется новый канал uw.Если u = u0 , то список Neighu0 изменяется за счет добавления вершины w, ноколь скоро в узле u значение переменной ndisu0 [w, v0 ] устанавливается равнымN, выполнимость формулы L(u0 , v0) сохраняется.4.3.2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
