Глобальные свойства системы — различия между версиями
Yeputons (обсуждение | вклад) |
м (rollbackEdits.php mass rollback) |
||
| (не показаны 4 промежуточные версии 2 участников) | |||
| Строка 7: | Строка 7: | ||
Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе. | Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе. | ||
| − | |||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
| Строка 16: | Строка 15: | ||
Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина. | Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина. | ||
Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени"). | Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени"). | ||
| + | |||
| + | Также в некоторых случаях их можно искать по-другому: как нестабильные предикаты (тогда можно найти наименьший согласованный срез), [[диффундирующие вычисления]], [[Локально стабильный предикат|локально-стабильные предикаты]]. | ||
{{Определение | {{Определение | ||
| Строка 26: | Строка 27: | ||
|definition= | |definition= | ||
Предикат $P$ является '''локальным''', если он зависит только от состояния одного конкретного процесса. | Предикат $P$ является '''локальным''', если он зависит только от состояния одного конкретного процесса. | ||
| + | Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0). | ||
}} | }} | ||
Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного. | Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного. | ||
Текущая версия на 11:44, 1 сентября 2022
Глобальные свойства системы — это предикаты от согласованных срезов системы (состояния процессов плюс сообщения в пути), которые бывают двух видов:
- стабильные предикаты;
- нестабильные предикаты.
Говорить "предикат сейчас верен" или "предикат сейчас неверен" некорректно, потому что нет "сейчас". Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе.
| Определение: |
| Предикат $P$ является стабильным, если для любых согласованных срезов $G \le H$ из $P(G)$ следует $P(H)$. |
Примеры стабильных предикатов: deadlock, завершение работы, потеря токена в алгоритм передаче токена по кругу.
Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина. Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени").
Также в некоторых случаях их можно искать по-другому: как нестабильные предикаты (тогда можно найти наименьший согласованный срез), диффундирующие вычисления, локально-стабильные предикаты.
| Определение: |
| Предикат $P$ является нестабильным, если он не является стабильным. |
Нестабильные предикаты сложно искать, потому что может быть множество разных согласованных срезов, которые не вкладываются друг в друга. Поэтому просто снять несколько согласованных срезов не поможет: мы можем не попасть в нужный.
| Определение: |
| Предикат $P$ является локальным, если он зависит только от состояния одного конкретного процесса. Например, если у процесса есть состояние (переменная) x, то локальным предикатом может быть (x < 0). |
Если у нас нестабильный предикат, но являющийся дизъюнкцией локальных предикатов, то надо просто попросить каждый процесс отследить свой локальный предикат на протяжении некоторого интервала и узнать, выполнялся ли там предикат хотя бы у одного.
