Pr-1st-1.1-m06-Slajd32

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Algorytm detekcji zakleszczenia dla modelu predykatowego (7)

Alg. detekcja 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 , to

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.

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 >>