Pr-1st-1.1-m06-Slajd32

Algorytm detekcji zakleszczenia dla modelu predykatowego (7)

Wysłanie wiadomości aplikacyjnej powoduje każdorazowo zwiększenie zmiennej $notAck_{i}$ informującej o niepotwierdzonych wiadomościach wysłanych przez proces $P_{i}$.

Odebranie wiadomości aplikacyjnej przez monitor $Q_{i}$ powoduje dostarczenie tej wiadomości do procesu $P_{i}$ i wysłanie potwierdzenia typu ACK do monitora skojarzonego z procesem nadawcy. Odebranie takiego potwierdzenia przez monitor umożliwia zmniejszenie o 1 wartości zmiennej $notAck_{i}$.

W sytuacji w której proces staje się procesem aktywnym, zmiennej $contPassive_{i}$ jest nadawana wartość False.

Jak wiadomo w celu wykazania poprawności algorytmu należy udowodnić twierdzenia mówiące o jego żywotności i bezpieczeństwie. Rozważając ciąg cykli wykonania algorytmu, oznaczymy przez $\tau _{i}^{k}$ moment czasu globalnego zakończenia cyklu k - tego w monitorze $Q_{i}$, a więc moment wysłania znacznika z $Q_{i}$ do $Q_{i+1}$ w k - tym cyklu. Analogicznie, $\tau _{\alpha }^{k}$ oznaczać będzie moment zakończenia cyklu k - tego w monitorze inicjatora $Q_{\alpha }$, to znaczy moment zakończenia całego cyklu k. Ponadto, dla każdego elementu $X$ (zmiennej, predykatu), $X[\tau ]$ oznaczać będzie wartości elementu $X$ w chwili $\tau$. W szczególności, ${\mathcal {PD}}[\tau _{i}^{k}]$ oznacza wartość zbioru ${\mathcal {PD}}$ zawartego w znaczniku, w momencie wysłania znacznika przez monitor $Q_{i}$ w ramach k - tego cyklu detekcji. Przyjmiemy jeszcze następującą definicję:

$contPassive_{i}^{*}(\tau ',\tau '')\equiv (\tau '\leq \tau '')\land \forall \tau ::\tau '\leq \tau \leq \tau ''::passive_{i}[\tau ]$

Jeżeli algorytm detekcji zakleszczenia zostanie zainicjowany w chwili $t_{b}$, to zakończy się w skończonym czasie, w pewnej chwili $t_{e}$, $t_{e}>t_{b}$.

Dowód:

Zauważmy, że znacznik przebywający i przetwarzany w monitorze $Q_{i}$ jest natychmiast przesyłany dalej, gdy $P_{i}\not \in {\mathcal {PD}}$. W przeciwnym razie, znacznik jest zatrzymywany i przechowywany w monitorze $Q_{i}$ aż do momentu $\tau$ spełnienia następującego warunku:

$(\neg contPassive_{i}[\tau ])\lor (activate_{i}({\mathcal {AV}}_{i}\cup ({\mathcal {P}}\setminus {\mathcal {PD}})[\tau ])\lor (notAck_{i}=0)[\tau ]$

Oczywiście warunek $(contPassive_{i}[\tau ])\land (notAck_{i}\neq 0)[\tau ])$ nie może zachodzić przez czas nieograniczony, gdyż procesy pasywne nie wysyłają nowych wiadomości i, z drugiej strony, wszystkie wiadomości zostają potwierdzone w skończonym czasie. Tak więc w końcu warunek wysłania znacznika zostanie spełniony, a w konsekwencji cały cykl również zakończy się w skończonym czasie. Następny cykl, k + 2 jest inicjowany, gdy $|{\mathcal {PD}}[\tau _{\alpha }^{k}]|>|{\mathcal {PD}}[t_{\alpha }^{k+1}]|$. Wówczas funkcja: $k\rightarrow |{\mathcal {PD}}[\tau _{\alpha }^{k}]|$ jest monotonicznie malejąca, z początkową wartością $|{\mathcal {P}}|=n$. Stąd liczba cykli jest skończona, a więc w skończonym czasie algorytm detekcji zakończy się.

Niech $\tau _{b}$ oraz $\tau _{e}$ oznaczają odpowiednio moment rozpoczęcia i zakończenia algorytmu detekcji zakleszczenia:

a) Jeżeli algorytm kończy się i zbiór ${\mathcal {PD}}$ jest zbiorem pustym (${\mathcal {PD}}=\emptyset$), to dla każdego zbioru ${\mathcal {B}}$,${\mathcal {B}}\neq \emptyset$ i ${\mathcal {B}}\subseteq {\mathcal {P}}$,

predykat $deadlock({\mathcal {B}})$ miał wartość $False$ w chwili $\tau _{b}$.

b) Jeżeli algorytm kończy się i zbiór ${\mathcal {PD}}$ nie jest zbiorem pustym (${\mathcal {PD}}\neq \emptyset$), to predykat $deadlock({\mathcal {PD}})$ ma wartość $True$ w chwili $\tau _{e}$. Ponadto dla każdego zbioru

${\mathcal {B}}$, takiego, że $deadlock({\mathcal {B}})$ miał wartość $True$ w chwili $\tau _{b}$, ${\mathcal {B}}$ jest podzbiorem zbioru ${\mathcal {PD}}$ (${\mathcal {B}}\subseteq {\mathcal {PD}})$.

Dowód implikacji a)

W celu udowodnienia implikacji a), wykażemy następującą implikację równoważną:

$(\exists {\mathcal {B}}::{\mathcal {B}}\subseteq {P}::deadlock({\mathcal {B}})[\tau _{b}])\Rightarrow ({\mathcal {PD}}[\tau _{e}]\neq \emptyset )$

Zgodnie z założeniem, w chwili $\tau _{b}$ zachodzi predykat deadlock(\mathcal{B}) i \mathcal{B}\ne \emptyset. ${\mathcal {PD}}$ początkowo jest równe ${\mathcal {P}}$ i stąd oczywiście w chwili $\tau _{b}$, \mathcal{B} Í \mathcal{PD}. Ponieważ deadlock(\mathcal{B}) jest predykatem stabilnym, prawdą jest, że:

$\forall \tau ::\tau \geq \tau _{b}::deadlock({\mathcal {B}})[\tau ]$ ${}^{(W1)}$

Stąd, korzystając z definicji zakleszczenia dla modelu predykatowego, otrzymujemy:

$\forall \tau ::\tau \geq \tau _{b}::(\forall P_{i}::P_{i}\in {\mathcal {B}}::passivei[\tau ]\land \neg activate_{i}({\mathcal {IT}}_{i}[\tau ]\cup {\mathcal {AV}}_{i}[\tau ]\cup {\mathcal {P}}\setminus {\mathcal {B}}))$

Wszystkie procesy $P_{i}$ należące do \mathcal{B} są stale pasywne począwszy od chwili $\tau _{b}$, a więc od pierwszej wizyty znacznika. Pokażemy teraz nie wprost, że żaden proces należący do ${\mathcal {B}}$ nie może być usunięty z ${\mathcal {PD}}$. Postawmy zatem hipotezę, że w chwili $\tau >\tau _{b}$, tuż przed możliwym usunięciem z ${\mathcal {PD}}$ pewnego procesu $P_{i}$, zachodzi relacja ${\mathcal {B}}\subseteq {\mathcal {PD}}$. Stale pasywny proces $P_{i}$ może być usunięty z ${\mathcal {PD}}$, pod warunkiem, że spełniona jest w chwili $\tau$ relacja:

$activate_{i}({\mathcal {AV}}_{i}[\tau ]\cup {\mathcal {P}}\setminus {\mathcal {PD}}[\tau ])=True$

Zauważmy jednak, że ${\mathcal {AV}}_{i}[\tau ]={\mathcal {AV}}_{i}[\tau _{b}]\cup \{P_{k}:{\mbox{ wiadomości wysłane z }}P_{k}{\mbox{ do }}P_{i}{\mbox{ stały sie dostepne dla }}P_{i}{\mbox{ w przedziale }}\left\langle \tau _{b},\tau \right\rangle \}$.

Rozważmy teraz wiadomość, która stała się dostępna dla $P_{i}$ w przedziale czasu $\left\langle \tau _{b},\tau \right\rangle$. Jej nadawca $P_{j}$ albo należał do ${\mathcal {P}}\setminus {\mathcal {B}}$, albo jest procesem należącym do ${\mathcal {B}}$, którego kanał wyjściowy $C_{j,i}$ nie był pusty w chwili $\tau _{b}$. Tak więc:

${\mathcal {AV}}_{i}[\tau ]\subseteq ({\mathcal {AV}}_{i}[\tau _{b}]\cup {\mathcal {IT}}_{i}[\tau _{b}]\cup {\mathcal {P}}\setminus {\mathcal {B}})$

Z postawionej hipotezy wiemy, że $activatei({\mathcal {AV}}_{i}[\tau ]\cup {\mathcal {P}}\setminus {\mathcal {PD}}[\tau ])=True$, a stąd otrzymujemy:

$activate_{i}({\mathcal {AV}}_{i}[\tau _{b}]\cup {\mathcal {IT}}_{i}[\tau _{b}]\cup {\mathcal {P}}\setminus {\mathcal {B}}\cup {\mathcal {P}}\setminus {\mathcal {PD}}[\tau ])=True$.

Ponieważ ${\mathcal {B}}\subseteq {\mathcal {DP}}[\tau ]$, powyższa relacja redukuje się do:

$activate_{i}({\mathcal {AV}}_{i}[\tau _{b}]\cup {\mathcal {IT}}_{i}[\tau _{b}]\cup {\mathcal {P}}\setminus {\mathcal {B}})=True$.

Zauważmy, że ostatnia równość jest w sprzeczności z przyjętym założeniem: $deadlock({\mathcal {B}})[\tau _{b}]=True$. Tak więc, żaden proces należący do ${\mathcal {B}}$ nie może być usunięty z ${\mathcal {PD}}$, co kończy dowód implikacji a).

Zauważmy jednak jeszcze, że gdy algorytm kończy się i ${\mathcal {PD}}\neq \emptyset$ to otrzymujemy:

${\mathcal {B}}\neq \emptyset \land {\mathcal {B}}\subseteq {\mathcal {PD}}$ ${}^{(W2)}$

Dowód implikacji b)

Zgodnie z konstrukcją, algorytm kończy się w chwili $\tau _{e}=\tau _{\alpha }^{k}+1$ z wynikiem ${\mathcal {PD}}\neq \emptyset$ wtedy i tylko wtedy, gdy

${\mathcal {PD}}[\tau _{\alpha }^{k}+1]|=|{\mathcal {PD}}[\tau _{\alpha }^{k}]|$ i ${\mathcal {PD}}[\tau _{\alpha }^{k}+1]\neq \emptyset$

Niech $\tau _{k}$, spełnia relację $max(\tau _{i}^{k})\leq \tau _{k}\leq min(\tau _{i}^{k}+1)$, Chwila taka istnieje, gdyż przykładowo $\tau _{k}$ może być równe $\tau _{i}^{k}$. W szczególności zachodzi:

$\forall P_{i}::P_{i}\in {\mathcal {P}}::\tau _{i}^{k}\leq \tau _{\alpha }^{k}\leq \tau _{k}\leq \tau _{i}^{k}+1\leq \tau _{\alpha }^{k}+1$

Ponieważ zbiór ${\mathcal {PD}}$ może jedynie ulegać redukcji, otrzymujemy:

$\forall P_{i}::P_{i}\in {\mathcal {P}}::{\mathcal {PD}}[\tau _{i}^{k}]\supseteq {\mathcal {PD}}[\tau _{\alpha }^{k}]\supseteq {\mathcal {PD}}[\tau _{k}]\supseteq {\mathcal {PD}}[\tau _{i}^{k}+1]\supseteq {\mathcal {PD}}[\tau _{\alpha }^{k}+1]$

Tak więc, jeżeli algorytm zakończy się w chwili $\tau =\tau _{\alpha }^{k}+1i{\mathcal {PD}}[\tau ]\neq \emptyset$, to

$\forall P_{i}::P_{i}\in {\mathcal {P}}::{\mathcal {PD}}[\tau _{\alpha }^{k}]={\mathcal {PD}}[\tau _{k}]={\mathcal {PD}}[\tau _{i}^{k}+1]={\mathcal {PD}}[\tau _{\alpha }^{k}+1]$

Niech${\mathcal {PD}}^{*}$ będzie oznaczać zbiór spełniający powyższą zależność. Udowodnimy, że $deadlock({\mathcal {PD}}^{*})$ zachodzi w chwili $\tau =\tau _{k}$, to znaczy, spełnione są w chwili $\tau _{k}$ następujące warunki:

C1. ${\mathcal {PD}}^{*}\neq \emptyset$i

C2. $(\forall P_{i}::P_{i}\in {\mathcal {PD}}^{*}::passive_{i}[\tau _{x}])$ i

C3. $(\forall P_{i}::P_{i}\in {\mathcal {PD}}^{*}::\neg activate_{i}({\mathcal {IT}}_{i}[\tau _{x}]\cup {\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})).$

Pokażemy teraz, że powyższe warunki są spełnione, jeżeli algorytm zakończy się z ${\mathcal {PD}}^{*}\neq \emptyset$. Z definicji warunku zakończenia wynika wprost, że jeżeli algorytm kończy się z ${\mathcal {PD}}^{*}\neq \emptyset$, to warunek C1 jest spełniony w chwili $\tau _{k}$. Niech teraz $P_{i}\in {\mathcal {PD}}^{*}$. Z konstrukcji algorytmu wynika, że tylko proces stale pasywny począwszy od zakończenia pierwszego cyklu w chwili $\tau _{i}^{1}$, może należeć do ${\mathcal {PD}}^{*}$. Stąd mamy:

$contPassive_{i}^{*}(\tau _{i}^{1},\tau _{i}^{k}+1)$, a więc $passive_{i}[\tau _{x}]$

Tym samym warunek C2 zajścia zakleszczenia został zweryfikowany. Ponieważ $P_{i}\in {\mathcal {PD}}^{*}$, wnioskujemy z konstrukcji algorytmu , że:

$\neg activate_{i}({\mathcal {AV}}_{i}[\tau _{i}^{k}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}*)=True$.

W przeciwnym bowiem razie, $P_{i}$ zostałby usunięty ze zbioru ${\mathcal {PD}}^{*}$. Ale, skoro ${\mathcal {AV}}_{i}$ może tylko zmienić się przez dołączanie nowych elementów, a ${\mathcal {P}}\setminus {\mathcal {PD}}^{*}$ nie zmienia się w przedziale $\left\langle \tau _{\alpha }^{k},\tau _{\alpha }^{k}+1\right\rangle$, otrzymujemy:

$({\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})\subseteq {\mathcal {AV}}_{i}[\tau _{i}^{k}+1]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})$

Z konstrukcji algorytmu wnioskujemy dalej, że wszystkie kanały wyjściowe procesów należących do ${\mathcal {PD}}^{*}$ są puste w chwili $\tau _{\alpha }^{k}$, gdyż znacznik jest zatrzymywany przez monitor skojarzony z pasywnym procesem należącym do ${\mathcal {PD}}^{*}$ do momentu uzyskania potwierdzeń dla wszystkich wysłanych wcześniej wiadomości ($notAck_{i}=0$).

Ponieważ procesy te są przy tym stale pasywne od pierwszej wizyty znacznika, ich kanały wyjściowe są puste w chwili $\tau _{x}$. Stąd:

$({\mathcal {IT}}_{i}[\tau _{x}]\cap {\mathcal {PD}}^{*})=0$ i dlatego ${\mathcal {IT}}_{i}[\tau _{x}]\in {\mathcal {P}}\setminus {\mathcal {PD}}^{*}$.

W konsekwencji:

$({\mathcal {IT}}_{i}[\tau _{x}]\cup {\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})=({\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})$

Z zależności i) otrzymujemy:

$({\mathcal {IT}}_{i}[\tau _{x}]\cup {\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})\subseteq ({\mathcal {AV}}_{i}[\tau _{i}^{k}+1]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})$

Z kolei z monotoniczności predykatu $activate_{i}$ oraz z powyższego równania wnioskujemy, że jeżeli zachodzi:

$\neg activate_{i}({\mathcal {AV}}_{i}[\tau _{i}^{k}+1]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})$

to zachodzi również

$\neg activate_{i}({\mathcal {IT}}_{i}[\tau _{x}]\cup {\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})$

Z konstrukcji wnosimy dalej, że predykat jest spełniony dla wszystkich $P_{i}\in {\mathcal {PD}}^{*}$. Tym samym warunek C3 został wykazany.

Powyższe punkty dowodzą, że predykat $deadlock({\mathcal {PD}}^{*})$ zachodzi w chwili $\tau _{x}$. Ponieważ jak wiadomo, predykat ten jest stabilny i $\tau _{x}\leq \tau _{e}$ , $deadlock({\mathcal {PD}}^{*})$ zachodzi również w chwili $\tau$.

Dowodzi to pierwszego stwierdzenia implikacji b). Zauważmy na koniec, że jeżeli istnieje zbiór ${\mathcal {B}}$, dla którego $deadlock({\mathcal {B}})[\tau _{b}]=True$, to z własności (W1) oraz (W2) wnioskujemy, że ${\mathcal {B}}\in {\mathcal {P}}\setminus {\mathcal {PD}}^{*}$. Tym samym drugie stwierdzenie implikacji b) zostało udowodnione.

<< Poprzedni slajd | Spis treści | Następny slajd >>