Реферат: Распределенные алгоритмы
Тип (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 Если топология сети остается неизменной после конечного числа топологических изменений, то алгоритм достигнет стабильной конфигурации за конечное число шагов.
Доказательство. Если сетевая топология остается постоянной только обрабатывая сообщения <mydist,.,.>которые имеют место, и, по предыдущей лемме, значение f уменьшается с каждым таким переходом. Это следует из хорошей обоснованности области f в которой может быть только конечное число таких переходов; следовательно алгоритм достигает стабильной конфигурации после конечного числа шагов. []
Формальные результаты правильности алгоритма, гарантирующие сходимость для исправления таблиц за конечное время после последнего топологического изменения, не очень хорошо показывают фактическое поведение алгоритма. Предикат stablе может быть ложным практически долгое время (а именно, если топологические изменения часты) и когда stablе ложен, ничто не известно о таблицы маршрутизации. Они могут содержать циклы или даже давать ошибочную информацию относительно достижимости узла назначения. Алгоритм поэтому может только применятся, где топологические изменения настолько редки, что время сходимости алгоритма является малым по сравнению с средним временем между топологических изменений. Тем более , потому что stablе - глобальное свойство, и устойчивые конфигурации алгоритма неразличимы от неустойчивых для узлов. Это означает, что узел никогда не знает, отражают ли таблицы маршрутизации правильно топологию сети, и не может отсрочить отправления пакетов данных , пока устойчивая конфигурация не достигнута.
Страницы: 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, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105
