Algorytm detekcji zakleszczenia dla modelu predykatowego (7)
Wysłanie wiadomości aplikacyjnej powoduje każdorazowo zwiększenie zmiennej
informującej o niepotwierdzonych wiadomościach wysłanych przez proces
.
Odebranie wiadomości aplikacyjnej przez monitor
powoduje dostarczenie tej wiadomości do procesu
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
.
W sytuacji w której proces staje się procesem aktywnym, zmiennej
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
moment czasu globalnego zakończenia cyklu k - tego w monitorze
, a więc moment wysłania znacznika z
do
w k - tym cyklu. Analogicznie,
oznaczać będzie moment zakończenia cyklu k - tego w monitorze inicjatora
, to znaczy moment zakończenia całego cyklu k. Ponadto, dla każdego elementu
(zmiennej, predykatu),
oznaczać będzie wartości elementu
w chwili
. W szczególności,
oznacza wartość zbioru
zawartego w znaczniku, w momencie wysłania znacznika przez monitor
w ramach k - tego cyklu detekcji. Przyjmiemy jeszcze następującą definicję:
![{\displaystyle contPassive_{i}^{*}(\tau ',\tau '')\equiv (\tau '\leq \tau '')\land \forall \tau ::\tau '\leq \tau \leq \tau ''::passive_{i}[\tau ]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/1a5b0ab5d6eec1e01aaae2b3093f8b8ea400f976)
Jeżeli algorytm detekcji zakleszczenia zostanie zainicjowany w chwili
, to zakończy się w skończonym czasie, w pewnej chwili
,
.
Dowód:
Zauważmy, że znacznik przebywający i przetwarzany w monitorze
jest natychmiast przesyłany dalej, gdy
. W przeciwnym razie, znacznik jest zatrzymywany i przechowywany w monitorze
aż do momentu
spełnienia następującego warunku:
![{\displaystyle (\neg contPassive_{i}[\tau ])\lor (activate_{i}({\mathcal {AV}}_{i}\cup ({\mathcal {P}}\setminus {\mathcal {PD}})[\tau ])\lor (notAck_{i}=0)[\tau ]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/228e569005dc9884ed29d0e55b70025599833398)
Oczywiście warunek
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
. Wówczas funkcja:
jest monotonicznie malejąca, z początkową wartością
. Stąd liczba cykli jest skończona, a więc w skończonym czasie algorytm detekcji zakończy się.
Niech
oraz
oznaczają odpowiednio moment rozpoczęcia i zakończenia algorytmu detekcji zakleszczenia:
- a) Jeżeli algorytm kończy się i zbiór
jest zbiorem pustym (
), to dla każdego zbioru
,
i
,
predykat
miał wartość
w chwili
.
- b) Jeżeli algorytm kończy się i zbiór
nie jest zbiorem pustym (
), to predykat
ma wartość
w chwili
. Ponadto dla każdego zbioru
, takiego, że
miał wartość
w chwili
,
jest podzbiorem zbioru
(
.
Dowód implikacji a)
W celu udowodnienia implikacji a), wykażemy następującą implikację równoważną:
![{\displaystyle (\exists {\mathcal {B}}::{\mathcal {B}}\subseteq {P}::deadlock({\mathcal {B}})[\tau _{b}])\Rightarrow ({\mathcal {PD}}[\tau _{e}]\neq \emptyset )}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/b7306f0c0f3d405178bbe4c4d32416870c5e14d5)
Zgodnie z założeniem, w chwili
zachodzi predykat deadlock(\mathcal{B}) i \mathcal{B}\ne \emptyset.
początkowo jest równe
i stąd oczywiście w chwili
, \mathcal{B} Í \mathcal{PD}. Ponieważ deadlock(\mathcal{B}) jest predykatem stabilnym, prawdą jest, że:

Stąd, korzystając z definicji zakleszczenia dla modelu predykatowego, otrzymujemy:
![{\displaystyle \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}}))}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/3395d79561224b26fdc15b429120e7c63a321148)
Wszystkie procesy
należące do \mathcal{B} są stale pasywne począwszy od chwili
, 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
, tuż przed możliwym usunięciem z
pewnego procesu
, zachodzi relacja
. Stale pasywny proces
może być usunięty z
, pod warunkiem, że spełniona jest w chwili
relacja:
![{\displaystyle activate_{i}({\mathcal {AV}}_{i}[\tau ]\cup {\mathcal {P}}\setminus {\mathcal {PD}}[\tau ])=True}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/6a326da1860089bee995f2674feab0a1850116b0)
Zauważmy jednak, że
.
Rozważmy teraz wiadomość, która stała się dostępna dla
w przedziale czasu
. Jej nadawca
albo należał do
, albo jest procesem należącym do
, którego kanał wyjściowy
nie był pusty w chwili
. Tak więc:
![{\displaystyle {\mathcal {AV}}_{i}[\tau ]\subseteq ({\mathcal {AV}}_{i}[\tau _{b}]\cup {\mathcal {IT}}_{i}[\tau _{b}]\cup {\mathcal {P}}\setminus {\mathcal {B}})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/6b6447a77736904e37de19dfb3716d54c5d2dd07)
Z postawionej hipotezy wiemy, że
, a stąd otrzymujemy:
.
Ponieważ
, powyższa relacja redukuje się do:
.
Zauważmy, że ostatnia równość jest w sprzeczności z przyjętym założeniem:
. 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
to otrzymujemy:

Dowód implikacji b)
Zgodnie z konstrukcją, algorytm kończy się w chwili
z wynikiem
wtedy i tylko wtedy, gdy
i ![{\displaystyle {\mathcal {PD}}[\tau _{\alpha }^{k}+1]\neq \emptyset }](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/9a30b957a078be91d00a76cd61acbcb0c9f535cc)
Niech
, spełnia relację
, Chwila taka istnieje, gdyż przykładowo
może być równe
. W szczególności zachodzi:

Ponieważ zbiór
może jedynie ulegać redukcji, otrzymujemy:
![{\displaystyle \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]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/59c1c485cb336975effc210fa4c47e599dcb143e)
Tak więc, jeżeli algorytm zakończy się w chwili
, to
![{\displaystyle \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]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/63ac836555397dda9e84a16e7f4de05c60a57adc)
Niech
będzie oznaczać zbiór spełniający powyższą zależność. Udowodnimy, że
zachodzi w chwili
, to znaczy, spełnione są w chwili
następujące warunki:
- C1.
i
- C2.
i
- C3.
![{\displaystyle (\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}}^{*})).}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/9d6e09630d5c9f3d3403bf22ac465b57448bd9fe)
Pokażemy teraz, że powyższe warunki są spełnione, jeżeli algorytm zakończy się z
. Z definicji warunku zakończenia wynika wprost, że jeżeli algorytm kończy się z
, to warunek C1 jest spełniony w chwili
.
Niech teraz
. Z konstrukcji algorytmu wynika, że tylko proces stale pasywny począwszy od zakończenia pierwszego cyklu w chwili
, może należeć do
. Stąd mamy:
, a więc ![{\displaystyle passive_{i}[\tau _{x}]}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/812554164b6c15ddb7f90d0a945ee02885ce609d)
Tym samym warunek C2 zajścia zakleszczenia został zweryfikowany. Ponieważ
, wnioskujemy z konstrukcji algorytmu , że:
.
W przeciwnym bowiem razie,
zostałby usunięty ze zbioru
. Ale, skoro
może tylko zmienić się przez dołączanie nowych elementów, a
nie zmienia się w przedziale
, otrzymujemy:
![{\displaystyle ({\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}}^{*})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/8c3d99602f67f7ac0019375eecac907a9a15324a)
Z konstrukcji algorytmu wnioskujemy dalej, że wszystkie kanały wyjściowe procesów należących do
są puste w chwili
, 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 (
).
Ponieważ procesy te są przy tym stale pasywne od pierwszej wizyty znacznika, ich kanały wyjściowe są puste w chwili
. Stąd:
i dlatego
.
W konsekwencji:
![{\displaystyle ({\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}}^{*})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/e4425f2955c3025a09447f7aaedd210232f0bfa0)
Z zależności i) otrzymujemy:
![{\displaystyle ({\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}}^{*})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/d09e4e582306298361c1a8894b1adff99dba5f67)
Z kolei z monotoniczności predykatu
oraz z powyższego równania wnioskujemy, że jeżeli zachodzi:
![{\displaystyle \neg activate_{i}({\mathcal {AV}}_{i}[\tau _{i}^{k}+1]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/f881ddbb09423bf38a1cc0d6338aa68d02f55374)
to zachodzi również
![{\displaystyle \neg activate_{i}({\mathcal {IT}}_{i}[\tau _{x}]\cup {\mathcal {AV}}_{i}[\tau _{x}]\cup {\mathcal {P}}\setminus {\mathcal {PD}}^{*})}](https://wazniak.mimuw.edu.pl/api/rest_v1/media/math/render/svg/237cf62e054531cbb0fd78ff4357af8c7f0f485b)
Z konstrukcji wnosimy dalej, że predykat jest spełniony dla wszystkich
. Tym samym warunek C3 został wykazany.
Powyższe punkty dowodzą, że predykat
zachodzi w chwili
. Ponieważ jak wiadomo, predykat ten jest stabilny i
,
zachodzi również w chwili
.
Dowodzi to pierwszego stwierdzenia implikacji b). Zauważmy na koniec, że jeżeli istnieje zbiór
, dla którego
, to z własności (W1) oraz (W2) wnioskujemy, że
. Tym samym drugie stwierdzenie implikacji b) zostało udowodnione.
<< Poprzedni slajd | Spis treści | Następny slajd >>