Pr-1st-1.1-m05-Slajd06

Warunek uaktywnienia

Ponadto, w dowolnej chwili aktywny proces $P_i$ może zmienić swój stan na pasywny, definiując jednocześnie zbiór warunkujący ${{𝒟}}_i$ (będący sumą zbiorów oczekiwanych nadawców wszystkich dopuszczalnych zdarzeń odbioru) oraz warunek uaktywnienia wyrażony przez predykat: $read{y}_i({𝒳})\equiv ({{𝒫}}_i^A\supseteq {𝒳})\wedge activat{e}_i({𝒳})$.

Po spełnieniu warunku uaktywnienia, proces $P_i$ zmienia swój stan na aktywny i w sposób atomowy (niepodzielny) pobiera z kanałów wejściowych wszystkie te wiadomości, których nadejście doprowadziło do spełnienia warunku uaktywnienia. Wprowadzimy jeszcze następujące oznaczenia:

$passiv{e}_i$ - zmienna logiczna (predykat) przyjmująca wartość True wtedy i tylko wtedy, gdy proces $P_i$ jest pasywny;

$availabl{e}_i$ - tablica [1…n] zmiennych logicznych procesu $P_i$ skojarzona z wiadomościami dostępnymi;

$availabl{e}_i[j]$ - j-ty element tablicy $availabl{e}_i$ przyjmujący wartość True wtedy i tylko wtedy, gdy dla $P_i$ jest dostępna wiadomość wysłana przez $P_j$;

$in\text{-}transi{t}_i$ - tablica zmiennych logicznych procesu $P_i$ skojarzona z wiadomościami transmitowanymi;

$in\text{-}transi{t}_i[j]$ - j-ty element tablicy $in\text{-}transi{t}_i$ przyjmujący wartość True wtedy i tylko wtedy, gdy wiadomość wysłana przez $P_j$ do $P_i$ należy do ${\mathit{L}}_{j,i}^T$, a więc jest transmitowana i nie jest jeszcze dostępna.

Niech ponadto:

${{𝒜}{𝒱}}_i=\{P_j:availabl{e}_i[j]=True\},{{ℐ}{𝒯}}_i=\{P_j:in\text{-}transi{t}_i[j]=True\}$.

Korzystając z powyższych oznaczeń, przedstawimy teraz formalne definicje zakleszczeń odpowiadające różnym modelom żądań: modelowi jednostkowemu, AND, OR, k spośród n, OR-AND, oraz modelowi predykatowemu. Dla uproszczenia, będziemy mówili o zakleszczeniu w określonym modelu, lub o modelu zakleszczenia.

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