Pr-1st-1.1-m05-Slajd10: 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>”
 
(Nie pokazano 2 wersji utworzonych przez 2 użytkowników)
Linia 1: Linia 1:
==Zakleszczenie w modelu OR==
==Zakleszczenie w modelu OR==


[[Image:pr-1st-1.1-m05-Slajd10.png|Zakleszczenie w modelu OR]]
[[Image:Pr-1st-1.1-m05-Slajd10.png|Zakleszczenie w modelu OR]]


W modelu OR do uaktywnienia procesu <math>P_i</math> wystarczy jedna wiadomość od któregokolwiek z procesów jego zbioru warunkującego <math>\mathcal{D}_i</math>. Dlatego:
W modelu OR do uaktywnienia procesu <math>P_i</math> wystarczy jedna wiadomość od któregokolwiek z procesów jego zbioru warunkującego <math>\mathcal{D}_i</math>. Dlatego:




<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  |\mathcal{D}_i|=1 \land </math>
<math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land  |\mathcal{D}_i|=1 \land</math>


<math> \qquad \mathcal{D} \subseteq \mathcal{B} \land </math>
<math>\qquad \mathcal{D} \subseteq \mathcal{B} \land</math>


<math>\qquad \qquad (\forall P_j :: P_j \in \mathcal{D}_i :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>
<math>\qquad \qquad (\forall P_j :: P_j \in \mathcal{D}_i :: (\neg in\mbox{-}transit_i[j] \land \neg available_i[j]))))</math>




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

Aktualna wersja na dzień 10:47, 5 wrz 2023

Zakleszczenie w modelu OR

Zakleszczenie w modelu OR

W modelu OR do uaktywnienia procesu Pi wystarczy jedna wiadomość od któregokolwiek z procesów jego zbioru warunkującego 𝒟i. Dlatego:


deadlock()

(𝒫)()

Pi::Pi(passivei|𝒟i|=1

𝒟

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


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