Pr-1st-1.1-m06-Slajd32
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ę: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: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ą:
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:
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: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:
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
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:Tak więc, jeżeli algorytm zakończy się w chwili
, toNiech
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.
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
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:
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:
Z zależności i) otrzymujemy:
Z kolei z monotoniczności predykatu
oraz z powyższego równania wnioskujemy, że jeżeli zachodzi:to zachodzi również
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 >>