Локально стабильный предикат

Материал из Викиконспекты
Версия от 11:44, 1 сентября 2022; Maintenance script (обсуждение | вклад) (rollbackEdits.php mass rollback)
(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)
Перейти к: навигация, поиск


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

Примеры

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

Поиск

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