Pr-1st-1.1-m05-Slajd14

Zakleszczenie w modelu predykatowym

W modelu predykatowym dla każdego pasywnego procesu $P_i$ ze zbiorem warunkującym ${{𝒟}}_i$ i dla każdego zbioru ${𝒳}\subseteq {{𝒟}}_i$ zdefiniowany jest predykat $activat{e}_i({𝒳})$. 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:

$deadlock({ℬ})\equiv$

$({ℬ}\subseteq {𝒫})\wedge ({ℬ}\ne \mathrm{\varnothing })\wedge$

$\mathrm{\forall }{P}_i::P_i\in {ℬ}(passiv{e}_i\wedge \mathrm{\neg }availabl{e}_i({{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i\cup ({𝒫}\setminus {ℬ}))))$

Definicja ta oznacza, że żaden proces $P_i\in {ℬ}$ nie może być uaktywniony nawet jeżeli uwzględnimy wszystkie wiadomości znajdujące się aktualnie w kanałach od oczekiwanych nadawców (${{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i$) 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 $P_i\in {ℬ}$.

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 ${ℬ}=\{P_i\}$, zachodzi $deadlock({ℬ})$ i żaden inny proces nie jest zakleszczony. Ponieważ $P_i\in ̸{{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i$ otrzymujemy: ${{𝒜}{𝒱}}_i\cup {{ℐ}{𝒯}}_i\cup {𝒫}\setminus {ℬ}={𝒫}\setminus {ℬ}$ Z drugiej strony, ${{𝒟}}_i\subseteq {𝒫}\setminus {ℬ}={𝒫}\setminus \{P_i\}$ i stąd: $\mathrm{\neg }activat{e}_i({𝒫}\setminus {ℬ})\Rightarrow \mathrm{\neg }activat{e}_i({{𝒟}}_i)$. Otrzymujemy zatem sprzeczność, gdyż z założenia ${{𝒟}}_i\ne \mathrm{\varnothing }$, a z definicji predykatu $activat{e}_i({𝒳})$, $activat{e}_i({{𝒟}}_i)=True$.

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