dr inż. Arkadiusz Danilecki
W oparciu o wykłady prof. J. Brzezińskiego
$\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
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.
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.
"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
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.
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.
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.
W sformułowaniu formalnym tego problemu wykorzystamy następujące oznaczenia:
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\}$$
Predykat ~~activate~~
Predykat ten jest monotoniczny; to znaczy: $$activate_i(\mathcal{X}) \land \mathcal{X} \subseteq \mathcal{Y} \Rightarrow activate_i(\mathcal{Y})$$
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})~~
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.
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.
Przetwarzanie rozproszone ${\mathit {\Pi }}$ jest w danej chwili w stanie zakończenia statycznego, jeżeli:
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}))}$$
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}})$$
$$ 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}))}$$
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 )$$
Przetwarzanie dyfuzyjne (ang. diffusing computation) jest specyficznym przetwarzaniem rozproszonym, w którym wyróżnia się:
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.
Założenia dodatkowe
Przedstawimy algorytm Dijkstry-Scholtena mocno zmodyfikowany i uproszczony na potrzeby prezentacji.
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~~
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
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
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
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}$$
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!
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!
Algorytm Dijkstra, Feijen, van Gasteren.
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?
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:
Bezpieczeństwo: Czy jeżeli wykryliśmy zakończenie, to zakończenie zaszło?
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?
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 )$$
W takim modelu wystarczy sprawdzić, czy kanały są puste. Kanały są puste, jeżeli wszystkie wiadomości wysłane są odebrane
Teoretycznie wystarczy sprawdzić, czy $RC(\tau) = SC(\tau)$. Proste! ... Proste?
Łą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$
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
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.
Jeżeli $$RC^{*}=SC^{*}=RC^{**}=SC^{**}$$ to monitorowane przetwarzanie aplikacyjne osiągnęło stan zakończenia przed zakończeniem procesu detekcji.
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 )$.
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})$
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})$$
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})$.
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})$$
Lemat 10.1.5
Dla wszystkich $\tau :RC(\tau )\leq SC(\tau )$
Dowód: Kanały są niezawodne, więc...
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?
Z założenia wynika, że:
$$RC^{*}=SC^{**}$$
Z kolei z przedstawionych lematów otrzymujemy, że:
$$SC^{**}\geq SC(\tau _{b}^{2})\geq SC(\tau _{e}^{1})\geq RC(\tau _{e}^{1})\geq RC^{*}$$
$$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^{*}$$
$$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
Łą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
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~~
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
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
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
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
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
Dowód poprawności na wykładzie powtórkowym.
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ł.
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~~
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
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
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
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
Łą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.
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).
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.