Реферат: Распределенные алгоритмы
Алгоритм реагирует на отказы и восстановления каналов изменением локальных таблиц, и посылая сообщение <mydist, ., .> если оценка расстояния изменилась. Мы предположим что уведомление которое узлы получают о падении или подъеме канала (предположение N3) представлено в виде сообщений < fail,. > и <repair, . >. Канал между узлами u1 и u2 смоделирован двумя очередями, Q u1 u2 для сообщений от u1 к u1 и Q u2 u1 для сообщений из u2 в u1. Когда канал отказывает эти очереди удаляются из конфигурации (фактически вызывается потеря всех сообщений в обоих очередях) и узлы на обоих концах канала получают сообщение < fail, . > . Если канал между u1 и u1 отказывает, u1 получает сообщение < fail, u2 > и u2 получает сообщение < fail, u1 > . Когда канал восстанавливается (или добавляется новый канал в сети) две пустые очереди добавляются в конфигурацию и два узлы соединяются через канал получая сообщение < repair, . > . Если канал между u1 и u2 поднялся u1 получает сообщение< repair, u2 > и u2 получает сообщение < repair, u1 > .
Обработка сообщения <mydist,v,d> от соседа w:
{ <mydist,v,d> через очередь Qwv}
begin получить <mydist,v,d> от w;
ndisu[w,v] := d ; Recompute (v)
end
Произошел отказ канала uw:
begin получить < fail, w> ; Neighu := Neighu \ {w} ,
forall v Î V do Recompute (v)
end
Произошло восстановление канала uw:
begin получить < repair, w> , Neighu := Neighu È {w} ;
forall v Î V do
begin ndisu[w, v] := N;
послать < mydist, v, Du{[v]> to w
end
end
Алгоритм 4.9 АЛГОРИТМ NETCHANGE (часть 2, для узла и).
Реакция алгоритма на отказы и восстановления выглядит следующим образом. Когда канал между u и w отказывает, w удаляется из Neighu и наоборот. Оценка расстояния перевычисляется для каждого пункта назначения и, конечно, рассылается всем существующим соседям если оно изменилось. Это случай если лучший маршрут был через отказавший канал и нет другого соседа w' с ndisu[w', v]= ndisu[w, v]. Когда канал восстановлен(или добавлен новый канал) то w добавляется в Neighu, но u имеет теперь неоцененное расстояние d(w, v) (и наоборот). Новый сосед w немедленно информирует относительно Du[v] для всех пунктов назначения v (посылая сообщения<mydist,v, Du[v]> ). До тех пор пока u получает подобное сообщения от w, u использует N как оценку для d(w,v), т.е., он устанавливает ndisu[w, v] в N.
P(u, w, V)º
up(u, w) Û w Î Neighu (1)
Ù up(u, w) Ù Qwu содержит сообщение <mydist,v,d> Þ
последнее такое сообщение удовлетворят d = Du[v] (2)
Ù up(u, w) Ù Qwu не содержит сообщение <mydist,v,d> Þ
ndisu[w, v] =Dw [v] (3)
L(u, v) º
u = v Þ (Du[v] = 0 Ù Nbu[v] = local) (4)
Ù (u ¹ v)Ù $w Î Neighu : ndisu[w, v] < N - 1)Þ
( Du[v] = 1 + min ndisu[w, v] = 1 + ndisu[Nbu[v], v]) (5)
w Î Neigh u
Ù (u ¹ v Ù "w Î Neighu : ndisu[w, v]³ N—1) Þ
(Du[v] = N Ù Nbu[v] = udef) (6)
Рисунок 4.10 Инварианты P(u, w, v) и L(u, v).
Инварианты алгоритма Netchange. Мы докажем что утверждения являются инвариантами; утверждения даны на Рисунке 4.10. Утверждение P(u, w, v) констатирует что если u закончил обработку сообщения <mydist, v, .> от w то оценка u расстояния d(w,v) эквивалентна оценке w расстояния d(w, v). Пусть предикат up(u, w) истинен тогда и только тогда когда (двунаправленный) канал между u и w существует и действует. Утверждение L(u, v) констатирует что оценка u расстояния d(u, v) всегда согласована с локальными данными u, и Nbu[v] таким образом означен.
Выполнение алгоритма заканчивается когда нет больше сообщений в любом канале. Эти конфигурации не терминальны для всей системы так как вычисления в системе могут продолжится позже, начавшись отказом или восстановлением канала (на которые алгоритм должен среагировать). Мы пошлем сообщение конфигурационной стабильности, и определим предикат stable как
stable = "u, w : up(u, w) Þ Qwu не содержит сообщений <mydist,., .>.
Это предполагает что переменные Neighu корректно отражают существующие рабочие коммуникационные каналы, т.е., что (1) существует изначально. Для доказательства инвариантности утверждений мы должны рассмотреть три типа переходов.
(1) Получение сообщения <mydist, .,.> . Первое выполнение результирующего кодового фрагмента, как принято, выполняется автоматически и рассматривается отдельным переходом. Обратите внимание что в данном переходе принимается сообщение и возможно множество сообщений отправляется
(2) Отказ канала и обработка сообщения < fail. . > узлами на обоих концах канала.
(3) Восстановление канала и обработка сообщения <repair. . > двумя соединенными узлами.
Лемма 4.14 Для всех uo, wo, и vo, P(uo, wo, vo) –– инвариант.
Доказательство. Изначально, т.e., после выполнения инициализационной процедуры каждым узлом, (1) содержится предположением. Если изначально мы имеем Øup(uo, wo), (2) и (3) тривиально содержатся. Если изначально мы имеем up(uo, wo), тогда ndisuo[wo, vo] = N. Если wo = vo то Dwo[wo] = 0 но сообщение < mydist, vo, 0> в Qw0u0, таким образом (2) и (3) истинны. Если wo ¹ vo то Dw0[vo]=N и нет сообщений в очереди, что также говорит что (2) и (3) содержаться. Мы рассмотрим три типа констатированных переходов упомянутых выше.
Тип (1). Предположим что u получает сообщение <mydist,v,d> от w. Следовательно нет топологических изменений и нет изменений в множестве Neigh , следовательно (1) остается истинно. Если v¹vo то это сообщение не меняет ничего в P(uo, wo, vo). Если v = vo, u =uo, и w=wo значение ndisu,[wo, vo] может изменится. Однако, если сообщение < mydist, vo, .> остается в канале значение этого сообщения продолжает удовлетворять (2), так как (2) в сохранности то и (3) также потому что посылка ложна. Если полученное сообщение было последним этого типа в канале то d = Dw0[vo] по (2), которое подразумевает что заключение (3) становится истинным и (3) в сохранности. Посылка (2) становится ложной, таким образом (2) в сохранности. Если v = vo, u = wo (и uo сосед u) заключение (2) или (3) может быть ложно если значение Dw0[vo] изменилось в следствие выполнения Recompute(v) в wo. В этом случае, однако, сообщение < mydist, vo, . > с новым значением посылается к uo, которое подразумевает что посылка (3) нарушена, и заключение (2) становится истинным, таким образом (2) и (3) сохранены. Это происходит и в случае когда сообщение < mydist, vo, . > добавляется в Qw0u0, и это всегда удовлетворяет d = Dw0[vo]. Если v = vo и u¹uo, wo ничего не изменяет в P(uo, wo, vo).
Тип (2). Предположим что канал uw отказал. Если u = uo и w = wo этот отказ нарушил посылку (2) и (3) таким образом эти правила сохранены. (1) в безопасности потому что wo удалился из Neighu0 и обратно. Нечто произойдет если u = wo и w = uo. Если u = wo но w¹ uo заключение (2) или (3) может быть нарушено так как значение Dw0 [vo] изменилось. В этом случае пересылка сообщения < mydist, vo, . > узлом wo опять нарушит посылку (3) и сделает заключение (2) истинным, следовательно (2) и (3) в безопасности. Во всех других случаях нет изменений в P(uo, wo, vo).
Тип (3). Предположим добавление канала uw. Если u = uo и w = wo то up(vo,wo) истинно, но добавлением wo в Neighu0 (и обратно) это защищает(1). Посылка < mydist, vo, Dw0 [vo]> узлом wo делает заключение (2) истинным и посылку (3) ложной, таким образом P(uo, wo, vo) обезопасен. Во всех других случаях нет изменений в P(uo, wo, vo).
ˆ
Лемма 4.15 Для каждого uq и vo, L(uo, vo) –инвариант.
Доказательство. Изначально Du0[uo] = 0 и Nbu[uo] = local. Для vo ¹uo , изначально ndisu[w, vo] = N для всех w Î Neighu, и Du0[vo] = N и Nbu0[vo] = udef.
Тип (1). Положим что u получил сообщение < mydist, v,d> от w. Если u¹ uo или v¹ vo нет переменных упомянутых изменениях L(uo, vo) . Если u = uo и v = vo значение ndisu[w, vo] меняется, но Du0 [vo] и Nbu0[vo] перевычисляется точно так как удовлетворяется L(vo, vo).
Тип (2). Положим что канал uw отказал. Если u = uo или w = uo то Neighu0 изменился, но опять Du0[vo] и Nbu0[vo] перевычисляются точно так как удовлетворяется L(uo, vo).
Тип (3). Положим что добавлен канал uw . Если u = uo то изменилсяNeighu0 добавлением w, но так как u устанавливает ndisu0[w, vo] в N это сохраняет L(uo, vo).
4.3.2 Корректность алгоритма Netchange
Должны быть доказаны два требования корректности.
Теорема 4.16 Когда достигнута стабильная конфигурация, таблицы Nbu[v] удовлетворяют :
(1) если u = v то Nbu[v] = local;
(2) если путь от u до v¹ u существует то Nbu[v] = w, где w первый сосед u на кратчайшем пути от u до v;
(3) если нет путь от u до v не существует то Nbu[v] = udef.
Доказательство. Когда алгоритм прекращает работу, предикат stable добавляется к P(u,w,v) для всех u, v, и w, и это подразумевает что для всех u, v, и w
up(u, w) Þ ndisu[w, v] = Dw[v]. (4.2)
Применив также L(u, v) для всех u и v мы получим
ì0 если u ¹ v
Du [v] = í 1+ min Dw[v] если u¹ v Ù$w Î Neighu : Dw[v] < N -1
îN w ÎNeigh u если u¹v Ù"w Î Neighu : Dw[v]³ N -1
(4.3)
которого достаточно для доказательства что Du[v] = d(u, v) если u и v в некотором связном компоненте сети, и Du[v] = N если u и v в различных связных компонентах.
Во-первых покажем индукцией по d{u, v) что если u и v в некотором связном компоненте то Du[v]£ d(u, v).
Случай d(u, v) = 0: подразумевает u = v и следовательно Du[v] = 0.
Случай d(u, v) = k +1: это подразумевает что существует узел w Î Neighu с d(w, v) = k. По индукции Du[v] £ k, которое по (4.3) подразумевает что Du[v] £ k + 1.
Теперь покажем индуктивно по Du[v] что если Du[v] < N то существует путь между u и v и d(u, v) £ Du[v].
Случай Du[v] = 0: Формула (4.3) подразумевает что Du[v] = 0 только для u = v, что дает пустой путь между u и v, и d(u, v) = 0.
Случай Du[v] = k +1 < N : Формула (4.3) подразумевает что существует узел w Î Neighu с Dw[v] = k. По индукции существует путь между w и v и d(w, v) £ k, что подразумевает существование пути между u и v и d(u, v) < k+ 1.
Следовательно что если u и v в некотором связном компоненте то Du[v] = d(u, v), иначе Du[v] = N. Это, Формула (4.2), и "u,v : L(u, v) и доказывает теорему о Nbu[v]. []
Докажем что стабильная ситуация в конечном счете достигается если топологические изменения прекращаются, норм-функция в отношении stable определена. Определим, для конфигурации алгоритма g,
ti = (число сообщений <mydist, .,i>) +
(число упорядоченных пар u, v таких что Du[v] = i)
и функцию f
f(g) = (to, t1,..., tN)
f(g) кортеж из (N + l) натуральных чисел, в некотором лексиграфическом порядке (обозначенном £l) . напомним что (N, £l) хорошо-обоснованное множество (Упражнение 2.5).
Лемма 4.17 Обработка сообщения < mydist,.,. > уменьшает f.
Доказательство. Пусть узел u с Du[v] = d1 получил сообщение < mydist, v, d2> , и после перевычислил новое значение Du[v] – d. Алгоритм подразумевает что d < di + 1.
Случай d < d1: Пусть d = d1 + 1 что подразумевает что td2 уменьшилось на 1 (и td1 следовательно), и только td с d > d1 увеличилось. Это подразумевает что значение f уменьшилось.
Случай d = d1: Не новое сообщение < mydist, ., .> посланное u, и влияет только на f так что td2 уменьшилось на 1, т.о. значение f уменьшилось.
Случай d > d1: Пусть td1 уменьшилось на 1 (и td2 следовательно), и только td с d > d1 увеличилось. Это подразумевает что значение f уменьшилось.
[]
Теорема 4.18 Если топология сети остается неизменной после конечного числа топологических изменений, то алгоритм достигнет стабильной конфигурации за конечное число шагов.
Страницы: 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, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62
