12 Задача сохранения моментального состояния. Алгоритм Чанди-Лампорта. Алгоритм Лаи-Янга, страница 2

å. ìîæåò ñëó÷èòñÿ â íåêîòîðîé ðåàëèçàöèèýòîãî âû÷èñëåíèÿ).Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿÎïðåäåëåíèå 3.Ìîìåíòàëüíîå ñîñòîÿíèå S ∗ íàçûâàåòñÿ çíà÷èìûì ââû÷èñëåíèè C , åñëè ñóùåñòâóåò òàêàÿ ðåàëèçàöèÿ E ∈ C , ÷òîγ ∗ ÿâëÿåòñÿ êîíôèãóðàöèåé E .Ìû áóäåì òðåáîâàòü îò àëãîðèòìà ïîñòðîåíèÿ ìîìåíòàëüíîãîñîñòîÿíèÿ òàê êîîðäèíèðîâàòü ðåãèñòðàöèþ ëîêàëüíûõìîìåíòàëüíûõ ñîñòîÿíèé îòäåëüíûõ ïðîöåññîâ, ÷òîáûïîëó÷åííîå â ðåçóëüòàòå ýòîãî ãëîáàëüíîå ìîìåíòàëüíîåñîñòîÿíèå îêàçàëîñü çíà÷èìûì.Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿÒåîðåìà 1.Ïóñòü S ∗ ìîìåíòàëüíîå ñîñòîÿíèå ñèñòåìû è L ñå÷åíèå,ïîðîæäåííîå S ∗ .

Òîãäà ðàâíîñèëüíû ñëåäóþùèå òðèóòâåðæäåíèÿ:1) S ∗ îñóùåñòâèìî;2) L ñîãëàñîâàíî;3) S ∗ çíà÷èìî.Äîêàçàòåëüñòâî.Ïîêàæåì ñïðàâåäëèâîñòü ñîîòíîøåíèé(1) =⇒ (2) =⇒ (3) =⇒ (1)Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿ(1) ⇒ (2)Äîïóñòèì, ÷òî ñîñòîÿíèå S ∗ îñóùåñòâèìî. ×òîáû óáåäèòüñÿ âòîì, ÷òî L ñîãëàñîâàíî, ðàññìîòðèì e ∈ L è e 0 e . Ïîîïðåäåëåíèþ îòíîøåíèÿ äîñòàòî÷íî ïîêàçàòü, ÷òîâêëþ÷åíèå e 0 ∈ L âûïîëíÿåòñÿ â ñëåäóþùèõ äâóõ ñëó÷àÿõ.1.

Âûïîëíÿåòñÿ ñîîòíîøåíèå e 0 p e (ãäå p ýòî ïðîöåññ, âêîòîðîì ïðîèñõîäÿò e 0 è e ).  òàêîì ñëó÷àå âêëþ÷åíèå e 0 ∈ Lâûïîëíÿåòñÿ áëàãîäàðÿ òîìó, ÷òî L ñå÷åíèå.2. Ñîáûòèå e 0 ýòî ñîáûòèå îòïðàâëåíèÿ ñîîáùåíèÿ, àñîáûòèå e ñîîòâåòñòâóþùåå åìó ñîáûòèå ïðèåìà ñîîáùåíèÿ.Ðàññìîòðèì ïðîöåññ p , â êîòîðîì ïðîèñõîäèò ñîáûòèå e 0 ,ïðîöåññ q , â êîòîðîì ïðîèñõîäèò e , è ñîîáùåíèå m , êîòîðûìîáìåíèâàþòñÿ ïðîöåññû. ÒîãäàÄîêàçàòåëüñòâî.e∈L∗ ,=⇒ m ∈ rcvdpq∗=⇒ m ∈ sentpq ,=⇒ e 0 ∈ L.ò.ê. e ïðåäìîìåíòàëüíîå ñîáûòèåò.ê.

S ∗ îñóùåñòâèìîÇàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿÄîêàçàòåëüñòâî.(2) ⇒ (3)Ïîñòðîèì òàêîå âûïîëíåíèå âû÷èñëåíèÿ, â êîòîðîì âñåïðåäìîìåíòàëüíûå ñîáûòèÿ ïðîèñõîäÿò ðàíåå ëþáîãîïîñòìîìåíòàëüíîãî ñîáûòèÿ.Ââåäåì ñëåäóþùóþ íóìåðàöèþ f = (f0 , f1 , . . .) ñîáûòèéìíîæåñòâà Ev .Âíà÷àëå ïåðå÷èñëèì âñå ïðåäìîìåíòàëüíûå ñîáûòèÿ èç Ev âïðîèçâîëüíîì ïîðÿäêå, ñîãëàñîâàííîì ñ îòíîøåíèåì , àäàëåå ïåðå÷èñëèì âñå ïîñòìîìåíòàëüíûå ñîáûòèÿ âïðîèçâîëüíîì ïîðÿäêå, ñîãëàñîâàííîì ñ îòíîøåíèåì .Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿuHHHHjuu Huu u u u uue uJuueJ QAeQJQAUAusuQeJJJJu u u u uÏðîñòðàíñòâåííîâðåìåííàÿäèàãðàììà CÏîñëåäîâàòåëüíîñòü fÇàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿÄîêàçàòåëüñòâî.(2) ⇒ (3)Ïîñòðîèì òàêîå âûïîëíåíèå âû÷èñëåíèÿ, â êîòîðîì âñåïðåäìîìåíòàëüíûå ñîáûòèÿ ïðîèñõîäÿò ðàíåå ëþáîãîïîñòìîìåíòàëüíîãî ñîáûòèÿ.Ââåäåì ñëåäóþùóþ íóìåðàöèþ f = (f0 , f1 , .

. .) ñîáûòèéìíîæåñòâà Ev .Âíà÷àëå ïåðå÷èñëèì âñå ïðåäìîìåíòàëüíûå ñîáûòèÿ èç Ev âïðîèçâîëüíîì ïîðÿäêå, ñîãëàñîâàííîì ñ îòíîøåíèåì , àäàëåå ïåðå÷èñëèì âñå ïîñòìîìåíòàëüíûå ñîáûòèÿ âïðîèçâîëüíîì ïîðÿäêå, ñîãëàñîâàííîì ñ îòíîøåíèåì .Âîñïîëüçóåìñÿ òåîðåìîé î âû÷èñëåíèÿõ.Ïóñòü f = (f0 , f1 , f2 , .

. .) ïåðåñòàíîâêà ñîáûòèé âûïîëíåíèÿE , ñîõðàíÿþùàÿ ïðè÷èííî-ñëåäñòâåííûé ïîðÿäîê ñîáûòèéâûïîëíåíèÿ . Òîãäà f îïðåäåëÿåò åäèíñòâåííîå âûïîëíåíèå F ,íà÷èíàþùååñÿ ñ òîé æå êîíôèãóðàöèè, ÷òî è âûïîëíåíèå E .Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿ×òîáû âîñïîëüçîâàòüñÿ ýòîé òåîðåìîé, ïîêàæåì, ÷òî âñÿïîñëåäîâàòåëüíîñòü f ñîãëàñîâàíà ñ îòíîøåíèåì .

Äîïóñòèì,÷òî fi fj .Åñëè îáà ñîáûòèÿ fi è fj ïðåäìîìåíòàëüíûå, òî i ≤ j ,ïîñêîëüêó â f ïðåäìîìåíòàëüíûå ñîáûòèÿ ïåðå÷èñëåíû âïîðÿäêå, ñîãëàñîâàííîì ñ îòíîøåíèåì .Ïî òåì æå ïðè÷èíàì ýòî íåðàâåíñòâî âûïîëíÿåòñÿ, êîãäà îáàñîáûòèÿ fi è fj ÿâëÿþòñÿ ïîñòìîìåíòàëüíûìè.Åñëè fi ïðåäìîìåíòàëüíîå ñîáûòèå, à fj ïîñòìîìåíòàëüíîå, òî íåðàâåíñòâî i ≤ j ñîáëþäàåòñÿ ò.ê. â fâñå ïðåäìîìåíòàëüíûå ñîáûòèÿ ïðåäøåñòâóþòïîñòìîìåíòàëüíûì.Ñëó÷àé, êîãäà fj ïðåäìîìåíòàëüíîå ñîáûòèå, à fi ïîñòìîìåíòàëüíîå, èñêëþ÷åí, ââèäó òîãî ÷òî ñå÷åíèå L ïîïðåäïîëîæåíèþ ÿâëÿåòñÿ ñîãëàñîâàííûì.Çàäà÷à ñîõðàíåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿÈòàê, ïîñëåäîâàòåëüíîñòü f ñîãëàñîâàíà ñ îòíîøåíèåì .Çíà÷èò, ïî òåîðåìå î âû÷èñëåíèÿõ ñóùåñòâóåò âûïîëíåíèåâû÷èñëåíèÿ F , ñîñòîÿùåå èç âñåõ ñîáûòèé ìíîæåñòâà Ev ,îñóùåñòâëÿåìûõ â òîì ïîðÿäêå, êîòîðûé ïðåäñòàâëåíïîñëåäîâàòåëüíîñòüþ f .

Âûïîëíåíèå F ñîäåðæèòêîíôèãóðàöèþ γ ∗ , êîòîðàÿ âîçíèêàåò ñðàçó æå ïîñëåîñóùåñòâëåíèÿ âñåõ ïðåäìîìåíòàëüíûõ ñîáûòèé.Äîêàçàòåëüñòâî.(3) ⇒ (1)Åñëè ìîìåíòàëüíîå ñîñòîÿíèå S ∗ ÿâëÿåòñÿ çíà÷èìûì, òîêîíôèãóðàöèÿ γ ∗ âîçíèêàåò ïðè âûïîëíåíèè âû÷èñëåíèÿ C . Âêàæäîì âûïîëíåíèè âñÿêîå ñîîáùåíèå íå ìîæåò áûòüäîñòàâëåíî ïî íàçíà÷åíèþ, ïðåæäå ÷åì îíî áóäåò îòïðàâëåíî.Îòñþäà ñëåäóåò, ÷òî äëÿ êàæäîé ïàðû ïðîöåññîâ p è q èìååò∗ ⊆ sent ∗ .

Ïîýòîìó ñîñòîÿíèå S ∗ìåñòî ñîîòíîøåíèå rcvdpqpqîñóùåñòâèìî.Àëãîðèòì ×àíäèËàìïîðòàÏî òåîðåìå 1 äîñòàòî÷íî ñêîîðäèíèðîâàòü ëîêàëüíûåìîìåíòàëüíûå ñîñòîÿíèÿ, ÷òîáû âûïîëíÿëèñü ñëåäóþùèå äâàñâîéñòâà:1. âûáðàííûå â êàæäîì ïðîöåññå ëîêàëüíûå ìîìåíòàëüíûåñîñòîÿíèÿ äîëæíû áûòü ðåàëèçîâàíû.2. ïîëó÷åíèå ïîñòìîìåíòàëüíîãî ñîîáùåíèÿ íå ìîæåòñîñòàâëÿòü ïðåäìîìåíòàëüíîå ñîáûòèå.Âî âñåõ àëãîðèòìàõ ïîñòðîåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿâñÿêèé ïðîöåññ çàïå÷àòëåâàåò ñâîå ëîêàëüíîå ìîìåíòàëüíîåñîñòîÿíèå, äî òîãî êàê ïîëó÷èò ïîñòìîìåíòàëüíîå ñîîáùåíèå.×òîáû îòëè÷àòü ñîîáùåíèÿ â àëãîðèòìå ïîñòðîåíèÿìîìåíòàëüíîãî ñîñòîÿíèÿ îò ñîîáùåíèé â ñàìîì âû÷èñëåíèè,ìû áóäåì íàçûâàòü ñîîáùåíèÿ ïåðâîãî âèäà êîíòðîëüíûìèñîîáùåíèÿìè , à ñîîáùåíèÿ âòîðîãî âèäà áàçîâûìèñîîáùåíèÿìè .Àëãîðèòì ×àíäèËàìïîðòàÀëãîðèòì ïðèìåíèì ê ñèëüíî ñâÿçíîé ñåòè ñ ïðîèçâîëüíîéòîïîëîãèåé, îäíîíàïðàâëåííûìè êàíàëàìè, â êîòîðûõïîääåðæèâàåòñÿ î÷åðåäíîñòü ñîîáùåíèé.Èäåÿ àëãîðèòìà. àëãîðèòìå ×åíäèËýìïîðòà ïðîöåññû ñîîáùàþò äðóã äðóãóî ïîñòðîåíèè ìîìåíòàëüíûõ ñîñòîÿíèé ïóòåì îòïðàâëåíèÿñïåöèàëüíûõ ñîîáùåíèé (ìàðêåðîâ) hmkri ïî êàæäîìó êàíàëó.Êàæäûé ïðîöåññ, çàïå÷àòëåâàÿ ñâîå ëîêàëüíîå ñîñòîÿíèå,îòïðàâëÿåò ìàðêåð â òî÷íîñòè îäèí ðàç ïî êàæäîìóïðèìûêàþùåìó ê íåìó êàíàëó; ìàðêåðû ðàññìàòðèâàþòñÿ êàêêîíòðîëüíûå ñîîáùåíèÿ.Ïîëó÷åíèå ñîîáùåíèÿ hmkri êàêèì-ëèáî ïðîöåññîì, êîòîðûéåùå íå çàïå÷àòëåë ñâîå ìîìåíòàëüíîå ñîñòîÿíèå, ïðèâîäèò êòîìó, ÷òî ýòîò ïðîöåññ çàïå÷àòëåâàåò ñâîå ìîìåíòàëüíîåñîñòîÿíèå è òàêæå îòïðàâëÿåò ìàðêåð hmkri , êîòîðûéâûïîëíÿåòñÿ ïàðàëëåëüíî ñ âû÷èñëåíèåì C .Àëãîðèòì ×àíäèËàìïîðòàvartakenp:boolinitfalse ;Äëÿ çàïóñêà àëãîðèòìà:begin çàïîìíèòü ëîêàëüíîå ñîñòîÿíèå ; takenp := true ;forall q ∈ Neighp do send hmkri to qendÅñëè áûë äîñòàâëåí ìàðêåð:begin receive hmkri ;if not takenp thenbegin çàïîìíèòü ëîêàëüíîå ñîñòîÿíèå ; takenp := true ;forall q ∈ Neighp do send hmkri to qendendÀëãîðèòì ×àíäèËàìïîðòàËåììà.Åñëè õîòÿ áû îäèí ïðîöåññ çàïóñòèòàëãîðèòì ×àíäèËàìïîðòà, òî ñïóñòÿ êîíå÷íûé ïðîìåæóòîêâðåìåíè âñå ïðîöåññû çàïå÷àòëåþò ñâîå ëîêàëüíîåìîìåíòàëüíîå ñîñòîÿíèå.Äîêàçàòåëüñòâî.ÑàìîñòîÿòåëüíîÀëãîðèòì ×àíäèËàìïîðòàÒåîðåìà 2.Àëãîðèòì ×åíäèËýìïîðòà âû÷èñëÿåò çíà÷èìîå ìîìåíòàëüíîåñîñòîÿíèå ñèñòåìû.Äîêàçàòåëüñòâî.Ñîãëàñíî ëåììå àëãîðèòìó íóæíî êîíå÷íîå âðåìÿ äëÿâû÷èñëåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿ ñèñòåìû.

Ïîêàæåì, ÷òîïîñòðîåííîå ìîìåíòàëüíîå ñîñòîÿíèå îñóùåñòâèìî.Ðàññìîòðèì ïîñòìîìåíòàëüíîå ñîîáùåíèå m , îòïðàâëåííîåïðîöåññîì p ïðîöåññó q . Ïåðåä îòïðàâëåíèåì m , ïðîöåññ pçàïå÷àòëåë ñâîå ìîìåíòàëüíîå ëîêàëüíîå ñîñòîÿíèå è îòïðàâèëñîîáùåíèå hmkri âñåì ñâîèì ñîñåäÿì, âêëþ÷àÿ ïðîöåññ q .Ò.ê.

â êàíàëàõ ïîääåðæèâàåòñÿ î÷åðåäíîñòü ñîîáùåíèé,ïðîöåññ q ïîëó÷èë ñîîáùåíèå hmkri , äî òîãî êàê ïîëó÷èë m ,è ïîýòîìó çàïå÷àòëåë ñâîå ìîìåíòàëüíîå ñîñòîÿíèå ñðàçó ïîïîëó÷åíèè ýòîãî ñîîáùåíèÿ èëè ðàíåå. Çíà÷èò, ïîëó÷åíèåñîîáùåíèÿ m îòíîñèòñÿ ê ÷èñëó ïîñòìîìåíòàëüíûõ ñîáûòèé. Àëãîðèòì ËàèßíãàÀëãîðèòì Ëàèßíãà íå îïèðàåòñÿ íà ñâîéñòâî ïîääåðæàíèÿî÷åðåäíîñòè ñîîáùåíèé â êàíàëàõ. Ïîýòîìó îòäåëèòüïðåäìîìåíòàëüíûå ñîáûòèÿ îò ïîñòìîìåíòàëüíûõ ïðè ïîìîùèìàðêåðîâ óæå íåâîçìîæíî.Èäåÿ àëãîðèòìà.Êàæäîå áàçîâîå ñîîáùåíèå ñíàáæàåòñÿ ïîìåòêîé, êîòîðàÿïîçâîëÿåò ïîíÿòü, ÿâëÿåòñÿ ëè ýòî ñîîáùåíèåïðåäìîìåíòàëüíûì èëè ïîñòìîìåíòàëüíûì.Äëÿ ýòîãî ïðîöåññ p , îòïðàâëÿÿ ñîîáùåíèå ïî õîäó âû÷èñëåíèÿ C , äîáàâëÿåò ê íåìó çíà÷åíèå takenp . Ñîäåðæàíèåñîîáùåíèé, îòíîñÿùèõñÿ ê âû÷èñëåíèþ C , íåñóùåñòâåííî;áóäåì îáîçíà÷àòü èõ ïðîñòî hmes, ci , ãäå c ýòî çíà÷åíèå,âêëþ÷åííîå â ñîñòàâ ñîîáùåíèÿ ïðîöåññîì-îòïðàâèòåëåì.Àëãîðèòì ïîñòðîåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿ ïðîâåðÿåòïîñòóïàþùèå ñîîáùåíèÿ è çàïèñûâàåò ìîìåíòàëüíîåëîêàëüíîå ñîñòîÿíèå â òîì âèäå, â êàêîì îíî áûëî äîïîñòóïëåíèÿ ïåðâîãî ïîñòìîìåíòàëüíîãî ñîîáùåíèÿ.Àëãîðèòì Ëàèßíãàvartakenp:boolinitfalse ;Äëÿ çàïóñêà àëãîðèòìà:begin çàïîìíèòü ëîêàëüíîå ñîñòîÿíèå ; takenp := trueendÄëÿ îòïðàâëåíèÿ ñîîáùåíèÿ ïî õîäó âû÷èñëåíèÿ C :send hmes, takenp iÅñëè ïîñòóïèëî ñîîáùåíèå hmes, ci;begin receive hmes, ci ;if c and not takenp thenbegin çàïîìíèòü ëîêàëüíîå ñîñòîÿíèå ; taken := true end;èçìåíèòü ñîñòîÿíèå íà òî, â êîòîðîì ïðåáûâàë ïðîöåññïðè ïîëó÷åíèè ñîîáùåíèÿ â âû÷èñëåíèè CendÀëãîðèòì Ëàèßíãà àëãîðèòìå Ëàèßíãà íåò îáìåíà êîíòðîëüíûìèñîîáùåíèÿìè, è îí íå ìîæåò ãàðàíòèðîâàòü òîãî, ÷òî êàæäûéïðîöåññ ðàíî èëè ïîçäíî çàïèøåò ñâîå ñîñòîÿíèå.

Ðàññìîòðèìïðîöåññ p , íå ÿâëÿþùèéñÿ èíèöèàòîðîì àëãîðèòìà ïîñòðîåíèÿìîìåíòàëüíîãî ñîñòîÿíèÿ, è ïðåäïîëîæèì, ÷òî íè îäèí èçñîñåäåé ïðîöåññà p íå îòïðàâëÿåò ïðîöåññó p ñîîáùåíèé, ïîñëåòîãî êàê ýòîò ñîñåä çàïå÷àòëåë ñâîå ìîìåíòàëüíîå ëîêàëüíîåñîñòîÿíèå.  òàêîì ñëó÷àå p íèêîãäà íå ïðîâåäåò çàïèñü ñâîåãîñîñòîÿíèÿ, è àëãîðèòì ïîñòðîåíèÿ ìîìåíòàëüíîãî ñîñòîÿíèÿçàâåðøèò ðàáîòó, èìåÿ íåïîëíîå ìîìåíòàëüíîå ñîñòîÿíèå.Ðåøåíèå ýòîé ïðîáëåìû çàâèñèò îò òîãî, ÷òî íàì èçâåñòíî îâû÷èñëåíèè C ; åñëè ìû èìååì ãàðàíòèþ, ÷òî ñâÿçü ñ êàæäûìïðîöåññîì ðàíî èëè ïîçäíî îñóùåñòâèòñÿ, òî è ïîëíîå ìîìåíòàëüíîå ñîñòîÿíèå âñåãäà ìîæíî áóäåò çàïå÷àòëåòü.  ïðîòèâíîì ñëó÷àå àëãîðèòì ìîæíî ñíàáäèòü áëîêîì îáìåíàêîíòðîëüíûìè ñîîáùåíèÿìè ìåæäó âñåìè ïðîöåññàìè.Àëãîðèòì ËàèßíãàÒåîðåìà 3.Àëãîðèòì Ëàÿßíãà âû÷èñëÿåò òîëüêî çíà÷èìûåìîìåíòàëüíûå ñîñòîÿíèÿ ñèñòåìû.Äîêàçàòåëüñòâî.Ðàññìîòðèì ìîìåíòàëüíîå ñîñòÿíèå, âû÷èñëåííîå àëãîðèòìîì,è ïóñòü m = hmes, ci ýòî ïîñòìîìåíòàëüíîå ñîîáùåíèå,îòïðàâëåííîå ïðîöåññîì p ïðîöåññó q .