Лекция 3. Коммуник. протоколы. Протокол раздвижного окна. Принципы обоснования корректности, страница 2

Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òî ïëîõîãî ìîæåò ñëó÷èòüñÿ?1. Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );2. Ñòâîðêè îêîí ìîãóò ¾çàñòûòü¿, è ïðîöåññû áóäóòîáðå÷åíû ïåðåäàâàòü îäíè è òå æå ñîîáùåíèÿ (àêòèâíûéòóïèê , livelock );Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òî ïëîõîãî ìîæåò ñëó÷èòüñÿ?1. Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );2. Ñòâîðêè îêîí ìîãóò ¾çàñòûòü¿, è ïðîöåññû áóäóòîáðå÷åíû ïåðåäàâàòü îäíè è òå æå ñîîáùåíèÿ (àêòèâíûéòóïèê , livelock );3. Äàííûå ìîãóò áûòü ïîòåðÿíû ïðè ïåðåäà÷å, è ïðîöåññ íåçàìåòèò ýòîãî;Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òî ïëîõîãî ìîæåò ñëó÷èòüñÿ?1.

Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );2. Ñòâîðêè îêîí ìîãóò ¾çàñòûòü¿, è ïðîöåññû áóäóòîáðå÷åíû ïåðåäàâàòü îäíè è òå æå ñîîáùåíèÿ (àêòèâíûéòóïèê , livelock );3. Äàííûå ìîãóò áûòü ïîòåðÿíû ïðè ïåðåäà÷å, è ïðîöåññ íåçàìåòèò ýòîãî;4. Ïðîöåññ ìîæåò ¾çàáûòü¿ ïåðåäàòü äàííûå;Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òî ïëîõîãî ìîæåò ñëó÷èòüñÿ?1.

Ñòâîðêè îêîí îáîèõ ïðîöåññîâ ìîãóò ¾çàõëîïíóòüñÿ¿, èïðîöåññû áóäóò îáðå÷åíû (áåçóñïåøíî) îæèäàòüñîîáùåíèé äðóã îò äðóãà (áëîêèðîâêà , deadlock );2. Ñòâîðêè îêîí ìîãóò ¾çàñòûòü¿, è ïðîöåññû áóäóòîáðå÷åíû ïåðåäàâàòü îäíè è òå æå ñîîáùåíèÿ (àêòèâíûéòóïèê , livelock );3. Äàííûå ìîãóò áûòü ïîòåðÿíû ïðè ïåðåäà÷å, è ïðîöåññ íåçàìåòèò ýòîãî;4. Ïðîöåññ ìîæåò ¾çàáûòü¿ ïåðåäàòü äàííûå;5.

Ñòâîðêè îêíà ìîãóò ðàçäâèãàòüñÿ, îòäàëàÿÿñü äðóã îòäðóãà íåîãðàíè÷åííî øèðîêî.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒðåáîâàíèÿ êîððåêòíîñòè.Íóæíî äîêàçàòü, ÷òî ïðîòîêîë ðàáîòàåò ïðàâèëüíî, ò.å. êàæäîåñëîâî èç âõîäíîãî ìàññèâà inp ïðîöåññà p áóäåò ðàíî èëèïîçäíî çàïèñàíî â âûõîäíîé ìàññèâ outq ïðîöåññà q , èíàîáîðîò.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒðåáîâàíèÿ êîððåêòíîñòè.Íóæíî äîêàçàòü, ÷òî ïðîòîêîë ðàáîòàåò ïðàâèëüíî, ò.å.

êàæäîåñëîâî èç âõîäíîãî ìàññèâà inp ïðîöåññà p áóäåò ðàíî èëèïîçäíî çàïèñàíî â âûõîäíîé ìàññèâ outq ïðîöåññà q , èíàîáîðîò.Áîëåå ñòðîãî ýòî âûðàæàåòñÿ äâóìÿ òðåáîâàíèÿìè.1. êàæäîé äîñòèæèìîéêîíôèãóðàöèè ïðîòîêîëà âûïîëíÿþòñÿ ñîîòíîøåíèÿoutp [0..sp −1] = inq [0..sp −1] è outq [0..sq −1] = inp [0..sq −1].Áåçîïàñíàÿ äîñòàâêà ñîîáùåíèé.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒðåáîâàíèÿ êîððåêòíîñòè.Íóæíî äîêàçàòü, ÷òî ïðîòîêîë ðàáîòàåò ïðàâèëüíî, ò.å.

êàæäîåñëîâî èç âõîäíîãî ìàññèâà inp ïðîöåññà p áóäåò ðàíî èëèïîçäíî çàïèñàíî â âûõîäíîé ìàññèâ outq ïðîöåññà q , èíàîáîðîò.Áîëåå ñòðîãî ýòî âûðàæàåòñÿ äâóìÿ òðåáîâàíèÿìè.1. êàæäîé äîñòèæèìîéêîíôèãóðàöèè ïðîòîêîëà âûïîëíÿþòñÿ ñîîòíîøåíèÿoutp [0..sp −1] = inq [0..sp −1] è outq [0..sq −1] = inp [0..sq −1].Áåçîïàñíàÿ äîñòàâêà ñîîáùåíèé.2.Äëÿ êàæäîãî öåëîãî÷èñëà k ≥ 0 , â õîäå âûïîëíåíèÿ ïðîòîêîëà áóäåòäîñòèãíóòà êîíôèãóðàöèÿ, â êîòîðîé sp ≥ k è sq ≥ k .Íåèçáåæíàÿ äîñòàâêà ñîîáùåíèé.À êàê äîêàçûâàåòñÿêîððåêòíîñòüïðîòîêîëîâ?Êàê îáîñíîâûâàòü ñâîéñòâà ñèñòåì ïåðåõîäîâÊëàññèôèêàöèÿ ñâîéñòâÌíîãèå ñâîéñòâà ðàñïðåäåëåííûõ àëãîðèòìîâ, íóæäàþùèåñÿ âïðîâåðêå, îòíîñÿòñÿ ê îäíîìó èç äâóõ òèïîâ:è.óñëîâèå áåçîïàñíîñòèóñëîâèå æèâîñòèÊàê îáîñíîâûâàòü ñâîéñòâà ñèñòåì ïåðåõîäîâÊëàññèôèêàöèÿ ñâîéñòâÌíîãèå ñâîéñòâà ðàñïðåäåëåííûõ àëãîðèòìîâ, íóæäàþùèåñÿ âïðîâåðêå, îòíîñÿòñÿ ê îäíîìó èç äâóõ òèïîâ:è.Óñëîâèå áåçîïàñíîñòè òðåáóåò, ÷òîáû êàæäàÿ äîñòèæèìàÿêîíôèãóðàöèÿ â ëþáîì âûïîëíåíèè ñèñòåìû îáëàäàëàîïðåäåëåííûì ñâîéñòâîì.óñëîâèå áåçîïàñíîñòèóñëîâèå æèâîñòèÊàê îáîñíîâûâàòü ñâîéñòâà ñèñòåì ïåðåõîäîâÊëàññèôèêàöèÿ ñâîéñòâÌíîãèå ñâîéñòâà ðàñïðåäåëåííûõ àëãîðèòìîâ, íóæäàþùèåñÿ âïðîâåðêå, îòíîñÿòñÿ ê îäíîìó èç äâóõ òèïîâ:è.Óñëîâèå áåçîïàñíîñòè òðåáóåò, ÷òîáû êàæäàÿ äîñòèæèìàÿêîíôèãóðàöèÿ â ëþáîì âûïîëíåíèè ñèñòåìû îáëàäàëàîïðåäåëåííûì ñâîéñòâîì.Óñëîâèå æèâîñòè òðåáóåò, ÷òîáû õîòÿ áû îäíà äîñòèæèìàÿêîíôèãóðàöèÿ â ëþáîì âûïîëíåíèè ñèñòåìû îáëàäàëàîïðåäåëåííûì ñâîéñòâîì.óñëîâèå áåçîïàñíîñòèóñëîâèå æèâîñòèÑâîéñòâà áåçîïàñíîñòèÑâîéñòâîì áåçîïàñíîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âêàæäîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P âñåãäà èñòèííî¿.Ñâîéñòâà áåçîïàñíîñòèÑâîéñòâîì áåçîïàñíîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âêàæäîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P âñåãäà èñòèííî¿.Îñíîâíîé ïðèåì, ïðè ïîìîùè êîòîðîãî óäàåòñÿ ïîêàçàòü, ÷òîóòâåðæäåíèå P âñåãäà èñòèííî, çàêëþ÷àåòñÿ â äîêàçàòåëüñòâåòîãî, ÷òî P ÿâëÿåòñÿ.èíâàðèàíòîìÑâîéñòâà áåçîïàñíîñòèÏóñòü çàäàíà ñèñòåìà ïåðåõîäîâ S = (C, →, I) èðàññìàòðèâàþòñÿ íåêîòðûå ñâîéñòâà êîíôèãóðàöèé P è Q .Ñâîéñòâà áåçîïàñíîñòèÏóñòü çàäàíà ñèñòåìà ïåðåõîäîâ S = (C, →, I) èðàññìàòðèâàþòñÿ íåêîòðûå ñâîéñòâà êîíôèãóðàöèé P è Q .Çàïèñü P(γ) , ãäå γ êîíôèãóðàöèÿ, áóäåò îáîçíà÷àòüëîãè÷åñêîå âûðàæåíèå (ôîðìóëó), ïðèíèìàþùåå èñòèííîåçíà÷åíèå â òîì ñëó÷àå, åñëè óòâåðæäåíèå P ñïðàâåäëèâî äëÿêîíôèãóðàöèè γ , è ëîæíîå çíà÷åíèå â ïðîòèâíîì ñëó÷àå.Ñâîéñòâà áåçîïàñíîñòèÏóñòü çàäàíà ñèñòåìà ïåðåõîäîâ S = (C, →, I) èðàññìàòðèâàþòñÿ íåêîòðûå ñâîéñòâà êîíôèãóðàöèé P è Q .Çàïèñü P(γ) , ãäå γ êîíôèãóðàöèÿ, áóäåò îáîçíà÷àòüëîãè÷åñêîå âûðàæåíèå (ôîðìóëó), ïðèíèìàþùåå èñòèííîåçíà÷åíèå â òîì ñëó÷àå, åñëè óòâåðæäåíèå P ñïðàâåäëèâî äëÿêîíôèãóðàöèè γ , è ëîæíîå çíà÷åíèå â ïðîòèâíîì ñëó÷àå.Çàïèñü {P} → {Q} áóäåò èñïîëüçîâàòüñÿ äëÿ îáîçíà÷åíèÿòîãî, ÷òî äëÿ êàæäîãî ïåðåõîäà γ → δ â ñèñòåìå S èñòèííîñòüP(γ) âëå÷åò èñòèííîñòü Q(δ) .Ñâîéñòâà áåçîïàñíîñòèÏóñòü çàäàíà ñèñòåìà ïåðåõîäîâ S = (C, →, I) èðàññìàòðèâàþòñÿ íåêîòðûå ñâîéñòâà êîíôèãóðàöèé P è Q .Çàïèñü P(γ) , ãäå γ êîíôèãóðàöèÿ, áóäåò îáîçíà÷àòüëîãè÷åñêîå âûðàæåíèå (ôîðìóëó), ïðèíèìàþùåå èñòèííîåçíà÷åíèå â òîì ñëó÷àå, åñëè óòâåðæäåíèå P ñïðàâåäëèâî äëÿêîíôèãóðàöèè γ , è ëîæíîå çíà÷åíèå â ïðîòèâíîì ñëó÷àå.Çàïèñü {P} → {Q} áóäåò èñïîëüçîâàòüñÿ äëÿ îáîçíà÷åíèÿòîãî, ÷òî äëÿ êàæäîãî ïåðåõîäà γ → δ â ñèñòåìå S èñòèííîñòüP(γ) âëå÷åò èñòèííîñòü Q(δ) .Îïðåäåëåíèå 3.1.Óòâåðæäåíèå P íàçûâàåòñÿñèñòåìû S , åñëè1.

P(γ) èñòèííî äëÿ êàæäîé íà÷àëüíîé êîíôèãóðàöèè γ ∈ I ,è2. {P} → {P} .èíâàðèàíòîìÑâîéñòâà áåçîïàñíîñòèÒåîðåìà 3.1.Åñëè óòâåðæäåíèå P ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâS , òî äëÿ ëþáîãî âûïîëíåíèÿ E ñèñòåìû S óòâåðæäåíèå Páóäåò èñòèííî â êàæäîé êîíôèãóðàöèè ýòîãî âûïîëíåíèÿ.Ñâîéñòâà áåçîïàñíîñòèÒåîðåìà 3.1.Åñëè óòâåðæäåíèå P ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâS , òî äëÿ ëþáîãî âûïîëíåíèÿ E ñèñòåìû S óòâåðæäåíèå Páóäåò èñòèííî â êàæäîé êîíôèãóðàöèè ýòîãî âûïîëíåíèÿ.Ðàññìîòðåòü ïðîèçâîëüíîå âûïîëíåíèåE = (γ0 , γ1 , γ2 , . . .) ñèñòåìû S è âîñïîëüçîâàòüñÿ èíäóêöèåé.Äîêàçàòåëüñòâî:Ñâîéñòâà áåçîïàñíîñòèÒåîðåìà 3.1.Åñëè óòâåðæäåíèå P ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâS , òî äëÿ ëþáîãî âûïîëíåíèÿ E ñèñòåìû S óòâåðæäåíèå Páóäåò èñòèííî â êàæäîé êîíôèãóðàöèè ýòîãî âûïîëíåíèÿ.Ðàññìîòðåòü ïðîèçâîëüíîå âûïîëíåíèåE = (γ0 , γ1 , γ2 , .

. .) ñèñòåìû S è âîñïîëüçîâàòüñÿ èíäóêöèåé.Äîêàçàòåëüñòâî:Òåîðåìà 3.2.Åñëè Q ÿâëÿåòñÿ èíâàðèàíòîì ñèñòåìû ïåðåõîäîâ S , è äëÿêàæäîé êîíôèãóðàöèè γ ∈ C âûïîëíÿåòñÿ Q(γ) =⇒ P(γ) , òîäëÿ ëþáîãî âûïîëíåíèÿ ñèñòåìû S óòâåðæäåíèå P áóäåòèñòèííî â êàæäîé êîíôèãóðàöèè âûïîëíåíèÿ.Ñâîéñòâà áåçîïàñíîñòèÇàäà÷è.1.

Âåðíî ëè, ÷òî óòâåðæäåíèå, êîòîðîå ÿâëÿåòñÿ èñòèííûì âêàæäîé êîíôèãóðàöèè ëþáîãî âûïîëíåíèÿ, îáÿçàòåëüíîÿâëÿåòñÿ èíâàðèàíòîì?Ñâîéñòâà áåçîïàñíîñòèÇàäà÷è.1. Âåðíî ëè, ÷òî óòâåðæäåíèå, êîòîðîå ÿâëÿåòñÿ èñòèííûì âêàæäîé êîíôèãóðàöèè ëþáîãî âûïîëíåíèÿ, îáÿçàòåëüíîÿâëÿåòñÿ èíâàðèàíòîì?2. Ïðèâåäèòå ïðèìåð òàêîé ñèñòåìû ïåðåõîäîâ S è òàêîãîóòâåðæäåíèÿ P , ÷òî P âñåãäà èñòèííî â ñèñòåìå S , íî ïðèýòîì íå ÿâëÿåòñÿ èíâàðèàíòîì S .Ñâîéñòâà áåçîïàñíîñòèÇàäà÷è.1. Âåðíî ëè, ÷òî óòâåðæäåíèå, êîòîðîå ÿâëÿåòñÿ èñòèííûì âêàæäîé êîíôèãóðàöèè ëþáîãî âûïîëíåíèÿ, îáÿçàòåëüíîÿâëÿåòñÿ èíâàðèàíòîì?2. Ïðèâåäèòå ïðèìåð òàêîé ñèñòåìû ïåðåõîäîâ S è òàêîãîóòâåðæäåíèÿ P , ÷òî P âñåãäà èñòèííî â ñèñòåìå S , íî ïðèýòîì íå ÿâëÿåòñÿ èíâàðèàíòîì S .3.

Ïðåäïîëîæèì, ÷òî P1 è P2 ýòî èíâàðèàíòû ñèñòåìû S .Äîêàæèòå, ÷òî (P1 ∨ P2) è (P1 ∧ P2) òàêæå ÿâëÿþòñÿèíâàðèàíòàìè.Ñâîéñòâà æèâîñòèÑâîéñòâîì æèâîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âíåêîòîðîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P êîãäà-òî îáÿçàòåëüíî ñòàíîâèòñÿ èñòèííûì¿.Ñâîéñòâà æèâîñòèÑâîéñòâîì æèâîñòè àëãîðèòìà ÿâëÿåòñÿ âñÿêîå ñâîéñòâî,êîòîðîå ìîæíî ñôîðìóëèðîâàòü â âèäå ñëåäóþùåãîïðåäëîæåíèÿ:¾Äëÿ ëþáîãî âûïîëíåíèÿ àëãîðèòìà óòâåðæäåíèå P èñòèííî âíåêîòîðîé êîíôèãóðàöèè âûïîëíåíèÿ¿.Áîëåå êðàòêî ýòî ñâîéñòâî ìîæíî ñôîðìóëèðîâàòü òàê:¾Óòâåðæäåíèå P êîãäà-òî îáÿçàòåëüíî ñòàíîâèòñÿ èñòèííûì¿.Îñíîâíîé ïðèåì, ïðè ïîìîùè êîòîðîãî óäàåòñÿ ïîêàçàòü, ÷òîóòâåðæäåíèå P êîãäà-òî îáÿçàòåëüíî ñòàíîâèòñÿ èñòèííûì,çàêëþ÷àåòñÿ â èñïîëüçîâàíèèè.ôóíêöèé íîðìèðîâêèîòñóòñòâèÿ áëîêèðîâêèÑâîéñòâà æèâîñòèÐàññìîòðèì ñèñòåìó ïåðåõîäîâ S è ïðåäèêàò P .

Áóäåìñ÷èòàòü, ÷òî ïðåäèêàòïî îïðåäåëåíèþ ïðèíèìàåòèñòèííîå çíà÷åíèå â êàæäîé çàêëþ÷èòåëüíîé êîíôèãóðàöèè, èëîæíîå çíà÷åíèå â êîíôèãóðàöèÿõ, êîòîðûå íå ÿâëÿþòñÿçàêëþ÷èòåëüíûìè.termÑâîéñòâà æèâîñòèÐàññìîòðèì ñèñòåìó ïåðåõîäîâ S è ïðåäèêàò P . Áóäåìñ÷èòàòü, ÷òî ïðåäèêàòïî îïðåäåëåíèþ ïðèíèìàåòèñòèííîå çíà÷åíèå â êàæäîé çàêëþ÷èòåëüíîé êîíôèãóðàöèè, èëîæíîå çíà÷åíèå â êîíôèãóðàöèÿõ, êîòîðûå íå ÿâëÿþòñÿçàêëþ÷èòåëüíûìè. Îáû÷íî áûâàåò íåæåëàòåëüíî äîñòè÷üçàêëþ÷èòåëüíîé êîíôèãóðàöèè ïðåæäå, ÷åì âûïîëíèòñÿ¾öåëåâîé¿ ïðåäèêàò P ; â ýòîì ñëó÷àå ãîâîðÿò, ÷òî ïðîèçîøëà.

Åñëè æå öåëü äîñòèãíóòà, òî âûïîëíåíèå ìîæíîçàâåðøèòü; â ýòîì ñëó÷àå ãîâîðÿò, ÷òî ïðîèçîøëî.termáëîêèðîâêàïðàâèëüíîåçàâåðøåíèåÑâîéñòâà æèâîñòèÐàññìîòðèì ñèñòåìó ïåðåõîäîâ S è ïðåäèêàò P . Áóäåìñ÷èòàòü, ÷òî ïðåäèêàòïî îïðåäåëåíèþ ïðèíèìàåòèñòèííîå çíà÷åíèå â êàæäîé çàêëþ÷èòåëüíîé êîíôèãóðàöèè, èëîæíîå çíà÷åíèå â êîíôèãóðàöèÿõ, êîòîðûå íå ÿâëÿþòñÿçàêëþ÷èòåëüíûìè. Îáû÷íî áûâàåò íåæåëàòåëüíî äîñòè÷üçàêëþ÷èòåëüíîé êîíôèãóðàöèè ïðåæäå, ÷åì âûïîëíèòñÿ¾öåëåâîé¿ ïðåäèêàò P ; â ýòîì ñëó÷àå ãîâîðÿò, ÷òî ïðîèçîøëà.