Pr-1st-1.1-m05-Slajd12: 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 – AND==
==Zakleszczenie w modelu OR – AND==


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


W modelu OR-AND zbiór warunkujący pasywnego procesu jest zdefiniowany jako  
W modelu OR-AND zbiór warunkujący pasywnego procesu jest zdefiniowany jako  
Linia 9: Linia 9:
<math>\mathcal{D}_i^u \subseteq \mathcal{P}</math>.
<math>\mathcal{D}_i^u \subseteq \mathcal{P}</math>.
Proces staje się aktywny po otrzymaniu wiadomości: od każdego z procesów tworzących zbiór <math>\mathcal{D}_i^1</math>, lub od każdego z procesów tworzących zbiór
Proces staje się aktywny po otrzymaniu wiadomości: od każdego z procesów tworzących zbiór <math>\mathcal{D}_i^1</math>, lub od każdego z procesów tworzących zbiór
<math>\mathcal{D}_i^2</math>, lub ... lub od każdego z procesów tworzących zbiór  <math>\mathcal{D}_i^{qi}</math>.
<math>\mathcal{D}_i^2</math>, lub... lub od każdego z procesów tworzących zbiór  <math>\mathcal{D}_i^{qi}</math>.




<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 \forall u, 1 \le u \le q_i</math>,
<math>\qquad \forall u, 1 \le u \le q_i</math>,
Linia 24: Linia 24:




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

Aktualna wersja na dzień 11:01, 5 wrz 2023

Zakleszczenie w modelu OR – AND

Zakleszczenie w modelu OR – AND

W modelu OR-AND zbiór warunkujący pasywnego procesu jest zdefiniowany jako 𝒟i1𝒟i1𝒟iqi, gdzie dla każdego naturalnego u, 1uqi, 𝒟iu𝒫. Proces staje się aktywny po otrzymaniu wiadomości: od każdego z procesów tworzących zbiór 𝒟i1, lub od każdego z procesów tworzących zbiór 𝒟i2, lub... lub od każdego z procesów tworzących zbiór 𝒟iqi.


deadlock()

(𝒫)()

Pi::Pi(passivei

u,1uqi,

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


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