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