Pr-1st-1.1-m05-Slajd14: Różnice pomiędzy wersjami
m Zastępowanie tekstu – „<math> ” na „<math>” |
m Zastępowanie tekstu – „ </math>” na „</math>” |
||
| Linia 7: | Linia 7: | ||
zdefiniowany jest predykat <math>activate_i(\mathcal{X})</math>. Predykat ten zachodzi, wtedy i tylko wtedy, gdy w związku z dostępnością wiadomości od wszystkich procesów tworzących zbiór, gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Wówczas: | zdefiniowany jest predykat <math>activate_i(\mathcal{X})</math>. Predykat ten zachodzi, wtedy i tylko wtedy, gdy w związku z dostępnością wiadomości od wszystkich procesów tworzących zbiór, gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Wówczas: | ||
<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 \neg available_i(\mathcal{AV}_i \cup \mathcal{IT}_i \cup | <math>\qquad \forall P_i :: P_i \in \mathcal{B} ( passive_i \land \neg available_i(\mathcal{AV}_i \cup \mathcal{IT}_i \cup | ||
| Linia 27: | Linia 27: | ||
<math>P_i \not\in \mathcal{AV}_i \cup \mathcal{IT}_i</math> | <math>P_i \not\in \mathcal{AV}_i \cup \mathcal{IT}_i</math> | ||
otrzymujemy: | otrzymujemy: | ||
<math>\mathcal{AV}_i \cup \mathcal{IT}_i \cup \mathcal{P} \setminus \mathcal{B} = \mathcal{P} \setminus \mathcal{B} </math> | <math>\mathcal{AV}_i \cup \mathcal{IT}_i \cup \mathcal{P} \setminus \mathcal{B} = \mathcal{P} \setminus \mathcal{B}</math> | ||
Z drugiej strony, | Z drugiej strony, | ||
<math>\mathcal{D}_i \subseteq \mathcal{P} \setminus \mathcal{B} = \mathcal{P} \setminus \{P_i\}</math> | <math>\mathcal{D}_i \subseteq \mathcal{P} \setminus \mathcal{B} = \mathcal{P} \setminus \{P_i\}</math> | ||
Aktualna wersja na dzień 10:49, 5 wrz 2023
Zakleszczenie w modelu predykatowym
W modelu predykatowym dla każdego pasywnego procesu ze zbiorem warunkującym i dla każdego zbioru zdefiniowany jest predykat . Predykat ten zachodzi, wtedy i tylko wtedy, gdy w związku z dostępnością wiadomości od wszystkich procesów tworzących zbiór, gotowe stanie się którekolwiek z dopuszczalnych zdarzeń odbioru. Wówczas:
Definicja ta oznacza, że żaden proces nie może być uaktywniony nawet jeżeli uwzględnimy wszystkie wiadomości znajdujące się aktualnie w kanałach od oczekiwanych nadawców () oraz potencjalne wiadomości od wszystkich procesów nie zakleszczonych. Dotarcie wszystkich tych wiadomości nie jest bowiem wystarczające dla spełnienia warunku uaktywnienia któregokolwiek z procesów .
Definicja zakleszczenia dla modelu predykatowego jest w pełni ogólna i może być dostosowana do innych, wcześniej omawianych modeli. Dlatego też ta definicja pozwala na jednorodne podejście do problemu zakleszczenia, abstrahując od konsekwencji szczególnych właściwości różnych modeli żądań.
Przy założeniu, że żaden proces nie osiąga stanu zakończenia, zakleszczenie dotyczy zawsze co najmniej dwóch procesów. Istotnie, przypuśćmy, że , zachodzi i żaden inny proces nie jest zakleszczony. Ponieważ otrzymujemy: Z drugiej strony, i stąd: . Otrzymujemy zatem sprzeczność, gdyż z założenia , a z definicji predykatu , .
