Срез, согласованный срез — различия между версиями
Yeputons (обсуждение | вклад) |
Yeputons (обсуждение | вклад) |
||
| Строка 9: | Строка 9: | ||
{{Определение | {{Определение | ||
|definition= | |definition= | ||
| − | '''Согласованный срез''' $G$ — подмножество $E такое, что <tex>\forall f \in E, \forall g \in G : f \rightarrow g \Rightarrow f \in G</tex>. | + | '''Согласованный срез''' $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> - согласованный срез). Можем говорить о том, что согласованный срез показывает некий глобальный снимок нашей системы. | Это означает, что не существует сообщения переданного "через срез" в обратную сторону, т.е не бывает такого, что событие отправки сообщения не вошло в согласованный срез, а принятия вошло (см. рисунок <tex>m_1</tex> - несогласованный срез, <tex>m_2</tex> - согласованный срез). Можем говорить о том, что согласованный срез показывает некий глобальный снимок нашей системы. | ||
| Строка 16: | Строка 16: | ||
Эквивалентное определение: не существует $f \in G, e \in E \setminus G$ таких, что $e \to f$. | Эквивалентное определение: не существует $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$, что и требовалось. | ||
Версия 22:35, 2 июня 2019
Мотивация: если у распределенной системы нет «глобального состояния», то как запомнить её состояние на диске, чтобы можно было продолжить работу после восстановления с диска?
Пусть $E$ — множество событий с полным порядком ($<$) в рамках каждого процесса.
| Определение: |
| Срез $F$ — подмножество $E$ такое, что если $e < f \in F$, то $e \in F$. |
| Определение: |
| Согласованный срез $G$ — подмножество $E$ такое, что . |
Это означает, что не существует сообщения переданного "через срез" в обратную сторону, т.е не бывает такого, что событие отправки сообщения не вошло в согласованный срез, а принятия вошло (см. рисунок - несогласованный срез, - согласованный срез). Можем говорить о том, что согласованный срез показывает некий глобальный снимок нашей системы.
Эквивалентное определение: не существует $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$. Доказательство: рассмотрим, какие сообщения могут пересылаться между различными частями системы:
| откуда\куда | $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$, что и требовалось.
