Изменения

Пусть E - система Мотивация: если у распределенной системы нет «глобального состояния», то как запомнить её состояние на основе событий (event-based system) диске, чтобы можно было продолжить работу после восстановления с полным порядком (<tex>\prec</tex>) в рамках каждого процесса. Тогда <br>'''Срез''' ''F'' - любое подмножество ''E'' такое, что <tex>f \in F, e \prec f \Rightarrow e \in F</tex>диска?

Пусть $E$ — множество событий с полным порядком ($<$) в рамках каждого процесса.{{Определение|definition='''Согласованный срезСрез''' $F$ — подмножество $E$ такое, что если $e < f \in F$, то $e \in F$.}}{{Определение|definition=''G'Согласованный срез' - любое подмножество ''$G$ — подмножество $E'' $ такое, что <tex>\forall f \in E, \forall g \in G : f \rightarrow g \Rightarrow f \in G</tex>.}}Это означает, что не существует сообщения переданного "через срез" в обратную сторону, т.е не бывает такого, что событие отправки сообщения не вошло в согласованный срез, а принятия вошло (см. рисунок <tex>m_1</tex> - несогласованный срез, <tex>m_2</tex> - согласованный срез). Можем говорить о том, что согласованный срез показывает некий глобальный снимок нашей системы.

Это означает[[Файл:Consistent.png]] Эквивалентное определение: не существует $f \in G, e \in E \setminus G$ таких, что $e \to f$. Пусть $G$ и $H$ — согласованные срезы. Будем говорить, что $G \le H$, если H достижимо из G (т.е. $G \subseteq H$ в смысле событий). == Теоремы ===== Нижняя граница для срезов ===Заметим, что если есть два согласованных среза $G_1$ и $G_2$, то срез $G_1 \cap G_2$ тоже согласован и, более того, $(G_1 \cap G_2) \le G_1, G_2$.Доказательство: рассмотрим, какие сообщения могут пересылаться между различными частями системы:{|border="1" style="text-align: center"|откуда\куда|$G_1 \cap G_2$|$G_1 \cap \bar G_2$|$\bar G_1 \cap G_2$|$\bar G_1 \cap \bar G_2$|-|$G_1 \cap G_2$ || + || + || + || +|-|$G_1 \cap \bar G_2$ || - || + || - || +|-|$\bar G_1 \cap G_2$ || - || - || + || +|-|$\bar G_1 \cap \bar G_2$ || - || - || - || +|-|} Заметим, что не существует сообщения переданного &quot;сообщений, которые бы пересылались из $E \setminus (G_1 \cap G_2)$ в $G_1 \cap G_2$, что и требовалось. === Признак согласованности среза через&quot; векторные часы ===Если у нас есть срез $G$, в обратную сторонукотором векторные часы последних отправленных сообщений всех процессов попарно несравнимы, тто этот срез согласован.Используется в алгоритме поиска слабого конъюнктивного предиката.е  Доказательство от противного: пусть $G$ не бывает такогосогласован, что тогда есть два события $f \in G$, $e \in E \setminus G$, причём $e \to f$. Тогда рассмотрим $e'$ — последнее событие отправки сообщения не вошло $proc(e)$ в согласованный срезсрезе $G$ (очевидно, а принятия вошло $e' \le e$) и $f'$ — последнее событие $proc(f)$ в срезе $G$ (смочевидно, что $f \le f'$). рисунок <tex>m_1</tex> - несогласованный срезТогда $e' \le e \to f \le f'$, т.е. $e' \to f'$, <tex>m_2</tex> - согласованный среза тогда $VC(e') \le VC(f'). Можем говорить о том$, что согласованный срез показывает некий глобальный снимок нашей системыпротиворечие.[[ФайлОбратное, впрочем, неверно:Consistentможно рассмотреть ситуацию, в которой один поток отправил одно сообщение второму. Тогда у них векторные часы $(1, 0)$ и $(1, 1)$, они сравнимы, но срез согласованный.png|left]]