Pr-1st-1.1-m09-Slajd44

Twierdzenie 9.3

Twierdzenie 9.3

Jeżeli przetwarzanie dyfuzyjne uległo zakończeniu, fakt ten ulega wykryciu przez algorytm Dijkstry-Scholtena.

Dowód Jeżeli przetwarzanie dyfuzyjne ulega zakończeniu, oznacza to, że nie ma żadnego aktywnego procesu ani nie ma żadnych wiadomości ani sygnałów w kanałach komunikacyjnych. Oznacza to także, że żaden proces nie może wysyłać żadnych wiadomości ani potwierdzeń. W związku z tym, można wywnioskować, że jeżeli przetwarzanie ulegnie zakończeniu, to w każdym procesie $P_{i}$ (za wyjątkiem procesu-inicjatora) zachodzi: $recvNo_{i}\geq 0\;andsentNo_{i}\geq 0$ oraz $recvNo_{i}>1\lor (recvNo_{i}=1\land sentNo_{i}=0)$. Spostrzeżenie to można uprościć do postaci $recvNo_{i}=0\lor (recvNo_{i}=1\land sentNo_{i}>0)$.

Z kolei dla procesu inicjującego oczywiste jest, że zachodzi $recvNo_{i}=0\land sentNo_{i}\geq 0)$.

Dalej można wywnioskować, że w stanie zakończenia przetwarzania $\forall P_{i}:recvNo_{i}\leq sentNo_{i}$. Ponieważ żadne wiadomości ani sygnały nie są przesyłane, więc suma wszystkich $recvNo_{i}$ wszystkich procesów musi być równa sumie wszystkich $sentNo_{i}$. Z tych dwóch wniosków oraz z spostrzeżenia tyczącego wartości zmiennych u inicjatora, wynika, że w wyniku zakończenia przetwarzania w procesie inicjatora zachodzi $recvNo_{i}=sentNo_{i}=0$, a ponieważ proces ten jest pasywny, więc zostaną spełnione warunki wykrycia zakończenia.

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