Лекция 11. Обнаруж завершения вычисл. Алгоритм Дейкстры-Шолтена_ Шави-Франчеза_ Сафры_ возвращения кредитов_ Рана (1185661), страница 2
Текст из файла (страница 2)
Ñîîáùåíèÿ ëèñòüÿ äåðåâà T ; â êàæäîì ïðîöåññå åñòü ïåðåìåííàÿ äëÿïîäñ÷åòà ÷èñëà âåðøèí-ïîñëåäîâàòåëåé ýòîãî ïðîöåññà âäåðåâå T . Óäàëåíèå èç äåðåâà âåðøèíû-ïîñëåäîâàòåëÿïðîöåññà p îñóùåñòâëÿåòñÿ â äðóãîì ïðîöåññå q â ðåçóëüòàòåòîãî, ÷òî âåðøèíà-ïîñëåäîâàòåëüa) ëèáî ñîîòâåòñòâóåò ñîîáùåíèþ, äîñòèãøåìó ïðîöåññà q ,b) ëèáî ñîîòâåòñòâóåò ñàìîìó ïðîöåññó q .×òîáû â ïðîöåññå p íå íàðóøàëñÿ ó÷åò âåðøèí-ïîñëåäîâàòåëåé,åìó îòïðàâëåòñÿ ñèãíàëüíîå ñîîáùåíèå sigp ïðè óäàëåíèèâåðøèíû-ïîñëåäîâàòåëÿ ïðîöåññà p .
Ýòî ñîîáùåíèå çàìåùàåòóäàëåííóþ âåðøèíó-ïîñëåäîâàòåëÿ ïðîöåññà p , à óäàëåíèå ýòîéâåðøèíû èç äåðåâà îñóùåñòâëÿåòñÿ ñàìèì ïðîöåññîì p ïîñëåïîëó÷åíèÿ óêàçàííîãî ñèãíàëà; ïðè ýòîì p óìåíüøàåò çíà÷åíèåñ÷åò÷èêà ïîñëåäîâàòåëåé íà 1.Àëãîðèòì Äåéêñòðû-Øîëòåíàvar statep : (active , passive ) init if p = p0 then active else passive ;scp: integerinit 0 ;fatherp : Pinit if p = p0 then p else udef ;Sp : { statep = active }begin send hmes, pi ; scp := scp + 1 endRp : {Ñîîáùåíèå hmes, qi äîñòèãëî ïðîöåññà p }begin receive hmes, qi ; statep := active ;if fatherp = udef then fatherp := q else send hsig, qi to qendIp : { statep = active }begin statep := passive ;if scp = 0 then(* Óäàëèòü p èç T *)begin if fatherp = pthen Announceelse send hsig, fatherp i to fatherp ;fatherp := udefendÀëãîðèòì Äåéêñòðû-ØîëòåíàAp : { Ñèãíàë hsig, pi äîñòèãàåò p }begin receive hsig, pi ; scp := scp − 1 ;if scp = 0 and statep = passive thenbegin if fatherp = pthen Announceelse send hsig, fatherp i to fatherp ;fatherp := udefendendÀëãîðèòì Äåéêñòðû-ØîëòåíàÄëÿ îáîñíîâàíèÿ êîððåêòíîñòè àëãîðèòìà íóæíî ïîêàçàòü, ÷òîãðàô T ÿâëÿåòñÿ äåðåâîì è ïðè ýòîì ñòàíîâèòñÿ ïóñòûìòîëüêî â òîì ñëó÷àå, êîãäà áàçîâîå âû÷èñëåíèå çàâåðøèëîñü.Äëÿ âñÿêîé êîíôèãóðàöèè γ îïðåäåëèì äâà ìíîæåñòâàVT ={p : fatherp 6= udef } ∪ {hmes, pi íà ýòàïå ïåðåñûëêè}∪ {hsig, pi íà ýòàïå ïåðåñûëêè}èET={(p, fatherp ) : fatherp 6= udef ∧ fatherp 6= p}∪ {(h, pi, p) : h, pi}∪ {(h , pi, p) : h , pi}.messigmes íà ýòàïå ïåðåñûëêèsig íà ýòàïå ïåðåñûëêèÀëãîðèòì Äåéêñòðû-ØîëòåíàÑâîéñòâî áåçîïàñíîñòè àëãîðèòìà îáåñïå÷èâàåòñÿèíâàðèàíòîì P , êîòîðûé îïðåäåëÿåòñÿñëåäóþùèì îáðàçîì:P≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ T äåðåâî ñ êîðíåì p0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT .Àëãîðèòì Äåéêñòðû-ØîëòåíàP≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ Tp0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT .
äåðåâî ñ êîðíåì(1)(2)(3)(4)(5)Cîãëàñíî îïðåäåëåíèþ ìíîæåñòâî âåðøèí ãðàôà T âêëþ÷àåòâñå ñîîáùåíèÿ (êàê áàçîâûå, òàê è êîíòðîëüíûå), à òàêæå,ñîãëàñíî ñîîòíîøåíèþ (1), âñå àêòèâíûå ïðîöåññû.Àëãîðèòì Äåéêñòðû-ØîëòåíàP≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ Tp0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT . äåðåâî ñ êîðíåìÑîîòíîøåíèå (2) èãðàåò âñïîìîãàòåëüíóþ ðîëü; â íåìóòâåðæäàåòñÿ, ÷òî T äåéñòâèòåëüíî ÿâëÿåòñÿ ãðàôîì è âñåäóãè íàïðàâëåíû ê ïðîöåññàì.(1)(2)(3)(4)(5)Àëãîðèòì Äåéêñòðû-ØîëòåíàP≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ Tp0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT . äåðåâî ñ êîðíåìÑîîòíîøåíèå (3) ãëàñèò î òîì, ÷òî ïîäñ÷åòâåðøèí-ïîñëåäîâàòåëåé ïðîâîäèòñÿ êàæäûì ïðîöåññîìêîððåêòíî(1)(2)(3)(4)(5)Àëãîðèòì Äåéêñòðû-ØîëòåíàP≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ Tp0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT .
äåðåâî ñ êîðíåì(1)(2)(3)(4)(5)â ñîîòíîøåíèè (4) óòâåðæäàåòñÿ, ÷òî T ÿâëÿåòñÿ äåðåâîì èïðîöåññ p0 ýòî åãî êîðåíü.Àëãîðèòì Äåéêñòðû-ØîëòåíàP≡∧∧∧∧statep = active =⇒ p ∈ VT(u, v ) ∈ ET =⇒ u ∈ VT ∧ v ∈ VT ∩ Pscp = #{v : (v , p) ∈ ET }VT 6= ∅ =⇒ Tp0(statep = passive ∧ scp = 0) =⇒ p 6∈ VT . äåðåâî ñ êîðíåìÑîîòíîøåíèå (5) ñëóæèò äëÿ òîãî, ÷òîáû ïîêàçàòü, ÷òî ýòîäåðåâî äåéñòâèòåëüíî èñ÷åçàåò, åñëè áàçîâîå âû÷èñëåíèåçàâåðøèòñÿ.(1)(2)(3)(4)(5)Àëãîðèòì Äåéêñòðû-ØîëòåíàËåììà 1.Ïðåäèêàò P ÿâëÿåòñÿ èíâàðèàíòîì àëãîðèòìàÄåéêñòðûØîëòåíà.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Âàøóðîâ, Êî÷åòêîâÀëãîðèòì Äåéêñòðû-ØîëòåíàÒåîðåìà 1.Àëãîðèòì ÄåéêñòðûØîëòåíà ÿâëÿåòñÿ êîððåêòíûìàëãîðèòìîì îáíàðóæåíèÿ çàâåðøåíèÿ âû÷èñëåíèÿ; â íåìèñïîëüçóåòñÿ M îáìåíîâ êîíòðîëüíûìè ñîîáùåíèÿìè.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Ëèíü, ØåðâàëûÀëãîðèòì Äåéêñòðû-Øîëòåíà àëãîðèòìå ÄåéêñòðûØîëòåíà äîñòèãíóò çàìå÷àòåëüíûéáàëàíñ ìåæäó êîíòðîëüíûìè è áàçîâûìè ñîîáùåíèÿìè; äëÿêàæäîãî áàçîâîãî ñîîáùåíèÿ, îòïðàâëåííîãî ïðîöåññîì pïðîöåññó q , ðàññìîòðåííûé àëãîðèòì îòïðàâëÿåò â òî÷íîñòèîäíî ñîîáùåíèå îò ïðîöåññà q ê ïðîöåññó p .Ñëîæíîñòü ïî ÷èñëó êîíòðîëüíûõ ñîîáùåíèé äîñòèãàåò íèæíåéîöåíêè, è ïîýòîìó äàííûé àëãîðèòì ÿâëÿåòñÿ îïòèìàëüíûì ïîñëîæíîñòè â íàèõóäøåì ñëó÷àå àëãîðèòìîì îáíàðóæåíèÿçàâåðøåíèÿ öåíòðàëèçîâàííûõ âû÷èñëåíèé.Àëãîðèòì ØàâèÔðàí÷åçàÎáîùàåò àëãîðèòì ÄåéêñòðûØîëòåíà äëÿ ñëó÷àÿäåöåíòðàëèçîâàííûõ áàçîâûõ âû÷èñëåíèé. àëãîðèòìå ØàâèÔðàí÷åçà ãðàô âû÷èñëåíèé ÿâëÿåòñÿëåñîì , êàæäîå äåðåâî êîòîðîãî èìååò â êà÷åñòâå êîðíÿ îäèí èçèíèöèàòîðîâ áàçîâîãî âû÷èñëåíèÿ.Äëÿ îáîçíà÷åíèÿ äåðåâà, êîðíåì êîòîðîãî ñëóæèò ïðîöåññ p ,áóäåì èñïîëüçîâàòü çàïèñü Tp .Àëãîðèòì ØàâèÔðàí÷åçà àëãîðèòìå ØàâèÔðàí÷åçà ñòðîèòñÿ òàêîé ãðàôF = (VF , EF ) , ÷òî(1) ëèáî F ïóñò, ëèáî F ïðåäñòàâëÿåò ñîáîé ëåñ, êàæäîåäåðåâî êîòîðîãî èìååò îäèí èç èíèöèàòîðîâ â êà÷åñòâåêîðíÿ,(2) ìíîæåñòâî VF ñîäåðæèò âñå àêòèâíûå ïðîöåññû è âñåáàçîâûå ñîîáùåíèÿ, ïðåáûâàþùèå íà ýòàïå ïåðåñûëêè.Çàâåðøåíèå áàçîâîãî âû÷èñëåíèÿ áóäåò îáíàðóæåíî, êîãäàóêàçàííûé ãðàô ñòàíîâèòñÿ ïóñòûì.Îäíàêî íå ïðîñòî óáåäèòüñÿ â òîì, ÷òî ýòîò ãðàô ñòàë ïóñòûì.Ïîñêîëüêó êîðíåì äåðåâà âû÷èñëåíèé ñëóæèò ïðîöåññ p0 ,èìåííî ïðîöåññ p0 ìîæåò îöåíèòü, ÿâëÿåòñÿ ëè äåðåâî ïóñòûì,è âûçâàòü â ýòîì ñëó÷àå ïðîöåäóðó Announce.Êîãäà ìû èìååì äåëî ñ ëåñîì, êàæäûé èíèöèàòîð ìîæåòóñòàíîâèòü ïóñòîòó ñâîåãî ñîáñòâåííîãî äåðåâà, íî ýòî åùå íåáóäåò îçíà÷àòü, ÷òî âåñü ëåñ ñòàë ïóñòûì ãðàôîì.Àëãîðèòì ØàâèÔðàí÷åçàÏðîâåðêà òîãî, ÷òî âñå äåðåâüÿ èñ÷åçëè, ïðîâîäèòñÿ ïðèïîìîùè îäíîé-åäèíñòâåííîé âîëíû.Ëåñ F ñòðîèòñÿ òàê, ÷òîáû âñÿêîå äåðåâî Tp , ñòàâøåå ïóñòûì,îñòàâàëîñü ïóñòûì è â äàëüíåéøåì.
Ýòî íå ïðåïÿòñòâóåòïðîöåññó p âíîâü ñòàíîâèòüñÿ àêòèâíûì, íî åñëè p ñòàíîâèòñÿàêòèâíûì ïîñëå èñ÷åçíîâåíèÿ åãî ñîáñòâåííîãî äåðåâà, òî îíçàíîñèòñÿ â äåðåâî äðóãîãî èíèöèàòîðà.Êàæäûé ïðîöåññ ïðèíèìàåò ó÷àñòèå â ðàñïðîñòðàíåíèè âîëíûòîëüêî òîãäà, êîãäà åãî äåðåâî èñ÷åçàåò; è åñëè âîëíà ïðèâîäèòê òîìó, ÷òî ïðèíèìàåòñÿ ðåøåíèå, òî âûçûâàåòñÿ ïðîöåäóðàîïîâåùåíèÿ Announce.Àëãîðèòì ØàâèÔðàí÷åçàÊàæäûé ïðîöåññ p ðàñïîëàãàåò ïåðåìåííîé fatherp .Çíà÷åíèå ýòîé ïåðåìåííîé ïîëàãàåòñÿ ðàâíûì udef, åñëèp 6∈ VT .Åñëè æå p ÿâëÿåòñÿ êîðíåì äåðåâà, òî çíà÷åíèåì ïåðåìåííîéfatherp ÿâëÿåòñÿ èìÿ ïðîöåññà p .È íàêîíåö, åñëè p ÿâëÿåòñÿ íåêîðíåâîé âåðøèíîé äåðåâà T , òîçíà÷åíèåì ïåðåìåííîé fatherp ñëóæèò èìÿ ðîäèòåëüñêîéâåðøèíû äàííîãî ïðîöåññà.Ïåðåìåííàÿ scp èñïîëüçóåòñÿ äëÿ ïîäñ÷åòà ÷èñëàïîñëåäîâàòåëåé âåðøèíû p â äåðåâå T .Áóëåâà ïåðåìåííàÿ emptyp ïðèíèìàåò çíà÷åíèå true òîãäà èòîëüêî òîãäà, êîãäà äåðåâî, â êîòîðîì ñîäåðæèòñÿ âåðøèíà p ,ñòàíîâèòñÿ ïóñòûì.Àëãîðèòì ØàâèÔðàí÷åçàvar statep : (active , passive ) init if p is initiator then active else passivescp: integerinit 0 ;fatherp : Pinit if p is initiator then p else udef ;emptyp : boolinit if p is initiator then false else true ;Sp : { statep = active }begin send hmes, pi ; scp := scp + 1 endRp : {Ñîîáùåíèå hmes, qi ïîñòóïèëî ïðîöåññó p }begin receive hmes, qi ; statep := active ;if fatherp = udef then fatherp := q else send hsig, qi to qendIp : { statep = active }begin statep := passive ;if scp = 0 then (* Óäàëèòü p èç F *)beginif fatherp = p then emptyp := true else send hsig, fatherp i tfatherp := udefendÀëãîðèòì ØàâèÔðàí÷åçàAp : { Ñèãíàë hsig, pi äîñòèãàåò p }begin receive hsig, pi ; scp := scp − 1 ;if scp = 0 and statep = passive thenbeginif fatherp = p then emptyp := true else send hsig, fatherp ifatherp := udefendendÀëãîðèòì ØàâèÔðàí÷åçàÏðèìå÷àíèÿ.1.
 ïðèâåäåííîì îïèñàíèè âîëíîâîé àëãîðèòì â ÿâíîì âèäåíå âûäåëåí.2. Âîëíîâîé àëãîðèòì çàïóñêàþò òîëüêî èíèöèàòîðû áàçîâûõâû÷èñëåíèé3. Âñå ïðîöåññû ïðîâîäÿò ïàðàëëåëüíîå âûïîëíåíèåâîëíîâîãî àëãîðèòìà, ïðè÷åì îòïðàâëåíèå ñîîáùåíèé èëèïðèíÿòèå ðåøåíèÿ ðàçðåøàåòñÿ òîëüêî òåì ïðîöåññàì p , óêîòîðûõ ïåðåìåííàÿ emptyp èìååò çíà÷åíèå true .4. Ïðè îñóùåñòâëåíèè ñîáûòèÿ decide âûçûâàåòñÿ ïðîöåäóðàAnnounce.Àëãîðèòì ØàâèÔðàí÷åçàÄëÿ âñÿêîé êîíôèãóðàöèè γ îïðåäåëèì ñëåäóþùåå ìíîæåñòâîâåðøèí:VT ={p : fatherp 6= udef } ∪ {hmes, pi íà ýòàïå ïåðåñûëêè}∪ {hsig, pi íà ýòàïå ïåðåñûëêè}è äóãEF={(p, fatherp ) : fatherp 6= udef ∧ fatherp =6 p}∪ {(h, pi, p) : h, pi}∪ {(h , pi, p) : h , pi}.messigmes íà ýòàïå ïåðåñûëêèsig íà ýòàïå ïåðåñûëêèÀëãîðèòì ØàâèÔðàí÷åçàÄîñòàòî÷íûå óñëîâèÿ êîððåêòíîñòè (òàêíàçûâàåìîå ñâîéñòâî áåçîïàñíîñòè àëãîðèòìà)îáåñïå÷èâàþòñÿ èíâàðèàíòîì Q :Q ⇐⇒∧∧∧∧∧statep = active =⇒ p ∈ VF(u, v ) ∈ EF =⇒ u ∈ VF ∧ v ∈ VF ∩ Pscp = #{v : (v , p) ∈ EF }VF 6= ∅ =⇒ F ÿâëÿåòñÿ ëåñîì(statep = passive ∧ scp = 0) =⇒ p 6∈ VFemptyp ⇐⇒ Tp ïóñòîÀëãîðèòì ØàâèÔðàí÷åçàËåììà 2.Ïðåäèêàò Q ÿâëÿåòñÿ èíâàðèàíòîì àëãîðèòìàØàâèÔðàí÷åçà.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Æàéëàóîâà, ÒàðàòóòàÀëãîðèòì ØàâèÔðàí÷åçàÒåîðåìà 2.Àëãîðèòì ØàâèÔðàí÷åçà ÿâëÿåòñÿ êîððåêòíûì àëãîðèòìîìîáíàðóæåíèÿ çàâåðøåíèÿ âû÷èñëåíèÿ; â íåì èñïîëüçóåòñÿM + W îáìåíîâ êîíòðîëüíûìè ñîîáùåíèÿìè.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.Íîâîñåëîâ, Ñû÷åâàÀëãîðèòì ÑàôðûÓñëîâèÿ ïðèìåíåíèÿ:I Áàçîâûé àëãîðèòì äåöåíòðàëèçîâàííûé.Àëãîðèòì ÑàôðûÓñëîâèÿ ïðèìåíåíèÿ:I Áàçîâûé àëãîðèòì äåöåíòðàëèçîâàííûé.I Êàíàëû ñâÿçè îäíîíàïðàâëåííûå.Àëãîðèòì ÑàôðûÓñëîâèÿ ïðèìåíåíèÿ:I Áàçîâûé àëãîðèòì äåöåíòðàëèçîâàííûé.I Êàíàëû ñâÿçè îäíîíàïðàâëåííûå.I  ñåòè ñóùåñòâóåò ãàìèëüòîíîâ êîíòóð, ïî êîòîðîìóðàñïðîñòðàíÿþòñÿ êîíòðîëüíûå ñîîáùåíèÿ; áàçîâûåñîîáùåíèÿ ìîãóò ïåðåäàâàòüñÿ ïî ëþáûì êàíàëàì.Àëãîðèòì ÑàôðûÓñëîâèÿ ïðèìåíåíèÿ:I Áàçîâûé àëãîðèòì äåöåíòðàëèçîâàííûé.I Êàíàëû ñâÿçè îäíîíàïðàâëåííûå.I  ñåòè ñóùåñòâóåò ãàìèëüòîíîâ êîíòóð, ïî êîòîðîìóðàñïðîñòðàíÿþòñÿ êîíòðîëüíûå ñîîáùåíèÿ; áàçîâûåñîîáùåíèÿ ìîãóò ïåðåäàâàòüñÿ ïî ëþáûì êàíàëàì.I Êîíòðîëüíûé àëãîðèòì öåíòðàëèçîâàííûé âîëíîâîéàëãîðèòì â îäíîíàïðàâëåííîì êîëüöå.Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.I Èíèöèàëèçàòîð êîíòðîëüíîãî àëãîðèòèìà çàïóñêàåò ìàðêåðöâåòà white .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.I Èíèöèàëèçàòîð êîíòðîëüíîãî àëãîðèòèìà çàïóñêàåò ìàðêåðöâåòà white .I Ïîñëå ïðèåìà áàçîâîãî ñîîáùåíèÿ ïðîöåññ îêðàøèâàåòñÿ âöâåò black .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.I Èíèöèàëèçàòîð êîíòðîëüíîãî àëãîðèòèìà çàïóñêàåò ìàðêåðöâåòà white .I Ïîñëå ïðèåìà áàçîâîãî ñîîáùåíèÿ ïðîöåññ îêðàøèâàåòñÿ âöâåò black .I Ïðîöåññ öâåòà black îêðàøèâàåò ìàðêåð â öâåò black .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.I Èíèöèàëèçàòîð êîíòðîëüíîãî àëãîðèòèìà çàïóñêàåò ìàðêåðöâåòà white .I Ïîñëå ïðèåìà áàçîâîãî ñîîáùåíèÿ ïðîöåññ îêðàøèâàåòñÿ âöâåò black .I Ïðîöåññ öâåòà black îêðàøèâàåò ìàðêåð â öâåò black .I Ïîñëå ïåðåäà÷è ìàðêåðà ïðîöåññ îêðàøèâàåòñÿ â öâåòwhite .Àëãîðèòì ÑàôðûÏðèíöèïû ðàáîòû.I Êàæäûé ïðîöåññ ìîæåò èìåòü íåêîòîðûé öâåò, êîòîðûéçàäàåòñÿ ïåðåìåííîé color ; ýòà ïåðåìåííàÿ ìîæåò èìåòüîäíî èç äâóõ çíà÷åíèé white èëè black .I Êîíòðîëüíûå ñîîáùåíèÿ (ìàðêåðû ) òàêæå îêðàøèâàþòñÿâ îäèí èç äâóõ öâåòîâ white èëè black .I Ìàðêåð ïåðåäàåòñÿ òîëüêî ïàññèâíûìè ïðîöåññàìè.I Èíèöèàëèçàòîð êîíòðîëüíîãî àëãîðèòèìà çàïóñêàåò ìàðêåðöâåòà white .I Ïîñëå ïðèåìà áàçîâîãî ñîîáùåíèÿ ïðîöåññ îêðàøèâàåòñÿ âöâåò black .I Ïðîöåññ öâåòà black îêðàøèâàåò ìàðêåð â öâåò black .I Ïîñëå ïåðåäà÷è ìàðêåðà ïðîöåññ îêðàøèâàåòñÿ â öâåòwhite .I Åñëè èíèöèàëèçàòîð ïðèíèìàåò ìàðêåð öâåòà white , òî îíîáúÿâëÿåò î çàâåðøåíèè áàçîâîãî àëãîðèòìà.Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passiveactivepassive@@@@R6passive?6g?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@@@Ri h6passivemsg?6g?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@@@Ri h6gpassivemsg?6?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@g@@Ri h6passivemsg?6?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@g@@Ri h6passivemsg?6?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@@@Ri h6gpassivemsg?6?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@@@R- ~6gactive?6?Àëãîðèòì ÑàôðûÏåðå÷èñëåííûõ ïðèíöèïîâ íåäîñòàòî÷íî äëÿ ïðàâèëüíîéðàáîòû àëãîðèòìà.passivepassivepassive@@@@R- ~6active?6g?Àëãîðèòì ÑàôðûÅùå òðè ïðèíöèïà ðàáîòû.I Êàæäûé ïðîöåññ p ñíàáæåí ñ÷åò÷èêîì áàçîâûõ ñîîáùåíèémcp , êîòîðûé óâåëè÷èâàåòñÿ íà 1 ïðè îòïðàâëåíèèïðîöåññîì áàçîâîãî ñîîáùåíèÿ è óìåíüøàåòñÿ íà 1 ïðèïðèåìå áàçîâîãî ñîîáùåíèÿ.Àëãîðèòì ÑàôðûÅùå òðè ïðèíöèïà ðàáîòû.I Êàæäûé ïðîöåññ p ñíàáæåí ñ÷åò÷èêîì áàçîâûõ ñîîáùåíèémcp , êîòîðûé óâåëè÷èâàåòñÿ íà 1 ïðè îòïðàâëåíèèïðîöåññîì áàçîâîãî ñîîáùåíèÿ è óìåíüøàåòñÿ íà 1 ïðèïðèåìå áàçîâîãî ñîîáùåíèÿ.I Ìàðêåð ïðè ïðîõîæäåíèè ÷åðåç ïðîöåññû ñóììèðóåòïîêàçàíèÿ èõ ñ÷åò÷èêîâ.Àëãîðèòì ÑàôðûÅùå òðè ïðèíöèïà ðàáîòû.I Êàæäûé ïðîöåññ p ñíàáæåí ñ÷åò÷èêîì áàçîâûõ ñîîáùåíèémcp , êîòîðûé óâåëè÷èâàåòñÿ íà 1 ïðè îòïðàâëåíèèïðîöåññîì áàçîâîãî ñîîáùåíèÿ è óìåíüøàåòñÿ íà 1 ïðèïðèåìå áàçîâîãî ñîîáùåíèÿ.I Ìàðêåð ïðè ïðîõîæäåíèè ÷åðåç ïðîöåññû ñóììèðóåòïîêàçàíèÿ èõ ñ÷åò÷èêîâ.I Çàâåðøåíèå ðàáîòû áàçîâîãî àëãîðèòìà ðåãèñòðèðóåòñÿ,åñëè ñóììà ñîáðàííûõ ìàðêåðîì ïîêàçàíèé ñ÷åò÷èêîâðàâíà 0.Àëãîðèòì Ñàôðûpassive0activepassive@@@@R006passive06g0?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@@@R10i h6passivemsg06g0?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@@@R10i h6g0passivemsg06?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@g1@@R10i h6passivemsg06?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@1 g@@R10i h6passivemsg06?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@@@R10i h61 gpassivemsg06?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@@@R- ~161 g06active?0?Àëãîðèòì Ñàôðûpassive0passivepassive@@@@R- ~1606active?01 g?Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðàâèëî Ì:Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðîöåññ-ïîëó÷àòåëü îêðàøèâàåòñÿ â öâåò black .Ïðàâèëî Ì:Ïðàâèëî 1:Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðîöåññ-ïîëó÷àòåëü îêðàøèâàåòñÿ â öâåò black .Òîëüêî ïàññèâíûé ïðîöåññ ìîæåò ðàáîòàòü ñìàðêåðîì, è åñëè ïðîöåññ ïåðåäàåò ìàðêåð, òî îíäîáàâëÿåò ê ïîìåòêå ìàðêåðà q çíà÷åíèå ñâîåãîñ÷åò÷èêà ñîîáùåíèé.Ïðàâèëî Ì:Ïðàâèëî 1:Ïðàâèëî 2:Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðîöåññ-ïîëó÷àòåëü îêðàøèâàåòñÿ â öâåò black .Òîëüêî ïàññèâíûé ïðîöåññ ìîæåò ðàáîòàòü ñìàðêåðîì, è åñëè ïðîöåññ ïåðåäàåò ìàðêåð, òî îíäîáàâëÿåò ê ïîìåòêå ìàðêåðà q çíà÷åíèå ñâîåãîñ÷åò÷èêà ñîîáùåíèé.Êîãäà ïðîöåññ öâåòà black ïåðåäàåò ìàðêåð,ìàðêåð ïðèîáðåòàåò îêðàñêó black .Ïðàâèëî Ì:Ïðàâèëî 1:Ïðàâèëî 2:Ïðàâèëî 3:Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðîöåññ-ïîëó÷àòåëü îêðàøèâàåòñÿ â öâåò black .Òîëüêî ïàññèâíûé ïðîöåññ ìîæåò ðàáîòàòü ñìàðêåðîì, è åñëè ïðîöåññ ïåðåäàåò ìàðêåð, òî îíäîáàâëÿåò ê ïîìåòêå ìàðêåðà q çíà÷åíèå ñâîåãîñ÷åò÷èêà ñîîáùåíèé.Êîãäà ïðîöåññ öâåòà black ïåðåäàåò ìàðêåð,ìàðêåð ïðèîáðåòàåò îêðàñêó black .Êîãäà ïðîõîæäåíèå âîëíû çàêàí÷èâàåòñÿíåóäà÷íî, ïðîöåññ p0 çàïóñêàåò íîâóþ âîëíó.Ïðàâèëî Ì:Ïðàâèëî 1:Ïðàâèëî 2:Ïðàâèëî 3:Ïðàâèëî 4:Àëãîðèòì ÑàôðûÈòàê, ïðàâèëà àëãîðèòìà.Êîãäà ïðîöåññ p îòïðàâëÿåò ñîîáùåíèå, îíóâåëè÷èâàåò çíà÷åíèå ñâîåãî ñ÷åò÷èêà; êîãäàïðîöåññ p ïîëó÷àåò ñîîáùåíèå, îí óìåíüøàåòçíà÷åíèå ñâîåãî ñ÷åò÷èêà.Ïðîöåññ-ïîëó÷àòåëü îêðàøèâàåòñÿ â öâåò black .Òîëüêî ïàññèâíûé ïðîöåññ ìîæåò ðàáîòàòü ñìàðêåðîì, è åñëè ïðîöåññ ïåðåäàåò ìàðêåð, òî îíäîáàâëÿåò ê ïîìåòêå ìàðêåðà q çíà÷åíèå ñâîåãîñ÷åò÷èêà ñîîáùåíèé.Êîãäà ïðîöåññ öâåòà black ïåðåäàåò ìàðêåð,ìàðêåð ïðèîáðåòàåò îêðàñêó black .Êîãäà ïðîõîæäåíèå âîëíû çàêàí÷èâàåòñÿíåóäà÷íî, ïðîöåññ p0 çàïóñêàåò íîâóþ âîëíó.Ñðàçó ïîñëå ïåðåäà÷è ìàðêåðà âñÿêèé ïðîöåññîêðàøèâàåòñÿ â öâåò white .Ïðàâèëî Ì:Ïðàâèëî 1:Ïðàâèëî 2:Ïðàâèëî 3:Ïðàâèëî 4:Ïðàâèëî 5:Àëãîðèòì Ñàôðûvar statep : (active , passive ) ;colorp: (white , black ) ;mcp: integer init 0 ;Sp : { statep = active }begin send hmesi ;mcp := mcp + 1 (* Ïðàâèëî M *)endRp : { Ñîîáùåíèå hmesi äîñòàâëåíî ïðîöåññó p }begin receive hmesi ; statep := active ;endmcp := mcp − 1colorp := black; (* Ïðàâèëî M *)(* Ïðàâèëî 1 *)Àëãîðèòì ÑàôðûIp : { statep = active }begin statep := passive endÏðèñòóïèòü ê îáíàðóæåíèþ çàâåðøåíèÿ âû÷èñëåíèÿ,âûïîëíÿåòñÿ îäèí ðàç ïðîöåññîì p0:begin send htok, white, 0i to pN−1 endTp : (* Ïðîöåññ p îáðàáàòûâàåò ìàðêåð htok, c, qi*){ statep = passive } (* Ïðàâèëî 2 *)begin if p = p0then if (c = white) ∧ (colorp = white) ∧ (mcp + q = 0)then Announceelse send htok, white, 0i to pN−1 (* Ïðàâèëî 4 *)else if (colorp = white) (* Ïðàâèëà 2 è 3 *)then send htok, c, q + mcp i to Nextpelse send htok, black, q + mcp i to Nextp ;colorp := white (* Ïðàâèëî 5 *)endÀëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:I B(γ) ÷èñëî ñîîáùåíèé, íàõîäÿùèõñÿ íà ýòàïå ïåðåñûëêèâ êîíôèãóðàöèè γ .Àëãîðèòì ÑàôðûÄëÿ äîêàçàòåëüñòâà êîððåêòíîñòè ââåäåì ñëåäóþùèå òåðìû èïðåäèêàòû:I B(γ) ÷èñëî ñîîáùåíèé, íàõîäÿùèõñÿ íà ýòàïå ïåðåñûëêèâ êîíôèãóðàöèè γ .I t(γ) íîìåð ïðîöåññà, êîòîðîìó íàïðàâëåí ìàðêåð èëèêîòîðûé âëàäååò ìàðêåðîì â êîíôèãóðàöèè γ .(Çàìå÷àíèå: ìàðêåð ïåðåïðàâëÿåòñÿ ïðîöåññàì â ïîðÿäêåóáûâàíèÿ íîìåðîâ p0, pN−1, pN−2, .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
