Zusammenfassung

  • Happened-before ist die kleinste partielle Ordnung aus lokaler Prozessreihenfolge, dem Senden vor dem Empfang derselben Nachricht und dem transitiven Abschluss dieser Beziehungen.
  • Die Clock Condition gilt nur vorwärts: a → b verlangt C(a) < C(b). Ein kleinerer Skalarwert beweist nicht, dass a b verursacht, informiert oder physisch früher stattgefunden hat.
  • Gleichzeitige, also nebenläufige Ereignisse besitzen in keiner Richtung einen happened-before-Pfad. Sie sind im beobachteten Modell ungeordnet, nicht zwingend zur selben physikalischen Zeit eingetreten.

Zwei Dienste liefern scheinbar eindeutige Datensätze. Ereignis A trägt die logische Zeit 41, B die 42. Das Dashboard sortiert, zeichnet einen Pfeil und legt nahe, A habe B verursacht. Die Zahlen machen die Geschichte einfach. Sie machen sie nicht bewiesen.

Leslie Lamports Aufsatz Time, Clocks, and the Ordering of Events in a Distributed System von 1978 suchte keine verborgene Weltuhr. Er zog eine präzise Grenze: Welche Ordnung darf ein verteiltes System ohne eine solche Uhr überhaupt rechtfertigen?

Die kleinste Ordnung aus beobachtbaren Kanten

Lamport modelliert Prozesse mit jeweils einer Ereignisfolge, die durch Nachrichten verbunden sind. Happened-before ist die kleinste Relation mit drei Regeln: Innerhalb eines Prozesses geht ein früheres einem späteren Ereignis voraus; das Senden geht dem Empfang derselben Nachricht voraus; und die Relation ist transitiv.

„Kleinste“ bedeutet, dass Lücken nicht mit Vermutungen gefüllt werden. Wenn weder a → b noch b → a gilt, sind die Ereignisse nebenläufig. Das Modell erfindet keine Reihenfolge, nur um eine saubere Zeitleiste zu liefern.

Lamport deutet a → b so, dass a b kausal beeinflussen kann. Es gibt einen Weg, über den Information wandern könnte. Das beweist weder, dass der Inhalt von a das Ergebnis von b tatsächlich verändert hat, noch Absicht oder Verantwortung. Kausale Erreichbarkeit und semantische Ursache sind unterschiedliche Beweisgegenstände.

Schon die Ereignisdefinition beeinflusst den Graphen. Eine Fußnote nennt den Empfang als Setzen eines Interrupt-Bits oder als Ausführung des Handlers; je nach Wahl ändert sich die Reihenfolge. Vor der Chronologie muss deshalb die Version dessen feststehen, was als Ereignis zählt.

Eine Implikation ohne Umkehrschluss

Eine logische Uhr ordnet jedem Ereignis eine Zahl zu. Die Clock Condition fordert: Gilt a → b, dann C(a) < C(b). Jeder Prozess erhöht seinen Zähler zwischen Ereignissen, versieht Nachrichten mit dem aktuellen Wert und setzt beim Empfang seine Uhr hinter den eigenen und den empfangenen Wert.

Diese Regeln erhalten bekannte Pfeile. Sie erlauben nicht den Umkehrschluss. Aus C(a) < C(b) folgt nicht a → b.

Das ist keine kleine Implementierungslücke. Würde jeder Zahlenvergleich happened-before beweisen, müssten nebenläufige Ereignisse denselben Wert tragen. Ein Ereignis kann jedoch mit zwei Ereignissen nebenläufig sein, die in einem anderen Prozess untereinander geordnet sind. Alle gleichzusetzen würde deren lokale Ordnung verletzen.

Die skalare Uhr bestätigt, dass eine bekannte Kante nicht numerisch umgedreht wurde. Sie bestätigt keine Kausalkante für jedes ansteigende Paar.

Eine Totalordnung ist eine Richtlinie

Manche Anwendungen brauchen eine Entscheidung, obwohl die partielle Ordnung mehrere zulässt. Lamport sortiert nach logischer Zeit und löst Gleichstände mit einer festen Prozessordnung. So entsteht eine mit happened-before konsistente Totalordnung.

Sie ist aber nicht eindeutig. Andere gültige Uhren oder andere Tie-Breaker können eine andere Linearisierung erzeugen. Eindeutig durch das Ereignissystem bestimmt ist allein die partielle Ordnung.

Eine Warteschlange oder Replikation darf eine deterministische Reihenfolge wählen. Sie muss den Tie-Breaker als Kontrollregel ausweisen. Wird er als Entdeckung der Vergangenheit dargestellt, wird eine Betriebsentscheidung zu einer falschen historischen Tatsache.

Der Anruf außerhalb des Systems

Lamports Beispiel für „anomales Verhalten“ beschreibt eine Person, die Anfrage A an einem Computer stellt, anschließend einen Freund in einer anderen Stadt anruft und ihn B stellen lässt. Weil das Telefonat außerhalb des Rechnersystems liegt, kann B einen kleineren Zeitstempel erhalten und vor A erscheinen.

Kein Algorithmus, der nur interne Ereignisse sieht, kann eine nie beobachtete Kante rekonstruieren. Lamport nennt zwei Wege: die fehlende Ordnungsinformation explizit ins System tragen oder unter stärkeren Annahmen ausreichend synchronisierte physische Uhren verwenden.

Heute kann die fehlende Kante ein Support-Anruf, eine menschliche Freigabe, ein Webhook oder eine externe Queue sein. „Kein Pfad gefunden“ bedeutet nur „kein Pfad in dieser Erfassung“, nicht „kein Einfluss in der Welt“.

Logische, vektorielle und physische Zeit

Lamports skalare Uhr bewahrt die Vorwärtsimplikation und ermöglicht eine konsistente Totalordnung. Rund zehn Jahre später entwickelten Colin Fidge und Friedemann Mattern Vektorzeitstrukturen, die mehr von der partiellen Ordnung erhalten. Mattern zeigte, dass die Abbildung auf linear geordnete ganze Zahlen Information verliert: möglicherweise nebenläufige Ereignisse bekommen verschiedene Werte, als wären sie eindeutig geordnet.

Vektoren können unvergleichbar bleiben, wenn keines der Ereignisse in der kausalen Vergangenheit des anderen liegt. Das hilft bei Fehlersuche, Snapshots und Konflikten. Auch diese Aussage hängt von den aufgezeichneten Prozessen, Ereignissen und Nachrichten ab; sie entdeckt keinen fehlenden Anruf und beweist kein menschliches Motiv.

Physische Uhren beantworten eine andere Frage. Lamports eigener Aufsatz behandelt später Strong Clock Condition, Gangfehler, Drift, minimale Nachrichtenlaufzeit und Synchronisationsgrenzen. Diese Annahmen nähern Markierungen der physischen Zeit mit ausgewiesener Unsicherheit an; sie machen aus einem logischen Zähler keine Wanduhr.

Auch die Urheberschaft braucht klare Grenzen. Lamport formulierte happened-before und skalare logische Uhren und würdigte Paul Johnson und Bob Thomas für die frühere Idee der Nachrichtenzeitstempel. Vektoruhren gehören zu den späteren Arbeiten von Fidge und Mattern.

Was ein Ordnungsbeleg enthalten muss

Eine belastbare Untersuchung nennt Ereignisdefinition und Version, Prozess, lokale Sequenz, Nachrichten-ID, Sende-Empfangs-Paar, Uhrenalgorithmus und Telemetriegrenze. Für physische Reihenfolge kommen Uhrenquelle und Fehler hinzu; für Ursache der Mechanismus, der das Ergebnis verändert hat.

Dann kann die Aussage präzise lauten: happened-before im erfassten Modell; nebenläufig in diesem Modell; durch Tie-Breaker früher gesetzt; physisch früher innerhalb einer Unsicherheit; oder semantische Ursache noch unbelegt.

Lamports Beitrag war keine Erlaubnis, alles zu sortieren und Wahrheit zu nennen. Er trennte die Ordnung, die ein System kennt, von der Ordnung, die es wählt, und jener, die es noch nicht beweisen kann.

Quellen