Pr-1st-1.1-m05-Slajd11: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Szopen (dyskusja | edycje)
Nie podano opisu zmian
m Zastępowanie tekstu – „ </math>” na „</math>”
Linia 8: Linia 8:




<math>deadlock(\mathcal{B}) \equiv </math>
<math>deadlock(\mathcal{B}) \equiv</math>


<math>\qquad ( \mathcal{B} \subseteq \mathcal{P} ) \land ( \mathcal{B} \ne \emptyset ) \land </math>
<math>\qquad ( \mathcal{B} \subseteq \mathcal{P} ) \land ( \mathcal{B} \ne \emptyset ) \land</math>


<math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land </math>
<math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land </math>


<math>\qquad (\exists\mathcal{B}_i :: \mathcal{B}_i \subseteq \mathcal{D}_i \cap \mathcal{B} :: </math>
<math>\qquad (\exists\mathcal{B}_i :: \mathcal{B}_i \subseteq \mathcal{D}_i \cap \mathcal{B} ::</math>


<math>\qquad (| \mathcal{D}_i \setminus \mathcal{B}_i | < k_i \land </math>
<math>\qquad (| \mathcal{D}_i \setminus \mathcal{B}_i | < k_i \land</math>


<math>\qquad (\forall P_j :: P_j \in \mathcal{B}_i :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>
<math>\qquad (\forall P_j :: P_j \in \mathcal{B}_i :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>
Linia 27: Linia 27:
Tak więc, <math>P_i</math> potencjalnie otrzyma co najwyżej
Tak więc, <math>P_i</math> potencjalnie otrzyma co najwyżej
<math>| \mathcal{D}_i \setminus \mathcal{B}_i |</math>
<math>| \mathcal{D}_i \setminus \mathcal{B}_i |</math>
wiadomości, co jednak nie wystarcza do uaktywnienia, gdyż <math>| \mathcal{D}_i \setminus \mathcal{B}_i | < k_i </math>.
wiadomości, co jednak nie wystarcza do uaktywnienia, gdyż <math>| \mathcal{D}_i \setminus \mathcal{B}_i | < k_i</math>.




[[Pr-1st-1.1-m05-Slajd10 | << Poprzedni slajd]] | [[Pr-1st-1.1-m05-toc|Spis treści ]] | [[Pr-1st-1.1-m05-Slajd12 | Następny slajd >>]]
[[Pr-1st-1.1-m05-Slajd10 | << Poprzedni slajd]] | [[Pr-1st-1.1-m05-toc|Spis treści ]] | [[Pr-1st-1.1-m05-Slajd12 | Następny slajd >>]]

Wersja z 10:50, 5 wrz 2023

Zakleszczenie w podstawowym modelu k spośród r

Zakleszczenie w podstawowym modelu k spośród r

W podstawowym modelu k spośród r, z pasywnym procesem Pi skojarzony jest zbiór warunkujący 𝒟i, liczba naturalna ki, 1ki|𝒟i|, oraz liczba naturalna ri=|𝒟i|. W modelu tym proces Pi staje się aktywny wówczas, gdy uzyska wiadomości od co najmniej ki różnych procesów ze zbioru warunkującego 𝒟i.


deadlock()

(𝒫)()

Pi::Pi(passivei

(i::i𝒟i::

(|𝒟ii|<ki

(Pj::Pji::(¬in-transiti[j]¬availablei[j]))))


Definicja powyższa oznacza, że dla każdego procesu Pi można znaleźć zbiór procesów i, od których nie jest możliwe otrzymanie wiadomości i i jednocześnie (Pj::Pji::(¬in-transiti[j]¬availablei[j])) Tak więc, Pi potencjalnie otrzyma co najwyżej |𝒟ii| wiadomości, co jednak nie wystarcza do uaktywnienia, gdyż |𝒟ii|<ki.


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