Pr-1st-1.1-m09-Slajd19

Klasyczna definicja zakończenia a zakończenie statyczne

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

Twierdzenie 9.2

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

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

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i)\equiv ({{𝒜}{𝒱}}_i=\mathrm{\varnothing })$

W konsekwencji:

$Sterm({𝒫})\equiv \mathrm{\forall }{P}_i::P_i\in {𝒫}::(passiv{e}_i\wedge ({{ℐ}{𝒯}}_i=\mathrm{\varnothing })\wedge$

$\mathrm{\neg }activat{e}_i({{𝒜}{𝒱}}_i))\equiv \mathrm{\forall }{P}_i::P_i\in {𝒫}::(passiv{e}_i\wedge ({{ℐ}{𝒯}}_i=\mathrm{\varnothing })\wedge ({{𝒜}{𝒱}}_i=\mathrm{\varnothing })\equiv Cterm({𝒫})$

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 >>