Глобальные свойства системы — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показано 7 промежуточных версий 3 участников)
Строка 1: Строка 1:
 
[[Категория: Параллельное программирование]]
 
[[Категория: Параллельное программирование]]
−
'''Глобальные свойства системы''' -- это предикаты, которые бывают двух видов:
+
'''Глобальные свойства системы''' — это предикаты от согласованных срезов системы (состояния процессов плюс сообщения в пути), которые бывают двух видов:
−
* стабильные предикаты  
+
* стабильные предикаты;
−
* нестабильные предикаты
+
* нестабильные предикаты.
  
−
Стабильные предикаты можно формализовать следующим образом:
+
Говорить "предикат сейчас верен" или "предикат сейчас неверен" некорректно, потому что нет "сейчас".
 +
Можно говорить "существует/не существует согласованный срез", но если у нас система ещё работает, то "не существует" мы можем заявить лишь на каком-то префиксе срезов системе.
  
−
Пусть G и H согласованные срезы, будем говорить, что G <= H, если H достижимо из G. Тогда B стабильный предикат тогда и только тогда, когда ∀ G, H: G <= H : B(G) ⇒ B(H), т.е В стабильный предикат, если однажды дав true, то остается true навсегда.
+
{{Определение
 +
|definition=
 +
Предикат $P$ является '''стабильным''', если для любых согласованных срезов $G \le H$ из $P(G)$ следует $P(H)$.
 +
}}
 +
Примеры стабильных предикатов: deadlock, завершение работы, потеря токена в алгоритм передаче токена по кругу.
  
−
Примеры стабильных предикатов: deadlock, termination, loss of token.
+
Такие предикаты можно найти наивно: снимаем согласованный сред (за $O(n^2)$ сообщений каждый раз) и смотрим, получилась ли истина.
 +
Если да — то был верен, если нет — то в какой-то "момент" был неверен (но "уже" может быть верен, у нас же нет "времени").
 +
 
 +
Также в некоторых случаях их можно искать по-другому: как нестабильные предикаты (тогда можно найти наименьший согласованный срез), [[диффундирующие вычисления]], [[Локально стабильный предикат|локально-стабильные предикаты]].
 +
 
 +
{{Определение
 +
|definition=
 +
Предикат $P$ является '''нестабильным''', если он не является стабильным.
 +
}}
 +
Нестабильные предикаты сложно искать, потому что может быть множество разных согласованных срезов, которые не вкладываются друг в друга.
 +
Поэтому просто снять несколько согласованных срезов не поможет: мы можем не попасть в нужный.
 +
{{Определение
 +
|definition=
 +
Предикат $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).

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

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=Глобальные_свойства_системы&oldid=84314»