Przetwarzanie rozproszone

Niezawodność przetwarzania

dr inż. Arkadiusz Danilecki

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

Plan wykładu

Podstawowe pojęcia
Kanały komunikacyjne z gwarancjami
Jak formalnie myśleć o poprawności i awariach ?
Detektory awarii
Własności detektorów awarii
Implementacje detektorów awarii

Podstawowe pojęcia

Proces poprawny działa zgodnie ze specyfikacją

Wysyła wiadomości wtedy i tylko wtedy, gdy tego oczekujemy, wykonuje kroki algorytmu, ostatecznie osiąga wyznaczone cele...

$$correct(P_i) = \mbox{ true }$$

Podstawowe pojęcia

Proces poprawny działa zgodnie ze specyfikacją

Wysyła wiadomości wtedy i tylko wtedy, gdy tego oczekujemy, wykonuje kroki algorytmu, ostatecznie osiąga wyznaczone cele...

$$correct(P_i) = \mbox{ true }$$

Proces niepoprawny działa niezgodnie ze specyfikacją (w szczególności, nie działa)

... albo prościej - nie jest poprawny

$$\neg correct(P_i) = \mbox{ true }$$

Podstawowe pojęcia: awaria, błąd, wada

ISO/IEC 2382-14:1997(en):

Failure The termination of the ability of a functional unit to perform a required function.

Error A discrepancy between a computed, observed or measured value or condition and the true, specified or theoretically correct value or condition

Fault An abnormal condition that may cause a reduction in, or loss of, the capability of a functional unit to perform a required function.

Podstawowe pojęcia: awaria, błąd, wada

ISO 10303-226

Failure The lack of ability of a component, equipment, sub system, or system to perform its intended function as designed. A failure may be the result of one or many faults

Error ??

Fault an abnormal condition or defect at the component, equipment, or sub-system level which may lead to a failure

Podstawowe pojęcia: awaria, błąd, wada

Federal Standard 1037C

Failure The temporary or permanent termination of the ability of an entity to perform its required function.

Error

The difference between a computed, estimated, or measured value and the true, specified, or theoretically correct value.
A deviation from a correct value caused by a malfunction in a system or a functional unit.

Fault

An accidental condition that causes a functional unit to fail to perform its required function.
A defect that causes a reproducible or catastrophic malfunction.

Podstawowe pojęcia: awaria, błąd, wada

Awaria (ang. failure) - działanie procesu niezgodne z algorytmem czy specyfikacją.

Błąd (ang. error) - część stanu procesu odpowiedzialna za będącą jego następstwem awarię

Wada (ang. fault) - stwierdzona lub hipotetyczna przyczyna wystąpienia błędu

Klasy awarii procesów

Kanały komunikacyjne... ale z gwarancjami

Kanały rzetelne (fair-loss): własności

rzetelne dostarczanie (ang. fair loss delivery) - jeżeli wiadomość $M$ wysyłana jest nieskończoną liczbę razy przez proces $P_{i}$ do procesu $P_{j}$ i żaden z tych procesów nie ulega awarii (oba są poprawne), to wiadomość $M$ jest dostarczona nieskończoną liczbę razy do $P_{j}$. Należy zauważyć, że własność ta dopuszcza zagubienia wiadomości $M$ nawet nieskończoną liczbę razy.
ograniczone powielanie (ang. finite duplication ) - jeżeli wiadomość $M$ wysyłana jest skończoną liczbę razy przez proces $P_{i}$ do procesu $P_{j}$, to wiadomość ta nie może być dostarczona nieskończoną liczbę razy do procesu $P_{j}$.
brak samogeneracji (ang. no creation ) - jeżeli wiadomość $M$ została dostarczona do procesu $P_{j}$, to została ona wcześniej wysłana do tego procesu przez jakiś inny proces $P_{i}$. Innymi słowy, kanał nie tworzy samorzutnie wiadomości.

Kanały rzetelne: operacje

Zwykle będziemy tylko mówić w założeniach, że operacje send oraz receive używają kanałów rzetelnych. Jeżeli jednak zajdzie potrzeba, używane operacje do wysyłania i odbioru zapisywać będziemy jako:

send $m$ using fair-loss channel

albo:

when message $m$ arrives at $P_i$ via fair-loss channel

Kanały wytrwałe (stubborn): własności

wytrwałe dostarczanie (ang. stubborn delivery) - jeżeli wiadomość $M$ wysyłana jest przez proces $P_{i}$ do procesu $P_{j}$ i żaden z tych procesów nie ulega awarii (oba są poprawne), to wiadomość $M$ jest dostarczona nieskończoną liczbę razy do $P_{j}$.
brak samogeneracji (ang. no creation ) - jeżeli wiadomość $M$ została dostarczona do procesu $P_{j}$, to została ona wcześniej wysłana do tego procesu przez jakiś inny proces $P_{i}$. Innymi słowy, kanał nie tworzy samorzutnie wiadomości.

Kanały wytrwałe: implementacja


when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
    while true
        send ~~m~~ to ~~P_j~~ using fair-loss channel
    end while
end when
when a message $m$ arrives at ~~P_i~~ from ~~{P}_{j}~~ via fair-loss channel do
    deliver $m$
end when

Kanały niezawodne (perfect): własności

niezawodne dostarczanie (ang. fair loss delivery) - jeżeli wiadomość $M$ wysłana jest przez proces $P_{i}$ do procesu $P_{j}$ i żaden z tych procesów nie ulega awarii (oba są poprawne), to wiadomość $M$ jest dostarczona do $P_{j}$.
brak powielania (ang. no duplication ) - żadna wiadomość $M$ nie jest dostarczona więcej niż raz.
brak samogeneracji (ang. no creation ) - jeżeli wiadomość $M$ została dostarczona do procesu $P_{j}$, to została ona wcześniej wysłana do tego procesu przez jakiś inny proces $P_{i}$. Innymi słowy, kanał nie tworzy samorzutnie wiadomości.

Kanały niezawodne: implementacja

 
    local set of messages ~~delivered_i~~ := ~~\emptyset~~


when process ~~P_i~~ wants to sent a message ~~m~~ to ~~{P}_{j}~~ do
    while true
        send ~~m~~ to ~~P_j~~ using stubborn channel
    end while
end when
when a message $m$ arrives at ~~P_i~~ from ~~{P}_{j}~~ via stubborn channel do
    if ~~\neg(m \in delivered_i)~~ then
        ~~delivered_i := delivered_i \cup m~~
        deliver $m$
    end if
end when

Modele systemów a rozumowanie o poprawności w obecności awarii

Problemy, które musimy rozważyć:

Jakie cechy systemów są ważne przy analizie poprawności?
Jak opisywać wymagania algorytmów wobec systemu?
Jakie są minimalne wymagania dla danego mechanizmu/algorytmu wobec systemu?

Systemy asynchroniczne

Brak zegara globalnego, brak synchronizacji zegarów
Brak ograniczeń na czas komunikacji
Brak ograniczeń na czas przetwarzania

Systemy synchroniczne

Zegar globalny/synchronizacja zegarów
Znane ograniczenia na czas komunikacji
Znane ograniczenia na czas przetwarzania

Systemy częściowo synchroniczne

Znane są maksymalne czasy komunikacji oraz/lub przetwarzania, lecz nie jest znany moment, po którym zaczną one obowiązywać
Istnieją pewne odcinki czasu, w których system działa jak system asynchroniczny, ale są też okresy, w których system działa jak synchroniczny

Systemy częściowo synchroniczne

synchroniczność procesorów - istnieje stała $k_{0}$ taka, że jeżeli pewien proces $P_{i}$ wykona $k_{0}+1$ kroków, to każdy inny proces wykona co najmniej 1 krok.
istnieją ograniczenia na czas przesyłania wiadomości (opóźnienie komunikacyjne).
porządek wiadomości - porządek synchroniczny oznacza, że jeżeli proces $P_{i}$ wysyła wiadomość $M$ do procesu $P_{j}$ w czasie $\tau _{i}$ oraz proces $P_{k}$ wysyła wiadomość $M'$ do procesu $P_{j}$ w czasie $\tau _{j}>\tau _{i}$, to wiadomość $M$ zostanie dostarczona do $P_{j}$ przed wiadomością $M'$.
rodzaj komunikacji, za pomocą niepodzielnej komunikacji rozgłaszania, czy też za pomocą komunikacji punkt-punkt.
typ operacji send/receive - operacje atomowe (tzn., czy operacja wysłania wiadomości $M$ kończy się dopiero po zakończeniu odbioru tej wiadomości przez adresata), czy też są rozłączne. Innymi słowy, czy komunikacja między procesami jest synchroniczna, czy też nie.

$2^5 = 32$ kombinacje

Detektory awarii

Jeżeli proces działa i kanał jest niezawodny, to w końcu się doczekamy na odpowiedź...

... a więc do rozważań o samej poprawności, wystarczy wiedzieć, które procesy uległy awarii!

Detektory awarii

Rozproszona oraz zawodna "wyrocznia" odpowiadająca na pytania o to, czy dany inny proces działa, czy też nie;

rozproszona - każdy proces może otrzymywać inne odpowiedzi. W praktyce wynika to z tego, że każdy proces będzie miał dostęp de facto do własnej instancji detektora.
zawodna - "wyrocznia" może się mylić, a więc detektor może twierdzić, że poprawny proces jest niepoprawny i na odwrót, detektor może też zmieniać zdanie.

Detektory awarii

${\mathcal {P}}=\{P_{1},P_{2},P_{3},\ldots ,P_{n}\}$
Kanały komunikacyjne są niezawodne.
Zegar globalny jest dyskretny, a jego dziedzina ${\mathcal {Y}}$ jest zbiorem liczb naturalnych $\mathbb {N}$.
Czasy komunikacji i przetwarzania są ograniczone lecz nieznane.

Wzorzec awarii

Cel - ujęcie w formalne zapisy faktu, że w systemie podczas wykonania zdarzają się w pewnych chwilach awarie.

Wzorzec awarii

Cel - ujęcie w formalne zapisy faktu, że w systemie podczas wykonania zdarzają się w pewnych chwilach awarie.

Niech wzorzec awarii $F$ będzie funkcją $F:{\mathcal {Y}}\rightarrow 2^{\mathcal {P}}$, gdzie $F(\tau )$ oznacza zbiór procesów, które uległy awarii do momentu $\tau$. Po awarii proces nie powraca do pracy, czyli prawdziwe jest wyrażenie: $$\forall \tau :F(\tau )\subseteq F(\tau +1)$$

Wzorzec awarii opisuje więc faktyczny stan wszystkich procesów w różnych odcinkach czasu. Ponadto zbiór procesów podejrzanych oraz poprawnych jest opisany odpowiednio przez równości: $$crashed(F)=\bigcup \tau \in {\mathcal {T}},F(\tau )$$ $$correct(F)={\mathcal {P}}\setminus crashed(F)$$

Historia detektora awarii

Cel - ujęcie w formalne zapisy tego, że procesy mają lokalne "wyrocznie", z których każda w różnych chwilach może uznawać inne procesy za niepoprawne (podejrzewa je o awarie).

Historia detektora awarii

Cel - ujęcie w formalne zapisy tego, że procesy mają lokalne "wyrocznie", z których każda w różnych chwilach może uznawać inne procesy za niepoprawne (podejrzewa je o awarie).

Rozważamy tylko wzorce uszkodzeń $\displaystyle F$, w których co najmniej jeden proces jest poprawny, czyli $correct(F)\neq \emptyset$.

Każdy detektor utrzymuje listę (zbiór) procesów, które podejrzewa.

Historia detektora awarii

Cel - ujęcie w formalne zapisy tego, że procesy mają lokalne "wyrocznie", z których każda w różnych chwilach może uznawać inne procesy za niepoprawne (podejrzewa je o awarie).

Rozważamy tylko wzorce uszkodzeń $\displaystyle F$, w których co najmniej jeden proces jest poprawny, czyli $correct(F)\neq \emptyset$.

Każdy detektor utrzymuje listę (zbiór) procesów, które podejrzewa.

Historia detektora awarii to funkcja odwzorowująca iloczyn kartezjański zbioru procesów i pewnego okresu czasu w rodzinę wszystkich podzbiorów zbioru ${\mathcal {P}}$.

Wartość $H^{FD}(P_{i},\tau )$ oznacza zbiór procesów podejrzewanych przez $P_{i}$ w chwili $\tau$.

Formalna definicja detektora awarii

Niech ${\mathcal {D}}(F)$ oznacza zbiór możliwych historii detektora awarii i jest sumę mnogościową wszystkich możliwych historii detektora awarii, które mogły się przydarzyć z wzorcem awarii $F$ i detektorem awarii $FD$.

$$FD: F(\tau) \rightarrow D(F)$$

Detektor awarii $FD$ jest to funkcja odwzorowująca wzorzec awarii $F$ w zbiór możliwych historii detektora ${\mathcal {D}}(F)$.

Własności detektorów awarii

NIEFORMALNIE

W formalnych definicjach $FD$ odwzorowywał "wzorzec awariii" w zbiór "możliwych historii", tj. rzeczywistemu zachowaniu systemu (gdzie procesy były poprawne lub ulegały awariom) przypisywał "historie detektora" tj. odpowiedzi "ten czy ów proces jest teraz poprawny".

Detektor, który by po prostu losował odpowiedzi, byłby zgodny z tą definicją.

Własności detektorów awarii

NIEFORMALNIE

Jak dobrze możliwe historie naszego detektora odwzorowują faktyczne awarie?

Kompletność (ang. completeness) - zdolność do podejrzewania wszystkich procesów niepoprawnych.

Czy możemy liczyć na to, że nasz (dla przypomnienia - rozproszony!) detektor wykryje awarię?

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych.

Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Własności detektorów awarii

Kompletność

Kompletność (ang. completeness) - zdolność do podejrzewania wszystkich procesów niepoprawnych.

Silna Kompletność (ang. strong completeness):

$$\forall F \forall H^{FD} \in D(F), \exists \tau \in \mathcal{Y}: \forall P_i \in crashed(F), \forall P_j \in correct(F) : \forall \tau ^i \geq \tau, P_i \in H^{FD}(P_j,\tau ^i ) $$

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Własności detektorów awarii

Kompletność

Kompletność (ang. completeness) - zdolność do podejrzewania wszystkich procesów niepoprawnych.

Silna Kompletność (ang. strong completeness):

$$ \forall P_i: crashed(P_i) \Rightarrow \forall P_j : correct(P_j), \Diamond \Box suspects( P_j, P_i ) $$

$\Diamond$ - eventually, ostatecznie coś się zdarzy;

$\Box$ - always, zawsze coś będzie/jest prawdziwe;

$\Diamond \Box$ ostatecznie dojdzie do tego, że coś będzie już zawsze prawdziwe

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Własności detektorów awarii

Kompletność

Kompletność (ang. completeness) - zdolność do podejrzewania wszystkich procesów niepoprawnych.

Słaba Kompletność (ang. weak completeness):

$$\forall F \forall H^{FD} \in D(F), \exists \tau \in \mathcal{Y}: \forall P_i \in crashed(F), \exists P_j \in correct(F) : \forall \tau ^i \geq \tau, P_i \in H^{FD}(P_j,\tau ^i ) $$

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Własności detektorów awarii

Kompletność

Kompletność (ang. completeness) - zdolność do podejrzewania wszystkich procesów niepoprawnych.

Słaba Kompletność (ang. weak completeness):

$$ \forall P_i: crashed(P_i) \Rightarrow \exists P_j : correct(P_j), \Diamond \Box suspects( P_j, P_i ) $$

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Własności detektorów awarii

Dokładność

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Silna dokładność (ang. strong accuracy):

$$\forall F \forall H^{FD} \in D(F), \forall \tau \in \mathcal{Y}, \forall P_i,P_j \not\in F(\tau): P_i \not\in H^{FD}(P_j,\tau ^i ) $$

Własności detektorów awarii

Dokładność

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Silna dokładność (ang. strong accuracy):

$$ \forall P_i: correct(P_i) \Rightarrow \forall P_j: \Box \neg suspects( P_j, P_i ) $$

Własności detektorów awarii

Dokładność

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Słaba dokładność (ang. weak accuracy):

$$\forall F \forall H^{FD} \in D(F), \forall \tau \in \mathcal{Y}, \exists P_i \in correct(F), \forall P_j \not\in F(\tau) : P_i \not\in H^{FD}(P_j,\tau ^i ) $$

Własności detektorów awarii

Dokładność

Dokładność (ang. accuracy) - zdolność do nie podejrzewania wszystkich procesów poprawnych. Czy możemy ufać naszemu detektorowi, że wykrywa rzeczywiste awarie?

Słaba dokładność (ang. weak accuracy):

$$ \exists P_i: correct(P_i) \Rightarrow \forall P_j: \Box \neg suspects( P_j, P_i ) $$

Rodzaje detektorów awarii

Redukcje i równoważność detektorów awarii

Detektor pewnej klasy może "udawać" detektor innej klasy, w sensie, że wyjście detektora klasy X można z łatwością tak przerobić, by spełniało własności klasy Y.

Gdy relacja ta zachodzi w obie strony, mówimy, że detektory są równoważne

Implementacje detektorów awarii

Mechanizm pulsu

Implementacje detektorów awarii

Mechanizm odpytywania

Implementacje detektorów awarii

Detektor klasy $P$

Implementacje detektorów awarii

Detektor klasy $P$

Algorytm z użyciem mechanizmu pulsu.

Zakładamy istnienie niezawodnych kanałów komunikacyjnych łączących procesy. Ponadto znany jest maksymalny czas transmisji komunikatu. W porównaniu do tej wartości czasy przetwarzania lokalnego i ewentualne różnice w szybkościach zegarów lokalnych są pomijalnie małe.

Implementacje detektorów awarii

Detektor klasy $P$


				    message $hearbeat$ 

				    local set of channels ~~suspected_i~~ := ~~\emptyset~~ 
				    local set of channels ~~correct_i~~ := ~~\mathcal{P}~~ 
				    local const int ~~period_i^{to}~~ 
				    local const int ~~period_i^{p}~~

Implementacje detektorów awarii

Detektor klasy $P$


				    at each ~~period_i^{to}~~ tick at ~~P_i~~ do
				        for all ~~P_k \in \mathcal{P}~~
				            if ~~P_k \not\in correct_i \land P_k \not\in suspected_i~~ then
				                ~~suspected_i~~ := ~~suspected_i \cup P_k~~
				            end if
				        end for
				        ~~correct_i~~ := ~~\emptyset~~
				    end at each

Implementacje detektorów awarii

Detektor klasy $P$


at each ~~period_i^{p}~~ tick at ~~P_i~~ do
    for all ~~P_k \in \mathcal{P}~~
        send ~~hearbeat~~ to ~~P_k~~
    end for
end at each

when message ~~heartbeat~~ arrives at ~~P_i~~ from ~~P_j~~ do
    ~~correct_i~~ := ~~correct_i \cup P_j~~
end when

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Algorytm z użyciem mechanizmu pulsu.

Zakładamy istnienie niezawodnych kanałów komunikacyjnych łączących procesy. Ponadto istnieje maksymalny czas transmisji komunikatu, chociaż nie jest on znany. W porównaniu do tej wartości czasy przetwarzania lokalnego i ewentualne różnice w szybkościach zegarów lokalnych są pomijalnie małe.

Implementacje detektorów awarii

Detektor klasy $\Diamond P$


				    message $hearbeat$ 

				    local set of channels ~~suspected_i~~ := ~~\emptyset~~ 
				    local set of channels ~~correct_i~~ := ~~\mathcal{P}~~ 
				    local int ~~period_i^{to}~~ := ~~t^1~~ 
				    local const ~~period_i^{p}~~

Implementacje detektorów awarii

Detektor klasy $\Diamond P$


at each ~~period_i^{p}~~ tick at ~~P_i~~ do
    for all ~~P_k \in \mathcal{P}~~
        send ~~hearbeat~~ to ~~P_k~~
    end for
end at each

when message ~~heartbeat~~ arrives at ~~P_i~~ from ~~P_j~~ do
    ~~correct_i~~ := ~~correct_i \cup P_j~~
end when

Implementacje detektorów awarii

Detektor klasy $\Diamond P$


				    at each ~~period_i^{to}~~ tick at ~~P_i~~ do
				        for all ~~P_k \in \mathcal{P}~~
				            if ~~P_k \not\in correct_i \land P_k \not\in suspected_i~~ then
				                ~~suspected_i~~ := ~~suspected_i \cup P_k~~
				            else if ~~P_k \in correct_i \land P_k \in suspected_i~~ then
				                ~~suspected_i~~ := ~~suspected_i \setminus P_k~~
				                ~~period_i^{to}~~ := ~~period_i^{to} + \Delta~~
				            end if
				        end for
				        ~~correct_i~~ := ~~\emptyset~~
				    end at each

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Silna kompletność - ostatecznie wszystkie błędne procesy będą podejrzewane.

Ostatecznie silna dokładność - ostatecznie żaden poprawny proces nie będzie podejrzewany.

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Postęp

Silna kompletność - ostatecznie wszystkie błędne procesy będą podejrzewane.

Bezpieczeństwo

Ostatecznie silna dokładność - ostatecznie żaden poprawny proces nie będzie podejrzewany.

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Postęp

Błędne procesy przestaną wysyłać nowe wiadomości, a wcześniej wysłane wiadomości ostatecznie wszystkie dotrą. Ostatecznie więc przestaną przychodzić nowe wiadomości od tych procesów, i gdy minie czas $period_i^{to}$, zostaną dodane do zbioru $suspected_i$

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Bezpieczeństwo

Zakładamy pomijalnie małe różnice w zegarach, oraz że istnieje ograniczenie na maksymalny czas przesyłania wiadomości (częściowo synchroniczny model systemu).

Załóżmy, że pewien poprawny proces $P_j$ został niesłusznie dodany do zbioru ~~suspected_i~~ w procesie $P_i$. Poprawne procesy zawsze wysyłają ~~heartbeat~~, a więc $P_j$ już wysłał albo ostatecznie wyśle ~~heartbeat~~ do $P_i$.

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Bezpieczeństwo

Kanały są niezawodne, więc wiadomości ~~hearbeat~~ od ~~P_j~~ w końcu dotrą do ~~P_i~~, co spowoduje usunięcie ~~P_j~~ ze zbioru ~~suspected_i~~ i zwiększenie stałej ~~period_i^{to}~~. Skoro istnieje ograniczenie na czas transmisji, to ostatecznie stała ta zostanie zwiększona tak, że będzie większa od tego czasu i wiadomości ~~heartbeat~~ będą przychodzić do $P_i$ na czas, i ostatecznie ~~P_j~~ przestanie być dodawany do ~~suspected_i~~.

Implementacje detektorów awarii

Detektor klasy $\Diamond P$

Dowód poprawności.

Bezpieczeństwo

Rozumowanie to można powtórzyć dla każdego niesłusznie podejrzewanego $P_j$, a więc każdy poprawny proces ostatecznie nie będzie już podejrzewany.