2016 Алгоритм Сафры_ корректность (подробное решение)
Описание файла
PDF-файл из архива "2016 Алгоритм Сафры_ корректность (подробное решение)", который расположен в категории "". Всё это находится в предмете "распределенные алгоритмы" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Çàäàíèå ïî êóðñó ¾Ðàñïðåäåë¼ííûå àëãîðèòìû¿Àëåêñàíäð ×èñòÿêîâ, Ðîìàí Øåìÿêèí15 ìàÿ 2016Äîêàçàòü òåîðåìó î êîððåêòíîñòè àëãîðèòìà Ñàôðû ñ èñïîëüçîâàíèåì èíâàðèàíòàP (γ).Òåîðåìà. Àëãîðèòì Ñàôðû ÿâëÿåòñÿ êîððåêòíûì àëãîðèòìîì îáíàðóæåíèÿ çàâåðøåíèÿâû÷èñëåíèÿ.Äîêàçàòåëüñòâî. Ïîêàæåì, ÷òî èç çàâåðøåíèÿ àëãîðèòìà Ñàôðû ñëåäóåò çàâåðø¼ííîñòüáàçîâîãî âû÷èñëåíèÿ. Âîñïîëüçóåìñÿ òåì, ÷òî äëÿ àëãîðèòìà Ñàôðû ïðåäèêàòP (γ) ≡ PM (γ) ∧ (P0 (γ) ∨ P1 (γ) ∨ P2 (γ) ∨ P3 (γ))ÿâëÿåòñÿ èíâàðèàíòîì.Çàìåòèì, ÷òî àëãîðèòì îáíàðóæèâàåò çàâåðøåíèå âû÷èñëåíèÿ òîëüêî òîãäà, êîãäà âûïîëíÿþòñÿ ðàâåíñòâàt=0state = passivep0colorp0 = whitemcp0 + q(γ) = 0èç êîòîðûõ ñëåäóåò ëîæíîñòü ïðåäèêàòîâÿíèèγ∗èñòèííûì îáÿçàí áûòü ïðåäèêàòP1 , P2 è P3 .
Òàêèì îáðàçîì â çàâåðøàþùåìPm (γ ∗ ) ∧ P0 (γ ∗ ). Ïîëó÷àåì ÷òî:ñîñòî-= passivet = 0P0 ⇒ ∀i(t < i < N ) : statepi = passive ⇒ ∀i(0 ≤ i < N ) : statepistatep0 = passivet = 0!X⇒ âû÷èñëåíèå∗P0 ⇒ q(γ ) =mcpi t<i<N⇒ B(γ ∗ ) = 0mcp0 + q = 0X∗∗PM (γ ) ⇒ B(γ ) =mcpi 0≤i<NÒåïåðü äîêàæåì, ÷òî ïîñëå çàâåðøåíèÿ áàçîâîãî âû÷èñëåíèÿ áóäåò çàâåðø¼í è àëãîðèòìmcpi áóäóò èìåòü ïî0.
Ïîñëå çàâåðøåíèÿ âîëíû, çàïóùåííîé èç òàêîéðàâåíñòâî mcp0 + q(γ) = 0 è âñå ïðîöåññû áóäóò îêðàøåíûÑàôðû. Çàìåòèì, ÷òî ïîñëå çàâåðøåíèÿ áàçîâîãî âû÷èñëåíèÿ ñ÷¼ò÷èêèñòîÿííûå çíà÷åíèÿ è èõ ñóììà áóäåò ðàâíàêîíôèãóðàöèè, áóäåò ñîáëþäåíîâ öâåòwhite. ðåçóëüòàòå ñëåäóþùåé âîëíû àëãîðèòì Ñàôðû çàâåðøèòñÿ.Òàêèì îáðàçîì çàâåðøåíèå àëãîðèòìà Ñàôðû ÿâëÿåòñÿ íåîáõîäèìûì è äîñòàòî÷íûì óñëîâèåì äëÿ çàâåðøåíèÿ áàçîâîãî âû÷èñëåíèÿ è êîððåêòíîñòü àëãîðèòìà Ñàôðû ïîëíîñòüþäîêàçàíà.1çàâåðøåíî.