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}\leq \tau ^{x}\leq \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 $dTerminationDetected_{\alpha }[\tau _{e}^{k+1}]=True$, to $Dterm({\mathcal {P}})[\tau ^{t}]=True$. Oznacza to dalej, że są spełnione następujące dwa warunki dla każdego $Q_{i},i\in \{1,2,\ldots ,n\}$,

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

C5. $activate_{i}({\mathcal {AV}}_{i}\cup {\mathcal {IT}}_{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 >>