Глобальные свойства системы

Глобальные свойства системы — это предикаты от согласованных срезов системы (состояния процессов плюс сообщения в пути), которые бывают двух видов:

• стабильные предикаты;
• нестабильные предикаты.

Говорить "предикат сейчас верен" или "предикат сейчас неверен" некорректно, потому что нет "сейчас". Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе.

Пусть $G$ и $H$ — согласованные срезы. Будем говорить, что $G \le H$, если H достижимо из G (т.е. $G \subseteq H$ в смысле событий).

Определение:

Предикат $P$ является стабильным, если для любых согласованных срезов $G \le H$ из $P(G)$ следует $P(H)$.

Примеры стабильных предикатов: deadlock, завершение работы, потеря токена в алгоритм передаче токена по кругу.

Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина. Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени").

Определение:

Предикат $P$ является нестабильным, если он не является стабильным.

Нестабильные предикаты сложно искать, потому что может быть множество разных согласованных срезов, которые не вкладываются друг в друга. Поэтому просто снять несколько согласованных срезов не поможет: мы можем не попасть в нужный.

Определение:

Предикат $P$ является локальным, если он зависит только от состояния одного конкретного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0).

Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного.