Happened-Before

Ursache und Wirkung, bzw. Vergangenheit und Zukunft, in einer Lamport-Uhr

Happened-Before (englisch für „passierte vorher“) ist in der Informatik eine logische Beziehung zwischen zwei Zeitpunkten.

Die Happened-Before-Relation ist wichtig, um die Kausalordnung von Ereignissen in asynchronen verteilten Systemen zu bestimmen. Sie wurde von Leslie Lamport formuliert. Die Happened-Before-Relation wird im Allgemeinen durch eine logische Uhr implementiert. Umgekehrt definiert die Happened-Before-Relation die Uhrenbedingung für diese logische Uhr.

Um die relative Zeit zwischen zwei auftretenden Ereignissen in einem verteilten System ohne eine globale Uhr herauszufinden, benutzt man die Happened-Before-Relation (→), die für Lamport-Uhren wie folgt definiert ist:

• Wenn auf demselben Prozess a vor b stattfindet, dann a → b.
• Wenn ein Prozess eine Nachricht zu einem anderen Prozess sendet, dann a → b wenn a der Sender und b der Empfänger ist.
• Für drei Ereignisse a, b, c, wenn a → b und b → c, dann a → c (Transitivität).

Dabei wird der Wert der lokalen Uhr jeweils der Nachricht als Zeitstempel beigefügt.

Die Happend-Before-Relation nach Lamport liefert eine strikte partielle Ordnung für die Ereignisse. Sie ist nicht ausreichend, wenn man nebenläufige Ereignisse betrachten will. Die Nebenläufigkeit lässt sich an einer Lamport-Uhr nicht ablesen. Zwar ist eine Lamport-Uhr so aufgebaut, dass a → b $\Rightarrow$ Zeit(a) < Zeit(b) gilt. Die Umkehrung Zeit(a) < Zeit(b) $\Rightarrow$ a → b gilt jedoch nicht (bzw. nur auf demselben Prozess).

Um eine totale Ordnung von Ereignissen zu erhalten, kann man z. B. Vektoruhren benutzen.