3 Коммуникационные протоколы. Ошибки, возникающие при передаче сообщений. Задача надежного обмена сообщениями, страница 3

Åñëè áåñêîíå÷íî ÷àñòî âîçíèêàåò âîçìîæíîñòü îòïðàâêèïàêåòà, òî ýòîò ïàêåò áóäåò îòïðàâëÿòüñÿ áåñêîíå÷íî ÷àñòî.F2. Åñëè îäèí è òîò æå ïàêåò îòïðàâëÿåòñÿ áåñêîíå÷íî ÷àñòî,òî è ïðèíèìàåòñÿ îí òàêæå áåñêîíå÷íî ÷àñòî.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÑòâîðêè îêîí ïðîöåññîâ p è q ¾ðàçúåçæàþòñÿ¿ íå ñëèøêîìäàëåêî äðóã îò äðóãà.Ëåììà 3.1. ëþáîé äîñòèæèìîé êîíôèãóðàöèè âûïîëíÿþòñÿ íåðàâåíñòâàsp − `q ≤ ap ≤ sq ≤ aq + `p ≤ sp + `p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:Èç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ apÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ apÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ ap ≤ sqÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ ap ≤ sqÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Èç (0q) è (2q) ñëåäóåò sq ≤ aq + `p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ ap ≤ sq ≤ aq + `pÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Èç (0q) è (2q) ñëåäóåò sq ≤ aq + `p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ ap ≤ sq ≤ aq + `pÈç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Èç (0q) è (2q) ñëåäóåò sq ≤ aq + `p .È, íàêîíåö, èç (3q) ñëåäóåò íåðàâåíñòâî aq + `p ≤ sp + `p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:sp − `q ≤ ap ≤ sq ≤ aq + `p ≤ sp + `p .Èç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )èíâàðèàíòà P ñëåäóåò íåðàâåíñòâî sp − `q ≤ ap .Ñâîéñòâî (3p): ap ≤ sqîáåñïå÷èâàåò âûïîëíèìîñòü íåðàâåíñòâà ap ≤ sq .Èç (0q) è (2q) ñëåäóåò sq ≤ aq + `p .È, íàêîíåö, èç (3q) ñëåäóåò íåðàâåíñòâî aq + `p ≤ sp + `p .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÑòâîðêè îêîí ïðîöåññîâ p è q íå ìîãóò ¾ñîìêíóòüñÿ¿îäíîâðåìåííî, ò.å.

ïðîòîêîë íèêîãäà íå áóäåò çàáëîêèðîâàí.Ëåììà 3.2. ëþáîé äîñòèæèìîé êîíôèãóðàöèè äîïóñòèìî õîòÿ áû îäíî èçäâóõ äåéñòâèé: îòïðàâëåíèå ïàêåòà h , inp [sq ], sq i ïðîöåññîìp èëè îòïðàâëåíèå ïàêåòà h, inq [sp ], sp i ïðîöåññîì q .packpackÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÄîêàçàòåëüñòâî:Ñîãëàñíî îãðàíè÷åíèþ `p + `q > 0 ïî êðàéíåé ìåðå îäíî èçíåðàâåíñòâ Ëåììû 3.1sp − `q ≤ ap ≤ sq ≤ aq + `p ≤ sp + `pÿâëÿåòñÿ ñòðîãèì, ò.å.,sq < sp + `p ∨ sp < sq + `q.Èç èíâàðèàíòà P òàêæå ñëåäóþò íåðàâåíñòâà(3p): ap ≤ sq è (3q): aq ≤ sp ,è ïîýòîìó ñïðàâåäëèâî ñîîòíîøåíèå(ap ≤ sq < sp + `p ) ∨ (aq ≤ sp < sq + `q ),Ýòî ñîîòíîøåíèå îçíà÷àåò, ÷òî ëèáî äåéñòâèå p äîïóñòèìîäëÿ i = sq , ëèáî äåéñòâèå q äîïóñòèìî äëÿ i = sp .SSÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒåîðåìà 3.6.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà óäîâëåòâîðÿåòòðåáîâàíèþ íåèçáåæíîé äîñòàâêè ñîîáùåíèé, ò.å. äëÿ êàæäîãîöåëîãî ÷èñëà k ≥ 0 , â õîäå ëþáîãî âûïîëíåíèÿ ïðîòîêîëàáóäåò äîñòèãíóòû êîíôèãóðàöèÿ, â êîòîðîé sp ≥ k è sq ≥ k .Äîêàçàòåëüñòâî:Ïðåäïîëîæèì, ÷òî åñòü âû÷èñëåíèå C , â êîòîðîì çíà÷åíèÿèç ïåðåìåííûõ sp è sq óâåëè÷èâàþòñÿ ëèøüêîíå÷íîå ÷èñëî ðàç.

Òîãäà, ñîãëàñíî íåðàâåíñòâó Ëåììû 3.1.sp − `q ≤ sq ≤ sp + `p , çíà÷åíèå äðóãîé ïåðåìåííîé òàêæå íåìîæåò óâåëè÷èâàòüñÿ áåñêîíå÷íî ÷àñòî.Ïóñòü σp è σq íàèáîëüøèå çíà÷åíèÿ ïåðåìåííûõ sp è sq .Òîãäà, cîãëàñíî Ëåììå 3.2., ëèáî îòïðàâëåíèå ïàêåòàh, inp [σq ], σq i ïðîöåññîì p , ëèáî îòïðàâëåíèå ïàêåòàh, inq [σp ], σp i ïðîöåññîì q äîïóñòèìî áåñêîíå÷íî äîëãîïîñëå òîãî, êàê ïåðåìåííûå sp , sq , ap è aq ïðèìóò ñâîèîêîí÷àòåëüíûå çíà÷åíèÿ.Òîãäà, cîãëàñíî äîïóùåíèþ F1, îäèí èç ýòèõ ïàêåòîâ(íàïðèìåð, h , inq [σp ], σp i) îòïðàâëÿåòñÿ áåñêîíå÷íî ÷àñòî,è, ñîãëàñíî äîïóùåíèþ F2, îí äîëæåí ïðèíèìàòüñÿ òàêæåáåñêîíå÷íî ÷àñòî.Ïîëó÷åíèå ïðîöåññîì p ïàêåòà h , inq [σp ], σp i ïðèâîäèò êòîìó, ÷òî çíà÷åíèå sp (ðàâíîå σp ) óâåëè÷èâàåòñÿ.Ýòî ïðîòèâîðå÷èò âûáîðó çíà÷åíèÿ σp .õîòÿ áû îäíîépackpackpackpackÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÇàäà÷è.1.

Ïîêàæèòå, ÷òî ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàíå óäîâëåòâîðÿåò òðåáîâàíèþ íåèçáåæíîé äîñòàâêèñîîáùåíèÿ, åñëè èç äâóõ äîïóùåíèé ñïðàâåäëèâîñòè F1 èF2 âûïîëíÿåòñÿ òîëüêî äîïóùåíèå F2.À ÷òî ïðîèçîéäåò, åñëè áóäåò âûïîëíÿòüñÿ òîëüêîäîïóùåíèå F1?2.  êàêîì ìåñòå îáîñíîâàíèÿ êîððåêòíîñòè ïðîòîêîëàèñïîëüçóåòñÿ ñâîéñòâî î÷åðåäíîñòè ïåðåäà÷è ñîîáùåíèéïî êàíàëàì ñâÿçè?3. Äîêàæèòå, ÷òî åñëè â ñèììåòðè÷íîì ïðîòîêîëåðàçäâèæíîãî îêíà `p + `q = 1 è íà÷àëüíûå çíà÷åíèÿïåðåìåííûõ ap è aq ðàâíû −`q è −`p , òî ðàâåíñòâàap + `q = sp è aq + `p = sq âñåãäà âûïîëíÿþòñÿ.Ðåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÀëãîðèòì â òîì âèäå, â êîòîðîì îí áûë ïðåäñòàâëåí,íåïðèãîäåí äëÿ ðåàëèçàöèè, òàê êàê â êàæäîì ïðîöåññåõðàíèòñÿ áåñêîíå÷íûé îáúåì èíôîðìàöèè (ìàññèâû in è out )è èñïîëüçóþòñÿ íåîãðàíè÷åííûå ïîðÿäêîâûå íîìåðà.Ïóñòü L = `p + `q .Ëåììà 3.3.Îòïðàâëåíèå ïàêåòà hòîãäà, êîãäà i < ap + L ., w , iipackïðîöåññîì p äîïóñòèìî òîëüêîÄîêàçàòåëüñòâî:Çàäà÷à.

Ðåøèòü ñàìîñòîÿòåëüíî.Ëåììà 3.4.Åñëè outp [i] 6= udef , òî âûïîëíÿåòñÿ íåðàâåíñòâî i < sp + L .Äîêàçàòåëüñòâî:Çàäà÷à. Ðåøèòü ñàìîñòîÿòåëüíî.Ðåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÈç ýòèõ ëåìì ñëåäóåò, ÷òîI Ïðîöåññ p äîëæåí õðàíèòü â ïàìÿòè òîëüêî ñëîâà èçîòðåçêà inp [ap . . . sp + `p − 1] , ïîñêîëüêó îí ìîæåòîòïðàâëÿòü òîëüêî ýòè ñëîâà. Óêàçàííûé îòðåçîê íàçîâåìîêíîì ïåðåäà÷è ïðîöåññà p .I Ïðîöåññ p ìîæåò îæèäàòü ïðèåìà òîëüêî òåõ ñëîâ, êîòîðûåîí ðàçìåòèò ÿ÷åéêàõ èç îòðåçêà outp [sp . .

. sp + L − 1] ,ïîñêîëüêó ïðîöåññ q ìîæåò îòïðàâëÿòü òîëüêî ýòè ñëîâà.Óêàçàííûé îòðåçîê íàçîâåì îêíîì ïðèåìà ïðîöåññà p .Ðåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÏðîòîêîë ñ îêíàìè ïðèåìà è ïåðåäà÷è.inpAAAASSSSp?inq A A A S S S S. . . . . . . . . Q.

p. . . . . . . . . . . .. . . . . . . . . . Q. q. . . . . . . . . . -.?= Ñáðîøåííûé âõîä= Îêíî ïåðåäà÷è= Çàïèñàííûå ñëîâà= Ïðèíÿòûå ñëîâàq?W W W W W W W u u R R u outpASWR?outq W W W W u R R u u u u uu= Íåîïðåäåëåííûå çíà÷åíèÿ= Îêíà ïåðåäà÷è/ïðèåìàÐåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíà òîì ñëó÷àå, åñëè êàíàëû ïîääåðæèâàþò î÷åðåäíîñòüïåðåäà÷è ñîîáùåíèé, ïîðÿäêîâûå íîìåðà ñëîâ òàêæå ìîæíîîãðàíè÷èòü.Òåîðåìà 3.7.Óòâåðæäåíèå P 0 , îïðåäåëÿåìîå ñëåäóþùåå ôîðìóëîéP0 ≡∧∧∧∧Phpack, w , iihpack, w 0 , i 0 ihpack, w , iihpack, w 0 , i 0 ihpack, w , ii ∈ Qp =⇒ i ≥ ap − `phpack, w , ii ∈ Qq =⇒ i ≥ aq − `qñëåäóåò çàñëåäóåò çàâ Qp ⇒ i > i 0 − Lâ Qq ⇒ i > i 0 − Lÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ðàçäâèæíîãî îêíà ïðèóñëîâèè, ÷òî â êàíàëàõ ñâÿçè ïîääåðæèâàåòñÿ î÷åðåäíîñòüïåðåäàâåìûõ ñîîáùåíèé.Äîêàçàòåëüñòâî:Çàäà÷à. Ðåøèòü ñàìîñòîÿòåëüíî.(4p)(4q)(5p)(5q)Ðåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÎòñþäà ñëåäóåòÒåîðåìà 3.8.Èç óòâåðæäåíèÿ P 0 âûòåêàþò ñëåäóþùèå ñîîòíîøåíèÿhpack, w , ii ∈ Qp =⇒ sp − L ≤ i < sp + Lèhpack, w , ii ∈ Qq =⇒ sq − L ≤ i < sq + L.Äîêàçàòåëüñòâî:Ðàññìîòðèì ïàêåò h , w , ii ∈ Qp .Ñîãëàñíî ñâîéñòâó (1p) èìååì íåðàâåíñòâî i < sq + `q , èçêîòîðîãî ïî Ëåììå 3.1 ñëåäóåò íåðàâåíñòâî i < sp + L .Ñîãëàñíî ñâîéñòâó (5p) èìååì íåðàâåíñòâî i ≥ ap − `p , èçêîòîðîãî ïî Ëåììå 3.1 ñëåäóåò íåðàâåíñòâî i ≥ sp − L .Àíàëîãè÷íûì îáðàçîì äîêàçûâåòñÿ ñîîòíîøåíèå î ïàêåòàõ èçî÷åðåäè Qq .packÐåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÊàê âèäíî èç Òåîðåìû 3.8, äîñòàòî÷íî, ÷òîáû íóìåðàöèÿïàêåòîâ ïðîâîäèëàñü ïî ìîäóëþ k , ãäå k ≥ 2L .sp − L ≤ i < sp + LÄåéñòâèòåëüíî, ðàñïîëàãàÿ çíà÷åíèåì ïåðåìåííîé sp , à òàêæåçíà÷åíèåì ïåðåìåííîé i ïî ìîäóëþ k , ïðîöåññ p ìîæåòâû÷èñëèòü íîìåð i .Ðåàëèçàöèè ïðîòîêîëà ðàçäâèæíîãî îêíàÎñîáî èíòåðåñíûé âàðèàíò ïðîòîêîëà ðàçäâèæíîãî îêíàâîçíèêàåò â òîì ñëó÷àå, êîãäà L = 1 , ò.å.