Локально стабильный предикат — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
Строка 7: Строка 7:
 
* Предикат "процессы <tex>P</tex>  и <tex>Q</tex> ждут друг друга" локально стабилен, потому что они ничего не делают;
 
* Предикат "процессы <tex>P</tex>  и <tex>Q</tex> ждут друг друга" локально стабилен, потому что они ничего не делают;
 
* Предикат "в системе не более одного токена" стабилен в системе, в которой не появляются новые токены, но не ''локально'' стабилен, потому что из-за получения / отправки токена состояние процесса может меняться.
 
* Предикат "в системе не более одного токена" стабилен в системе, в которой не появляются новые токены, но не ''локально'' стабилен, потому что из-за получения / отправки токена состояние процесса может меняться.
 +
 +
== Поиск ==
 +
Находим [[Барьерная синхронизация (3 алгоритма)|барьерно-синхронизированный интервал]] $[F, G]$.
 +
Если предикат выполняется просто в $F$, в $G$ или в обоих, то это ещё ничего не значит — эти срезы могут не быть согласованными.
 +
Однако если предикат выполнялся в $F$, и состояния всех процессов, участвующих в предикате, не поменялись между $F$ и $G$, то мы знаем, что предикат выполнялся на всех срезах между $F$ и $G$, включая обязательно существующий там согласованный.
 +
Это более сильное требование, чем просто "предикат выполнялся в F и в G".

Версия 09:19, 3 июня 2019


Определение:
Стабильный предикат называется локально стабильным, если все процессы, участвующие в предикате, не меняют свое состояние после того, как предикат удовлетворен.

Примеры

  • Предикат "процессы [math]P[/math] и [math]Q[/math] ждут друг друга" локально стабилен, потому что они ничего не делают;
  • Предикат "в системе не более одного токена" стабилен в системе, в которой не появляются новые токены, но не локально стабилен, потому что из-за получения / отправки токена состояние процесса может меняться.

Поиск

Находим барьерно-синхронизированный интервал $[F, G]$. Если предикат выполняется просто в $F$, в $G$ или в обоих, то это ещё ничего не значит — эти срезы могут не быть согласованными. Однако если предикат выполнялся в $F$, и состояния всех процессов, участвующих в предикате, не поменялись между $F$ и $G$, то мы знаем, что предикат выполнялся на всех срезах между $F$ и $G$, включая обязательно существующий там согласованный. Это более сильное требование, чем просто "предикат выполнялся в F и в G".