Pr-1st-1.1-m10-Slajd48

Szkic dowodu twierdzenia 10.3

Ponieważ cykle są inicjowane sekwencyjnie, istnieje taki moment ${\tau }^x$, że:

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

Udowodnimy, że jeżeli $sTerminationDetecte{d}_{\alpha }[{\tau }_e^{k+1}]=True$, to w chwili $\tau ={\tau }^x$ przetwarzanie aplikacyjne jest statycznie zakończone, a więc:

$Sterm({𝒫})[{\tau }^x]=True$

Innymi słowy wykażemy, że dla wszystkich procesów spełnione będą następujące warunki:

C1.$passiv{e}_i[{\tau }^x]=True$ (proces jest pasywny w chwili ${\tau }^x$)

C2. ${{ℐ}{𝒯}}_i[{\tau }^x]=\mathrm{\varnothing }$. (nie ma żadnych procesów, od których wiadomości jeszcze nie dotarły do $P_i$ )

C3. $activate({{𝒜}{𝒱}}_i)[{\tau }^x]=False$. (dostępne wiadomości nie wystarczają do uaktywnienia procesu)

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