Pr-1st-1.1-m07-Slajd16

Predykaty globalne i ich własności

Przez predykat globalny ${\mathit {\vartheta }}({\mathit {\Sigma }})$ będziemy rozumieć predykat zdefiniowany na zbiorze osiągalnych stanów globalnych przetwarzania rozproszonego.

Predykaty opisują właściwości przetwarzania w poszczególnych stanach. Szczególne znaczenie mają w praktyce predykaty stabilne (określane czasami własnościami stabilnymi. ang. stable properties ), których zajście w pewnym stanie globalnym ${\mathit {\Sigma }}$ implikuje, że dla każdego stanu ${\mathit {\Sigma }}'$ osiągalnego ze stanu ${\mathit {\Sigma }}$ predykat ten jest również prawdziwy. Innymi słowy, predykat jest nazywany stabilnym, gdy spełniany jest następujący warunek:

${\mathit {(}}\vartheta ({\mathit {\Sigma }}))\land ({\mathit {\Sigma }}\rightsquigarrow \Sigma '))\Rightarrow {\mathit {\vartheta }}({\mathit {\Sigma }}')$

gdzie ${\mathit {\Sigma }}\rightsquigarrow {\mathit {\Sigma }}'$ oznacza, że stan ${\mathit {\Sigma }}'$ jest osiągalny ze stanu $\Sigma$.

Predykaty, które nie spełniają tego warunku nazwiemy predykatami niestabilnymi .

Przykładami predykatów stabilnych są predykaty definiujące stan zakleszczenia, zakończenia przetwarzania, utraty znacznika, przekroczenia czasu obliczeń czy czasu transmisji itp.

Predykaty można także klasyfikować w inny sposób. Przykładem są tutaj predykaty słabe, które uznaje się za predykaty prawdziwe w przetwarzaniu rozproszonym, jeżeli istnieje taki spójny stan globalny, w którym są spełnione, oraz predykaty silne , które uznaje się za prawdziwe w przetwarzaniu rozproszonym wtedy, gdy są uznawane za prawdziwe w pewnej chwili przez wszystkich uczestników przetwarzania.

Duże znaczenie praktyczne posiadają też predykaty zdefiniowane na zbiorze wykonań ${\boldsymbol {\Upsilon }}$, a w szczególności predykaty possibly oraz definitely .

Predykat possibly (${\mathit {\boldsymbol {\vartheta }}}$) zachodzi wtedy i tylko wtedy, gdy istnieje wykonanie ${\mathit {\Upsilon }}\in {\boldsymbol {\Upsilon }}$ zawierające stan globalny ${\mathit {\Sigma }}$ , dla którego zachodzi predykat ${\mathit {\vartheta }}({\mathit {\Sigma }})$.

Predykat definitely (${\boldsymbol {\vartheta }}$) jest prawdziwy wtedy i tylko wtedy, gdy w każdym możliwym wykonaniu osiągalny jest stan ${\mathit {\Sigma }}$ , dla którego zachodzi ${\mathit {\vartheta }}({\mathit {\Sigma }})$.

W ogólności, wyznaczenie predykatów globalnych w pełni asynchronicznym systemie rozproszonym bez przyjęcia dodatkowych założeń jest niemożliwe, jeżeli chociaż jeden proces może ulec awarii.

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