Pr-1st-1.1-m05-Slajd14

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

Zakleszczenie w modelu predykatowym

Zakleszczenie w modelu predykatowym

W modelu predykatowym dla każdego pasywnego procesu ze zbiorem warunkującym i dla każdego zbioru zdefiniowany jest predykat . Predykat ten zachodzi, wtedy i tylko wtedy, gdy w związku z dostępnością wiadomości od wszystkich procesów tworzących zbiór, gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Wówczas:

Definicja ta oznacza, że żaden proces nie może być uaktywniony nawet jeżeli uwzględnimy wszystkie wiadomości znajdujące się aktualnie w kanałach od oczekiwanych nadawców () oraz potencjalne wiadomości od wszystkich procesów nie zakleszczonych. Dotarcie wszystkich tych wiadomości nie jest bowiem wystarczające dla spełnienia warunku uaktywnienia któregokolwiek z procesów .

Definicja zakleszczenia dla modelu predykatowego jest w pełni ogólna i może być dostosowana do innych, wcześniej omawianych modeli. Dlatego też ta definicja pozwala na jednorodne podejście do problemu zakleszczenia, abstrahując od konsekwencji szczególnych właściwości różnych modeli żądań.

Przy założeniu, że żaden proces nie osiąga stanu zakończenia, zakleszczenie dotyczy zawsze co najmniej dwóch procesów. Istotnie, przypuśćmy, że , zachodzi i żaden inny proces nie jest zakleszczony. Ponieważ otrzymujemy: Z drugiej strony, i stąd: . Otrzymujemy zatem sprzeczność, gdyż z założenia , a z definicji predykatu , .

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