4 Коммуникационный протокол с таймером - устройство и обоснование корректности

ÐàñïðåäåëåííûåàëãîðèòìûËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 4.Êîììóíèêàöèîííûé ïðîòîêîë ñ òàéìåðàìè.Äîïóùåíèÿ î âðåìåíè. Òàéìåðû.Óñòðîéñòâî ïðîòîêîëà ñ òàéìåðàìè.Îáîñíîâàíèå êîððåêòíîñòè ïðîòîêîëà ñ òàéìåðàìè.Ìîäèôèêàöèè ïðîòîêîëà.Êîììóíèêàöèîííûé ïðîòîêîë ñ òàéìåðàìèÏðè ïåðåäà÷å ñîîáùåíèé íà ¾äàëüíèå¿ ðàññòîÿíèÿ ïðèõîäèòñÿèñïîëüçîâàòü ïðîìåæóòî÷íûå óçëû â êà÷åñòâåðåòðàíñëÿöèîííûõ ñòàíöèé.  ýòîì ñëó÷àå âîçíèêàþòñëåäóþùèå äîïîëíèòåëüíûå òðóäíîñòè:Iíåîáõîäèìî óñòàíàâëèâàòü è çàâåðøàòü ñîåäèíåíèÿ(ñåàíñû ñâÿçè);Iñîîáùåíèÿ ìîãóò íå òîëüêî òåðÿòüñÿ, íî òàêæåäóáëèðîâàòüñÿ è ïåðåìåøèâàòüñÿ (èçìåíÿòüîòíîñèòåëüíûé ïîðÿäîê ñëåäîâàíèÿ).Äëÿ ðåøåíèÿ ýòîé çàäà÷è Ôëåò÷åð è Âàòñîí ïðåäëîæèëè ∆t-ïðîòîêîë ñêâîçíîé ïåðåäà÷è ñîîáùåíèé ñ èñïîëüçîâàíèåìñèíõðîíèçîâàííûõ òàéìåðîâ.Êîììóíèêàöèîííûé ïðîòîêîë ñ òàéìåðàìèÌû ðàññìîòðèì óïðîùåííûé âàðèàíò ýòîãî ïðîòîêîëà.Óïðîùåíèÿ êàñàþòñÿ ñëåäóþùèõ ÷åòûðåõ àñïåêòîâ ýòîãîïðîòîêîëà.Îäíîíàïðàâëåííîñòü.

Ïåðåäà÷à äàííûõ èäåò òîëüêî â îäíîìíàïðàâëåíèè îò ïðîöåññà p ê ïðîöåññó q . Ìû áóäåì íàçûâàòüïðîöåññ p îòïðàâèòåëåì, à ïðîöåññ q ïîëó÷àòåëåì. îêíå ïðèåìà îäíî ñëîâî. Ïîñòóïèâøèé ïàêåò ïîëó÷àòåëüäîñòàâëÿåò ïî íàçíà÷åíèþ òîëüêî â òîì ñëó÷àå, êîãäà åãîïîðÿäêîâûé íîìåð ñîâïàäàåò ñ îæèäàåìûì íîìåðîì.Ïàêåòû ñîñòîÿò èç îäíîãî ñëîâà.  êàæäûé ïàêåò äàííûõîòïðàâèòåëü ìîæåò ïîìåñòèòü îäíî-åäèíñòâåííîå ñëîâî.Óïðîùåííûå äîïóùåíèÿ î âðåìåíè. Èñïîëüçóåòñÿ ìèíèìàëüíîåêîëè÷åñòâî òàéìåðîâ. Íàïðèìåð, ïðåäïîëàãàåòñÿ, ÷òîïîäòâåðæäåíèå ìîæåò áûòü îòïðàâëåíî â ëþáîå âðåìÿ äî òåõïîð, ïîêà ïîëó÷àòåëü ïîääåðæèâàåò ñîåäèíåíèå îòêðûòûì.Ñèíõðîíèçàöèÿ òàéìåðîâ. Ôèçè÷åñêîå âðåìÿ îäèíàêîâîâîçäåéñòâóåò íà ïîêàçàíèÿ âñåõ òàéìåðîâ.Äîïóùåíèÿ î âðåìåíè. ÒàéìåðûÒàéìåðû óñòðîéñòâà, èçìåðÿþùèå ôèçè÷åñêîå âðåìÿ.

Ìûáóäåì îïèðàòüñÿ íà ñëåäóþùèå îñíîâíûå ïðåäïîëîæåíèÿ îâðåìåíè è òàéìåðàõ.1. Ãëîáàëüíîå âðåìÿ. Âñå ïðîöåññû ñèñòåìû ôóíêöèîíèðóþòâ ðàìêàõ åäèíîé ãëîáàëüíîé øêàëû âðåìåíè. Êàæäîåñîáûòèå ïðîèñõîäèò ìãíîâåííî, è ïðîöåññû íå ìîãóòðåãèñòðèðîâàòü òå ìîìåíòû âðåìåíè, â êîòîðûåïðîèñõîäÿò ñîáûòèÿ.2.

Îãðàíè÷åííîå âðåìÿ æèçíè ïàêåòà. Âðåìÿ æèçíè ïàêåòàîãðàíè÷åíî íåêîòîðîé êîíñòàíòîé µ (ìàêñèìàëüíîå âðåìÿæèçíè ïàêåòà ). Åñëè ïàêåò áûë îòïðàâëåí â ìîìåíòâðåìåíè σ è ïîëó÷åí â ìîìåíò âðåìåíè τ , òî ñïðàâåäëèâîíåðàâåíñòâîσ < τ < σ + µ.Åñëè â êàíàëå ïðîèçîøëî äóáëèðîâàíèå ïàêåòà, òî êàæäàÿêîïèÿ äîëæíà áûòü ïîëó÷åíà ñïóñòÿ íå áîëåå µ åäèíèöâðåìåíè ïîñëå îòïðàâëåíèÿ èñõîäíîãî ïàêåòà (â ïðîòèâíîìñëó÷àå êîïèè áóäóò óòðà÷åíû).Óòî÷íåíèå óñëîâèé çàäà÷è êîììóíèêàöèèÏîñòóïëåíèå âõîäíûõ ñëîâ.Âõîäíûå ñëîâà, ïîäëåæàùèå îòïðàâëåíèþ, ìîäåëèðóþòñÿáåñêîíå÷íûì ìàññèâîì inp .  êàæäûé ìîìåíò âðåìåíèïðîöåññ p èìååò äîñòóï òîëüêî ê íåêîòîðîé ÷àñòè ìàññèâà.Ïðåäïîëàãàåòñÿ, ÷òî èìååòñÿ íåêîòîðûé ïðîöåññ-ãåíåðàòîð(àãåíò), ïîðîæäàþùèé ñëîâà âõîäíîãî ìàññèâà.Ïðîöåññ-îòïðàâèòåëü p ïîëó÷àåò âñå íîâûå è íîâûå ñëîâà îòàãåíòà, ïîðîæäàþùåãî ýòè ñëîâà. Ýòó îïåðàöèþ áóäåìíàçûâàòü ïîñòóïëåíèåì ñëîâ ê ïðîöåññó-îòïðàâèòåëþ.Âðó÷åíèå âûõîäíûõ ñëîâ.Ïðåäïîëàãàåòñÿ, ÷òî èìååòñÿ íåêîòîðûé ïðîöåññ-ïîòðåáèòåëü(àãåíò), êîòîðîìó äîëæíû áûòü äîñòàâëåíû ñëîâà âõîäíîãîìàññèâà.

Ïðîöåññ-ïîëó÷àòåëü áóäåò âðó÷àòü ýòè ñëîâàïðîöåññó-ïîòðåáèòåëþ ïîñðåäñòâîì îïåðàöèè, êîòîðóþóñëîâèìñÿ íàçûâàòü âðó÷åíèåì ñëîâà.Çàäà÷à íàäåæíîãî îáìåíà èíôîðìàöèåéÃåíåðàòîðÏîñòóïëåíèåÏîòðåáèòåëü6Âðó÷åíèå6Óâåäîìëåíèå?ÎòïðàâèòåëüÏðîöåññ pÏîëó÷àòåëü66??Ñåòü ïåðåäà÷è äàííûõ (DN)Ðèñ.: Óïðîùåííàÿ àðõèòåêòóðà ñåòè.Ïðîöåññ qÓòî÷íåíèå óñëîâèé çàäà÷è êîììóíèêàöèèÑâîéñòâà ïðîòîêîëà.1. Îòñóòñòâèå ïîòåðü. Êàæäîå ñëîâî èç ìàññèâà inp áóäåòâðó÷åíî ïðîöåññîì q ïîòðåáèòåëþ èëè çàðåãèñòðèðîâàíîïðîöåññîì p (êàê ¾âåðîÿòíî ïîòåðÿííîå¿) ñïóñòÿîãðàíè÷åííûé îòðåçîê âðåìåíè ñ ìîìåíòà ïîñòóïëåíèÿýòîãî ñëîâà îò ãåíåðàòîðà ê ïðîöåññó p .2.

Ñîáëþäåíèå ïîðÿäêà. Ñëîâà, êîòîðûå âðó÷àþòñÿïîòðåáèòåëþ ïðîöåññîì q , ñëåäóþò â ïîðÿäêå ñòðîãîãîâîçðàñòàíèÿ íîìåðîâ â ìàññèâå inp .Íèêàêîé ïðîòîêîë íå ìîæåò ïðåäîñòàâèòü ãàðàíòèè òîãî,÷òî ñëîâî áóäåò äîñòàâëåíî ïî íàçíà÷åíèþ çàîãðàíè÷åííûé ñðîê âðåìåíè.Ïî÷åìó?Îïèñàíèå ïðîòîêîëà ñ òàéìåðàìèÑïèñîê êîíñòàíò.Ñåòåâàÿ êîíñòàíòà:µ :; (* ìàêñèìàëüíîå âðåìÿ æèçíè ïàêåòà *)realÊîíñòàíòû ïðîòîêîëà:U :R :S; (* Ïðîäîëæèòåëüíîñòü ïåðèîäà îòïðàâëåíèÿ ñîîáùåíèÿ *); (* Ïðîäîëæèòåëüíîñòü ïåðåðûâà ïðè ïðèåìå ñîîáùåíèÿ:R ≥ U + µ *): real; (* Ïðîäîëæèòåëüíîñòü ïåðåðûâà ïðè ïåðåäà÷å ñîîáùåíèÿ:S ≥ R + 2µ *)realrealÎïèñàíèå ïðîòîêîëà ñ òàéìåðàìèÑïèñîê ïåðåìåííûõ è ìàññèâîâ.Ó÷åòíûå çàïèñè îòïðàâèòåëÿ:Low: integer; (* Ïîäòâåðæäåííûå ñëîâà òåêóùåãî ñåàíñà ñâÿçè *)High : integer; (* Ïîñòóïèâøèå ñëîâà òåêóùåãî ñåàíñà ñâÿçè *)Ut: array of timers ; (* Ìàññèâ òàéìåðîâ *)St: timer ; (* Òàéìåð îòïðàâèòåëÿ*)Ó÷åòíûå çàïèñè ïîëó÷àòåëÿ:Exp: integer; (* Î÷åðåäíîé îæèäàåìûé ïîðÿäêîâûé íîìåð *)Rt: timer ; (* Òàéìåð ïîëó÷àòåëÿ *)Êîììóíèêàöèîííàÿ ïîäñèñòåìà:Mq: channel ; (* Ïàêåòû äàííûõ äëÿ ïðîöåññà q *)Mp: channel ; (* Ïàêåòû ïîäòâåðæäåíèé äëÿ ïðîöåññà p *)Âñïîìîãàòåëüíûå ïåðåìåííûå:B: integer init 0 (* Ñëîâà èç ïðåäûäóùåãî ñåàíñà ñâÿçè *)cr: bool init false ; (* Ó÷àñòèå ïîëó÷àòåëÿ â ñåàíñå ñâÿçè *)cs: bool init false ; (* Ó÷àñòèå îòïðàâèòåëÿ â ñåàíñå ñâÿçè *)Ñöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüw?pqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüUtw :=U w pqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÏðîõîäèò âðåìÿÃåíåðàòîðÏîòðåáèòåëüw pqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðUtw > 0?ÏîòðåáèòåëüSt :=Spqhw , i, µi?ÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÏðîõîäèò âðåìÿÃåíåðàòîðÏîòðåáèòåëüpqhw , i, µiÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüpρ > 0?Ñåòüq6hw , i, ρiÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðpÏîòðåáèòåëüi = Exp?Ñåòüq6hw , i, ρiÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëü6wpqÑåòüRt :=RÑöåíàðèé ðàáîòû ïðîòîêîëàÏðîõîäèò âðåìÿÃåíåðàòîðÏîòðåáèòåëüpqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüpqhack, Exp, µi?ÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÏðîõîäèò âðåìÿÃåíåðàòîðÏîòðåáèòåëüpqÑåòühack, Exp, µiÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüp St > 0?6hack, Exp, τ iÑåòüqÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüp τ > 0?6hack, Exp, τ iÑåòüqÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëü6îò÷åòpqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÏðîõîäèò âðåìÿÃåíåðàòîðÏîòðåáèòåëüpqÑåòüÑöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðÏîòðåáèòåëüpqÑåòüRt > 0?Ñöåíàðèé ðàáîòû ïðîòîêîëàÃåíåðàòîðpÏîòðåáèòåëüSt > 0?ÑåòüqÎïèñàíèå ïðîòîêîëà ñ òàéìåðàìè(ïðîöåññîòïðàâèòåëü)Ap :cs thencreate(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := S end;Ut[B + High] := U ; High := High + 1begin if notbeginendSp : { cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SRp : { cs ∧ hack, i, ρi ∈ Mp }begin receivehack, i, ρi ; Low := max (Low , i) endEp : { cs ∧ Ut[B + Low ] ≤ −2µ − R }begin error [B + Low ] := true ; Low := Low + 1 endCp : { cs ∧ St < 0 ∧ Low = High }begin B := B + High ; delete (St, High, Low ) end(* cs := false *)endÎòêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Ap : (* Ïîñòóïëåíèå î÷åðåäíîãî ñëîâà *)begin if not cs thenbegin(* Âíà÷àëå îòêðûâàåòñÿ ñåàíñ ñâÿçè *)create(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := Send;Ut[B + High] := U ; High := High + 1endÏðîòîêîë îòêðûâàåò ñåàíñ ñâÿçè âñÿêèé ðàç, êîãäà ñîåäèíåíèåîòñóòñòâóåò, íî ïðè ýòîì ê îòïðàâèòåëþ ïîñòóïàåò íåêîòîðîåñëîâî.Ïðåäèêàò cs èìååò çíà÷åíèå true , êîãäà îòïðàâèòåëü îòêðûëñåàíñ ñâÿçè.

Äëÿ òîãî, ÷òîáû âûÿñíèòü, îòêðûò ëè ñåàíñ ñâÿçè,ïðîöåññ ïðîâåðÿåò, ñóùåñòâóåò ëè ó÷åòíàÿ çàïèñü ñîåäèíåíèÿ âñïèñêå çàïèñåé îòêðûòûõ ñåàíñîâ ñâÿçè.Îòêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Ap : (* Ïîñòóïëåíèå î÷åðåäíîãî ñëîâà *)begin if not cs thenbegin(* Âíà÷àëå îòêðûâàåòñÿ ñåàíñ ñâÿçè *)create(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := Send;Ut[B + High] := U ; High := High + 1endÊîãäà îòïðàâèòåëü îòêðûâàåò ñåàíñ ñâÿçè, îí íà÷èíàåòíóìåðàöèþ ïîñòóïèâøèõ ê íåìó ñëîâ ñ 0 . Ïåðåìåííàÿ Highïðåäíàçíà÷åíà äëÿ ïîäñ÷åòà êîëè÷åñòâà ñëîâ, ïîñòóïèâøèõ âòåêóùåì ñåàíñå ñâÿçè, à ïåðåìåííàÿ Low ñëóæèò äëÿ ïîäñ÷åòàêîëè÷åñòâà ñëîâ, ïîäòâåðæäåííûõ â òåêóùåì ñåàíñå ñâÿçè.Îòïðàâèòåëü ìîæåò ïåðåñûëàòü ïàêåòû, ïîðÿäêîâûå íîìåðàêîòîðûõ ðàñïîëîæåíû â èíòåðâàëå ìåæäó äâóìÿ ÷èñëàìè Lowè High − 1 .Îòêðûòèå ñåàíñà ñâÿçè (ïðîöåññîòïðàâèòåëü)Ap : (* Ïîñòóïëåíèå î÷åðåäíîãî ñëîâà *)begin if not cs thenbegin(* Âíà÷àëå îòêðûâàåòñÿ ñåàíñ ñâÿçè *)create(St, High, Low ) ; (* cs := true *)Low := High := 0 ; St := Send;Ut[B + High] := U ; High := High + 1endÊàæäîå âíîâü ïîñòóïèâøåå ñëîâî ¾ñòàâèòñÿ íà ó÷åò¿ äëÿíåãî çàâîäèòñÿ îòäåëüíûé òàéìåð, â êîòîðûé óñòàíàâëèâàåòñÿïðåäåëüíî äîïóñòèìûé ñðîê îòïðàâëåíèÿ ýòîãî ñëîâà.

Åñëè ïîèñòå÷åíèè âðåìåíè U ñëîâî íå áóäåò îòïðàâëåíî, òî îíî áóäåòñ÷èòàòüñÿ ïîòåðÿííûì.Îòïðàâëåíèå ñîîáùåíèÿ(ïðîöåññîòïðàâèòåëü)Sp :(* Îòïðàâèòü i -å ñëîâî òåêóùåãî ñåàíñà ñâÿçè *){ cs ∧ Low ≤ i < High ∧ Ut[B + i] > 0 }begin sendhdata, (i = Low ), i, inp [B + i], µi ; St := SendÏðè îòêðûòîì ñåàíñå ñâÿçè äëÿ ïåðåäà÷è âûáèðàþòñÿ ëèøü òåñëîâà, íîìåðà êîòîðûõ ðàñïîëîæåíû â äèàïàçîíåLow . .