Pr-1st-1.1-m10-Slajd67

Szkic dowodu twierdzenia 10.5

Dowód Oznaczymy dwa ostatnie cykle detekcyjne odpowiednio przez k ik+1 , a przez ${\tau }^x$ taki moment, że:

${\tau }_b^k<{\tau }_e^k\le {\tau }^x\le {\tau }_b^{k+1}<{\tau }_e^{k+1}$

W dalszej części dowodu pokażemy, że jeżeli algorytm zakończy się w chwili ${\tau }_e^{k+1}$ z $dTerminationDetecte{d}_{\alpha }[{\tau }_e^{k+1}]=True$, to $Dterm({𝒫})[{\tau }^t]=True$. Oznacza to dalej, że są spełnione następujące dwa warunki dla każdego $Q_i,i\in \{1,2,\dots ,n\}$,

C4. $passiv{e}_i$ [${\tau }^x$] = True (Wszystkie procesy są pasywne w chwili ${\tau }^x$)

C5. $activat{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i)[{\tau }^x]=False$ (Ani wiadomości już dostępne, ani znajdujące się w kanałach komunikacyjnych nie wystarczą do uaktywnienia procesu $P_i$)

Dowód warunku C4 pomijamy, jako identyczny jak w przypadku warunku C1 dla twierdzenia o poprawności algorytmu zakończenia detekcji zakończenia statycznego.

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