6 Алгоритм Netchange. Разнообразие алгоритмов маршрутизации, страница 2

åãî ïðåäïîñûëêà ëîæíà.Åñëè â Qw u áîëüøå íåò ñîîáùåíèé îá óçëå v0 , òî ñîãëàñíî (2)âåðíî d = Dw [v0] , è (3) ñòàíîâèòñÿ âåðíûì. Ò.ê. ïðåäïîñûëêàóòâåðæäåíèÿ (2) ñòàíîâèòñÿ ëîæíîé, (2) îñòàåòñÿ âåðíûì.0 00 000Proc-1 : Îáðàáîòêà ñîîáùåíèÿ h, v , di îò ñîñåäà w :{ Ñîîáùåíèå h, v , di â íà÷àëå î÷åðåäè Qwu }receive h, v , di from w ;ndisu [w , v ] := d ; Update (v )mydistmydistbeginmydistendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]v = v0 , u = w0 u0u,v0 ,di(3)Åñëèè ñîñåä , òî çàêëþ÷åíèÿóòâåðæäåíèé (2) èëè (3) ìîãóò ñòàòü ëîæíûìè â òîì ñëó÷àå,êîãäà çíà÷åíèå Dw [v0] èçìåíÿåòñÿ â ðåçóëüòàòå âûïîëíåíèÿïðîöåäóðû Update (v ) â óçëå w0 .0Ïðîöåäóðà Update(v )begin ififv =u···ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xthenforalldomydistendw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hmydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,,v0 ,div0 ] = Dw0 [v0 ]Dw0 [v0 ](3)Íî èçìåíåíèå çíà÷åíèÿïðîöåäóðîé Update (v0) â óçëåñîïðîâîæäàåòñÿ îòïðàâêîé ñîîáùåíèÿ h, v0 , ..i ñíîâûì çíà÷åíèåì óçëó u0 .

Ïîñëå ýòîãî ïðåäïîñûëêà (3)ñòàíîâèòñÿ ëîæíîé, à çàêëþ÷åíèå (2) èñòèííûì.Ýòî åäèíñòâåííûé ñëó÷àé, êîãäà ñîîáùåíèå h, v0 , ..iñòàíîâèòñÿ â î÷åðåäü Qw u . Òîãäà d = Dw [v0] .w0mydistmydist0 00Ïðîöåäóðà Update(v )begin ififv =u···ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xthenforalldomydistendw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hmydist(1), v0 , di(2)0mydist0 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]v = v0 u 6= u0 , w0Åñëèèíå èçìåíÿåòñÿ.,v0 ,di(3), òî â ôîðìóëå P(u0, w0, v0) íè÷åãîProc-2 :  ñëó÷àå âûõîäà èç ñòðîÿ êàíàëà uw :receive h , w i ; Neighu := Neighu \ {w } ;beginfailforallv ∈VdoUpdate(v )endw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hmydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ](uw ),v0 ,di(3)Ïðåäïîëîæèì, ÷òî êàíàëâûõîäèò èç ñòðîÿ.Åñëè u = u0, w = w0 , òî âîçíèêøàÿ íåèñïðàâíîñòü êàíàëàïðèâîäèò ê òîìó, ÷òî ïðåäïîñûëêè (2) è (3) ñòàíîâÿòñÿëîæíûìè, è ïîýòîìó âûïîëíèìîñòü ýòèõ óòâåðæäåíèéñîõðàíÿåòñÿ.

Âûïîëíèìîñòü (1) ñîõðàíÿåòñÿ, ââèäó òîãî ÷òî w0óäàëÿåòñÿ èç ñïèñêà Neighu .Òî æå ñàìîå èìååò ìåñòî è â ñëó÷àå u = w0 è w = u0 .0Proc-2 :  ñëó÷àå âûõîäà èç ñòðîÿ êàíàëà uw :receive h , w i ; Neighu := Neighu \ {w } ;beginfailforallv ∈VdoUpdate(v )endup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]u = w0w 6= u0Update (v0 )Dw0 [v0 ]Åñëè, íîëîæíûìè, ïîñêîëüêóçíà÷åíèå.,v0 ,di(3), òî çàêëþ÷åíèÿ (2) è (3) ìîãóò ñòàòüâ óçëå w0 ìîæåò èçìåíèòüÏðîöåäóðà Update(v )begin ififv =u···ïåðåìåííàÿ Du [v ] èçìåíèëà çíà÷åíèåx ∈ Neighusend h, v , Du [v ]i to xthenforalldomydistendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒w0ndisu0 [w0 ,v0 ] = Dw0 [v0 ]hmydist, v0 , ..i,v0 ,di(3)Íî îòïðàâëÿåò ñîîáùåíèÿ, è ïðåäïîñûëêà (3)ñòàíîâèòñÿ ëîæíîé, à çàêëþ÷åíèå (2) ñòàíîâèòñÿ èñòèííûì.Ïîýòîìó ñïðàâåäëèâîñòü (2) è (3) ñîõðàíÿåòñÿ.Proc-2 :  ñëó÷àå âûõîäà èç ñòðîÿ êàíàëà uw :receive h , w i ; Neighu := Neighu \ {w } ;beginfailforallv ∈VdoUpdate(v )endw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hmydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ]P(u0 , w0 , v0 )Âî âñåõ îñòàëüíûõ ñëó÷àÿõ âèçìåíåíèé.,v0 ,diíå ïðîèñõîäèò(3)Proc-3 :  ñëó÷àå âîññòàíîâëåíèÿ êàíàëà uw :receive h, w i ; Neighu := Neighu ∪ {w } ;beginrepairforallv ∈Vbegindondisu [w ,v ] := N; send hmydist, v , Du [v ]ito wendendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0(1)mydist, v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ],v0 ,di(3)Ïðåäïîëîæèì, ÷òî â ñåòè ïîÿâèëñÿ êàíàë (uw ) .

Òîãäà Proc-3âûïîëíÿåòñÿ ñèíõðîííî â îáîèõ óçëàõ u è v .Åñëè u = u0, w = w0 , òî ïðåäèêàò up(u0, w0) ïðèíèìàåòçíà÷åíèå true, íî ââèäó òîãî ÷òî âåðøèíà w0 äîáàâëÿåòñÿ âñïèñîê Neighu (à âåðøèíà u0 â ñïèñîê Neighw ),âûïîëíèìîñòü óòâåðæäåíèÿ (1) ñîõðàíÿåòñÿ.00Proc-3 :  ñëó÷àå âîññòàíîâëåíèÿ êàíàëà uw :receive h, w i ; Neighu := Neighu ∪ {w } ;beginrepairforallv ∈Vbegindondisu [w ,v ] := N; send hmydist, v , Du [v ]ito wendendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ]w0,v0 ,di(3)hmydist, v0 , Dw0 [v0 ]iÏîñëå îòïðàâëåíèÿ óçëîì ñîîáùåíèÿçàêëþ÷åíèå óòâåðæäåíèÿ (2) ñòàíîâèòñÿ èñòèííûì, àïðåäïîñûëêà óòâåðæäåíèÿ (3) ñòàíîâèòñÿ ëîæíîé, è ïîýòîìóâûïîëíèìîñòü ôîðìóëû P(u0, w0, v0) ñîõðàíÿåòñÿ.Âî âñåõ îñòàëüíûõ ñëó÷àÿõ â ôîðìóëå P(u0, w0, v0) íåïðîèñõîäèò íèêàêèõ èçìåíåíèé.Èíâàðèàíòû àëãîðèòìà NetchangeÈíâàðèàíò P(u0, w0, v0) ïîäòâåðæäàåò ñîãëàñîâàííîñòü äàííûõâ ðàçíûõ óçëàõ ñåòè ïî õîäó âû÷èñëåíèÿ àëãîðèòìà.Íàì ïîíàäîáèòñÿ åùå îäèí èíâàðèàíò, êîòîðûé ïîäòâåðæäàåòñîãëàñîâàííîñòü äàííûõ â êàæäîì îòäåëüíîì óçëå ñåòè.L(u, v ) ≡u = v =⇒ (Du [v ] = 0 ∧ Nbu [v ] = local)(4)∧(u 6= v ∧ ∃w ∈ Neighu : ndisu [w , v ] < N − 1)⇒ (Du [v ] = 1+ min ndisu [w , v ] = 1+ndisu [Nbu [v ], v ]) (5)w ∈Neighu∧(u 6= v ∧ ∀w ∈ Neighu : ndisu [w , v ] ≥ N − 1)⇒ (Du [v ] = N ∧ Nbu [v ] = udef )Ôîðìóëà L(u, v ) ãëàñèò, ÷òî îöåíêè ðàññòîÿíèé d(u, v ) èñîäåðæèìîå ñïèñêà Nbu [v ] â óçëå u âñåãäà ñîãëàñîâàíî ñ òåìèäàííûìè, êîòîðûå õðàíÿòñÿ â ëîêàëüíîé ïàìÿòè óçëà u .(6)Èíâàðèàíòû àëãîðèòìà NetchangeËåììà 2.Äëÿ ëþáîé ïàðû âåðøèí u0, v0 ôîðìóëà L(u0, v0) ÿâëÿåòñÿèíâàðèàíòîì.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Êîððåêòíîñòü àëãîðèòìà NetchangeÒåîðåìà 1.Êàê òîëüêî äîñòèãàåòñÿ ñòàáèëüíàÿ êîíôèãóðàöèÿ, òàáëèöûNbu [v ] óäîâëåòâîðÿþò ñëåäóþùèì óñëîâèÿì1) åñëè u = v , òî Nbu [v ] = local ;2) åñëè ñóùåñòâóåò ïóòü èç âåðøèíû u â âåðøèíó v 6= u , òîNbu [v ] = w , ãäå w ïåðâûé ñîñåä âåðøèíû u , êîòîðûéâñòðå÷àåòñÿ íà êðàò÷àéøåì ïóòè èç u â v ;3) åñëè ïóòè èç âåðøèíû u â âåðøèíó v íå ñóùåñòâóåò, òîNbu [v ] = udef .Äîêàçàòåëüñòâî.Êîãäà àëãîðèòì çàâåðøàåò ñâîå âûïîëíåíèå, íàðÿäó ñïðåäèêàòîìâûïîëíÿåòñÿ è ôîðìóëà P(u, w , v ) äëÿ âñåõòðîåê âåðøèí u, v , w , è îòñþäà ñëåäóåò, ÷òî äëÿ âñåõ òðîåêu, v , w ñïðàâåäëèâî ñîîòíîøåíèåup(u, w ) =⇒ ndisu [w , v ] = Dw [v ].(1)stableÊîððåêòíîñòü àëãîðèòìà NetchangeÏðèíèìàÿ âî âíèìàíèå óòâåðæäåíèå L(u, v ) äëÿ âñåõ ïàðâåðøèí u è v , ìû ïîëó÷àåì ñëåäóþùåå ñîîòíîøåíèå: 0, åñëè u = v ,1+ min Dw [v ], åñëè u 6= v ∧∃w ∈ Neighu : Dw [v ] < N − 1,Du [v ] =w ∈NeighN, åñëè u 6= v ∧∀w ∈ Neighu : Dw [v ] ≥ N − 1.(2)êîòîðîãî äîñòàòî÷íî, ÷òîáû äîêàçàòü, ÷òî Du [v ] = d(u, v )âñÿêèé ðàç, êîãäà âåðøèíû u è v íàõîäÿòñÿ â îäíîé è òîé æåêîìïîíåíòå ñâÿçíîñòè ñåòè, è Du [v ] = N , åñëè u è v íàõîäÿòñÿâ ðàçíûõ êîìïîíåíòàõ ñâÿçíîñòè.uÊîððåêòíîñòü àëãîðèòìà NetchangeÂíà÷àëå ìû ïîêàæåì, âîñïîëüçîâàâøèñü èíäóêöèåé ïî 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 .

Ïî èíäóêòèâíîìó ïðåäïîëîæåíèþDw [v ] ≤ k , è îòñþäà âñëåäñòâèå ñîîòíîøåíèÿDu [v ] = 1+ min Dw [v ]w ∈Neighuìû ïîëó÷àåì Du [v ] ≤ k + 1 .Êîððåêòíîñòü àëãîðèòìà NetchangeÒåïåðü ïîêàæåì èíäóêöèåé ïî Du [v ] , ÷òî âñÿêèé ðàç, êîãäà, èç âåðøèíû u â âåðøèíó v ñóùåñòâóåò ïóòü, è ïðèýòîì.Ñëó÷àé Du[v] = 0 .Èç ôîðìóëû (2) ñëåäóåò, ÷òî Du [v ] = 0 òîëüêî òîãäà, êîãäàu = v . Ýòî îçíà÷àåò, ÷òî ìåæäó âåðøèíàìè u è v åñòü ïóñòîéïóòü è d(u, v ) = 0 .Du [v] = k + 1 < N .Èç ôîðìóëû (2) ñëåäóåò, ÷òî ñóùåñòâóåò òàêàÿ âåðøèíàw ∈ Neighu , äëÿ êîòîðîé Dw [v ] = k .

Ïî èíäóêòèâíîìóïðåäïîëîæåíèþ ìåæäó âåðøèíàìè w è v ñóùåñòâóåò ïóòü èd(w , v ) ≤ k . Îòñþäà ñëåäóåò, ÷òî ìåæäó âåðøèíàìè u è vòàêæå åñòü ïóòü è d(u, v ) ≤ k + 1 .Du [v ] < Nd(u, v ) ≤ Du [v ]Êîððåêòíîñòü àëãîðèòìà Netchangeu = v =⇒ (Du [v ] = 0 ∧ Nbu [v ] = local)(4)(u 6= v ∧ ∃w ∈ Neighu : ndisu [w , v ] < N − 1)⇒ (Du [v ] = 1+ min ndisu [w , v ] = 1+ndisu [Nbu [v ], v ]) (5)w ∈Neighu(u =6 v ∧ ∀w ∈ Neighu : ndisu [w , v ] ≥ N − 1)⇒ (Du [v ] = N ∧ Nbu [v ] = udef )åñëè(6)u = v, 0,1+minDw [v ],u 6= v ∧∃w ∈ Neighu : Dw [v ] < N − 1,Du [v ] =w ∈NeighuN,u 6= v ∧∀w ∈ Neighu : Dw [v ] ≥ N − 1.åñëèåñëèÒàêèì îáðàçîì, åñëè u è v íàõîäÿòñÿ â îäíîé è òîé æåêîìïîíåíòå ñâÿçíîñòè, òî Du [v ] = d(u, v ) , à â ïðîòèâíîìñëó÷àå Du [v ] = N .

Îòñþäà, ïðèíèìàÿ âî âíèìàíèå ôîðìóëó (2)è ïðåäëîæåíèå ∀u, v : L(u, v ) , ïîëó÷àåì çàÿâëåííûé âóòâåðæäåíèè òåîðåìû ðåçóëüòàò î òàáëèöàõ Nbu [v ] .Çàâåðøàåìîñòü àëãîðèòìà Netchange×òîáû óáåäèòüñÿ â òîì, ÷òî ñòàáèëüíàÿ ñèòóàöèÿ ðàíî èëèïîçäíî íàñòóïèò, ïîñëå òîãî êàê çàâåðøàòñÿ èçìåíåíèÿòîïîëîãèè, ìû ââåäåì íîðìèðóþùóþ ôóíêöèþ ïî îòíîøåíèþê ïðåäèêàòó.Äëÿ êîíôèãóðàöèè γ íàøåãî àëãîðèòìàáóäåì ïîëàãàòüti =(÷èñëî ñîîáùåíèé òèïà h, .., ii)++ (÷èñëî óïîðÿäî÷åííûõ ïàð u, v , äëÿ êîòîðûõ Du [v ] = i),è çíà÷åíèåì ôóíêöèè f áóäåì ñ÷èòàòü (N + 1) -ìåñòíûé íàáîðstablemydistf (γ) = (t0 , t1 , .