Введение в распределённые алгоритмы. Ж. Тель (2009) (1185665), страница 39
Текст из файла (страница 39)
Конфигурацию, не имеющую в каналах связи ниодного сообщения, мы будем называть стабильной; предикат stable определяется следующим соотношением:stable = V и, да : ир(и, да) =£■ Qwa не содержит сообщений типа mydist.Необходимо принять во внимание, что первоначально каждый список Neighuправильно отражает наличие и работоспособность каналов связи между узлами,т. е.
первоначально соотношение (1) считается верным. Чтобы доказать инвариантность приведенных утверждений, мы должны рассмотреть три типа переходов.1. Прием сообщения типа mydist. Все выполнение соответствующего фрагмента кода проводится автоматически и укладывается в один переход. В этом переходе происходит прием одного сообщения и (возможно) отправление нескольких сообщений.2. Обрыв канала и обработка сообщения типа fail в узлах по обе стороныканала.3. Восстановление канала и обработка сообщения типа repair в обоих узлах,соединенных этим каналом.Лемма 4.14. Для любой тройки вершинявляется инвариантом.даои vo формула Р(ио,дао, vo)Д о к а з а т е л ь с т в о . В самом начале после выполнения процедуры инициализации в каждом узле соотношение ( 1 ) выполняется согласно сделанномудопущению. Если первоначально выполняется условие ~^ир(ио, дао), то соотношения (2) и (3), очевидно, выполняются.
Если же вначале выполняется условие ир{щ, дао), то имеет место равенство ndisUo[wo, wo] = N. Если дао = vo, тоDWo[wo\ = 0, но при этом в очереди QW[)U[) содержится сообщение (mydist, Vo, 0),и поэтому верны соотношения (2) и (3). Если да0 ф Vo, то DWo[у0] = N и в очередиканала нет сообщений, поэтому соотношения (2) и (3) также будут верны.
Теперьрассмотрим поочередно три типа переходов, которые были упомянуты выше.Гл. 4. Алгоритмы маршрутизации142Тип 1. Предположим, что узел и получает сообщение (mydist, у, d) от узлада. Это не влечет за собой никаких изменений топологии сети, и поэтому спискивершин-соседей Neigh не изменяются, и соотношение (1) остается верным. Еслиd ^ Do, то с получением этого сообщения в формуле Р(ио, дао, уо) ничего неизменяется.Если v = Уо, и = Чо и да = wo, то значение ndisUQ[wo, Уо] может измениться. Однако если в канале связи есть еще одно сообщение типа mydist, тозначения, содержащиеся в этом сообщении, удовлетворяют соотношению (2 ), ипоэтому выполнимость соотношения (2) сохраняется.
Выполнимость соотношения (3) также сохраняется, поскольку его предпосылка ложна. Если полученноесообщение было последним сообщением в очереди сообщений этого канала, тосогласно соотношению (2) имеет место равенство d = DWo[vо]. Отсюда следует,что заключение формулы (3) становится истинным, и, значит, соотношение (3)остается верным. Поскольку предпосылка утверждения (2) становится ложной,выполнимость соотношения (2 ) сохраняется.Если v = vq, и = wo (и Uq является соседом вершины и), то заключения утверждений (2) или (3) могут стать ложными в том случае, когда значение DWo[vо]изменяется в результате выполнения процедуры Перевычислить(р) в узле дао.Однако в этом случае сообщение (mydist, уо, .
. . ) с новым значением отправляется узлу U , и э т о приводит к тому, что предпосылка утверждения (3) становитсяложной, а заключение утверждения (2 ) становится истинным; поэтому оба утверждения (2) и (3) остаются верными. Это единственно возможный случай, когдасообщение (mydist, Уо, . . . ) становится в очередь QWou0> и в этом случае имеетместо равенство d = DWo[vo\.Если у = Уо и и Ф ио, wo, то в формуле Р(ио, дао, уо) ничего не изменяется.Тип 2. Предположим, что канал мда выходит из строя.Если и = Uq и да = дао, то возникшая неисправность канала приводит ктому, что предпосылки утверждений (2 ) и (3) становятся ложными, и поэтомувыполнимость этих утверждений сохраняется.
Выполнимость утверждения (1)сохраняется, ввиду того что дао удаляется из списка NeighUo. То же самое имеетместо и в случае и = дао и да = ио.Если и = wo, но w Ф Uq, то заключения утверждений (2) и (3) могут статьложными, поскольку может измениться значение DWo[vо]. Однако в этом случаепосле отправления узлом дао сообщения (mydist, vo, ..) предпосылка утверждения (3) становится ложной, а заключение утверждения (2 ) становится истинным,и поэтому выполнимость утверждений (2 ) и (3) сохранется.Во всех остальных случаях в формуле P(uq, дао, Уо) не происходит никакихизменений.Тип 3. Предположим, что в сети появился канал мда.Если и = Uq и да = дао, то предикат ир(ио, дао) принимает значение true,но ввиду того что вершина дао добавляется в список NeighUo (а вершина ио —в список NeighWo), выполнимость утверждения (1) сохраняется.После отправления узлом дао сообщения (mydist, Уо, DWq[vо]) заключениеутверждения (2 ) становится истинным, а предпосылка утверждения (3) становится ложной, и поэтому выполнимость формулы Р(ио, wo, У о ) сохраняется.q4.3.
Алгоритм Netchange143Во всех остальных случаях в формуле P( uq, дао , Vq) не происходит никаких□изменений.Лемма 4.15. Для любой пары вершин ио и vq формула L( uq,инвариантом.vq)являетсяД о к а з а т е л ь с т в о . Первоначально DU[)[uo\ = 0 и NbUo[uo\ = local.Если Vo Ф ио, то в самом начале ndisUo[w, t>o] = N для всех w eNeigha, D u0 [у0] == jV и NbUo[vo\ = udef.Тип 1. Предположим, что узел и получает сообщение (mydist, v, d) от узла да.Если и Ф ио или v ф Vo, то ни одна переменная, фигурирующая в формулеL(uo, Vo), не изменяет значения.
Если и = м0 и v = vq, т о значение переменной ndisUo[w, ио] изменяется, но при этом DU[)[vо] и NbUo[vo\ перевычисляютсяв точности так, чтобы выполнялось утверждение L{ uq, do).Тип 2. Предположим, что канал uw оказывается неисправным.Если и = ио или да = «о, то список NeighUo изменяется, но при этом значенияDUo[vо] и NbUo[vo\ вновь перевычисляются в точности так, чтобы выполнялосьутверждение L{ uq, Vo).Тип 3. Предположим, что в сети образуется новый канал uw.Если и = ио, то список Neighua изменяется за счет добавления вершины да, ноколь скоро в узле и значение переменной ndisUo[w, ио] устанавливается равнымN, выполнимость формулы L( uq, Vq) сохраняется.□4.3.2.
Корректность алгоритма NetchangeТеперь мы докажем два требования корректности для рассматриваемого алгоритма.Теорема 4.16. Как только достигается стабильная конфигурация , таблицы Nbu[v] удовлетворяют следующим условиям1) если и = v, то Nbu[v] = local;2) если существует путь из вершины и в вершину v Ф и, то Nbu[v] == да, где да — первый сосед вершины и, который встречается накратчайшем пути из и в v;3) если пути из вершины и в вершину v не существует, то Nbu[v] == udef.Д о к а з а т е л ь с т в о . Когда алгоритм завершает свое выполнение, нарядус предикатом stable выполняется и формула Р(и, да, v) для всех троек вершин и,и и да, и отсюда следует, что для всех троек и, о и да справедливо соотношение(4.2)Гл. 4. Алгоритмы маршрутизации144Принимая во внимание утверждение L(u, v) для всех пар вершин и и и, мы получаем следующее соотношение:О,1+{min Dw[v],если и = V,если и ф v A 3w е Neighu: Dw[v] < N — 1,weNeighaN,(4 3)v'если и ф у A Vffii е Neigh a : Dw[и] > N - 1.которого достаточно, чтобы доказать, что Du[u] = d(u, v) всякий раз, когда вершины и и v находятся в одной и той же компоненте связности сети, и Du[v] = N,если и и v находятся в разных компонентах связности.Вначале мы покажем, воспользовавшись индукцией по d(u, v), что всякийраз, когда вершины и и и находятся в одной и той же компоненте связности сети,верно неравенство Du[v\ ф d(u, v).Случай d (u , v) = 0.
В этом случае u = v, и поэтому Du\u\ = 0.Случай d (u , v) = k + 1. В этом случае существует такая вершина w ( E N e i g h a.для которой d(w, v ) = k. По индуктивному предположению Dw[v\ ^ k, и отсюдавследствие соотношения (4.3) мы получаем Da[v] ^ k + 1.Теперь мы продемонстрируем, воспользовавшись индукцией по Da[v\, чтовсякий раз, когда Du[v] < N, из вершины и в вершину v существует путь, и приэтом d(u, v ) ^ Du[v],Случай D u [v] = 0. Из формулы (4.3) следует, что l ) u \v \ = 0 только тогда,когда и = v; это означает, что между вершинами и ии есть пустой путь и d(u, и) == 0.Случай D u [v] = k + 1 < N. Из формулы (4.3) следует, что существует такая вершина w € Neighu, для которой Dw\v] = k.
По индуктивному предположению между вершинами w и v существует путь и d(w, v) ф k; отсюда следует, чтомежду вершинами и и v также есть путь и d(u, v) ^ k + 1 .Таким образом, если и н и находятся в одной и той же компоненте связности, то Du[v] = d(u, v ) , а в противном случае Du[v] = N. Отсюда, принимаяво внимание формулу (4.2) и предложение \/и, v : L(u, v), получаем заявленныйв утверждении теоремы результат о таблицах Nbu[v],□Чтобы убедиться в том, что стабильная ситуация рано или поздно наступит,после того как завершатся изменения топологии, мы введем нормирующую функцию по отношению к предикату stable. Для конфигурации у нашего алгоритмабудем полагатьU = (число сообщений типа (mydist, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
