1632
правки
Изменения
м
Пусть $G$ и $H$ — согласованные срезы. Будем говорить, что $G \le H$, если H достижимо из G (т.е. $G \subseteq H$ в смысле событий).
rollbackEdits.php mass rollback
Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе.
{{Определение
|definition=
Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина.
Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени").
Также в некоторых случаях их можно искать по-другому: как нестабильные предикаты (тогда можно найти наименьший согласованный срез), [[диффундирующие вычисления]], [[Локально стабильный предикат|локально-стабильные предикаты]].
{{Определение
|definition=
Предикат $P$ является '''локальным''', если он зависит только от состояния одного конкретного процесса.
Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).
}}
Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного.
