Happened-before

В інформатиці, відношення відношення happened-before (англ. happened-before — «сталося раніше») (позначається: ${\displaystyle \to \;}$ ) - це відношення між результатом двох подій, таким чином, що якщо одна подія повинна відбутися до іншої події, результат повинен відображати це, навіть якщо ці події насправді виконуються поза порядком (як правило, для оптимізації потоку програми). Це включає впорядкування подій на основі потенційного причинно-наслідкового зв’язку пар подій у паралельній системі, особливо розподілених систем . Його сформулював Леслі Лампорт . Спеціально для Java відносини " раніше" - це гарантія того, що пам'ять, записана в оператор A, є видимою для оператора B, тобто те, що A завершує його запис до того, як твердження B розпочне його читання. [1] [ 6 січня 2020 у Wayback Machine.]

Ставлення happened-before формально визначається як найменш суворий частковий порядок подій:

• Якщо події ${\displaystyle a\;}$ і ${\displaystyle b\;}$ відбуваються в одному і тому ж процесі, ${\displaystyle a\to b\;}$ якщо поява події ${\displaystyle a\;}$ передує виникнення події ${\displaystyle b\;}$.
• Якщо подія ${\displaystyle a\;}$ це відправлення повідомлень та подія ${\displaystyle b\;}$ - це прийом повідомлень, відправлених у разі ${\displaystyle a\;}$, ${\displaystyle a\to b\;}$.

Якщо між подіями в даній системі існують інші причинно-наслідкові зв’язки, наприклад, між створенням процесу та його першою подією, ці зв'язки також додаються до визначення.

Як і всі суворі часткові порядки, відносини, що відбулися раніше, є транзитивними, нерефлексивними та антисиметричними, тобто:

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

Процеси, що складають розподілену систему, не знають відношення, що сталося раніше, якщо вони не використовують ^[en], наприклад, ^[en] або ^[en] . Це дозволяє розробляти алгоритми взаємного виключення та такі завдання, як налагодження чи оптимізація розподілених систем.