Przetwarzanie rozproszone

Detekcja zakończenia

dr inż. Arkadiusz Danilecki

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

Plan wykładu

  1. Wprowadzenie
  2. Definicje
  3. Algorytmy dla przetwarzania dyfuzyjnego
  4. Algorytm Dijkstra, Feijen, van Gasteren
  5. Algorytmy dla modelu atomowego
  6. Algorytm detekcji zakończenia statycznego
  7. Algorytm detekcji zakończenia dynamicznego
  8. Algorytm Misra'83

Przypomnienie

$\Pi , \Sigma^i, \Sigma(\tau)$ - Proces globalny, $i$-ty stan globalny, stan globalny w chwili $\tau$ czasu globalnego

$P_i$ - $i$-ty proces

$S_i$ - stan $i$-tego procesu

$E_i^k$ - $k$-te zdarzenie w $i$-tym procesie

$C_{i,j} \in \mathcal{C}$ - kanał od $P_i$ do $P_j$

$\mathcal{P}, \mathcal{S}, \mathcal{T}, \mathcal{E}$ - zbiory elementów

Co właściwie nas interesuje?

Co właściwie nas interesuje?

Czy przetwarzanie rozproszone osiągnęło swój cel? Czy algorytm się zakończył? Czy jest jeszcze jakiś proces, który kontynuuje pracę?

Jak zawsze w środowisku rozproszonym, problem nie jest trywialny. Odpytanie po kolei procesów "czy już skończyliście pracę" może skutkować błędnym przeświadczeniem, że przetwarzanie się zakończyło.

Co właściwie nas interesuje?

Jak zawsze w środowisku rozproszonym, problem nie jest trywialny. Odpytanie po kolei procesów "czy już skończyliście pracę" może skutkować błędnym przeświadczeniem, że przetwarzanie się zakończyło.

A dlaczego właściwie nie wyznaczyć spójnego obrazu stanu globalnego?

"Czy zaszło zakończenie" jest predykatem stabilnym, więc jak najbardziej można!

Specjalizowane algorytmy bywają czasami wydatniejsze... A poza tym problem jest ciekawy sam w sobie

Definicja nieformalna

Nieformalnie problem detekcji zakończenia przetwarzania rozproszonego polega na sprawdzeniu, czy wszystkie procesy przetwarzania są w stanie pasywnym oraz czy żadna wiadomość będąca w kanale (transmitowana lub dostępna) nie uaktywni któregokolwiek z tych procesów.

Definicja nieformalna

Nieformalnie problem detekcji zakończenia przetwarzania rozproszonego polega na sprawdzeniu, czy wszystkie procesy przetwarzania są wstanie pasywnym oraz czy żadna wiadomość będąca w kanale (transmitowana lub dostępna) nie uaktywni któregokolwiek z tych procesów.

Przez proces aktywny rozumiemy tutaj wykonujący kroki algorytmu; w przeciwnym wypadku uznajemy go za pasywny.

Przez zakończenie obliczeń rozproszonych mamy tutaj na myśli osiągnięcie pewnej końcowej konfiguracji, w której nie są już możliwe dalsze kroki algorytmu.

Definicja nieformalna

Przez proces aktywny rozumiemy tutaj wykonujący kroki algorytmu; w przeciwnym wypadku uznajemy go za pasywny.

Zakładamy, że proces aktywny może spontanicznie w każdej chwili stać się pasywny. Proces pasywny może być uaktywniony dopiero po otrzymaniu jednej lub więcej wiadomości.

Definicja formalna: oznaczenia

W sformułowaniu formalnym tego problemu wykorzystamy następujące oznaczenia:

  • $passive_{i}$ – zmienna logiczna (predykat) przyjmująca wartość True wtedy i tylko wtedy, gdy proces $P_{i}$ jest pasywny
  • $available_{i}$ – tablica [1..n ] zmiennych logicznych procesu $P_{i}$ skojarzona z wiadomościami dostępnymi
  • $available_{i}[j]$ – j-ty element tablicy $available_{i}$ przyjmujący wartość True, gdy dla $P_{i}$ jest dostępna wiadomość wysłana przez $P_{j}$

Definicja formalna: oznaczenia

  • ${in\mathrm {-} transit_{i}}$ – tablica [1..n ] zmiennych logicznych procesu $P_{i}$ skojarzona z wiadomościami transmitowanymi
  • $in\mathrm{-}transit_{i}[j]$ – j-ty element tablicy $in\mathrm {-} transit_{i}$ przyjmujący wartość True, gdy wiadomość wysłana przez $P_j$ do $P_i$ jest transmitowana i nie jest jeszcze dostępna

Oprócz tego przyjmiemy oznaczenie dwóch zbiorów procesów ${\mathcal {AV}}_{i}$ oraz ${\mathcal {IT}}_{i}$, zdefiniowanych w następujący sposób:

$${\mathcal {AV}}_{i}=\{P_{j}:available_{i}[j]=True\}$$ $${\mathcal {IT}}_{i}=\{P_{j}:in\mathrm {-} transit_{i}[j]=True\}$$

Definicja formalna: oznaczenia

Predykat ~~activate~~

  • $activate_i(\mathcal{X})$ – predykat przyjmujący wartość true, gdy dostarczenie wiadomości od procesów w zbiorze ~~\mathcal{X}~~ spowoduje uaktywnienie procesu.

Predykat ten jest monotoniczny; to znaczy: $$activate_i(\mathcal{X}) \land \mathcal{X} \subseteq \mathcal{Y} \Rightarrow activate_i(\mathcal{Y})$$

Definicja formalna: oznaczenia

Predykat ~~activate~~

Predykat ~~activate_i~~ określony na zbiorach ~~IT_i~~ oraz ~~AV_i~~ w pewnym sensie wybiega w przyszłość. Oczywiste jest, że jeżeli zachodziło $$activate_i(\mathcal{X})\land\mathcal{X} \subseteq \mathcal{IT_i}$$ to gdy wiadomości od procesów ze zbioru ~~\mathcal{X}~~ staną się dostępne (tj. ~~\mathcal{X} \subseteq\mathcal{AV_i}~~), to ~~activate_i(\mathcal{X})~~ dalej będzie prawdziwe. Analogicznie będzie dla relacji ~~\neg activate(\mathcal{X})~~

Zakończenie dynamiczne

Przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia dynamicznego, jeżeli żaden proces składowy przetwarzania rozproszonego nie będzie już nigdy uaktywniony. Stan ten będzie utrzymywany pomimo, że pewne wiadomości są wciąż transmitowane, a pewne wiadomości są już dostępne.

Zakończenie dynamiczne

Przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia dynamicznego, gdy spełniony jest predykat: $$ 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}))$$ Predykat ten oznacza, że żaden proces składowy przetwarzania rozproszonego nie będzie już nigdy uaktywniony. Stan ten będzie utrzymywany pomimo, że pewne wiadomości są wciąż transmitowane (${\mathcal {IT}}_{i}$), a pewne wiadomości są już dostępne (${\mathcal {AV}}_{i}$).

Jest to oczywiście predykat stabilny.

Zakończenie statyczne

Przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia statycznego, jeżeli:

  • wszystkie procesy są pasywne,
  • wszystkie wiadomości znajdujące się w kanałach są dostępne
  • dla żadnego procesu nie jest spełniony warunek uaktywnienia.

Zakończenie statyczne

Przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia statycznego, gdy spełniony jest predykat: $${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}))}$$

Zakończenie statyczne a dynamiczne

Niech $ \vartheta \leftrightsquigarrow \vartheta '$ oznacza, że zajście predykatu $ \vartheta$ prowadzi w skończonym, choć nieprzewidzianym czasie do zajścia predykatu ${\displaystyle \vartheta '}$. W takim razie:

$$Dterm({\mathcal {P}}) \leftrightsquigarrow Sterm({\mathcal {P}})$$

Zakończenie statyczne a dynamiczne

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

Zakończenie klasyczne

W klasycznej definicji zakończenia przyjmowano, że przetwarzanie rozproszone jest w stanie zakończenia, jeżeli w danej chwili wszystkie procesy są pasywne i wszystkie kanały są puste, awięc gdy zachodzi następujący predykat: $$Cterm({\mathcal {P}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land ({\mathcal {AV}}_{i}=\emptyset )\land ({\mathcal {IT}}_{i}=\emptyset )$$

Algorytmy detekcji zakończenia

Model przetwarzania dyfuzyjnego

Przetwarzanie dyfuzyjne (ang. diffusing computation) jest specyficznym przetwarzaniem rozproszonym, w którym wyróżnia się:

  • inicjatora (środowisko) – może w dowolnej chwili rozpocząć przetwarzanie dyfuzyjne wysyłając wiadomość aplikacyjną do jednego lub wielu procesów kooperujących (zakłada się, że inicjacja taka zachodzi tylko raz),
  • hierarchię kooperujących procesów, wykonujących zlecone zadania

Każdy proces po uzyskaniu pierwszej wiadomości aplikacyjnej, nadawcę tej wiadomości traktuje jako proces angażujący (ang. engager, controlling agent) i realizuje dalsze przetwarzanie wysyłając wiadomości do innych procesów, w tym ewentualnie do inicjatora.

Model przetwarzania dyfuzyjnego

Założenia dodatkowe

  • Proces zawsze staje się aktywny po otrzymaniu wiadomości
  • Otrzymanie wiadomości oznacza zlecenie pewnej pracy, proces po jej skończeniu zawsze odpowiada
  • Po zakończeniu wszystkich prac, proces zawsze staje się pasywny

Przedstawimy algorytm Dijkstry-Scholtena mocno zmodyfikowany i uproszczony na potrzeby prezentacji.

Algorytm Dijkstra-Scholten


				    message $signal$, $work$

				    local int ~~sentNo_i~~ := 0
				    local int ~~recvNo_i~~ := 0
				    local processId ~~engager_i~~ := 0
				    local set of ~~\left< \mbox{work}, \mbox{processId}\right>~~ ~~works_i~~ 
				    

Algorytm Dijkstra-Scholten


				    when ~~{P}_{\alpha}~~ wants to start computation
				       ~~\mathcal{P_{\alpha}^R}~~ := "processes initiator wants to engage"
				       ~~sentNo_{\alpha}~~ := ~~\left| \mathcal{{P}_{\alpha}^R} \right|~~    

				       send ~~work~~ to ~~\mathcal{P_{\alpha}^R}~~

				       wait until ~~passive_{\alpha}~~ and ~~sentNo_{\alpha}~~ = 0 and ~~recvNo_{\alpha}~~ = 0
				       decide termination detected
				    end when
				    

Algorytm Dijkstra-Scholten


when process ~~P_i~~ wants to sent a message ~~work~~ to ~~{P}_{j}~~ do
    ~~sentNo_i~~ := ~~sentNo_i~~ + 1 
    send ~~work~~ to ~~P_j~~
end when

when a message ~~work~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
    if ~~recvNo_i~~ = 0 then
        ~~engager_i~~ := ~~P_j~~
    else
        remember that ~~work~~ was submitted by ~~P_j~~
    end if
    ~~recvNo_i~~ := ~~recvNo_i~~ + 1 
    deliver ~~m~~ and schedule ~~work~~
end when
				    

Algorytm Dijkstra-Scholten


when a message ~~signal~~ arrives at process ~~P_i~~ from ~~{P}_{j}~~ do
    ~~sentNo_i~~ := ~~sentNo_i~~ - 1
end when

when a process ~~P_i~~ finishes ~~work~~ from ~~P_j~~ do
    if ~~P_j~~ = ~~engager_i~~ then
        wait until ~~sentNo_i~~ = 0 and ~~passive_i~~ 
    end if
    sent ~~signal~~ to ~~P_j~~
    ~~recvNo_i~~ := ~~recvNo_i~~ - 1 
end when
				    

Model przetwarzania synchronicznego

W modelu przetwarzania synchronicznego przyjmuje się, że transmisje są natychmiastowe. Stąd kanały mogą być uznane za puste przez cały czas i problem zakończenia sprowadza się do sprawdzenia czy wszystkie procesy są jednocześnie pasywne.

Stan zakończenia opisuja więc następujący predykat: $$Iterm({\mathcal {P}})\equiv P_{i}::P_{i}\in {\mathcal {P}}::passive_{i}$$

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Algorytm Dijkstra, Feijen, van Gasteren.

Procesy łączymy w wirtualny pierścień na potrzeby algorytmu; wiadomości aplikacyjne przesyłane są jednak w topologii grafu w pełni połączonego!

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Algorytm Dijkstra, Feijen, van Gasteren.

Procesy łączymy w wirtualny pierścień na potrzeby algorytmu; wiadomości aplikacyjne przesyłane są jednak w topologii grafu w pełni połączonego!

  • Procesom przypisany jest kolor White albo Black.
  • Procesy przesyłają wzdłuż pierścienia wiadomość kontrolną – znacznik typu TOKEN, który również może mieć kolor White albo Black .
  • Początkowo procesy mają kolor White, a zmieniają kolor na Black, gdy wyślą wiadomość aplikacyjną do procesu "wstecz" pierścienia
  • Proces inicjujący detekcję zakończenia $P_{\alpha }=P_{1}$ wysyła znacznik koloru White do swego następnika w pierścieniu gdy stanie się pasywny

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Algorytm Dijkstra, Feijen, van Gasteren.

  • Procesom przypisany jest kolor White albo Black.
  • Procesy przesyłają wzdłuż pierścienia wiadomość kontrolną – znacznik typu TOKEN, który również może mieć kolor White albo Black .
  • Początkowo procesy mają kolor White, a zmieniają kolor na Black, gdy wyślą wiadomość aplikacyjną do procesu "wstecz" pierścienia
  • Proces inicjujący detekcję zakończenia $P_{\alpha }=P_{1}$ wysyła znacznik koloru White do swego następnika w pierścieniu gdy stanie się pasywny
  • Każdy kolejny proces $P_{i}$ odbierający znacznik czeka aż stanie się pasywny i wówczas wysyła znacznik o kolorze zgodnym z kolorem procesu.
  • Po wysłaniu znacznika procesowi przypisywany jest kolor White.

Detekcja zakończenia: Przykład

Detekcja zakończenia: Przykład 2

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Dowód poprawności

Postęp: Czy jeżeli zakończenie zaszło, wykryjemy to w skończonym czasie?

Bezpieczeństwo: Czy jeżeli wykryliśmy zakończenie, to zakończenie zaszło?

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Dowód poprawności

Postęp: Czy jeżeli zakończenie zaszło, wykryjemy to w skończonym czasie?

Co może powstrzymać algorytm przed zakończeniem:

  • Token jest zatrzymany w procesach (kiedy?)
  • Token podróżuje przez kanały (czy w końcu dotrze?)

Bezpieczeństwo: Czy jeżeli wykryliśmy zakończenie, to zakończenie zaszło?

Detekcja zakończenia dla modelu przetwarzania synchronicznego

Dowód poprawności

Postęp: Czy jeżeli zakończenie zaszło, wykryjemy to w skończonym czasie?

Bezpieczeństwo: Czy jeżeli wykryliśmy zakończenie, to zakończenie zaszło?

Co może się stać, by po zakończeniu algorytmu jakieś procesy były wciąż aktywne?

  • Gdy opuszczamy proces, jaki jest jego stan?
  • Czy stan procesu odwiedzonego może się zmienić po tym, jak token go opuści?
  • Czy dowiemy się o tym, że stan odwiedzonego procesu może się zmienić?

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
				    

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.

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.

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