Przetwarzanie rozproszone

Detekcja zakończenia

dr inż. Arkadiusz Danilecki

W oparciu o wykłady prof. J. Brzezińskiego

Plan wykładu

  1. Algorytm detekcji zakończenia statycznego
  2. Algorytm detekcji zakończenia dynamicznego
  3. Algorytm Misra'83

Algorytm 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.

Algorytm detekcji zakończenia statycznego


				    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~~
				    

Algorytm detekcji zakończenia statycznego


				    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
				    

Algorytm detekcji zakończenia statycznego


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
				    

Algorytm detekcji zakończenia statycznego


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
				    

Algorytm detekcji zakończenia statycznego

  • Złożoność czasowa 4 (lub 2, jeżeli procesy nie były aktywowane - pomijając cykl bieżący)
  • Złożoność komunikacyjna 4*n (lub 2*n, jw i pomijając cykl bieżący) oraz dodatkowe wiadomości ~~ack~~

Dowód poprawności

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 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.

Dowód poprawności

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).

Dowód poprawnoś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.

$${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}))}$$

Dowód poprawności

Oznaczenia

  • ~~\tau_b^k~~ - czas rozpoczęcia ~~k~~-tego cyklu detekcji
  • ~~\tau_i^k~~ - czas wysłania ~~reply~~ przez ~~P_i~~ w ~~k~~-tym cyklu detekcji
  • ~~\tau_e^k~~ - czas zakończenia ~~k~~-tego cyklu detekcji

Oczywiście ~~\tau_b^k \lt \tau_i^k \lt \tau_e^k~~

Dowód poprawnoś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.

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).

Dowód poprawnoś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.

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.

Dowód poprawnoś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).

Dowód poprawnoś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~~ 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.

Algorytm detekcji zakończenia dynamicznego

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}))$$

Algorytm detekcji zakończenia dynamicznego


				    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~~
				    

Algorytm detekcji zakończenia dynamicznego


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
				    

Algorytm detekcji zakończenia dynamicznego


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
				    

Algorytm detekcji zakończenia statycznego


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

				    

Algorytm detekcji zakończenia dynamicznego

  • Złożoność czasowa 4 (2 cykle)
  • Złożoność komunikacyjna 4*n, bez dodatkowych wiadomości ~~ack~~

Wykrywa szybciej zakończenie, ale ma większe wiadomości.

Dowód poprawnoś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.

Dowód poprawności

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 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}))$$

Dowód poprawności

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ć.

Dowód poprawności

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)$$

Dowód poprawności

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).

Dowód poprawności

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

Dowód poprawności

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)

Dowód poprawności

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})~~

Dowód poprawności

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~~.

Dowód poprawności

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)~~.

Dowód poprawności

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

Rozwiązanie uniwersalne?

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)

  • żadnych założeń co do topologii przetwarzania
  • brak założeń co do czasu przesyłania.
  • niezawodne kanały FIFO
  • musi być dany z góry cykl ~~channelCycle~~ obejmujący wszystkie kanały

Dowód poprawności na wykładzie powtórkowym.

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)


				    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
				    

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)


				    when ~~{P}_{\alpha}~~ wants to start termination detection
				       ~~token.nb~~ := 0

				       send ~~token~~ to ~~succ_{\alpha}~~
				    end when
				    

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)


when a message ~~m~~ arrives at ~~{P}_{i}~~ from ~~{P}_{j}~~ do
	~~procColor_i~~ := red 
	~~passive_i~~ := false 

	deliver ~~m~~
end when
				    

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)


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
				    

Detekcja zakończenia dla modelu asynchronicznego (Misra'83)


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
				    

Podsumowanie

  • Dijkstra, Feijen, van Gasteren - dla modelu synchronicznego
  • Algorytmy z licznikami - dla modelu atomowego
  • 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.

  • Misra'3 - uniwersalny
  • Algorytm dla zakończenia statycznego - dodatkowe wiadomości