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 ${\mathcal {D}}_{i}={\mathcal {D}}_{i}^{1}\cup {\mathcal {D}}_{i}^{1}\cup \ldots {\mathcal {D}}_{i}^{q_{i}}$, liczby naturalne $k_{i}^{1},k_{i}^{2},\ldots ,k_{i}^{q_{i}}$, i liczby naturalne $r_{i}^{1},r_{i}^{2},\ldots ,r_{i}^{q_{i}}$, gdzie ${\mathcal {D}}_{i}\subseteq {\mathcal {P}}$ oraz dla każdego naturalnego $u$, $1\leq u\leq q_{i}$, $1\leq k_{i}^{u}\leq 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 ${\mathcal {D}}_{i}^{1}$, lub wiadomości od co najmniej $k_{i}^{2}$ różnych procesów ze zbioru ${\mathcal {D}}_{i}^{2}$, lub... lub wiadomości od co najmniej $k_{i}^{q_{i}}$ różnych procesów ze zbioru ${\mathcal {D}}_{i}^{q_{i}}$,. Wówczas:

$deadlock({\mathcal {B}})\equiv$

$\qquad ({\mathcal {B}}\subseteq {\mathcal {P}})\land ({\mathcal {B}}\neq \emptyset )\land$

$\qquad \forall P_{i}::P_{i}\in {\mathcal {B}}(passive_{i}\land (\forall u,1\leq u\leq q_{i}::$

$\qquad (\exists {\mathcal {B}}_{i}^{u}\subseteq {\mathcal {D}}_{i}^{u}\cap {\mathcal {B}}::$

$\qquad (|{\mathcal {D}}_{i}^{u}\setminus {\mathcal {B}}_{i}^{u}|<k_{i}^{u}\land$

$\qquad (\forall P_{j}::P_{j}\in {\mathcal {B}}_{i}^{u}::(\neg in{\mbox{-}}transit_{i}[j]\land \neg available_{i}[j]))))))$

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