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: $recvN{o}_i\ge 0andsentN{o}_i\ge 0$ oraz $recvN{o}_i>1\vee (recvN{o}_i=1\wedge sentN{o}_i=0)$. Spostrzeżenie to można uprościć do postaci $recvN{o}_i=0\vee (recvN{o}_i=1\wedge sentN{o}_i>0)$.

Z kolei dla procesu inicjującego oczywiste jest, że zachodzi $recvN{o}_i=0\wedge sentN{o}_i\ge 0)$.

Dalej można wywnioskować, że w stanie zakończenia przetwarzania $\mathrm{\forall }{P}_i:recvN{o}_i\le sentN{o}_i$. Ponieważ żadne wiadomości ani sygnały nie są przesyłane, więc suma wszystkich $recvN{o}_i$ wszystkich procesów musi być równa sumie wszystkich $sentN{o}_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 $recvN{o}_i=sentN{o}_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 >>