Ù (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>) +
Страницы: 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
