Лекция 6. Алгоритм Netchange_ описание_ инварианты_ корректность_ сходимость. Другие виды маршрутизаци (1185656), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

å. çíà÷åíèå ïåðåìåííîé ndisu [w , v ]ïîëàãàåòñÿ ðàâíûì N .mydistÎïèñàíèå àëãîðèòìà NetchangeÂû÷èñëåíèå àëãîðèòìà çàâåðøàåòñÿ, êîãäà â êàíàëàõ ñâÿçè íåîñòàåòñÿ íè îäíîãî ñîîáùåíèÿ, íàõîäÿùåãîñÿ íà ýòàïåïåðåñûëêè.Êîíôèãóðàöèè òàêîãî âèäà íå ÿâëÿþòñÿ çàêëþ÷èòåëüíûìèêîíôèãóðàöèÿìè äëÿ âñåé ñèñòåìû â öåëîì, ïîòîìó ÷òîâû÷èñëåíèå ñèñòåìû ìîæåò áûòü ïðîäîëæåíî, ïîñëå òîãî êàêêàêîé-íèáóäü êàíàë âûéäåò èç ñòðîÿ èëè âîññòàíîâèò ñâîþðàáîòîñïîñîáíîñòü (÷òî ïîòðåáóåò ðåàêöèè ñî ñòîðîíûàëãîðèòìà).Êîíôèãóðàöèþ, íå èìåþùóþ â êàíàëàõ ñâÿçè íè îäíîãîñîîáùåíèÿ, ìû áóäåì íàçûâàòü ñòàáèëüíîé . Äëÿ îïèñàíèÿýòîãî ÿâëåíèÿ ââåäåì äâà ïðåäèêàòà:up(u, w ) ≡ êàíàë ñâÿçè ìåæäó óçëàìè u, w èñïðàâåístable ≡ ∀ u, w : up(u, w ) ⇒ Qwuíå ñîäåðæèò ñîîáùåíèémydist.Èíâàðèàíòû àëãîðèòìà Netchange×òîáû îáîñíîâàòü êîððåêòíîñòü àëãîðèòìà Netchangeîòíîñèòåëüíî òðåáîâàíèé R1 è R2 íàì ïîíàäîáÿòñÿ (êàê âûäóìàåòå ÷òî?)Èíâàðèàíòû àëãîðèòìà Netchange×òîáû îáîñíîâàòü êîððåêòíîñòü àëãîðèòìà Netchangeîòíîñèòåëüíî òðåáîâàíèé R1 è R2 íàì ïîíàäîáÿòñÿ (êàê âûäóìàåòå ÷òî?) ÈÍÂÀÐÈÀÍÒÛ !P(u, w , v ) ≡up(u,∧w ) ⇐⇒ w ∈ Neighuñîäåðæèò ñîîáùåíèå h, v , diïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v ]up(u, w ) ∧ Qwu=⇒∧up(u, w )∧Qwu=⇒(1)mydistíå ñîäåðæèò ñîîáùåíèé hmydistndisu [w ,,v ,div ] = Dw [v ]Ôîðìóëà P(u, w , v ) óòâåðæäàåò: åñëè ïðîöåññ u çàâåðøèëîáðàáîòêó ñîîáùåíèé òèïà, ïîëó÷åííûõ îò ïðîöåññà w ,òî îöåíêà ðàññòîÿíèÿ d(w , v ) â óçëå u ñîâïàäàåò ñ îöåíêîéðàññòîÿíèÿ d(w , v ) â óçëå w .mydist(2)(3)Èíâàðèàíòû àëãîðèòìà NetchangeËåììà 1.Äëÿ ëþáîé òðîéêè âåðøèí u0, w0, v0 ôîðìóëà P(u0, w0, v0)ÿâëÿåòñÿ èíâàðèàíòîì.Èíâàðèàíòû àëãîðèòìà NetchangeËåììà 1.Äëÿ ëþáîé òðîéêè âåðøèí u0, w0, v0 ôîðìóëà P(u0, w0, v0)ÿâëÿåòñÿ èíâàðèàíòîì.Äîêàçàòåëüñòâî.Áóäåì ñ÷èòàòü, ÷òî âíà÷àëå âñå ñïèñêè Neighu ïðàâèëüíîîòðàæàþò ðàáîòîñïîñîáíîñòü êàíàëîâ ñâÿçè ìåæäó óçëàìè, ò.

å.ñîîòíîøåíèå (1) ñ÷èòàåòñÿ âåðíûì.Èíâàðèàíòû àëãîðèòìà NetchangeËåììà 1.Äëÿ ëþáîé òðîéêè âåðøèí u0, w0, v0 ôîðìóëà P(u0, w0, v0)ÿâëÿåòñÿ èíâàðèàíòîì.Äîêàçàòåëüñòâî.Áóäåì ñ÷èòàòü, ÷òî âíà÷àëå âñå ñïèñêè Neighu ïðàâèëüíîîòðàæàþò ðàáîòîñïîñîáíîñòü êàíàëîâ ñâÿçè ìåæäó óçëàìè, ò. å.ñîîòíîøåíèå (1) ñ÷èòàåòñÿ âåðíûì.Íóæíî ðàññìîòðåòü èíèöèàëèçàöèþ è òðè òèïà ïðîöåäóð:1. Proc-1 : ïðèåì ñîîáùåíèÿ òèïà. Ïðîèñõîäèò ïðèåìîäíîãî ñîîáùåíèÿ è (âîçìîæíî) îòïðàâëåíèå íåñêîëüêèõñîîáùåíèé.2. Proc-2 : îáðûâ êàíàëà è îáðàáîòêà ñîîáùåíèÿ òèïà âóçëàõ ïî îáå ñòîðîíû êàíàëà.3. Proc-3 : âîññòàíîâëåíèå êàíàëà è îáðàáîòêà ñîîáùåíèÿòèïàâ îáîèõ óçëàõ, ñîåäèíåííûõ ýòèì êàíàëîì.mydistfailrepair,w ∈ Neighu v ∈ V do ndisu [w , v ] := Nv ∈ V dobegin Du [v ] := NNbu [v ] := udef endDu [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0iwbegin forallforall;;send;;;toendup(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 ],v0 ,di(3) ñàìîì íà÷àëå ïîñëå âûïîëíåíèÿ ïðîöåäóðû èíèöèàëèçàöèè âêàæäîì óçëå ñîîòíîøåíèå (1) âûïîëíÿåòñÿ ñîãëàñíîñäåëàííîìó äîïóùåíèþ î ñïèñêàõ Neighu .,w ∈ Neighu v ∈ V do ndisu [w , v ] := Nv ∈ V dobegin Du [v ] := NNbu [v ] := udef endDu [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0iwbegin forallforall;;send;;;toendw0 ) ⇐⇒ 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 ],v0 ,diÅñëè ïåðâîíà÷àëüíî âûïîëíÿåòñÿ óñëîâèå ¬up(u0, w0) , òîñîîòíîøåíèÿ (2) è (3), î÷åâèäíî, âûïîëíÿþòñÿ.(3),w ∈ Neighu v ∈ V do ndisu [w , v ] := Nforall v ∈ V dobegin Du [v ] := NNbu [v ] := udef endDu [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0iwbegin forall;;send;;;toendup(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 ],v0 ,di(3)Åñëè æå âíà÷àëå âûïîëíÿåòñÿ óñëîâèå up(u0, w0) , òîñîãëàñíî (1), è ïîýòîìó ïîñëå èíèöèàëèçàöèè.w0 ∈ Neighu0ndisu0 [w0 , v0 ] = N,w ∈ Neighu v ∈ V do ndisu [w , v ] := Nforall v ∈ V dobegin Du [v ] := NNbu [v ] := udef endDu [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0iwbegin forall;;send;;;toendup(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 = v0Dw0 [w0 ] = 0hmydist, v0 , 0iÅñëè, òîñîäåðæèòñÿ ñîîáùåíèåñîîòíîøåíèÿ (2) è (3).,v0 ,di(3), íî ïðè ýòîì â î÷åðåäè Qw u, è ïîýòîìó âåðíû0 0,w ∈ Neighu v ∈ V do ndisu [w , v ] := Nv ∈ V dobegin Du [v ] := NNbu [v ] := udef endDu [u] := 0 Nbu [u] := localforall w ∈ Neighu dohmydist, u, 0iwbegin forallforall;;send;;;toendup(u0 ,w0 ) ⇐⇒ w0 ∈ Neighu0ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist(1), v0 , di(2)00 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]w0 6= v0Dw0 [v0 ] = Nv0mydist,v0 ,di(3)Åñëè, òîè â î÷åðåäè êàíàëà (w0u0) íåòñîîáùåíèé îá óçëå , ïîýòîìó ñîîòíîøåíèÿ (2) è (3) òàêæåáóäóò âåðíû.Proc-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 u0(1)mydist, v0 , di(2)0mydist0 0=⇒ndisu) [w0 ,v0 ] = Dw0 [v0 ]u,v0 ,di(3)hmydist, v , diÏðåäïîëîæèì, ÷òî óçåë ïîëó÷àåò ñîîáùåíèåîòóçëà w .Ýòî íå âëå÷åò çà ñîáîé íèêàêèõ èçìåíåíèé òîïîëîãèè ñåòè, èïîýòîìó ñïèñêè âåðøèí-ñîñåäåé Neigh íå èçìåíÿþòñÿ, èñîîòíîøåíèå (1) îñòàåòñÿ âåðíûì.Åñëè v 6= v0 , òî ñ ïîëó÷åíèåì ýòîãî ñîîáùåíèÿ â ôîðìóëåP(u0 , w0 , v0 ) íè÷åãî íå èçìåíÿåòñÿ.Proc-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(1)ñîäåðæèò ñîîáùåíèå h=⇒ ïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé hup(u0 , w0 ) ∧ Qw0 u0mydist, v0 , di(2)00 0=⇒ ndisu0 [w0 , v0 ] = Dw0 [v0 ]v = v0 , u = u0 , w = w0mydist,v0 ,di(3)Åñëè, òî çíà÷åíèå ndisu [w0, v0] ìîæåòèçìåíèòüñÿ.Åñëè Qw u ñîäåðæèò åùå îäíî ñîîáùåíèå îá óçëå v0 , òîçíà÷åíèÿ, ñîäåðæàùèåñÿ â ýòîì ñîîáùåíèè, óäîâëåòâîðÿþò (2).Cîîòíîøåíèÿ (3) ñîõðàíÿåòñÿ, ò.ê.

åãî ïðåäïîñûëêà ëîæíà.Åñëè â 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 )mydistmydistbeginmydistendw0 ) ⇐⇒ 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 = w0u0,v0 ,di(3)Åñëè(è ñîñåä u), òî çàêëþ÷åíèÿóòâåðæäåíèé (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 wendendw0 ) ⇐⇒ w0 ∈ Neighu0up(u0 , w0 ) ∧ Qw0 u0=⇒up(u0 ,ñîäåðæèò ñîîáùåíèå hïîñëåäíåå ñîîáùåíèå â î÷åðåäèóäîâëåòâîðÿåò ðàâåíñòâó d = Dw [v0]up(u0 , w0 )∧Qw u íå ñîäåðæèò ñîîáùåíèé h(1)mydist, v0 , di(2)0mydist0 0=⇒ndisu0 [w0 ,v0 ] = Dw0 [v0 ],v0 ,di(3)Ïðåäïîëîæèì, ÷òî â ñåòè ïîÿâèëñÿ êàíàë (uw ) .Åñëè 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=⇒ndisu [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) ïîäòâåðæäàåò ñîãëàñîâàííîñòü äàííûõâ ðàçíûõ óçëàõ ñåòè ïî õîäó âû÷èñëåíèÿ àëãîðèòìà.Íàì ïîíàäîáèòñÿ åùå îäèí èíâàðèàíò, êîòîðûé ïîäòâåðæäàåòñîãëàñîâàííîñòü äàííûõ â êàæäîì îòäåëüíîì óçëå ñåòè.Èíâàðèàíòû àëãîðèòìà 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Ëåììà 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 .Êîððåêòíîñòü àëãîðèòìà 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 ) .Êîððåêòíîñòü àëãîðèòìà NetchangeÂíà÷àëå ìû ïîêàæåì, âîñïîëüçîâàâøèñü èíäóêöèåé ïî d(u, v ), ÷òî âñÿêèé ðàç, êîãäà âåðøèíû u è v íàõîäÿòñÿ â îäíîé è òîéæå êîìïîíåíòå ñâÿçíîñòè ñåòè, âåðíî íåðàâåíñòâîDu [v ] ≤ d(u, v ) .Ñëó÷àé d(u, v) = 0 . ýòîì ñëó÷àå u = v , è ïîýòîìó Du [v ] = 0 .Êîððåêòíîñòü àëãîðèòìà 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 .

Характеристики

Список файлов лекций