Случилось-раньше

В информатике произошло -раньше отношение (обозначается: $\to \;$ ) — это отношение между результатом двух событий, такое, что если одно событие должно произойти раньше другого события, результат должен это отражать, даже если эти события в действительности выполняются не по порядку (обычно для оптимизации потока программы). Это предполагает упорядочивание событий на основе потенциальной причинно-следственной связи пар событий в параллельной системе, особенно в асинхронных распределенных системах . Его сформулировал Лесли Лэмпорт . ^[1]

Отношение «произошло до» формально определяется как наименее строгий частичный порядок событий, такой что:

Если события $a\;$ и $b\;$ происходят в рамках одного и того же процесса, $a\to b\;$ если наступление события $a\;$ предшествовало наступлению события $b\;$ .
Если событие $a\;$ это отправка сообщения и события $b\;$ это прием сообщения, отправленного в событии $a\;$ , $a\to b\;$ .

Если два события происходят в разных изолированных процессах (которые не обмениваются сообщениями прямо или косвенно через сторонние процессы), то два процесса называются параллельными, что не является ни тем, ни другим. $a\to b$ ни $b\to a$ это правда. ^[2]

Если между событиями в данной системе существуют другие причинно-следственные связи, например, между созданием процесса и его первым событием, эти отношения также добавляются в определение. Например, в некоторых языках программирования, таких как Java, ^[3] В C, C++ или Rust край «происходит до» существует, если память, записанная оператором A, видна оператору B, то есть, если оператор A завершает запись до того, как оператор B начинает чтение.

Как и все строгие частичные порядки, отношение «произошло до» является транзитивным , иррефлексивным (и бессмысленным, асимметричным ), т.е.:

$\forall a,b,c$ , если $a\to b\;$ и $b\to c\;$ , затем $a\to c\;$ (транзитивность). Это означает, что для любых трех событий $a,b,c$ , если $a$ случилось раньше $b$ , и $b$ случилось раньше $c$ , затем $a$ должно быть, это произошло раньше $c$ .
$\forall a,a\nrightarrow a$ (иррефлексивность). Это означает, что ни одно событие не может произойти раньше самого себя.
$\forall a,b,$ если $a\to b$ затем $b\nrightarrow a$ (асимметрия). Это означает, что для любых двух событий $a,b$ , если $a$ случилось раньше $b$ затем $b$ не могло случиться раньше $a$ .

Заметим, что свойство асимметрии непосредственно вытекает из предыдущих свойств: от противного предположим, что $\forall a,b,$ у нас есть $a\to b\;$ и $b\to a$ . Тогда по транзитивности имеем $a\to a,$ что противоречит иррефлексивности.

Процессы, составляющие распределенную систему, не знают об отношении «произошло до», если только они не используют логические часы , такие как часы Лэмпорта или векторные часы . Это позволяет разрабатывать алгоритмы взаимного исключения и решать такие задачи, как отладка или оптимизация распределенных систем.

См. также

Цитаты

^ Лэмпорт, Лесли (1978). «Время, часы и порядок событий в распределенной системе» , Communications of ACM , 21 (7), 558-565.
^ «Распределенные системы, 3-е издание (2017 г.)» . РАСПРЕДЕЛЕННЫЕ-СИСТЕМЫ.NET . Проверено 20 марта 2021 г.
^ Гетц и др. 2006 , стр. 339–342, §16.1.3 Модель памяти Java в 500 словах или меньше.

Ссылки

Гетц, Брайан; Пайерлс, Тим; Блох, Джошуа; Боубир, Джозеф; Холмс, Дэвид; Леа, Дуг (2006). Параллелизм Java на практике . Эддисон Уэсли. ISBN 0-321-34960-1 .

[1] Лэмпорт, Лесли (1978). «Время, часы и порядок событий в распределенной системе» , Communications of ACM , 21 (7), 558-565.

[2] «Распределенные системы, 3-е издание (2017 г.)» . РАСПРЕДЕЛЕННЫЕ-СИСТЕМЫ.NET . Проверено 20 марта 2021 г.

[FOOTNOTEGoetzPeierlsBlochBowbeer2006339–342§16.1.3_The_Java_Memory_Model_in_500_words_or_less-3] Гетц и др. 2006 , стр. 339–342, §16.1.3 Модель памяти Java в 500 словах или меньше.

[1]

[2]

[3]