dr inż. Arkadiusz Danilecki
W oparciu o wykłady prof. J. Brzezińskiego
Łączymy procesy w wirtualną gwiazdę. Inicjator okresowo sprawdza, czy wszystkie procesy są pasywne i czy wszystkie wysłane przez nie wiadomości zostały już odebrane.
message $reply$ is a struct $\left\langle \mbox{ bool } contPassive \right\rangle$
message $query$, $ack$
local int ~~notAck_i~~ := ~~0~~
local bool ~~contPassive_i~~ := true
local bool ~~AV_i~~ := ~~\emptyset~~
when ~~{P}_{\alpha}~~ wants to start termination detection
repeat
local bool sTermDetected := true
send ~~query~~ to all ~~P_k~~ in ~~\mathcal{ P }~~
for all ~~P_k~~ in ~~\mathcal{ P }~~ do
receive ~~reply~~ from ~~P_k~~
~~sTermDetected~~ := ~~sTermDetected \land reply.contPassive~~
end for
until sTermDetected = true
decide "termination detected"
end when
when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
~~notAck_i~~ := ~~notAck_i~~ + 1
send ~~m~~ to ~~P_j~~
end when
when a message ~~m~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
send ~~ack~~ to ~~P_j~~
deliver ~~m~~
end when
when a message ~~ack~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
~~notAck_i~~ := ~~notAck_i~~ - 1
end when
when a message ~~query~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
wait until ~~passive_i~~ and ~~notAck_i = 0~~ and ~~\neg activate( AV_i )~~
~~reply.contPassive~~ := ~~contPassive_i~~
~~contPassive_i~~ := true
send ~~reply~~ to ~~P_j~~
end when
when a process ~~P_i~~ activates do
~~contPassive_i~~ := false
end when
Postęp
Jeżeli przetwarzanie zakończyło się przed ~~k~~-tym cyklu algorytmu, to algorytm w skończonym czasie wykryje zakończenie.
Skoro kanały są niezawodne, to wszystkie wiadomości w skończonym czasie dotrą do adresatów (1), a więc wiadomości ~~query~~ wysłane w ~~k~~-tym cyklu dotrą do każdego procesu. Procesy czekają z odpowiedzią, aż będą pasywne, nie uaktywnią je wiadomości dostępne oraz ~~notAck~~ będzie równe zero.
Skoro zakończenie zaszło, procesy są pasywne i nie będą uaktywnione. Z (1), każdy proces ostatecznie otrzyma ~~ack~~ w odpowiedzi na wysłaną wiadomość, a więc ~~notAck~~ będzie równe zero. Każdy proces więc odeśle ~~reply~~, który z (1) dotrze do inicjatora, kończąc ~~k~~-ty cykl.
Postęp
Jeżeli przetwarzanie zakończyło się przed ~~k~~-tym cyklu algorytmu, to algorytm w skończonym czasie wykryje zakończenie.
~~k~~-ty cykl mógł się nie zakończyć wykryciem zakończenia, jeżeli chociaż dla jednej wiadomości ~~reply~~ pole ~~contPassive~~ było równe false.
Przed wysłaniem ~~reply~~ każdy proces ~~P_i~~ ustawia ~~contPassive_i~~ na wartość true. Skoro zakończenie zaszło, proces już się nie uaktywni i nie zmieni dalej wartości tej zmiennej na false.
Po zakończeniu ~~k~~-tego cyklu inicjator w skończonym czasie zacznie ~~k~~+1szy cykl. Rozumując analogicznie jak poprzednio, cykl ten zakończy się w skończonym czasie, ale tym razem z (2) wynika, że ~~reply.contPassive~~ dla każdego ~~reply~~ będzie równe true, a więc inicjator wyskoczy z pętli stwierdzając zakończenie w skończonym czasie (c.b.d.u).
Bezpieczeństwo
Jeżeli ~~k+1~~-szy cykl algorytm zakończył się wykryciem zakończenia, to przetwarzanie faktycznie uległo zakończeniu przed końcem ~~k+1~~-szym cyklem.
$${Sterm({\mathcal {P}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land ({\mathcal {IT}}_{i}=\emptyset )\land \neg activate_{i}({\mathcal {AV}}_{i}))}$$
Oznaczenia
Oczywiście ~~\tau_b^k \lt \tau_i^k \lt \tau_e^k~~
Bezpieczeństwo
Jeżeli ~~k+1~~-szy cykl algorytm zakończył się wykryciem zakończenia, to przetwarzanie faktycznie uległo zakończeniu przed końcem ~~k+1~~-szym cyklem.
Skoro algorytm zakończył się w chwili ~~\tau_e^{k+1}~~, to inicjator musiał otrzymać od każdego innego procesu ~~reply~~, wysłany w chwili ~~\tau_i^{k+1}~~ z polem ~~contPassive~~ równym true. Z tego wynika, że żaden proces nie był uaktywniony od końca poprzedniego cyklu, a dokładniej od chwili gdy w poprzednim cyklu wysłał ~~reply~~.
Istniała więc jakaś chwila ~~\tau_x~~, ~~\tau_i^k \lt \tau^x \lt \tau_i^{k+1}~~, w której ~~passive_i(\tau^x)~~ było równe true (C1).
Bezpieczeństwo
Jeżeli ~~k+1~~-szy cykl algorytm zakończył się wykryciem zakończenia, to przetwarzanie faktycznie uległo zakończeniu przed końcem ~~k+1~~-szym cyklem.
Czy dla każdego procesu, prowadzące do niego kanały są puste (~~IT_i = \emptyset~~)?
Proces mógł wysłać ~~reply~~ w chwili ~~\tau_i^{k}~~ tylko, gdy otrzymał ~~ack~~ na każdą wysłaną wiadomość. Proces jest pasywny od czasu ~~\tau_i^k~~, gdy poprzednio wysłał ~~ack~~ (bo ~~contPassive~~ w ~~reply~~ musi równy true, więc i ~~contPassive_i~~ musi być równy true), a więc od chwili ~~\tau_i^k~~ do ~~\tau_i^{k+1}~~ nie wysyłał nowych wiadomości.
Bezpieczeństwo
Jeżeli ~~k+1~~-szy cykl algorytm zakończył się wykryciem zakończenia, to przetwarzanie faktycznie uległo zakończeniu przed końcem ~~k+1~~-szym cyklem.
Proces mógł wysłać ~~reply~~ w chwili ~~\tau_i^{k}~~ tylko, gdy otrzymał ~~ack~~ na każdą wysłaną wiadomość. Proces jest pasywny od czasu ~~\tau_i^k~~, gdy poprzednio wysłał ~~ack~~ (bo ~~contPassive~~ w ~~reply~~ musi równy true, więc i ~~contPassive_i~~ musi być równy true), a więc od chwili ~~\tau_i^k~~ do ~~\tau_i^{k+1}~~ nie wysyłał nowych wiadomości.
Pewien proces ~~P_j~~ mógłby wysłać wiadomość do ~~P_j~~ przed ~~\tau_i^{k+1}~~, gdyby ~~\tau_j^{k+1} < \tau_i^{k+j}~~ , i gdyby uaktywniła go wiadomość od procesu ~~P_l~~, dla którego ~~\tau_l^{k+1} < \tau_j^{k+j}~~ , który z kolei musiałby dostać wiadomość od innego procesu ... W ten sposób dotrzemy do jakiegoś procesu ~~P_m~~ o najmniejszym ~~\tau_m^{k+1}~~, którego już nie ma kto uaktywnić (bo kanały do niego na pewno są puste).
Skoro więc ~~\tau_i^k \lt \tau^x \lt \tau_i^{k+1}~~, to ~~IT_i~~ było wtedy równe ~~\emptyset~~ (kanały w chwili ~~\tau^x~~ do są puste) (C2).
Bezpieczeństwo
Jeżeli ~~k+1~~-szy cykl algorytm zakończył się wykryciem zakończenia, to przetwarzanie faktycznie uległo zakończeniu przed końcem ~~k+1~~-szym cyklem.
Proces mógł wysłać ~~reply~~ w chwili ~~\tau_i^k~~ dopiero, gdy zaszło ~~\neg activate(AV_i)~~. Skoro kanały są puste od ~~\tau_i^k~~ do ~~\tau_i^{k+1}~~, to do żadnego procesu nie mogą dotrzeć nowe wiadomości, a więc ~~AV_i~~ w żadnym procesie ~~P_i~~ nie ulegnie zmianie w tym przedziale czasu.
Skoro więc ~~\tau_i^k \lt \tau^x \lt \tau_i^{k+1}~~, to ~~activate(AV_i)~~ w chwili ~~\tau^x~~ jest równe false (C3).
Udowodniliśmy wszystkie trzy składniki zakończenia statycznego, a więc jeżeli wykryliśmy zakończenie w chwili ~~\tau_e^{k+1}~~, to w jakiejś chwili ~~\tau^x \lt \tau_i^{k+1}~~ faktycznie zaszło zakończenie statyczne.
Jak przy detekcji zakończenia statycznego, łączymy procesy w wirtualną gwiazdę. Inicjator okresowo sprawdza, czy wszystkie procesy są pasywne i czy wszystkie wysłane przez nie wiadomości zostały już odebrane.
Naszym celem jest wyznaczenie następującego predykatu: $$ Dterm({\boldsymbol {\mathcal {P}}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land \neg activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i}))$$
message $query$ is a struct $\left\langle \mbox{ array of int } vSentNo \right\rangle$
message $reply$ is a struct $\left\langle \mbox{ array of int } vSentNo, \mbox{bool } contPassive \right\rangle$
local array of int ~~sentNo_i~~ := ~~0~~
local array of int ~~recvNo_i~~ := ~~0~~
local array of array of int ~~tSentNo_i~~ := ~~0~~
local bool ~~contPassive_i~~ := true
local set of processId ~~AIT_i~~ := ~~\emptyset~~
local set of processId ~~AV_i~~ := ~~\emptyset~~
when ~~{P}_{\alpha}~~ wants to start termination detection
repeat
local bool dTermDetected := true
for all ~~P_j~~ in ~~\mathcal{ P }~~ do
~~query.vSentNo~~ := ~~tSentNo_{\alpha}[*,j]~~
send ~~query~~ to ~~P_j~~
end for
for all ~~P_j~~ in ~~\mathcal{ P }~~ do
receive ~~reply~~ from ~~P_j~~
~~tSentNo_{\alpha}[j]~~ := ~~reply.vSentNo~~
~~sTermDetected~~ := ~~sTermDetected \land reply.contPassive~~
end for
until sTermDetected = true
decide "termination detected"
end when
when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
~~vSentNo_i[j]~~ := ~~vSentNo_i[j]~~ + 1
send ~~m~~ to ~~P_j~~
end when
when a message ~~m~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
~~vRecvNo_i[j]~~ := ~~vRecvNo[j]~~ + 1
deliver ~~m~~
end when
when a process ~~P_i~~ activates do
~~contPassive_i~~ := false
end when
when a message ~~query~~ arrives at process ~~P_i~~ from ~~{P}_{\alpha}~~ do
~~AIT_i~~ := ~~\left\{ P_j : query.vSentoNo[j] \gt vRecvNo_i[j]\right\}~~
~~reply.contPassive~~ := ~~contPassive_i \land \neg activate\left( AV_i \cup AIT_i \right)~~
~~reply.vSentNo~~ := ~~vSentNo_i~~
~~contPassive_i~~ := ~~passive_i~~
send ~~reply~~ to ~~P_{\alpha}~~
end when
Wykrywa szybciej zakończenie, ale ma większe wiadomości.
Postęp
Jeżeli przetwarzanie zakończyło się w przed rozpoczęciem ~~k~~-tego cyklu algorytmu, to algorytm w skończonym czasie wykryje zakończenie.
Oznaczmy przez ~~\tau^t~~ czas, w którym przetwarzanie się zakończyło, zaś przez ~~\tau_b^k~~ czas, w którym zaczął się ~~k~~-ty cykl algorytmu, zaś przez ~~\tau_i^k~~ czas, w którym proces ~~P_i~~ wysłał ~~reply~~ w ~~k~~-tym cyklu.
Postęp
Skoro kanały są niezawodne, to wszystkie wiadomości w skończonym czasie dotrą do adresatów (1), a więc wiadomości ~~query~~ oraz ~~reply~~ wysłane ostatecznie dotrą do adresatów. Procesy nigdy nie wstrzymują ~~reply~~, a więc inicjator ~~P_{\alpha}~~ ostatecznie otrzyma ~~reply~~ od wszystkich procesów. Pytanie tylko, czy ~~reply.contPassive~~ będzie true w każdej odpowiedzi ~~reply~~?
Zakończenie zaszło w chwili ~~\tau^{t} \lt \tau_b^k~~, procesy są pasywne i nie będą uaktywnione. A więc dla każdego ~~\tau^x \geq \tau^t~~, zachodzi $$ Dterm({\boldsymbol {\mathcal {P}}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land \neg activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{i}))$$
Postęp
Skoro procesy są pasywne od chwili ~~\tau^t \lt \tau_b^k~~, to zmiennym ~~contPassive_i~~ w każdym ~~P_i~~ zostanie nadana wartość true najpóźniej w ~~k~~-tym cyklu i już się nie zmienią.
Zarazem wiemy, że inicjator w ~~k~~-tym cyklu odbierze od każdego procesu wartości ~~vSentNo_i~~, które już się nie zmienią. Zmienić się się mogą co najwyżej wartości ~~vRecvNo_i~~. Zbiór ~~AIT_i~~ może się więc tylko zmniejszać, a procesy z niego mogą przechodzić do zbioru ~~AV_i~~ lub znikać.
Postęp
Skoro tak, to ~~AIT_i(\tau_b^{k+1}) \subseteq IT_i(\tau^t)~~, a więc skoro ~~\neg activate_i(IT_i(\tau^t))~~ to i ~~\neg activate_i(AIT_i(\tau_i^{k+1}))~~. Analogicznie możemy rozumować dla ~~AV_i(\tau^t)~~ i ~~AV_i(\tau_i^{k+1})~~
Niech ~~X~~ to będą procesy, które przeszły ze zbioru ~~IT_i(\tau^t)~~ do ~~AV_i~~. Skoro ~~\neg activate_i(X)~~ gdy ~~X\subset IT_i~~, to i ~~\neg activate_i(X)~~ gdy ~~X\subset AV_i(\tau_i^{k+1})~~.
Wnioskujemy z tego, że w chwili ~~\tau_i^{k+1}~~ dla każdego ~~P_i~~ zajdzie: $$contPassive_i \land \neg activate_i( AIT_i \cup AV_i)$$
Postęp
Skoro tak, to ~~AIT_i(\tau_b^{k+1}) \subseteq IT_i(\tau^t)~~, a więc skoro ~~\neg activate_i(IT_i(\tau^t))~~ to i ~~\neg activate_i(AIT_i(\tau_i^{k+1}))~~. Analogicznie możemy rozumować dla ~~AV_i(\tau^t)~~ i ~~AV_i(\tau_i^{k+1})~~
Niech ~~X~~ to będą procesy, które przeszły ze zbioru ~~IT_i(\tau^t)~~ do ~~AV_i~~. Skoro ~~\neg activate_i(X)~~ gdy ~~X\subset IT_i~~, to i ~~\neg activate_i(X)~~ gdy ~~X\subset AV_i(\tau_i^{k+1})~~.
Wnioskujemy z tego, że w chwili ~~\tau_i^{k+1}~~ dla każdego ~~P_i~~ zajdzie: $$contPassive_i \land \neg activate_i( AIT_i \cup AV_i)$$
Skoro tak, dla każdej wiadomości ~~reply~~ wysłanej w ~~k+1~~ cykly ~~reply.contPassive~~ będzie równe true, a więc inicjator zakończy się wykrywając zakończenie (c.b.d.u).
Bezpieczeństwo
Jeżeli algorytm stwierdził, że przetwarzanie zakończyło się, to rzeczywiście przetwarzanie jest w stanie zakończenia dynamicznego.
Pokażemy, że zakończenie dynamiczne zachodzi w pewnej chwili ~~\tau^x~~, gdzie ~~\tau_b^{k}\lt\tau_e^{k}\leq\tau^x\leq\tau_b^{k+1}\leq\tau_e^{k+1}~~
Założenie Algorytm zakończył się w ~~\tau_e^{k+1}~~, otrzymując od każdego procesu ~~P_i~~ wiadomość ~~reply~~ z polem ~~reply.contPassive~~ równym true
Bezpieczeństwo
Skoro dla każdego ~~reply~~ wysłanego w ~~k+1~~ cyklu przez ~~P_i~~, ~~reply.contPassive~~ jest równe true, to proces ~~P_i~~ musiał być pasywny w cyklu ~~k~~-tym, gdy zmiennej tej nadano wartość i nie był uaktywniony. A więc od ~~\tau_i^k~~ do ~~\tau_i^{k+1}~~, a więc i w każdej chwili ~~\tau^x~~ w tym okresie, zachodziło ~~passive_i~~ dla każdego procesu (C1)
Bezpieczeństwo
Skoro dla każdego ~~reply~~ wysłanego w ~~k+1~~ cyklu przez ~~P_i~~, ~~reply.contPassive~~ jest równe true, to dla ~~P_i~~ musiało być spełnione ~~\neg activate_i(AIT_i \cup AV_i)~~ w chwili ~~\tau_i^{k+1}~~. Skoro ustaliliśmy, że od ~~\tau_i^{k}~~ wszystkie procesy były pasywne, to zachodzi:
~~AV_i(\tau_x)\subseteq AV_i(\tau_i^{k+1})~~
~~vSentNo_i[j](\tau_x) = vSentNo_i[j](\tau_i^{k+1})~~
Bezpieczeństwo
Wyznaczając zbiór ~~AV_i~~ proces bierze pod uwagę te procesy ~~P_j~~, dla których ~~vSentNo_i[j]\gt vRecvNo_i[j]~~. Skoro ~~vSentNo_i~~ nie zmienił się od poprzedniego cyklu, a ~~vRecvNo_i[j]~~ może tylko rosnąć, to ~~IT_i(\tau^x) \subseteq (AIT_i\cup AV_i)(\tau_i^{k+1})~~ A skoro tak, to jeżeli ~~\neg activate_i((AIT_i\cup AV_i)(\tau_i^{k+1}))~~, to i ~~\neg activate_i(IT_i)(\tau^{x}))~~.
Z kolei wiadomości od procesów ~~X \subset AV_i(\tau^x)~~ jeżeli zostały dostarczone, to nie uaktywniły procesu, a więc nie mógł być spełniony dla tych procesów warunek ~~activate_i~~ w chwili ~~\tau^x~~. Z kolei jeżeli nie zostały dostarczone, to są wciąż w ~~AV_i~~ w chwili ~~\tau_i^{k+1}~~ i nie jest spełniony dla nich warunek ~~activate_i~~, a więc i nie mógł być spełniony wcześniej w ~~\tau^x~~.
Bezpieczeństwo
Wyznaczając zbiór ~~AIT_i~~ proces bierze pod uwagę te procesy ~~P_j~~, dla których ~~vSentNo_i[j]\gt vRecvNo_i[j]~~. Skoro ~~vSentNo_i~~ nie zmienił się od poprzedniego cyklu, a ~~vRecvNo_i[j]~~ może tylko rosnąć, to ~~IT_i(\tau^x) \subseteq (AIT_i\cup AV_i)(\tau_i^{k+1})~~ A skoro tak, to jeżeli ~~\neg activate_i((AIT_i\cup AV_i)(\tau_i^{k+1}))~~, to i ~~\neg activate_i(IT_i)(\tau^{x}))~~.
Z kolei wiadomości od procesów ~~X \subset AV_i(\tau^x)~~ jeżeli zostały dostarczone, to nie uaktywniły procesu, a więc nie mógł być spełniony dla tych procesów warunek ~~activate_i~~ w chwili ~~\tau^x~~. Z kolei jeżeli nie zostały dostarczone, to są wciąż w ~~AV_i~~ w chwili ~~\tau_i^{k+1}~~ i nie jest spełniony dla nich warunek ~~activate_i~~, a więc i nie mógł być spełniony wcześniej w ~~\tau^x~~.
Jeżeli ~~\neg activate_i(X)~~ oraz ~~\neg activate_i(Y)~~, to i ~~\neg activate_i(X\cup Y)~~. Wynika z tego, że skoro w chwili ~~\tau^x~~ zachodzić musiało ~~\neg activate_i(AV_i)~~ oraz ~~\neg activate_i(IT_i)~~ a więc i ~~\neg activate_i(AV_i\cup IT_i)~~.
Bezpieczeństwo
Podsumowując - udowodniliśmy że jeżeli algorytm się zakończył wykrywając zakończenie, to istniała chwila ~~\tau^x~~ przed zakończeniem algorytmu, taka że w tej chwili zachodziło dla każdego procesu ~~P_i~~ $$passive_i \land \neg activate_i(AV_i\cup IT_i)$$ c.b.d.u
Dowód poprawności na wykładzie powtórkowym.
enum color = { white, red }
message $token$ is a struct $\left\langle \mbox{int } nb \right\rangle$
local enum color procColor_i := white
local set of channels ~~channelCycle~~
local function ~~succ_i~~
local bool ~~tokenPresent_i~~ := false
when ~~{P}_{\alpha}~~ wants to start termination detection
~~token.nb~~ := 0
send ~~token~~ to ~~succ_{\alpha}~~
end when
when a message ~~m~~ arrives at ~~{P}_{i}~~ from ~~{P}_{j}~~ do
~~procColor_i~~ := red
~~passive_i~~ := false
deliver ~~m~~
end when
when a ~~token~~ arrives at ~~{P}_{i}~~ from ~~{P}_{j}~~ do
~~tokenPresent_i~~ := true
wait until ~~passive_i~~ = true
if ~~procColor_i~~ = red then
~~token.nb~~ := 0
else
~~token.nb~~ := ~~token.nb~~ + 1
end then
send ~~token~~ to ~~succ_i~~
~~tokenPresent_i~~ := false
~~procColor_i~~ := white
end when
when a ~~token~~ arrives at ~~{P}_{\alpha}~~ from ~~{P}_{j}~~ do
~~tokenPresent_i~~ := true
if ~~procColor_i~~ = white ~~\land\mbox{ }token.nb~~ = ~~\left|channelCycle\right|~~ then
decide termination detected
else
if ~~procColor_i~~ = red then
~~token.nb~~ := 0
else
~~token.nb~~ := ~~token.nb~~ + 1
end then
send ~~token~~ to ~~succ_i~~
~~procColor_i~~ := white
~~tokenPresent_i~~ := false
end then
end when
Te algorytmy nie zadziałają w innym modelu!
W domu - zastanowić się i udowodnić, dlaczego np jednofazowy algorytm z licznikami nie zadziała w modelu, w którym przetwarzanie nie jest natychmiastowe.