Pr-1st-1.1-m10-Slajd46

Twierdzenie 10.2

Twierdzenie 10.2

Jeżeli algorytm detekcji zakończenia statycznego jest wykonywany wchwili, gdy przetwarzanie aplikacyjne osiągnęło stan zakończenia statycznego, to algorytm ten zakończy się wskończonym czasie, stwierdzając wystąpienie zakończenia statycznego przetwarzania aplikacyjnego ($sTerminationDetecte{d}_{\alpha }$ = True ).

Dowód Jeżeli przetwarzanie aplikacyjne osiągnęło stan zakończenia wchwili ${\tau }^t$, to zgodnie zdefinicją, od tego momentu wszystkie procesy będą zawsze pasywne ($passiv{e}_i=True$ ), ich warunki uaktywnienia nie będą spełnione ($activat{e}_i({{𝒜}{𝒱}}_i)=False$), a ponadto w kanałach nie będzie znajdowała się żadna wiadomość aplikacyjna (${{ℐ}{𝒯}}_i=\mathrm{\varnothing }$).

Stąd, w skończonym czasie zostaną w systemie odebrane potwierdzenia od monitorów, i liczniki $notAc{k}_i$ przyjmą wartość 0. Oznaczmy tę chwilę przez ${\tau }^x$. Oczywiście ${\tau }^x>{\tau }^t$. Od momentu ${\tau }^x$ bieżący cykl detekcyjny nie będzie z pewnością wstrzymywany przez monitory.

Zauważmy jednak, że pewne monitory w tym cyklu mogły wysłać odpowiedzi REPLY przed momentem ${\tau }^t$. Stąd, dopiero następny cykl detekcyjny z pewnością przypisze już na stałe wszystkim zmiennym $contPassiv{e}_i$ wartość True.

W konsekwencji, przez cały kolejny cykl detekcyjny k+1 , wszystkie zmienne logiczne $contPassiv{e}_i$ będą miały wartość True dla każdego $i\in \{1,2,...n\}$. Po odebraniu zatem wiadomości REPLY i przyjęciu przez $sTerminationDetecte{d}_{\alpha }$ wartości True , algorytm zakończy się.

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