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

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

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

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

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

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

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

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

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

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

• Состояние гонки
• Модель памяти Java
• Временные метки Лампорта
• Логические часы

• Goetz, Brian; Peierls, Tim; Bloch, Joshua; Bowbeer, Joseph; Holmes, David; Lea, Doug (2006). Java Concurrency in Practice. Addison Wesley. ISBN 0-321-34960-1.