Pr-1st-1.1-m09-Slajd19

Klasyczna definicja zakończenia a zakończenie statyczne

Rozważmy teraz relację między$Sterm({\mathcal {P}})$ a $Cterm({\mathcal {P}})$.

Twierdzenie 9.2

Jeżeli procesy są uaktywnione przez każdą dostępną wiadomość, to przetwarzanie rozproszone obejmujące zbiór procesów ${\mathcal {P}}$ jest statycznie zakończone wtedy i tylko wtedy, gdy zachodzi predykat $Cterm({\mathcal {P}})$.

Dowód W wypadku procesów uaktywnianych każdą wiadomością:

$\neg activate_{i}({\mathcal {AV}}_{i})\equiv ({\mathcal {AV}}_{i}=\emptyset )$

W konsekwencji:

$Sterm({\mathcal {P}})\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land ({\mathcal {IT}}_{i}=\emptyset )\land$

$\neg activate_{i}({\mathcal {AV}}_{i}))\equiv \forall P_{i}::P_{i}\in {\mathcal {P}}::(passive_{i}\land ({\mathcal {IT}}_{i}=\emptyset )\land ({\mathcal {AV}}_{i}=\emptyset )\equiv Cterm({\mathcal {P}})$

Warto zauważyć silne związki między pojęciami zakończenia i zakleszczenia. W istocie, zakończenie jest szczególnym wypadkiem zakleszczenia, w którym zakleszczone są wszystkie procesy przetwarzania rozproszonego.

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