Мотивация: если у распределенной системы нет «глобального состояния», то как запомнить её состояние на диске, чтобы можно было продолжить работу после восстановления с диска?
Пусть $E - система на основе $ — множество событий (event-based system) с полным порядком ($<tex>\prec</tex>$) в рамках каждого процесса. Тогда <br>{{Определение|definition='''Срез''' $F$ — подмножество $E$ такое, что если $e < f \in F$, то $e \in F$.}}{{Определение|definition=''F'Согласованный срез' - любое подмножество ''$G$ — подмножество $E'' $ такое, что <tex>\forall f \in FE, e \prec forall g \in G : f \rightarrow g \Rightarrow e f \in FG</tex>.}}Это означает, что не существует сообщения переданного "через срез" в обратную сторону, т.е не бывает такого, что событие отправки сообщения не вошло в согласованный срез, а принятия вошло (см. рисунок <tex>m_1</tex> - несогласованный срез, <tex>m_2</tex>- согласованный срез). Можем говорить о том, что согласованный срез показывает некий глобальный снимок нашей системы.
'''Согласованный срез''' ''G'' - любое подмножество ''E'' такое, что <tex>\forall f \in E, \forall g \in G [[Файл: f \rightarrow g \Rightarrow f \in G</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$ || - || - || - || +|-|} Заметим, что не существует сообщения переданного "сообщений, которые бы пересылались из $E \setminus (G_1 \cap G_2)$ в $G_1 \cap G_2$, что и требовалось. === Признак согласованности среза через" векторные часы ===Если у нас есть срез $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]]
