Лекция 4. Коммуникационный протокол. Устройство_ корректность и модификации протокола с таймером (1185654), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

Ïîýòîìóçàïèñü â îò÷åòå áóäóò ñäåëàíà 2µ + R + λ åäèíèö âðåìåíè ïîñëåîêîí÷àíèÿ ñðîêà, îòâåäåííîãî äëÿ îòïðàâëåíèÿ ñîîáùåíèÿ, ò.å.ñïóñòÿ U + 2µ + R + λ åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿñëîâà. Ïîýòîìó I < B + Low , è ðàññìàòðèâàåìîå ñëîâî áóäóòëèáî îòìå÷åíî â îò÷åòå, ëèáî äîñòàâëåíî ïî íàçíà÷åíèþñîãëàñíî ñîîòíîøåíèþ (10): cs =⇒ ∀i < B + Low : Ok(i) . Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìè×òîáû óñòàíîâèòü âòîðîå òðåáîâàíèå êîððåêòíîñòè ïðîòîêîëà,íåîáõîäèìî ïîêàçàòü, ÷òî êàæäîå ñëîâî, êîòîðîå áûëî âðó÷åíîïîòðåáèòåëþ, èìååò áîëüøèé ïîðÿäêîâûé íîìåð (â ìàññèâå inp), ÷åì ðàíåå âðó÷åííîå ñëîâî.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìè×òîáû óñòàíîâèòü âòîðîå òðåáîâàíèå êîððåêòíîñòè ïðîòîêîëà,íåîáõîäèìî ïîêàçàòü, ÷òî êàæäîå ñëîâî, êîòîðîå áûëî âðó÷åíîïîòðåáèòåëþ, èìååò áîëüøèé ïîðÿäêîâûé íîìåð (â ìàññèâå inp), ÷åì ðàíåå âðó÷åííîå ñëîâî.

Âîñïîëüçóåìñÿ çàïèñüþ pr äëÿîáîçíà÷åíèÿ ïîðÿäêîâîãî íîìåðà ñàìîãî ïîñëåäíåãî èçâðó÷åííûõ ïîòðåáèòåëþ ñëîâ (äëÿ óäîáñòâà áóäåì ïîëàãàòü,÷òî âíà÷àëå pr = −1 è Ut[−1] = −∞ ).Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4.Ñëåäóþùåå óòâåðæäåíèå ÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ñòàéìåðàìè.P2 ≡∧∧∧∧∧P1hdata, s, i, w , ρi ∈ Mq =⇒ Ut[B + i] > ρ − µi1 ≤ i2 < B + High =⇒ Ut[i1 ] ≤ Ut[i2 ]cr =⇒ Rt ≥ Ut[pr ] + µpr < B + High ∧ (Ut[pr ] > −µ =⇒ cr )cr =⇒ B + Exp = pr + 1Äîêàçàòåëüñòâî.ÑÀÌÎÑÒÎßÒÅËÜÍÎ.(14)(15)(16)(17)(18)Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4.

(î ñîõðàíåíèè ïîðÿäêà âðó÷åíèÿ)Ñëîâà, äîñòàâëåííûå ïðîöåññîì q ïîòðåáèòåëþ, ðàñïîëîæåíû âñòðîãî âîçðàñòàþùåì ïîðÿäêå â ìàññèâå inp .ÄîêàçàòåëüñòâîÏðåæäå âñåãî çàìåòèì, ÷òî èç ôîðìóëû P2 ñëåäóåòñîîòíîøåíèå hdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr ).Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4. (î ñîõðàíåíèè ïîðÿäêà âðó÷åíèÿ)Ñëîâà, äîñòàâëåííûå ïðîöåññîì q ïîòðåáèòåëþ, ðàñïîëîæåíû âñòðîãî âîçðàñòàþùåì ïîðÿäêå â ìàññèâå inp .ÄîêàçàòåëüñòâîÏðåæäå âñåãî çàìåòèì, ÷òî èç ôîðìóëû P2 ñëåäóåòñîîòíîøåíèå hdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr ).Äåéñòâèòåëüíî, ñîãëàñíî ñîîòíîøåíèþ(14): hdata, s, i, w , ρi ∈ Mq =⇒ Ut[B + i] > ρ − µèç hdata, s, i1 , w , ρi ∈ Mq ñëåäóåò Ut[B + i1 ] > ρ − µ > −µ.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4. (î ñîõðàíåíèè ïîðÿäêà âðó÷åíèÿ)Ñëîâà, äîñòàâëåííûå ïðîöåññîì q ïîòðåáèòåëþ, ðàñïîëîæåíû âñòðîãî âîçðàñòàþùåì ïîðÿäêå â ìàññèâå inp .ÄîêàçàòåëüñòâîÏðåæäå âñåãî çàìåòèì, ÷òî èç ôîðìóëû P2 ñëåäóåòñîîòíîøåíèå hdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr ).Äåéñòâèòåëüíî, ñîãëàñíî ñîîòíîøåíèþ(14): hdata, s, i, w , ρi ∈ Mq =⇒ Ut[B + i] > ρ − µèç hdata, s, i1 , w , ρi ∈ Mq ñëåäóåò Ut[B + i1 ] > ρ − µ > −µ.Åñëè B + i1 ≤ pr , òî, ó÷èòûâàÿ, ÷òî ñîãëàñíî ñîîòíîøåíèþ(15): i1 ≤ i2 < B + High =⇒ Ut[i1 ] ≤ Ut[i2 ]ñïðàâåäëèâî íåðàâåíñòâî pr < B + High ,ïîëó÷àåì íåðàâåíñòâî Ut[pr ] > −µ , èç êîòîðîãî íà îñíîâàíèèñîîòíîøåíèÿ(17): pr < B + High ∧ (Ut[pr ] > −µ =⇒ cr )ñëåäóåò èñòèííîñòü ïðåäèêàòà cr .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâî (ïðîäîëæåíèå)Ïðåäïîëîæèì, ÷òî ïðîöåññ q ïîëó÷àåò ïàêåò hdata, s, i1 , w , ρi èâðó÷àåò ïîòðåáèòåëþ ñëîâî w .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâî (ïðîäîëæåíèå)Ïðåäïîëîæèì, ÷òî ïðîöåññ q ïîëó÷àåò ïàêåò hdata, s, i1 , w , ρi èâðó÷àåò ïîòðåáèòåëþ ñëîâî w .Åñëè ïåðåä ïîëó÷åíèåì íå áûë îòêðûò ñåàíñ ñâÿçè (ò.å.cr = false ), òî èç ñîîòíîøåíèÿhdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr )ñëåäóåò B + i1 > pr , è ïîýòîìó ñëîâî w â ìàññèâå inpðàñïîëàãàëîñü â ïîçèöèè, íîìåð êîòîðîé ñëåäóåò çà pr .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâî (ïðîäîëæåíèå)Ïðåäïîëîæèì, ÷òî ïðîöåññ q ïîëó÷àåò ïàêåò hdata, s, i1 , w , ρi èâðó÷àåò ïîòðåáèòåëþ ñëîâî w .Åñëè ïåðåä ïîëó÷åíèåì íå áûë îòêðûò ñåàíñ ñâÿçè (ò.å.cr = false ), òî èç ñîîòíîøåíèÿhdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr )ñëåäóåò B + i1 > pr , è ïîýòîìó ñëîâî w â ìàññèâå inpðàñïîëàãàëîñü â ïîçèöèè, íîìåð êîòîðîé ñëåäóåò çà pr .Åñëè ñåàíñ ñâÿçè áûë îòêðûò (ò.å.

cr = true ), òî i1 = Exp .Òîãäà, èç ñîîòíîøåíèÿ (18): cr =⇒ B + Exp = pr + 1 ñëåäóþòðàâåíñòâàB + i1 = B + Exp = pr + 1,èç êîòîðûõ âûòåêàåò, ÷òî w = inp [pr + 1] .Êà÷åñòâåííûé àíàëèç ïðîòîêîëàÕîðîøèì ñ÷èòàåòñÿ òàêîå ðåøåíèå, êîòîðîå íå òîëüêîóäîâëåòâîðÿåò òðåáîâàíèÿì Îòñóòñòâèÿ ïîòåðü è Ñîõðàíåíèåïîðÿäêà âðó÷åíèÿ , íî òàêæå ñîîáùàåò îá óòðàòå êàê ìîæíîìåíüøåãî ÷èñëà ñëîâ.

×òîáû äîñòè÷ü ýòîé öåëè ìû äîëæíûñíàáäèòü ïðîòîêîë, îïèñàííûé â ýòîì ðàçäåëå, íåêîòîðûììåõàíèçìîì, êîòîðûé ïîçâîëÿë áû îòïðàâëÿòü êàæäîå ñëîâîïîâòîðíî (íà ïðîòÿæåíèè èíòåðâàëà îòïðàâëåíèÿ ñëîâà) äî òåõïîð, ïîêà íå áóäåò ïîëó÷åíî ïîäòâåðæäåíèå î åãî äîñòàâêå.Èíòåðâàë îòïðàâëåíèÿ äîëæåí áûòü äîñòàòî÷íî ïðîòÿæåííûì,÷òîáû ïîçâîëèòü îñóùåñòâëÿòü ìíîãîêðàòíóþ ïåðåäà÷óîïðåäåëåííûõ ñëîâ è ñäåëàòü òåì ñàìûì âåðîÿòíîñòü óòðàòûñëîâà êàê ìîæíî ìåíüøåé.Îãðàíè÷åííûå ïîðÿäêîâûå íîìåðàÏîðÿäêîâûå íîìåðà, èñïîëüçóåìûå â ïðîòîêîëå, ìîæíîîãðàíè÷èòü, äîêàçàâ óòâåðæäåíèå, àíàëîãè÷íîå Òåîðåìå 3.8 äëÿñèììåòðè÷íîãî ïðîòîêîëà ðàçäâèæíîãî îêíà.Îãðàíè÷åííûå ïîðÿäêîâûå íîìåðàÏîðÿäêîâûå íîìåðà, èñïîëüçóåìûå â ïðîòîêîëå, ìîæíîîãðàíè÷èòü, äîêàçàâ óòâåðæäåíèå, àíàëîãè÷íîå Òåîðåìå 3.8 äëÿñèììåòðè÷íîãî ïðîòîêîëà ðàçäâèæíîãî îêíà.Äëÿ ýòîãî íåîáõîäèìî ââåñòè äîïóùåíèå î òîì, ÷òî ñêîðîñòüïîñòóïëåíèÿ ñëîâ íà âõîä ïðîöåññà p îãðàíè÷åíà òàêèìîáðàçîì, ÷òîáû î÷åðåäíîå ñëîâî ïîñòóïàëî ñïóñòÿ íå ìåíååU + 2µ + R åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿ L -ãî ïîïîðÿäêó ïðåäøåñòâóþùåãî ñëîâà.Îãðàíè÷åííûå ïîðÿäêîâûå íîìåðàÏîðÿäêîâûå íîìåðà, èñïîëüçóåìûå â ïðîòîêîëå, ìîæíîîãðàíè÷èòü, äîêàçàâ óòâåðæäåíèå, àíàëîãè÷íîå Òåîðåìå 3.8 äëÿñèììåòðè÷íîãî ïðîòîêîëà ðàçäâèæíîãî îêíà.Äëÿ ýòîãî íåîáõîäèìî ââåñòè äîïóùåíèå î òîì, ÷òî ñêîðîñòüïîñòóïëåíèÿ ñëîâ íà âõîä ïðîöåññà p îãðàíè÷åíà òàêèìîáðàçîì, ÷òîáû î÷åðåäíîå ñëîâî ïîñòóïàëî ñïóñòÿ íå ìåíååU + 2µ + R åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿ L -ãî ïîïîðÿäêó ïðåäøåñòâóþùåãî ñëîâà.Äëÿ ýòîãî äåéñòâèå Ap íóæíî ñíàáäèòü ïðåäîõðàíèòåëåì{(High < L) ∨ (Ut[B + High − L] < −R − 2µ)}.Îãðàíè÷åííûå ïîðÿäêîâûå íîìåðàÏîðÿäêîâûå íîìåðà, èñïîëüçóåìûå â ïðîòîêîëå, ìîæíîîãðàíè÷èòü, äîêàçàâ óòâåðæäåíèå, àíàëîãè÷íîå Òåîðåìå 3.8 äëÿñèììåòðè÷íîãî ïðîòîêîëà ðàçäâèæíîãî îêíà.Äëÿ ýòîãî íåîáõîäèìî ââåñòè äîïóùåíèå î òîì, ÷òî ñêîðîñòüïîñòóïëåíèÿ ñëîâ íà âõîä ïðîöåññà p îãðàíè÷åíà òàêèìîáðàçîì, ÷òîáû î÷åðåäíîå ñëîâî ïîñòóïàëî ñïóñòÿ íå ìåíååU + 2µ + R åäèíèö âðåìåíè ïîñëå ïîñòóïëåíèÿ L -ãî ïîïîðÿäêó ïðåäøåñòâóþùåãî ñëîâà.Äëÿ ýòîãî äåéñòâèå Ap íóæíî ñíàáäèòü ïðåäîõðàíèòåëåì{(High < L) ∨ (Ut[B + High − L] < −R − 2µ)}.Òîãäà ïîðÿäêîâûå íîìåðà ïîëó÷åííûõ ïàêåòîâ äàííûõ îòñòîÿòíå áîëåå, ÷åì íà 2L îò îæèäàåìîãî íîìåðà Exp , à ïîðÿäêîâûåíîìåðà â ïîäòâåðæäàþùèõ ñîîáùåíèÿõ îòñòîÿò íå áîëåå, ÷åìíà L îò íîìåðà High .

Ñëåäîâàòåëüíî, ïðè ïåðåäà÷å óâåëè÷åíèåïîðÿäêîâûõ íîìåðîâ ìîæíî ïðîâîäèòü ïî ìîäóëþ 2L .Íåñêîëüêî ñëîâ îá èíâàðèàíòàõÂñå ñîîòíîøåíèÿ (äèçúþíêòû), âõîäÿùèå â ñîñòàâðàññìîòðåííûõ íàìè èíâàðèàíòîâ è êàñàþùèåñÿ ïàêåòîâ,èìåþò ñëåäóþùèé îáùèé âèä:∀m ∈ M : A(m),Íåòðóäíî óáåäèòüñÿ, ÷òî âûïîëíèìîñòü ñîîòíîøåíèé òàêîãîâèäà ñîõðàíÿåòñÿ ïðè äóáëèðîâàíèè èëè ïîòåðå ïàêåòîâ.Íåñêîëüêî ñëîâ îá èíâàðèàíòàõÂñå ñîîòíîøåíèÿ (äèçúþíêòû), âõîäÿùèå â ñîñòàâðàññìîòðåííûõ íàìè èíâàðèàíòîâ è êàñàþùèåñÿ ïàêåòîâ,èìåþò ñëåäóþùèé îáùèé âèä:∀m ∈ M : A(m),Íåòðóäíî óáåäèòüñÿ, ÷òî âûïîëíèìîñòü ñîîòíîøåíèé òàêîãîâèäà ñîõðàíÿåòñÿ ïðè äóáëèðîâàíèè èëè ïîòåðå ïàêåòîâ.Èíîãäà ïðèõîäèòñÿ èñïîëüçîâàòü èíâàðèàíòû áîëåå îáùåãîâèäà, íàïðèìåðXf (m) = Kèëèm∈Mïðåäóñëîâèå =⇒ ∃m ∈ M : A(m).Ïðåäëîæåíèÿ òàêîãî âèäà ìîãóò óòðàòèòü èñòèííîñòü â ñëó÷àåïîòåðè èëè äóáëèðîâàíèÿ ïàêåòîâ, è ïîýòîìó èõ íåëüçÿèñïîëüçîâàòü ïðè äîêàçàòåëüñòâå êîððåêòíîñòè àëãîðèòìîâ, îòêîòîðûõ òðåáóåòñÿ óñòîé÷èâîñòü ê ïîäîáíûì ñáîÿì.Çàäà÷èÇàäà÷à 1. ïðîòîêîëå ñ òàéìåðàìè îòïðàâèòåëü ìîæåò çàíåñòè â îò÷åòñëîâî êàê âîçìîæíî óòðà÷åííîå, â òî âðåìÿ êàê ýòî ñëîâî áûëîáëàãîïîëó÷íî äîñòàâëåíî ïîëó÷àòåëþ.1.

Îïèøèòå âûïîëíåíèå ýòîãî ïðîòîêîëà, â õîäå êîòîðîãîïðîèñõîäèò ïîäîáíûé ýôôåêò.2. Ìîæíî ëè ðàçðàáîòàòü òàêîé ïðîòîêîë, â êîòîðîìîòïðàâèòåëü çà îãðàíè÷åííîå âðåìÿ ñîñòàâëÿåò îò÷åò îáîøèáêå â òîì è òîëüêî òîì ñëó÷àå, êîãäà ñëîâî íåäîñòàâëÿåòñÿ ïîëó÷àòåëþ?Çàäà÷èÇàäà÷à 2.Ïðåäïîëîæèì, ÷òî â ñâÿçè ñ âûõîäîì èç ñòðîÿ ÷àñîâîãîìåõàíèçìà, ïîëó÷àòåëü íå ìîæåò çàêðûòü ñåàíñ ñâÿçè âîâðåìÿ.Îïèøèòå âû÷èñëåíèå ïðîòîêîëà ñ òàéìåðàìè, â õîäå êîòîðîãîñëîâî áóäåò óòðà÷åíî, íî îòïðàâèòåëü íå ñìîæåò îòìåòèòü ýòî âîò÷åòå.Çàäà÷à 3.Îïèøèòå òàêîå âû÷èñëåíèå ïðîòîêîëà ñ òàéìåðàìè, â õîäåêîòîðîãî ïîëó÷àòåëü îòêðûâàåò ñåàíñ ñâÿçè ïîñëå ïîëó÷åíèÿïàêåòà ñ ïîðÿäêîâûì íîìåðîì áîëüøèì íóëÿ.Çàäà÷èÇàäà÷à 4.Ïðîåêòèðîâùèê ñåòè õîòåë áû âîñïîëüçîâàòüñÿ ïðîòîêîëîì ñòàéìåðàìè, íî ïðè ýòîì æåëàåò, ÷òîáû î âîçìîæíî óòðà÷åííûõñëîâàõ çàïèñü â îò÷åòå îñóùåñòâëÿëàñü ïîðàíüøå.

Äëÿ ýòîãî îíìîäèôèöèðóåò äåéñòâèå Ep ñëåäóþùèì îáðàçîì:Ep : (* Ñôîðìèðîâàòü îò÷åò îá îøèáêåäëÿ âîçìîæíî óòðà÷åííîãî ñëîâà *){ Ut[B + Low ] < 0 }begin error [B + Low ] := true ; Low := Low + 1endÁóäåò ëè ìîäèôèöèðîâàííûé òàêèì îáðàçîì ïðîòîêîëóäîâëåòâîðÿòü òðåáîâàíèÿì Îòñóòñòâèÿ ïîòåðü èÑîõðàíåíèÿ ïîðÿäêà âðó÷åíèÿ èëè äëÿ ýòîãî íåîáõîäèìîâíåñòè òàêæå äðóãèå èçìåíåíèÿ?Êàêîâû, ïî Âàøåìó ìíåíèþ, ïðåèìóùåñòâà è íåäîñòàòêèóêàçàííîé ìîäèôèêàöèè.ÊÎÍÅÖ ËÅÊÖÈÈ 4..

Характеристики

Список файлов лекций