Лекция 11. Обнаруж завершения вычисл. Алгоритм Дейкстры-Шолтена_ Шави-Франчеза_ Сафры_ возвращения кредитов_ Рана (1185661), страница 3
Текст из файла (страница 3)
. . , p1, p0, . . . ).Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:I B(γ) ÷èñëî ñîîáùåíèé, íàõîäÿùèõñÿ íà ýòàïå ïåðåñûëêèâ êîíôèãóðàöèè γ .I t(γ) íîìåð ïðîöåññà, êîòîðîìó íàïðàâëåí ìàðêåð èëèêîòîðûé âëàäååò ìàðêåðîì â êîíôèãóðàöèè γ .(Çàìå÷àíèå: ìàðêåð ïåðåïðàâëÿåòñÿ ïðîöåññàì â ïîðÿäêåóáûâàíèÿ íîìåðîâ p0, pN−1, pN−2, . .
. , p1, p0, . . . ).I q(γ) ÷èñëî, êîòîðîå õðàíèò ìàðêåð â êîíôèãóðàöèè γ .Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsÀëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsIP0 (γ) ≡ (∀i (N > i > t(γ)) : statepi = passive) ∧Pq(γ) =mcpiN>i>t.Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsIP0 (γ) ≡ (∀i (N > i > t(γ)) : statepi = passive) ∧Pq(γ) =mcpiN>i>t!PP1 (γ) ≡mcpi + q(γ) > 0.Ii≤t(γ).Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsIP0 (γ) ≡ (∀i (N > i > t(γ)) : statepi = passive) ∧Pq(γ) =mcpiN>i>t!PP1 (γ) ≡mcpi + q(γ) > 0.Ii≤t(γ)I.P2 (γ) ≡ ∃j (t(γ) ≥ j ≥ 0) : colorpj = black.Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsIP0 (γ) ≡ (∀i (N > i > t(γ)) : statepi = passive) ∧Pq(γ) =mcpiN>i>t!PP1 (γ) ≡mcpi + q(γ) > 0.Ii≤t(γ).IP2 (γ) ≡ ∃j (t(γ) ≥ j ≥ 0) : colorpj = blackIP3 (γ) ≡ìàðêåð ÷åðíûé ..Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:PI PM (γ) ≡ (B(γ) =mcp ) .p∈procsIP0 (γ) ≡ (∀i (N > i > t(γ)) : statepi = passive) ∧Pq(γ) =mcpiN>i>t!PP1 (γ) ≡mcpi + q(γ) > 0.Ii≤t(γ)..IP2 (γ) ≡ ∃j (t(γ) ≥ j ≥ 0) : colorpj = blackIP3 (γ) ≡IP(γ) ≡ PM (γ) ∧ (P0 (γ) ∨ P1 (γ) ∨ P2 (γ) ∨ P3 (γ))ìàðêåð ÷åðíûé ..Àëãîðèòì ÑàôðûËåììà 3.Ïðåäèêàò P(γ) ÿâëÿåòñÿ èíâàðèàíòîì àëãîðèòìà Ñàôðû.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Ñòåïàíîâ, ÑëþñàðüÀëãîðèòì ÑàôðûÇàäà÷è.Êàêîâà ñëîæíîñòü àëãîðèòìà Ñàôðû ïî ÷èñëó îáìåíîâñîîáùåíèÿìè?À ìîæíî ëè àäàïòèðîâàòü àëãîðèòì Ñàôðû äëÿ ïðîâåðêèçàâåðøåíèÿ ðàáîòû áàçîâîãî àëãîðèòìà â ïðîèçâîëüíîé ñèëüíîñâÿçíîé ñåòè?Àëãîðèòì ÑàôðûÒåîðåìà 3.Àëãîðèòì Ñàôðû ÿâëÿåòñÿ êîððåêòíûì àëãîðèòìîìîáíàðóæåíèÿ çàâåðøåíèÿ âû÷èñëåíèÿ.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî ñ èñïîëüçîâàíèåì èíâàðèàíòà P(γ) .×èñòÿêîâ, ØåìÿêèíÀëãîðèòì âîçâðàùåíèÿ êðåäèòàÌàòòåðí ïðåäëîæèë àëãîðèòì, ïîçâîëÿþùèé îáíàðóæèâàòüçàâåðøåíèå âû÷èñëåíèÿ ñïóñòÿ íå áîëåå îäíîé åäèíèöûâðåìåíè, ïîñëå òîãî êàê ýòî ñëó÷èëîñü.Àëãîðèòì îáíàðóæèâàåò çàâåðøåíèå öåíòðàëèçîâàííîãîâû÷èñëåíèÿ ïðè óñëîâèè, ÷òî êàæäûé ïðîöåññ ñïîñîáåíîòïðàâèòü ñîîáùåíèå íåïîñðåäñòâåííî ñàìîìó èíèöèàòîðóâû÷èñëåíèÿ (ò.
å., ñåòü ñîäåðæèò ïîäãðàô, èìåþùèé ôîðìóçâåçäû, â öåíòðå êîòîðîé ðàñïîëîæåí èíèöèàòîð).Àëãîðèòì âîçâðàùåíèÿ êðåäèòà ýòîì àëãîðèòìå êàæäîìó ñîîáùåíèþ è êàæäîìó ïðîöåññóâðó÷àåòñÿ íåêîòîðûé êðåäèò ; åãî çíà÷åíèåì ñëóæèòâåùåñòâåííîå ÷èñëî, ðàñïîëîæåííîå ìåæäó 0 è 1(âêëþ÷èòåëüíî). Àëãîðèòì ñòðåìèòñÿ ñîõðàíèòüèíâàðèàíòíîñòü ñëåäóþùèõ óòâåðæäåíèé.S1. Ñóììàðíûé êðåäèò, âûäàííûé ñîîáùåíèÿì è ïðîöåññàì,ðàâåí 1.S2.
Âñÿêîìó áàçîâîìó ñîîáùåíèþ âðó÷àåòñÿ ïîëîæèòåëüíûéêðåäèò.S3. Âñÿêîìó àêòèâíîìó ïðîöåññó âðó÷àåòñÿ ïîëîæèòåëüíûéêðåäèò.Ïðîöåññû, èìåþùèå ïîëîæèòåëüíûé êðåäèò è íå ïîäïàäàþùèåïîä ïåðå÷èñëåííûå çàêîíû (ò. å. ïàññèâíûå ïðîöåññû),âîçâðàùàþò êðåäèò èíèöèàòîðó. Èíèöèàòîð ïîñòóïàåò ïîäîáíîáàíêó è ñîáèðàåò âñå êðåäèòû, êîòîðûå åìó îòïðàâëÿþò, âïåðåìåííîé ret (âîçâðàùåííûå êðåäèòû).Êîãäà èíèöèàòîð âëàäååò âñåìè êðåäèòàìè, òî îí ñîîáùàåò îçàâåðøåíèè áàçîâîãî àëãîðèòìà.Àëãîðèòì âîçâðàùåíèÿ êðåäèòàÏðàâèëî 1.Åñëè ret = 1 , òî èíèöèàòîð âûçûâàåò ïðîöåäóðóAnnounce.Àëãîðèòì âîçâðàùåíèÿ êðåäèòàÏðàâèëî 1.Ïðàâèëî 2.Åñëè ret = 1 , òî èíèöèàòîð âûçûâàåò ïðîöåäóðóAnnounce.Êàê òîëüêî ïðîöåññ ñòàíîâèòñÿ ïàññèâíûì, îíîòïðàâëÿåò ñâîé êðåäèò èíèöèàòîðó.Àëãîðèòì âîçâðàùåíèÿ êðåäèòàÏðàâèëî 1.Ïðàâèëî 2.Ïðàâèëî 3.Ïðàâèëî 4.Åñëè ret = 1 , òî èíèöèàòîð âûçûâàåò ïðîöåäóðóAnnounce.Êàê òîëüêî ïðîöåññ ñòàíîâèòñÿ ïàññèâíûì, îíîòïðàâëÿåò ñâîé êðåäèò èíèöèàòîðó.Êîãäà àêòèâíûé ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå,èìåþùèéñÿ â åãî ðàñïîðÿæåíèè êðåäèòðàçäåëÿåòñÿ ìåæäó ñàìèì ïðîöåññîì p è ýòèìñîîáùåíèåì.Êîãäà ïðîöåññ àêòèâèçèðóåòñÿ, åìó âðó÷àåòñÿêðåäèò, êîòîðûì îáëàäàëî àêòèâèçèðîâàâøåå åãîñîîáùåíèå.Àëãîðèòì âîçâðàùåíèÿ êðåäèòàÏðàâèëî 1.Ïðàâèëî 2.Ïðàâèëî 3.Ïðàâèëî 4.Ïðàâèëî 5.Åñëè ret = 1 , òî èíèöèàòîð âûçûâàåò ïðîöåäóðóAnnounce.Êàê òîëüêî ïðîöåññ ñòàíîâèòñÿ ïàññèâíûì, îíîòïðàâëÿåò ñâîé êðåäèò èíèöèàòîðó.Êîãäà àêòèâíûé ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå,èìåþùèéñÿ â åãî ðàñïîðÿæåíèè êðåäèòðàçäåëÿåòñÿ ìåæäó ñàìèì ïðîöåññîì p è ýòèìñîîáùåíèåì.Êîãäà ïðîöåññ àêòèâèçèðóåòñÿ, åìó âðó÷àåòñÿêðåäèò, êîòîðûì îáëàäàëî àêòèâèçèðîâàâøåå åãîñîîáùåíèå.Êàê òîëüêî àêòèâíûé ïðîöåññ ïîëó÷àåò áàçîâîåñîîáùåíèå, êðåäèò, êîòîðûì îáëàäàëî ýòîñîîáùåíèå, äîáàâëÿåòñÿ ê òîìó êðåäèòó, êîòîðûìðàñïîëàãàë ñàì ïðîöåññ.Àëãîðèòì âîçâðàùåíèÿ êðåäèòàvar statep : (active , passive ) init if p = p0 then active else passive ;credp: fractioninit if p = p0 then 1 else 0 ;ret: fractioninit 0 ; for p0 onlySp : { statep = active } (* Ïðàâèëî 3 *)begin send hmes, credp /2i ; credp := credp /2 endRp : { ñîîáùåíèå hmes, ci ïîñòóïèëî ïðîöåññó p }begin receive hmes, ci ; statep := active ;credp := credp + c (* Ïðàâèëà 4 è 5 *)endIp : { statep = active }begin statep := passive ;send hret, credp i to p0 ; credp := 0 (* Ïðàâèëî 2 *)endAp : { Ñîîáùåíèå hret, ci ïîñòóïèëî ïðîöåññó p0 }begin receive hret, ci ; ret := ret + c ;if ret = 1 then Announce (* Ïðàâèëî 1 *)end0Àëãîðèòì âîçâðàùåíèÿ êðåäèòàÒåîðåìà 4.Àëãîðèòì âîçâðàùåíèÿ êðåäèòà ÿâëÿåòñÿ êîððåêòíûìàëãîðèòìîì îáíàðóæåíèÿ çàâåðøåíèÿ âû÷èñëåíèé.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî ñôîðìèðóéòå íóæíûé èíâàðèàíò è ïðîâåäèòåäîêàçàòåëüñòâî.Ãóñüêîâ, Çàïóòëÿåâ, ÑàâêîâÀëãîðèòì ÐàíûÄëÿ ðåøåíèÿ çàäà÷è îáíàðóæåíèÿ çàâåðøåíèÿ âû÷èñëåíèÿìîæíî èñïîëüçîâàòü øòåìïåëè âðåìåíè.
Ïðåäïîëàãàåòñÿ, ÷òîâñå ïðîöåññû ñíàáæåíû ÷àñàìè; äëÿ ýòîé öåëè ïðèãîäíû êàêàïïàðàòíûå òàéìåðû, òàê è ëîãè÷åñêèå ÷àñû Ëàìïîðòà. îñíîâó àëãîðèòìà ïîëîæåí ëîêàëüíûé ïðåäèêàò quiet(p) ,îïðåäåëåííûé äëÿ êàæäîãî ïðîöåññà p òàê, ÷òîquiet(p)=⇒statep = passive ∧∧íèêàêîå áàçîâîå ñîîáùåíèå, îòïðàâëåííîå píå ïðåáûâàåò íà ýòàïå ïåðåñûëêè,îòêóäà ñëåäóåò èìïëèêàöèÿ (∀p quiet(p)) =⇒ term .Óñëîâèå quiet îïðåäåëÿåòñÿ ñëåäóþùèì ñîîòíîøåíèåìquiet(p) ≡ (statep = passive ∧ unackp = 0).Àëãîðèòì ÐàíûÖåëü àëãîðèòìà ïðîâåðèòü, âåðíî ëè, ÷òî â îïðåäåëåííûéìîìåíò âðåìåíè t âñå ïðîöåññû óäîâëåòâîðÿþò óñëîâèþ quiet .Ýòî îñóùåñòâëÿåòñÿ ïðè ïîìîùè âîëíû, ïî õîäó êîòîðîéêàæäîìó ïðîöåññó çàäàåòñÿ âîïðîñ î òîì, äîñòèã ëè ýòîòïðîöåññ â äàííûé ìîìåíò ñîñòîÿíèÿ quiet è áóäåò ëè îíîñòàâàòüñÿ â ýòîì ñîñòîÿíèè â äàëüíåéøåì.
Âñÿêèé ïðîöåññ, íåïðåáûâàþùèé â ñîñòîÿíèè quiet , íå ðåàãèðóåò íà ñîîáùåíèÿâîëíû, òåì ñàìûì ýôôåêòèâíî ãàñÿ ñàìó âîëíó.  êà÷åñòâåâîëíîâîãî àëãîðèòìà ìîæíî èñïîëüçîâàòü êîëüöåâîé àëãîðèòì.Âçàèìîäåéñòâèå âîëíû ñ ïðîöåññîì p íå îêàçûâàåò âëèÿíèÿ íàïåðåìåííûå ïðîöåññà p , èñïîëüçóåìûå äëÿ îáíàðóæåíèÿçàâåðøåíèÿ âû÷èñëåíèÿ. Âñëåäñòâèå ýòîãî ïðàâèëüíîñòüðàáîòû àëãîðèòìà íå íàðóøàåòñÿ ïðè ïàðàëëåëüíîìðàñïðîñòðàíåíèè íåñêîëüêèõ âîëí.Àëãîðèòì ÐàíûÏðîöåññ p , ïåðåéäÿ â ñîñòîÿíèå quiet , ñîõðàíÿåò â ïàìÿòè òîòìîìåíò âðåìåíè qtp , êîãäà ïðîèçîøëî ýòî ñîáûòèå, èçàïóñêàåò âîëíó, ÷òîáû ïðîâåðèòü, âñå ëè ïðîöåññû óæåïåðåøëè â ñîñòîÿíèå quiet ê ìîìåíòó âðåìåíè qtp .Åñëè ýòî òàê, òî çàâåðøåíèå âû÷èñëåíèÿ ñ÷èòàåòñÿîáíàðóæåííûì.
 ïðîòèâíîì ñëó÷àå ñóùåñòâóåò ïðîöåññ,êîòîðûé ïåðåéäåò â ñîñòîÿíèå quiet ïîçæå, è îí çàïóñòèò íîâóþâîëíó.Àëãîðèòì Ðàíûvar statep : (active , passive ) ;θp: integer init 0 ; (* Ëîãè÷åñêèå ÷àñû *)unackp : integer init 0 ; (* ×èñëî íåïîäòâåðæäåííûõ ñîîáùåíèéqtp: integer init 0 ; (* Âðåìÿ íåäàâíî ñëó÷èâøåãîñÿ ïåðåõîäàSp : { statep = active }begin θp := θp + 1 ; send hmes, θp i ; unackp := unackp + 1 endRp : { Ñîîáùåíèå hmes, θi èç q äîñòèãëî p }begin receive hmes, θi; θp := max(θp , θ) + 1 ;send hack, θp i to q ; statep := activeendIp : { statep = active }begin θp := θp + 1 ; statep := passive ;if unackp = 0 then (* p ïåðåõîäèò â ñîñòîÿíèå quite *)begin qtp := θp ; send htok, θp , qtp , pi to Nextp endendÀëãîðèòì Ðàíû (ïðîäîëæåíèå)Ap : { Ïîäòâåðæäåíèå hack, θi äîñòèãëî p }begin receive hack, θi ; θp := max(θp , θ) + 1 ;unackp := unackp − 1 ;if unackp = 0 and statep = passive then (* p ïåðåõîäèò â quibegin qtp := θp ; send htok, θp , qtp , pi to Nextp endendTp : { Ìàðêåð htok, θ, qt, qi äîñòèã p }begin receive htok, θ, qt, qi ; θp := max(θp , θ) + 1 ;if quiet(p) thenif p = q then Announceelse if qt ≥ qtp then send htok, θp , qt, qi to NextpendÀëãîðèòì ÐàíûÒåîðåìà 5.Àëãîðèòì Ðàíû ÿâëÿåòñÿ êîððåêòíûì àëãîðèòìîì îáíàðóæåíèÿçàâåðøåíèÿ âû÷èñëåíèé.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî ñôîðìèðóéòå íóæíûé èíâàðèàíò è ïðîâåäèòåäîêàçàòåëüñòâî.Áàãðîâ, Âàñèëåíêî, ÕàõàëèíÊÎÍÅÖ ËÅÊÖÈÈ 11..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
