Изменения

Перейти к: навигация, поиск

Согласованный интервал

2656 байт добавлено, 19:28, 4 сентября 2022
м
rollbackEdits.php mass rollback
[[Категория: Параллельное программирование]]
Рассмотрим {{Определение|definition='''Интервал''' — упорядоченная пара [[Срез, согласованный срез|срезысрезов]](не обязательно согласованных) <tex>[G, H] ''</tex> такая, что <tex>G'' и ''\le H''.<br/tex>.}}{{Определение|definition=Интервал $[G, H]$ является '''Согласованный интервалсогласованным''' , если <tex>F = \{f \in Hforall e, g: \nexists g \in EG \setminus H: land e \rightarrow g\rightarrow fRightarrow e \}in H</tex>.}}Это значит, что нет сообщений, которые пересекают весь согласованный интервал в обратную сторону (или, что то же самое, нет и "произошло-до" в обратную сторону).Если взять $[G, G]$, то получим в точности определение согласованного среза.
Это значитТеорема: "интервал $[G, H]$ согласован" равносильно "существует согласованный срез $X$ внутри интервала: $G \le X \le H$". В одну сторону очевидно: если внутри интервала есть согласованный срез, то этот срез в обратную сторону сообщенияпересекать не могут. Значит, не могут они пересекать и весь интервал. В обратную сторону (на экзамене не требуется): рассмотрим произвольный согласованный интервал <tex>[G, H]</tex>.В доказательстве ниже будем считать, что $a \to a$ для простоты (но можно переписать доказательство и без рефлексивности). <tex>G</tex> может не быть согласованным срезом (если есть стрелочка из <tex>H \setminus G</tex> в <tex>G</tex>), что печально.Но можно попробовать пойти по стрелочкам в обратную сторону.Придумаем формальное "замыкание" <tex>G</tex>: возьмём множество <tex>X = \{ e \mid \exists g \in G \colon e \rightarrow g \}</tex>.* $G \subseteq X$ по построению (тут пользуемся тем, что нет сообщений через $a \to a$).* $X \subseteq H$, иначе есть стрелочка, пересекающая согласованный интервал в обратную сторону. Отсюда следует* $X$ является срезом, так как если есть $a < b$ и $b \in X$, есть $g \in G$ такое, что $b \rightarrow g$. По транзитивности имеем $a \rightarrow g$, что в согласованном интервале и требуется.* $X$ является согласованным срезом. Пусть есть события $a \rightarrow b$, причём $b \in X$. Тогда есть согласованный срезтакое $g \in G$, что $b \rightarrow g$. Следовательно, $a \rightarrow g$. Значит, $a \in X$, что и требовалось.
1632
правки

Навигация