Локально стабильный предикат — различия между версиями
Yeputons (обсуждение | вклад) |
Yeputons (обсуждение | вклад) |
||
| Строка 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
| Определение: |
| Стабильный предикат называется локально стабильным, если все процессы, участвующие в предикате, не меняют свое состояние после того, как предикат удовлетворен. |
Примеры
- Предикат "процессы и ждут друг друга" локально стабилен, потому что они ничего не делают;
- Предикат "в системе не более одного токена" стабилен в системе, в которой не появляются новые токены, но не локально стабилен, потому что из-за получения / отправки токена состояние процесса может меняться.
Поиск
Находим барьерно-синхронизированный интервал $[F, G]$. Если предикат выполняется просто в $F$, в $G$ или в обоих, то это ещё ничего не значит — эти срезы могут не быть согласованными. Однако если предикат выполнялся в $F$, и состояния всех процессов, участвующих в предикате, не поменялись между $F$ и $G$, то мы знаем, что предикат выполнялся на всех срезах между $F$ и $G$, включая обязательно существующий там согласованный. Это более сильное требование, чем просто "предикат выполнялся в F и в G".
