Pr-1st-1.1-m07-Slajd16

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Predykaty globalne i ich własności

Predykaty globalne i ich własności


Przez predykat globalny 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 implikuje, że dla każdego stanu osiągalnego ze stanu predykat ten jest również prawdziwy. Innymi słowy, predykat jest nazywany stabilnym, gdy spełniany jest następujący warunek:

gdzie oznacza, że stan jest osiągalny ze stanu .

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ń , a w szczególności predykaty possibly oraz definitely .

Predykat possibly () zachodzi wtedy i tylko wtedy, gdy istnieje wykonanie zawierające stan globalny , dla którego zachodzi predykat .

Predykat definitely () jest prawdziwy wtedy i tylko wtedy, gdy w każdym możliwym wykonaniu osiągalny jest stan , dla którego zachodzi .

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