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

Áóäåìñ÷èòàòü, ÷òî ïðåäèêàòïî îïðåäåëåíèþ ïðèíèìàåòèñòèííîå çíà÷åíèå â êàæäîé çàêëþ÷èòåëüíîé êîíôèãóðàöèè, èëîæíîå çíà÷åíèå â êîíôèãóðàöèÿõ, êîòîðûå íå ÿâëÿþòñÿçàêëþ÷èòåëüíûìè.Îáû÷íî áûâàåò íåæåëàòåëüíî äîñòè÷ü çàêëþ÷èòåëüíîéêîíôèãóðàöèè ïðåæäå, ÷åì âûïîëíèòñÿ ¾öåëåâîé¿ ïðåäèêàò P; â ýòîì ñëó÷àå ãîâîðÿò, ÷òî ïðîèçîøëà. Åñëè æåöåëü äîñòèãíóòà, òî âûïîëíåíèå ìîæíî çàâåðøèòü; â ýòîìñëó÷àå ãîâîðÿò, ÷òî ïðîèçîøëî.termáëîêèðîâêàïðàâèëüíîå çàâåðøåíèåÎïðåäåëåíèå 3.2.Ïóñòü çàäàí ïðèçíàê ïðàâèëüíîãî çàâåðøåíèÿ âûïîëíåíèé P .Ñèñòåìà S(èëè, èíûìèñëîâàìè,), åñëè ïðåäèêàò(=⇒ P) âñåãäà ÿâëÿåòñÿ èñòèííûì äëÿ ñèñòåìû S .ïðàâèëüíî çàâåðøàåò âûïîëíåíèÿñâîáîäíà îò áëîêèðîâêètermÑâîéñòâà æèâîñòè îñíîâó ôóíêöèé íîðìèðîâêè ïîëîæåíî ìàòåìàòè÷åñêîåïîíÿòèåìíîæåñòâà.ôóíäèðîâàííîãîÎïðåäåëåíèå 3.3.×àñòè÷íî óïîðÿäî÷åííîå ìíîæåñòâî (W , <) íàçûâàåòñÿ, åñëè èç åãî ýëåìåíòîâ íåëüçÿ ñîñòàâèòüáåñêîíå÷íî óáûâàþùóþ ïîñëåäîâàòåëüíîñòüôóíäèðîâàííûìw1 > w2 > w3 · · · .Ïðèìåðû ôóíäèðîâàííûõ ìíîæåñòâ:I ìíîæåñòâî íàòóðàëüíûõ ÷èñåë ñ îáû÷íûì îòíîøåíèåìïîðÿäêà,I ìíîæåñòâî âñåõ íàáîðîâ äëèíû n , ñîñòîÿùèõ èçíàòóðàëüíûõ ÷èñåë, ñ îòíîøåíèåì ëåêñèêîãðàôè÷åñêîãîïîðÿäêà.Ñâîéñòâà æèâîñòèÎòñóòñòâèå áåñêîíå÷íî óáûâàþùèõ ïîñëåäîâàòåëüíîñòåé,ñîñòîÿùèõ èç ýëåìåíòîâ ôóíäèðîâàííîãî ìíîæåñòâà, ìîæíîèñïîëüçîâàòü äëÿ äîêàçàòåëüñòâà òîãî, ÷òî íåêîòîðîåóòâåðæäåíèå P íàâåðíÿêà ñòàíåò èñòèííûì.

Äëÿ ýòîãî íóæíîïîêàçàòü, ÷òî ñóùåñòâóåò ôóíêöèÿ f , îòîáðàæàþùàÿ C âôóíäèðîâàííîå ìíîæåñòâî W òàê, ÷òî êàæäûé ïåðåõîäïðèâîäèò ê òîìó, ÷òî ëèáî çíà÷åíèå f óìåíüøàåòñÿ, ëèáî Pñòàíîâèòñÿ èñòèííûì.Îïðåäåëåíèå 3.4.Ïóñòü çàäàíû ñèñòåìà ïåðåõîäîâ S è óòâåðæäåíèå P . Ôóíêöèÿf , îòîáðàæàþùàÿ ìíîæåñòâî C â ôóíäèðîâàííîå ìíîæåñòâîW , íàçûâàåòñÿ(ïî îòíîøåíèþ ê P ) ,åñëè äëÿ êàæäîãî ïåðåõîäà γ → δ , ëèáî âûïîëíÿåòñÿf (γ) > f (δ) , ëèáî P(δ) ïðèíèìàåò èñòèííîå çíà÷åíèå.ôóíêöèåé íîðìèðîâêèÑâîéñòâà æèâîñòèÒåîðåìà 3.3.Ïóñòü çàäàíû ñèñòåìà ïåðåõîäîâ S è óòâåðæäåíèå P .

Åñëè Sïðàâèëüíî çàâåðøàåò âûïîëíåíèÿ, è ñóùåñòâóåò ôóíêöèÿíîðìèðîâêè f (ïî îòíîøåíèþ ê P ), òî äëÿ êàæäîãîâûïîëíåíèÿ S óòâåðæäåíèå P ñòàíîâèòñÿ èñòèííûì âíåêîòîðîé êîíôèãóðàöèè.Äîêàçàòåëüñòâî:Äîïóñòèì, ÷òî åñòü áåñêîíå÷íîå âûïîëíåíèå E = (γ0, γ1, γ2, . . .)ñèñòåìû S , â êîòîðîì P âñåãäà ëîæíî.Ïî îïðåäåëåíèþ ôóíêöèè íîðìèðîâêè f , ïîñëåäîâàòåëüíîñòüs = (f (γ0 ), f (γ1 ), . . .) ÿâëÿåòñÿ óáûâàþùåé.Òàê êàê W ôóíäèðîâàííîå ìíîæåñòâî, ïîñëåäîâàòåëüíîñòü säîëæíà áûòü êîíå÷íîé. Ïðîòèâîðå÷èå.Cèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàvarSpsp , apinpoutp:: array of word: array of word: { ap ≤ i < sp + `p }Rp: {hinitinitbegin}send hpackreceive(*endelse}, w , ii ∈ QpQp := Qp \ hpack, w , iipackbeginto qend;èãíîðèðîâàòü ïîâòîðíîå ïîëó÷åíèå ïàêåòà *)end: {h, inp [i], ii;;Lp0, 0, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packbegin;(* Data to be sent *) ;udef , udef , .

. . ;integer{}endÑèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÐàññìîòðèì óòâåðæäåíèåP≡∧∧∧∧∧∧∧∀i < sp : outp [i] 6= udef∀i < sq : outq [i] 6= udef∀i : hpack, w , ii ∈ Qp ⇒ w = inq [i] ∧ (i < sq + `q )∀i : hpack, w , ii ∈ Qq ⇒ w = inp [i] ∧ (i < sp + `p )∀i : outp [i] 6= udef ⇒ outp [i] = inq [i] ∧ (ap > i − `q )∀i : outq [i] 6= udef ⇒ outq [i] = inp [i] ∧ (aq > i − `p )ap ≤ s qaq ≤ s pÒåîðåìà 3.4.Óòâåðæäåíèå P ÿâëÿåòñÿ èíâàðèàíòîì àëãîðèòìà ðàçäâèæíîãîîêíà.(0p)(0q)(1p)(1q)(2p)(2q)(3p)(3q)Äîêàçàòåëüñòâî Òåîðåìû 3.4.Âîñïîëüçóåìñÿ îïðåäåëåíèåì èíâàðèàíòà è ïîêàæåì, ÷òî1.

P(γ) èñòèííî äëÿ êàæäîé íà÷àëüíîé êîíôèãóðàöèè γ ∈ I ,è2. {P} → {P} .1. íà÷àëüíîé êîíôèãóðàöèè î÷åðåäè Qp è Qq ïóñòû,äëÿ âñÿêîãî i , çíà÷åíèÿ outp [i] è outq [i] ðàâíû udef ,çíà÷åíèÿ ïåðåìåííûõ ap , aq , sq è sp ðàâíû 0 .Îòñþäà ñëåäóåò èñòèííîñòü óòâåðæäåíèÿ P äëÿ êàæäîéíà÷àëüíîé êîíôèãóðàöèè γ .Áàçèñ.Äîêàçàòåëüñòâî Òåîðåìû 3.4.2.Èíäóêòèâíûé ïåðåõîä.Äàëåå ðàññìîòðèì ïîî÷åðåäíî âñå ïåðåõîäû ïðîòîêîëà èïîêàæåì, ÷òî ïðè êàæäîì èç íèõ óòâåðæäåíèå P ñîõðàíÿåòèñòèííîñòü.Ïðè ýòîì áóäåì èìåòü â âèäó, ÷òî çíà÷åíèÿ ìàññèâîâ inp èinq íèêîãäà íå èçìåíÿþòñÿ.Îáîñíîâàíèå {P} → {P} ïðîâåäåì íà ïðèìåðå äåéñòâèÿp ïðèåìà ñîîáùåíèÿ ïðîöåññîì p .RÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif;;endend}, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;Äîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (0p): ∀i < sp : outp [i] 6= udefîñòàåòñÿ âåðíûì ïîñëå âûïîëíåíèÿ îïåðàòîðàsp := min {j| outp [j] = udef } .Äîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (0q): ∀i < sq : outq [i] 6= udefîñòàåòñÿ âåðíûì, ïîñêîëüêó äåéñòâèå p íå èçìåíÿåò çíà÷åíèÿïåðåìåííîé sq è íå çàïèñûâàåò â ìàññèâ outq [i]íåîïðåäåëåííîãî çíà÷åíèÿ udef .RÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (1p):∀i : hpack, w , ii ∈ Qp =⇒ w = inq [i] ∧ (i < sq + `q )ñîõðàíÿåò èñòèííîñòü, ïîñêîëüêó äåéñòâèå p íå äîáàâëÿåòíîâûõ ïàêåòîâ â î÷åðåäü Qp è íå óìåíüøàåò çíà÷åíèÿïåðåìåííîé sq .RÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (1q):∀i : hpack, w , ii ∈ Qq =⇒ w = inp [i] ∧ (i < sp + `p )ñîõðàíÿåò èñòèííîñòü, ïîñêîëüêó äåéñòâèå p íå äîáàâëÿåòíîâûõ ïàêåòîâ â î÷åðåäü Qq è íå óìåíüøàåò çíà÷åíèÿïåðåìåííîé sp .RÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (2p):∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )îñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òî1) p ïðè ïîëó÷åíèè ïàêåòà h , w , ii èç î÷åðåäè Qpçàïèñûâàåò w â ýëåìåíò outp [i] âûõîäíîãî ìàññèâà, à èçóñëîâèÿ (1p) ñëåäóåò, ÷òî w = inq [i] ;RpackÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;;endendÓñëîâèå (2p):∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )îñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òî1) p ïðè ïîëó÷åíèè ïàêåòà h , w , ii èç î÷åðåäè Qpçàïèñûâàåò w â ýëåìåíò outp [i] âûõîäíîãî ìàññèâà, à èçóñëîâèÿ (1p) ñëåäóåò, ÷òî w = inq [i] ;2) ïðèñâàèâàíèå ap := max (ap , i − `q + 1) ãàðàíòèðóåò, ÷òîíåðàâåíñòâî ap > i − `q áóäåò âåðíî è ïîñëå âûïîëíåíèÿ p .RpackRÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;;endendÓñëîâèå (2q):∀i : outq [i] 6= udef =⇒ outq [i] = inp [i] ∧ (aq > i − `p )îñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òîïåðåìåííîé aq è ìàññèâà outq .Rpíå èçìåíÿåò çíà÷åíèéÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hpackbegin, w , ii ∈ Qpreceive hif};, w , iioutp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }pack;endendÓñëîâèå (3p): ap ≤ sqîñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òî1) p íå èçìåíÿåò çíà÷åíèÿ ïåðåìåííîé sq ;R;Äîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;;endendÓñëîâèå (3p): ap ≤ sqîñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òî1) p íå èçìåíÿåò çíà÷åíèÿ ïåðåìåííîé sq ;2) êîãäà ïðè ïîëó÷åíèè ïàêåòà h , w , ii âûïîëíÿåòñÿïðèñâàèâàíèå ap := max(ap , i − `q + 1) , èç óñëîâèÿ (1p) ñëåäóåòíåðàâåíñòâî i < sq + `q , è ïîýòîìó íåðàâåíñòâî ap ≤ sqîñòàåòñÿ âåðíûì.RpackÄîêàçàòåëüñòâî Òåîðåìû 3.4.Rp:{hbegin}, w , ii ∈ Qphpack, w , iiif outp [i] = udef thenbegin outp [i] := wap := max (ap , i − `q + 1)sp := min {j| outp [j] = udef }packreceive;;;endendÓñëîâèå (3q): aq ≤ spîñòàåòñÿ èñòèííûì â ñâÿçè ñ òåì, ÷òî çíà÷åíèå ïåðåìåííîé aqíå èçìåíÿåòñÿ, à çíà÷åíèåì ïåðåìåííîé sp ìîæåò ëèøüóâåëè÷èòüñÿ ïîñëå âûïîëíåíèÿ äåéñòâèÿ p .RÄîêàçàòåëüñòâî Òåîðåìû 3.4.Sp: { ap ≤ i < sp + `p }Lp:{h, w , ii ∈ Qppackbegin}send hbeginpack, inp [i], iito q{Qp := Qp \ hpack, w , iiend}endÇàäà÷à: äîêàçàòü, ÷òî ýòèäåéñòâèÿ ïðîöåññîâ òàêæåñîõðàíÿþò èíâàðèàíòP.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÒåîðåìà 3.5.Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà óäîâëåòâîðÿåòòðåáîâàíèþ áåçîïàñíîé äîñòàâêè ñîîáùåíèé, ò.å.

â êàæäîéäîñòèæèìîé êîíôèãóðàöèè ïðîòîêîëà âûïîëíÿþòñÿñîîòíîøåíèÿoutp [0..sp − 1] = inq [0..sp − 1] è outq [0..sq − 1] = inp [0..sq − 1].Äîêàçàòåëüñòâî:Ñëåäóåò èç Òåîðåìû 3.2 (î ñâîéñòâå èíâàðèàíòîâ) è Òåîðåìû3.4.Èç óñëîâèé(0p): ∀i < sp : outp [i] 6= udef(2p): ∀i : outp [i] 6= udef =⇒ outp [i] = inq [i] ∧ (ap > i − `q )ñëåäóåò âûïîëíèìîñòü ðàâåíñòâà outp [0..sp − 1] = inq [0..sp − 1] ,à èç óñëîâèé (0q) è (2q) ñëåäóåò âûïîëíèìîñòü ðàâåíñòâàoutq [0..sq − 1] = inp [0..sq − 1] .Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíà×òîáû óáåäèòüñÿ â òîì, ÷òî äîñòàâêà ñîîáùåíèé íåèçáåæíà,íåîáõîäèìîI ââåñòè äîïóùåíèÿ ñïðàâåäëèâîñòè,I à òàêæå ââåñòè îãðàíè÷åíèÿ íà çíà÷åíèÿ `p è `q .Áåç ýòèõ îãðàíè÷åíèé ïðîòîêîë íå áóäåò îáëàäàòü ñâîéñòâîìæèâîñòè.(Ïî÷åìó?)Ñèììåòðè÷íûé ïðîòîêîë ðàçäâèæíîãî îêíàÎãðàíè÷åíèÿII êà÷åñòâå `p è `q ìîæíî âçÿòü ëþáûå íåîòðèöàòåëüíûåêîíñòàíòû, óäîâëåòâîðÿþùèå íåðàâåíñòâó `p + `q > 0 .Âûäâèãàþòñÿ äâà òðåáîâàíèÿ ñïðàâåäëèâîñòè:F1.