Pr-1st-1.1-m06-Slajd32

Algorytm detekcji zakleszczenia dla modelu predykatowego (7)

Wysłanie wiadomości aplikacyjnej powoduje każdorazowo zwiększenie zmiennej $notAc{k}_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 $notAc{k}_i$.

W sytuacji w której proces staje się procesem aktywnym, zmiennej $contPassiv{e}_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, ${𝒫}{𝒟}[{\tau }_i^k]$ oznacza wartość zbioru ${𝒫}{𝒟}$ zawartego w znaczniku, w momencie wysłania znacznika przez monitor $Q_i$ w ramach k - tego cyklu detekcji. Przyjmiemy jeszcze następującą definicję:

$contPassiv{e}_i^{*}({\tau }^{\prime },{\tau }^{″})\equiv ({\tau }^{\prime }\le {\tau }^{″})\wedge \mathrm{\forall }\tau ::{\tau }^{\prime }\le \tau \le {\tau }^{″}::passiv{e}_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\in ̸{𝒫}{𝒟}$. W przeciwnym razie, znacznik jest zatrzymywany i przechowywany w monitorze $Q_i$ aż do momentu $\tau$ spełnienia następującego warunku:

$(\mathrm{\neg }contPassiv{e}_i[\tau ])\vee (activat{e}_i({{𝒜}{𝒱}}_i\cup ({𝒫}\setminus {𝒫}{𝒟})[\tau ])\vee (notAc{k}_i=0)[\tau ]$

Oczywiście warunek $(contPassiv{e}_i[\tau ])\wedge (notAc{k}_i\ne 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 $|{𝒫}{𝒟}[{\tau }_{\alpha }^k]|>|{𝒫}{𝒟}[t_{\alpha }^{k+1}]|$. Wówczas funkcja: $k\to |{𝒫}{𝒟}[{\tau }_{\alpha }^k]|$ jest monotonicznie malejąca, z początkową wartością $|{𝒫}|=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 ${𝒫}{𝒟}$ jest zbiorem pustym (${𝒫}{𝒟}=\mathrm{\varnothing }$), to dla każdego zbioru ${ℬ}$,${ℬ}\ne \mathrm{\varnothing }$ i ${ℬ}\subseteq {𝒫}$,

predykat $deadlock({ℬ})$ miał wartość $False$ w chwili ${\tau }_b$.

b) Jeżeli algorytm kończy się i zbiór ${𝒫}{𝒟}$ nie jest zbiorem pustym (${𝒫}{𝒟}\ne \mathrm{\varnothing }$), to predykat $deadlock({𝒫}{𝒟})$ ma wartość $True$ w chwili ${\tau }_e$. Ponadto dla każdego zbioru

${ℬ}$, takiego, że $deadlock({ℬ})$ miał wartość $True$ w chwili ${\tau }_b$, ${ℬ}$ jest podzbiorem zbioru ${𝒫}{𝒟}$ (${ℬ}\subseteq {𝒫}{𝒟})$.

Dowód implikacji a)

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

$(\mathrm{\exists }{ℬ}::{ℬ}\subseteq P::deadlock({ℬ})[{\tau }_b])\Rightarrow ({𝒫}{𝒟}[{\tau }_e]\ne \mathrm{\varnothing })$

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

$\mathrm{\forall }\tau ::\tau \ge {\tau }_b::deadlock({ℬ})[\tau ]$ ${}^{(W1)}$

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

$\mathrm{\forall }\tau ::\tau \ge {\tau }_b::(\mathrm{\forall }{P}_i::P_i\in {ℬ}::passivei[\tau ]\wedge \mathrm{\neg }activat{e}_i({{ℐ}{𝒯}}_i[\tau ]\cup {{𝒜}{𝒱}}_i[\tau ]\cup {𝒫}\setminus {ℬ}))$

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 ${ℬ}$ nie może być usunięty z ${𝒫}{𝒟}$. Postawmy zatem hipotezę, że w chwili $\tau >{\tau }_b$, tuż przed możliwym usunięciem z ${𝒫}{𝒟}$ pewnego procesu $P_i$, zachodzi relacja ${ℬ}\subseteq {𝒫}{𝒟}$. Stale pasywny proces $P_i$ może być usunięty z ${𝒫}{𝒟}$, pod warunkiem, że spełniona jest w chwili $\tau$ relacja:

$activat{e}_i({{𝒜}{𝒱}}_i[\tau ]\cup {𝒫}\setminus {𝒫}{𝒟}[\tau ])=True$

Zauważmy jednak, że ${{𝒜}{𝒱}}_i[\tau ]={{𝒜}{𝒱}}_i[{\tau }_b]\cup \{P_k:\text{ wiadomości wysłane z }{P}_k\text{ do }{P}_i\text{ stały sie dostepne dla }{P}_i\text{ w przedziale }⟨{\tau }_b,\tau ⟩\}$.

Rozważmy teraz wiadomość, która stała się dostępna dla $P_i$ w przedziale czasu $⟨{\tau }_b,\tau ⟩$. Jej nadawca $P_j$ albo należał do ${𝒫}\setminus {ℬ}$, albo jest procesem należącym do ${ℬ}$, którego kanał wyjściowy $C_{j,i}$ nie był pusty w chwili ${\tau }_b$. Tak więc:

${{𝒜}{𝒱}}_i[\tau ]\subseteq ({{𝒜}{𝒱}}_i[{\tau }_b]\cup {{ℐ}{𝒯}}_i[{\tau }_b]\cup {𝒫}\setminus {ℬ})$

Z postawionej hipotezy wiemy, że $activatei({{𝒜}{𝒱}}_i[\tau ]\cup {𝒫}\setminus {𝒫}{𝒟}[\tau ])=True$, a stąd otrzymujemy:

$activat{e}_i({{𝒜}{𝒱}}_i[{\tau }_b]\cup {{ℐ}{𝒯}}_i[{\tau }_b]\cup {𝒫}\setminus {ℬ}\cup {𝒫}\setminus {𝒫}{𝒟}[\tau ])=True$.

Ponieważ ${ℬ}\subseteq {𝒟}{𝒫}[\tau ]$, powyższa relacja redukuje się do:

$activat{e}_i({{𝒜}{𝒱}}_i[{\tau }_b]\cup {{ℐ}{𝒯}}_i[{\tau }_b]\cup {𝒫}\setminus {ℬ})=True$.

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

Zauważmy jednak jeszcze, że gdy algorytm kończy się i ${𝒫}{𝒟}\ne \mathrm{\varnothing }$ to otrzymujemy:

${ℬ}\ne \mathrm{\varnothing }\wedge {ℬ}\subseteq {𝒫}{𝒟}$ ${}^{(W2)}$

Dowód implikacji b)

Zgodnie z konstrukcją, algorytm kończy się w chwili ${\tau }_e={\tau }_{\alpha }^k+1$ z wynikiem ${𝒫}{𝒟}\ne \mathrm{\varnothing }$ wtedy i tylko wtedy, gdy

${𝒫}{𝒟}[{\tau }_{\alpha }^k+1]|=|{𝒫}{𝒟}[{\tau }_{\alpha }^k]|$ i ${𝒫}{𝒟}[{\tau }_{\alpha }^k+1]\ne \mathrm{\varnothing }$

Niech ${\tau }_k$, spełnia relację $max({\tau }_i^k)\le {\tau }_k\le 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:

$\mathrm{\forall }{P}_i::P_i\in {𝒫}::{\tau }_i^k\le {\tau }_{\alpha }^k\le {\tau }_k\le {\tau }_i^k+1\le {\tau }_{\alpha }^k+1$

Ponieważ zbiór ${𝒫}{𝒟}$ może jedynie ulegać redukcji, otrzymujemy:

$\mathrm{\forall }{P}_i::P_i\in {𝒫}::{𝒫}{𝒟}[{\tau }_i^k]\supseteq {𝒫}{𝒟}[{\tau }_{\alpha }^k]\supseteq {𝒫}{𝒟}[{\tau }_k]\supseteq {𝒫}{𝒟}[{\tau }_i^k+1]\supseteq {𝒫}{𝒟}[{\tau }_{\alpha }^k+1]$

Tak więc, jeżeli algorytm zakończy się w chwili $\tau ={\tau }_{\alpha }^k+1i{𝒫}{𝒟}[\tau ]\ne \mathrm{\varnothing }$, to

$\mathrm{\forall }{P}_i::P_i\in {𝒫}::{𝒫}{𝒟}[{\tau }_{\alpha }^k]={𝒫}{𝒟}[{\tau }_k]={𝒫}{𝒟}[{\tau }_i^k+1]={𝒫}{𝒟}[{\tau }_{\alpha }^k+1]$

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

C1. ${{𝒫}{𝒟}}^{*}\ne \mathrm{\varnothing }$i

C2. $(\mathrm{\forall }{P}_i::P_i\in {{𝒫}{𝒟}}^{*}::passiv{e}_i[{\tau }_x])$ i

C3. $(\mathrm{\forall }{P}_i::P_i\in {{𝒫}{𝒟}}^{*}::\mathrm{\neg }activat{e}_i({{ℐ}{𝒯}}_i[{\tau }_x]\cup {{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*}))$.

Pokażemy teraz, że powyższe warunki są spełnione, jeżeli algorytm zakończy się z ${{𝒫}{𝒟}}^{*}\ne \mathrm{\varnothing }$. Z definicji warunku zakończenia wynika wprost, że jeżeli algorytm kończy się z ${{𝒫}{𝒟}}^{*}\ne \mathrm{\varnothing }$, to warunek C1 jest spełniony w chwili ${\tau }_k$. Niech teraz $P_i\in {{𝒫}{𝒟}}^{*}$. 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 ${{𝒫}{𝒟}}^{*}$. Stąd mamy:

$contPassiv{e}_i^{*}({\tau }_i^1,{\tau }_i^k+1)$, a więc $passiv{e}_i[{\tau }_x]$

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

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i[{\tau }_i^k]\cup {𝒫}\setminus {𝒫}{𝒟}*)=True$.

W przeciwnym bowiem razie, $P_i$ zostałby usunięty ze zbioru ${{𝒫}{𝒟}}^{*}$. Ale, skoro ${{𝒜}{𝒱}}_i$ może tylko zmienić się przez dołączanie nowych elementów, a ${𝒫}\setminus {{𝒫}{𝒟}}^{*}$ nie zmienia się w przedziale $⟨{\tau }_{\alpha }^k,{\tau }_{\alpha }^k+1⟩$, otrzymujemy:

$({{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})\subseteq {{𝒜}{𝒱}}_i[{\tau }_i^k+1]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})$

Z konstrukcji algorytmu wnioskujemy dalej, że wszystkie kanały wyjściowe procesów należących do ${{𝒫}{𝒟}}^{*}$ są puste w chwili ${\tau }_{\alpha }^k$, gdyż znacznik jest zatrzymywany przez monitor skojarzony z pasywnym procesem należącym do ${{𝒫}{𝒟}}^{*}$ do momentu uzyskania potwierdzeń dla wszystkich wysłanych wcześniej wiadomości ($notAc{k}_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:

$({{ℐ}{𝒯}}_i[{\tau }_x]\cap {{𝒫}{𝒟}}^{*})=0$ i dlatego ${{ℐ}{𝒯}}_i[{\tau }_x]\in {𝒫}\setminus {{𝒫}{𝒟}}^{*}$.

W konsekwencji:

$({{ℐ}{𝒯}}_i[{\tau }_x]\cup {{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})=({{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})$

Z zależności i) otrzymujemy:

$({{ℐ}{𝒯}}_i[{\tau }_x]\cup {{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})\subseteq ({{𝒜}{𝒱}}_i[{\tau }_i^k+1]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})$

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

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i[{\tau }_i^k+1]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})$

to zachodzi również

$\mathrm{\neg }activat{e}_i({{ℐ}{𝒯}}_i[{\tau }_x]\cup {{𝒜}{𝒱}}_i[{\tau }_x]\cup {𝒫}\setminus {{𝒫}{𝒟}}^{*})$

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

Powyższe punkty dowodzą, że predykat $deadlock({{𝒫}{𝒟}}^{*})$ zachodzi w chwili ${\tau }_x$. Ponieważ jak wiadomo, predykat ten jest stabilny i ${\tau }_x\le {\tau }_e$ , $deadlock({{𝒫}{𝒟}}^{*})$ zachodzi również w chwili $\tau$.

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

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