292
правки
Изменения
Нет описания правки
Пусть $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$.
Доказательство: рассмотрим, какие сообщения могут пересылаться между различными частями системы:
Заметим, что не существует сообщений, которые бы пересылались из $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'$). Тогда $e' \le e \to f \le f'$, т.е. $e' \to f'$, а тогда $VC(e') \le VC(f')$, противоречие.
Обратное, впрочем, неверно: можно рассмотреть ситуацию, в которой один поток отправил одно сообщение второму. Тогда у них векторные часы $(1, 0)$ и $(1, 1)$, они сравнимы, но срез согласованный.
