Przetwarzanie rozproszone

Detekcja zakończenia

dr inż. Arkadiusz Danilecki

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

Plan wykładu

  1. Algorytmy dla modelu atomowego
  2. Algorytm detekcji zakończenia statycznego
  3. Algorytm detekcji zakończenia dynamicznego
  4. Algorytm Misra'83

Model atomowy

Detekcja zakończenia dla modelu atomowego

W atomowym modelu przetwarzania, czasy przetwarzania lokalnego są zaniedbywalne (zerowe), a opóźnienia są związane tylko z transmisją.

Można przyjąć, że procesy (uaktywniane natychmiastowo) są przez cały czas pasywne i sprowadzić problem detekcji zakończenia do wyznaczania stanów kanałów. Przyjmijmy dla uproszczenia, że dowolna wiadomość w kanale uaktywni proces.

Wówczas zakończenie przetwarzania opisuje następujący predykat: $$Aterm({\mathcal {P}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::({\mathcal {IT}}_{i}=\emptyset )$$

Detekcja zakończenia dla modelu atomowego

W takim modelu wystarczy sprawdzić, czy kanały są puste. Kanały są puste, jeżeli wszystkie wiadomości wysłane są odebrane
  • $sc_{i}(\tau )$ – liczba wiadomości wysłanych do chwili $\tau$ przez $P_i$
  • $rc_{i}(\tau )$ – liczba wiadomości odebranych do chwili $\tau$ przez $P_i$
  • $SC(\tau )$ – sumaryczna liczba wiadomości wysłanych przez wszystkie procesy przetwarzania rozproszonego do chwili $\tau$
  • $RC(\tau )$ – sumaryczna liczba wiadomości odebranych przez wszystkie procesy przetwarzania rozproszonego do chwili $\tau$

Detekcja zakończenia dla modelu atomowego

Teoretycznie wystarczy sprawdzić, czy $RC(\tau) = SC(\tau)$. Proste! ... Proste?

  • $sc_{i}(\tau )$ – liczba wiadomości wysłanych do chwili $\tau$ przez $P_i$
  • $rc_{i}(\tau )$ – liczba wiadomości odebranych do chwili $\tau$ przez $P_i$
  • $SC(\tau )$ – sumaryczna liczba wiadomości wysłanych przez wszystkie procesy przetwarzania rozproszonego do chwili $\tau$
  • $RC(\tau )$ – sumaryczna liczba wiadomości odebranych przez wszystkie procesy przetwarzania rozproszonego do chwili $\tau$

Algorytm z licznikami

Łączymy procesy w wirtualny pierścień i przesyłamy między nimi znacznik. Każdy proces po otrzymaniu znacznika dodaje do niego swoje liczniki $sc_i$ oraz $rc_i$.

Problem polega na tym, że zebrane liczniki pochodzą z różnych momentów $\tau _{i}$, $1\leq i\leq n$

Algorytm z licznikami

Oznaczmy przez ${SC^{*}}$ i ${RC^{*}}$ odpowiednio sumy zebranych przez znacznik liczników, a więc:

${SC^{*}=\sum _i^n sc_{i}(\tau _{i})}$, ${RC^{*}=\sum _i^n rc_{i}(\tau _{i})}$

pamiętając, że:

$SC(\tau )=sc_{i}(\tau )$, $RC(\tau )=rc_{i}(\tau )$

Różnica - w pierwszym wypadku różne chwile, w drugim ta sama chwila

Przykład wyznaczania liczników

Dwufazowy algorytm z licznikami

A gdybyśmy tak przesłali token dwukrotnie i dopiero wtedy sprawdzali, czy liczniki są równe?

W algorytmie detekcji zakończenia będą dwie fazy detekcji. Pierwsza rozpoczyna się o chwili $\tau _{b}^{1}$ i kończy w chwili $\tau _{e}^{1}$, a druga odpowiednio w chwilach $\tau _{b}^{2}$ i $\tau _{e}^{2}$. Przyjęto ponadto, że: $\tau _{b}^{1}<\tau _{e}^{1}<\tau _{b}^{2}<\tau _{e}^{2}$

Oznaczmy teraz przez $SC^{*}$ i $RC^{*}$ liczniki wyznaczone w pierwszej fazie, a przez $SC^{**}$ i $RC^{**}$ liczniki oznaczone w drugiej fazie.

Dwufazowy algorytm z licznikami

Jeżeli $$RC^{*}=SC^{*}=RC^{**}=SC^{**}$$ to monitorowane przetwarzanie aplikacyjne osiągnęło stan zakończenia przed zakończeniem procesu detekcji.

Dowód

Lemat 10.1.1

Lokalne liczniki wiadomości są monotoniczne. Tak więc, jeżeli $\tau \leq \tau \prime$, to $sc_{i}(\tau )\leq sc_{i}(\tau \prime )$ i $rc_{i}(\tau )\leq rc_{i}(\tau \prime )$.

Lemat 10.1.2

Sumaryczna liczba wiadomości wysłanych lub odebranych jest monotoniczna. Jeżeli zatem $\tau \leq \tau \prime$, to $SC(\tau )\leq SC(\tau \prime )$ i $RC(\tau )\leq RC(\tau \prime )$.

Dowód

Lemat 10.1.3

$$RC^{*}\leq RC(\tau _{e}^{1})$$

Dowód: Licznik $RC^{*}$ z definicją jest sumą zebranych liczników $rc_{i}(\tau _{i})$, przy czym dla każdego $i\in \{1,2,\ldots ,n\}$, $\tau _{b}^{1}\leq \tau _{i}\leq \tau _{e}^{1}$.

Z kolei, $RC(\tau _{e}^{1})$ jest sumą liczników $rc_{i}(\tau _{e}^{1})$

Dowód

Lemat 10.1.3

Dowód: Licznik $RC^{*}$ z definicją jest sumą zebranych liczników $rc_{i}(\tau _{i})$, przy czym dla każdego $i\in \{1,2,\ldots ,n\}$, $\tau _{b}^{1}\leq \tau _{i}\leq \tau _{e}^{1}$.

Z kolei, $RC(\tau _{e}^{1})$ jest sumą liczników $rc_{i}(\tau _{e}^{1})$

Ponieważ liczniki są monotoniczne i dla każdego $i\in \{1,2,...,n\}:\tau _{i}\leq \tau _{e}^{1}$, więc tym samym $rc_{i}(\tau _i)\leq rc_{i}(\tau _{e}^{1})$ dla każdego $i$, a w konsekwencji:

$$RC^{*}\leq RC(\tau _{e}^{1})$$

Dowód

Lemat 10.1.4

$$SC^{**}\geq SC(\tau _{b}^{2})$$

Dowód: Z definicji, $SC^{**}$ jest sumą liczników $sc_{i}(\tau _i)$, przy czym dla każdego $i\in \{1,2,...,n\},\tau _{b}^{2}\leq \tau _{i}\leq \tau _{e}^{2}$.

Z kolei, $SC(\tau _{b}^{2})$ jest sumą liczników $sc_{i}(\tau _{b}^{2})$.

Dowód

Lemat 10.1.4

Dowód: Z definicji, $SC^{**}$ jest sumą liczników $sc_{i}(\tau i)$, przy czym dla każdego $i\in \{1,2,...,n\},\tau _{b}^{2}\leq \tau _{i}\leq \tau _{e}^{2}$.

Z kolei, $SC(\tau _{b}^{2})$ jest sumą liczników $sc_{i}(\tau _{b}^{2})$.

Ponieważ liczniki są monotoniczne i dla każdego $i\in \{1,2,...,n\}$, $ \tau _{b}^{2}\leq \tau _{i}$, więc tym samym $sc_{i}(\tau _{b}^{2})\leq sc_{i}(\tau _{i})$ dla każdego $i$, a w konsekwencji:

$$SC^{**}\geq SC(\tau _{b}^{2})$$

Dowód

Lemat 10.1.5

Dla wszystkich $\tau :RC(\tau )\leq SC(\tau )$

Dowód: Kanały są niezawodne, więc...

Dowód

Dla przypomnienia, próbujemy udowodnić, że jeżeli algorytm się zakończył i wyszło $RC^{*}=SC^{**}$, to istnieje taka chwila $\tau$, że $RC(\tau) = SC(\tau)$.

... Pamiętamy, co to będzie znaczyć, prawda?

Dowód

Z założenia wynika, że:

$$RC^{*}=SC^{**}$$

Z kolei z przedstawionych lematów otrzymujemy, że:

  • $SC^{**}\geq SC(\tau _{b}^{2})$ (lemat 10.1.4)
  • $SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})$ (lemat 10.1.2)
  • $SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1})$ (lemat 10.1.5)
  • $RC(\tau _{e}^{1})\geq RC^{*}$ (lemat 10.1.3)

$$SC^{**}\geq SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1})\geq RC^{*}$$

Dowód

$$RC^{*}=SC^{**}$$

$$SC^{**}\geq SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1})\geq RC^{*}$$

$$SC^{**} = SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1}) = RC^{*}$$

Dowód

$$RC^{*}=SC^{**}$$

$$SC^{**}\geq SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1})\geq RC^{*}$$

$$SC^{**} = SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1}) = RC^{*}$$

$$SC^{**} = SC(\tau _{b}^{2}) = SC(\tau _{e}^{1}) = RC(\tau _{e}^{1}) = RC^{*}$$

$$SC(\tau _{e}^{1}) = RC(\tau _{e}^{1})$$

C.B.D.U

Detekcja w jednym cyklu?

Łączymy procesy w wirtualny pierścień i przesyłamy pierścień kumulujący różnice między lokalnymi licznikami.

... ale dodatkowo wykrywamy, czy na tej podstawie możemy wnioskować, czy faktycznie kanały są puste i zaszło zakończenie. Jak?

SPRYTNIE

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


				    message $token$ is a struct $\left\langle \mbox{int } detectNo, \mbox{int } accu, \mbox{bool } invalid \right\rangle$
				    message $m$ is a struct $\left\langle \mbox{int } detectNo, \mbox{data } appdata \right\rangle$

				    local int ~~accu_i~~ := 0
				    local int ~~detectNo_i~~ := 0
				    local int ~~maxDetectNo_i~~ := 0
				    local function ~~succ_i~~

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


				    when ~~{P}_{\alpha}~~ wants to start termination detection
				       ~~detectNo_i~~ := ~~detectNo_{\alpha}~~ + 1
				       ~~token.invalid~~ := false    
				       ~~token.detectNo~~ := ~~detectNo_{\alpha}~~    
				       ~~token.accu~~ := ~~accu_{\alpha}~~    

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

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
    ~~accu_i~~ := ~~accu_i~~ + 1 
    ~~m.detectNo~~ := ~~detectNo_i~~ 
    send ~~m~~ to ~~P_j~~
end when

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


when a message ~~m~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
    ~~accu_i~~ := ~~accu_i~~ - 1 
    ~~maxDetectNo_i~~ := max(~~m.detectNo~~, ~~maxDetectNo_i~~) 
    deliver ~~m~~ 
end when

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


when a ~~token~~ arrives at process ~~P_{i\neq\alpha}~~ from ~~{P}_{j}~~ do
    ~~detectNo_{i}~~ := max(~~m.detectNo~~, ~~detectNo_{i}~~) 
    ~~token.detectNo~~ := ~~detectNo_{i}~~    
    ~~token.accu~~ := ~~token.accu~~ + ~~accu_{i}~~    
    ~~token.invalid~~ := ~~token.invalid \lor \left(maxDetectNo_{i}\geq token.detectNo\right)~~    
    send ~~token~~ to ~~succ_{i}~~
end when

Jednofazowy alg. detekcji zakończenia dla modelu atomowego 


when a ~~token~~ arrives at process ~~P_{\alpha}~~ from ~~{P}_{j}~~ do
    ~~detectNo_{\alpha}~~ := max(~~m.detectNo~~, ~~detectNo_{\alpha}~~) 
    if ~~token.accu~~ = 0 ~~\land \neg token.invalid~~ then 
    	decide termination is detected
    else 
    	~~detectNo_{\alpha}~~ := ~~detectNo_{\alpha}~~ + 1 
    	~~token.invalid~~ := false    
    	~~token.detectNo~~ := ~~detectNo_{\alpha}~~    
    	~~token.accu~~ := ~~accu_{\alpha}~~    

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

Kiedy token będzie unieważniony?

Złożoność czasowa i komunikacyjna

  • Złożoność czasowa n
  • Złożoność komunikacyjna n

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

Wektorowy algorytm detekcji zakończenia

Bardzo podobny jak poprzednio: łączymy procesy w wirtualny pierścień i przesyłamy w pierścień token zbierający informacje, ile wiadomości potencjalnie może jeszcze podróżować do i-tego procesu. Token jest wstrzymywany, jeżeli dany proces zauważa, że istnieją jakieś wiadomości, których jeszcze nie odebrał.

Wektorowy algorytm detekcji zakończenia


				    message $token$ is a struct $\left\langle \mbox{array of int } vAccu \right\rangle$

				    local int ~~vNo_i[1 \ldots n]~~ := ~~\left\{0,\ldots,0\right\}~~
				    local bool ~~firstWave_i~~ := true
				    local function ~~succ_i~~

Wektorowy algorytm detekcji zakończenia


				    when ~~{P}_{\alpha}~~ wants to start termination detection
				       ~~token.vAccu[\ldots]~~ := ~~\left\{ 0 \ldots 0 \right\}~~
				       ~~firstwave_{\alpha}~~ := false

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

Wektorowy algorytm detekcji zakończenia


when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
    ~~vNo_i[j]~~ := ~~vNo_i[j]~~ + 1 
    send ~~m~~ to ~~P_j~~
end when

Wektorowy algorytm detekcji zakończenia


when a ~~token~~ arrives at process ~~P_{i}~~ from ~~{P}_{j}~~ do
    ~~vNo_{i}~~ := ~~vNo_i + token.vAccu~~
    if ~~vNo_i[i] \leq~~ 0 then
        if ~~\forall k :: k\in\left\{1\ldots n\right\} :: vNo_i[k] = \mbox{ 0} \land \neg firstWave_i~~ then
            decide termination is detected
        else 
            ~~token.vAccu~~ := ~~vNo_i~~
            send ~~token~~ to ~~succ_{i}~~
            ~~vNo_i~~ := ~~\left\{ 0 \ldots 0 \right\}~~
            ~~firstwave_{i}~~ := false
        end if
    end if
end when

Wektorowy algorytm detekcji zakończenia


when a message ~~m~~ arrives at process ~~P_{i}~~ from ~~{P}_{j}~~ do
    ~~vNo_{i}[i]~~ := ~~vNo_i[i]~~ - 1
    deliver ~~m~~

    if ~~vNo_i[i]~~ = 0 then
        if ~~\forall k :: k\in\left\{1\ldots n\right\} :: vNo_i[k] = \mbox{ 0} \land \neg firstWave_i~~ then
            decide termination is detected
        else 
            ~~token.vAccu~~ := ~~vNo_i~~
            send ~~token~~ to ~~succ_{i}~~
            ~~vNo_i~~ := ~~\left\{ 0 \ldots 0 \right\}~~
            ~~firstwave_{i}~~ := false
        end if
    end if
end when