Pr-1st-1.1-m05-Slajd13

Zakleszczenie w modelu dysjunkcyjnym k spośród r

W modelu dysjunkcyjnym k spośród r z każdym pasywnym procesem $P_i$ skojarzony jest zbiór warunkujący ${{𝒟}}_i={{𝒟}}_i^1\cup {{𝒟}}_i^1\cup \dots {{𝒟}}_i^{q_i}$, liczby naturalne $k_i^1,k_i^2,\dots ,k_i^{q_i}$, i liczby naturalne $r_i^1,r_i^2,\dots ,r_i^{q_i}$, gdzie ${{𝒟}}_i\subseteq {𝒫}$ oraz dla każdego naturalnego $u$, $1\le u\le q_i$, Parser nie mógł rozpoznać (błąd składni): {\displaystyle 1 \le k_^u \le r_i^u = | \mathcal{D}_i^u|} . Proces staje się aktywny po otrzymaniu: wiadomości od co najmniej $k_i^1$ różnych procesów ze zbioru ${{𝒟}}_i^1$, lub wiadomości od co najmniej $k_i^2$ różnych procesów ze zbioru ${{𝒟}}_i^2$, lub ... lub wiadomości od co najmniej $k_i^{q_i}$ różnych procesów ze zbioru ${{𝒟}}_i^{q_i}$, . Wówczas:

$deadlock({ℬ})\equiv$

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

$\mathrm{\forall }{P}_i::P_i\in {ℬ}(passiv{e}_i\wedge (\mathrm{\forall }u,1\le u\le q_i::$

$(\mathrm{\exists }{{ℬ}}_i^u\subseteq {{𝒟}}_i^u\cap {ℬ}::$

$(|{{𝒟}}_i^u\setminus {{ℬ}}_i^u|<k_i^u\wedge$

$(\mathrm{\forall }{P}_j::P_j\in {{ℬ}}_i^u::(\mathrm{\neg }in\text{-}transi{t}_i[j]\wedge \mathrm{\neg }availabl{e}_i[j]))))))$

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