Pr-1st-1.1-m10-Slajd48

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Szkic dowodu twierdzenia 10.3

Szkic dowodu twierdzenia 10.3

Ponieważ cykle są inicjowane sekwencyjnie, istnieje taki moment , że:

Udowodnimy, że jeżeli , to w chwili przetwarzanie aplikacyjne jest statycznie zakończone, a więc:

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

C1. (proces jest pasywny w chwili )

C2. . (nie ma żadnych procesów, od których wiadomości jeszcze nie dotarły do )

C3. . (dostępne wiadomości nie wystarczają do uaktywnienia procesu)


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