Der große digitale Handschlag, der nie stattfand

Stellen Sie sich vor, Sie betreiben einen geschäftigen Limonadenstand. Sie haben zwei Aufgaben: Erstens schreiben Sie jeden verkauften Becher in Ihr offizielles Kassenbuch (die „Quelle“), und zweitens übergeben Sie dem Kunden eine Quittung (das „Senke“ oder „Sink“). In der perfekten Welt der Informatik möchten Sie beides exakt gleichzeitig tun, damit Sie – falls Ihnen der Stift herunterfällt – genau wissen, was passiert ist. Aber in der realen Welt geschehen Dinge in Schritten. Sie schreiben „Ein Becher“ in das Buch und übergeben dann die Quittung. Wenn ein plötzliches Gewitter Sie nachdem Sie die Zahl aufgeschrieben haben, aber bevor Sie die Quittung übergeben haben, niederstreckt, haben Sie ein Problem. Wenn Sie aufwachen, schauen in Ihr Buch, sehen, dass der Becher verkauft wurde, und denken: „Ich muss wohl vergessen haben, die Quittung zu übergeben!“ Also übergeben Sie eine zweite. Nun hat der Kunde zwei Quittungen für einen Becher.

Dies ist die Welt der „Dual Writes“ (doppelten Schreibvorgänge). Es ist die knifflige Situation, in der ein Computersystem zwei verschiedene Orte (wie eine Datenbank und eine Message Queue) separat aktualisieren muss. Wenn der Computer in der winzigen Lücke zwischen diesen beiden Aktualisierungen abstürzt, wird er verwirrt. Er weiß nicht, ob der zweite Ort die Nachricht bereits erhalten hat oder nicht. Jahrelang haben Ingenieure versucht, dies mit cleveren Tricks wie „Idempotenz-Schlüsseln“ (speziellen Tags, die sagen: „Das habe ich schon gesehen“) oder „Fencing“ (einer Barriere, die alte Nachrichten stoppt) zu lösen. Aber bis jetzt hatte niemand eine perfekte, mathematische Landkarte darüber, wann genau diese Tricks funktionieren und wann sie versagen. Dieses Paper ist diese Landkarte. Es verwendet eine superstrenge Art der Mathematik, die „formale Verifikation“, um mit absoluter Gewissheit zu beweisen, dass man nicht einfach nur in sein eigenes Notizbuch schauen kann, um zu wissen, ob die andere Seite die Nachricht erhalten hat. Man muss die andere Seite direkt fragen, und selbst dann muss man vorsichtig mit dem Timing sein.

Das Geheimnis der Geister-E-Mail

Tauchen wir ein in die Geschichte, die dieses Paper erzählt. Stellen Sie sich ein Computerprogramm vor, das Bestellungen verarbeitet. Es tut zwei Dinge: Es speichert die Bestellung in einer Datenbank und sendet dann eine E-Mail-Bestätigung. Das Programm ist darauf ausgelegt, „exactly-once“ (genau einmal) zu arbeiten, was bedeutet, dass jeder Kunde genau eine E-Mail erhält, nicht mehr und nicht weniger.

Eines Tages stürzt das Programm ab. Es hat die Bestellung in der Datenbank gespeichert, die E-Mail gesendet, aber es ist gestorben, bevor es eine Notiz in seinem eigenen „Checkpoint“-Log schreiben konnte: „Okay, ich habe diese E-Mail gesendet.“ Wenn das Programm aufwacht, schaut es in seinen Checkpoint. Es sieht: „Oh, ich habe die E-Mail für Bestellung Nr. 5 noch nicht gesendet!“ Also sendet es die E-Mail erneut. Der Kunde erhält zwei E-Mails. Die Ingenieure sind verwirrt: „Aber wir haben die Datenbank überprüft! Die Bestellung war da! Warum haben wir sie doppelt gesendet?“

Das Paper sagt: Hören Sie auf, dem Checkpoint die Schuld zu geben. Der Checkpoint hat seinen Job perfekt gemacht. Das Problem ist, dass der Checkpoint auf das Falsche schaut. Er schaut in das Gedächtnis des Senders, aber die Antwort liegt im Gedächtnis des Empfängers.

Der Autor hat ein mathematisches Modell gebaut, um zu beweisen, dass egal wie intelligent Ihr „Checkpoint“ oder Ihr „Cursor“ auch ist: Wenn Sie nur auf Ihrer eigenen Seite des Gesprächs schauen, sind Sie dazu verdammt, einen Fehler zu machen. Er erschuf zwei imaginäre Welten, die für den abgestürzten Computer identisch aussehen. In Welt A wurde die E-Mail vor dem Absturz erfolgreich zugestellt. In Welt B wurde die E-Mail nie zugestellt. Für den abgestürzten Computer sehen beide Welten exakt gleich aus. Er kann den Unterschied nicht erkennen. Wenn er sich also entscheidet, die E-Mail erneut zu senden, könnte er sie in Welt A versehentlich duplizieren. Wenn er sich entscheidet, die E-Mail nicht erneut zu senden, könnte er in Welt B eine Bestellung verlieren.

Die große Entdeckung: Sie können dies nicht lösen, indem Sie nur Ihre eigenen Protokolle betrachten. Sie müssen den „akzeptierten Datensatz“ des Empfängers prüfen. Hat der E-Mail-Anbieter gesagt: „Ja, ich habe sie erhalten“? Wenn Sie diesen Datensatz lesen können, können Sie das Problem lösen.

Das Zombie-Problem und der magische Zaun

Aber warten Sie! Es wird noch komplizierter. Stellen Sie sich vor, die E-Mail wurde gesendet, aber sie blieb in einer „Retry-Queue“ stecken (wie ein Briefkasten, der noch nicht geöffnet wurde). Der Computer stürzt ab, wacht auf, prüft den Datensatz des Empfängers, sieht, dass die E-Mail dort noch nicht vorhanden war, und sendet sie erneut. Dann kommt die alte, feststeckende E-Mail endlich an. Nun hat der Empfänger wieder zwei E-Mails. Dies wird als „Straggler“ (Nachzügler) oder „Zombie-Nachricht“ bezeichnet.

Das Paper beweist, dass es nicht ausreicht, einfach nur den Datensatz des Empfängers zu lesen, wenn alte Nachrichten noch später eintreffen können. Um dies zu beheben, schlägt der Autor einen „Fence“ (Zaun) vor. Stellen Sie sich einen Zaun wie einen Türsteher in einem Club vor. Wenn der Computer aufwacht, sendet er nicht einfach nur die E-Mail; er errichtet auch einen Zaun. Er sagt dem Empfänger: „Ich befinde mich jetzt in einer neuen Generation (einer neuen Schicht). Wenn versuchen, alte Nachrichten aus der vorherigen Schicht einzutreten, wird der Türsteher sie rauswerfen.“

Dieser Zaun ist ein Kompromiss. Er garantiert, dass Sie keine Duplikate erhalten, aber es kann bedeuten, dass Sie eine Nachricht verlieren, die eigentlich noch unterwegs war. Das Paper beweist mathematisch, dass dies der einzige Weg ist, um sicher zu sein. Man kann nicht gleichzeitig „perfekte Sicherheit“ und „perfekte Rettung“ alter Nachrichten haben; man muss wählen, an welcher Grenze (welchem Zeitpunkt) man sicher sein möchte.

Das Double-Header-Problem

Es gibt noch eine weitere Wendung. Was ist, wenn zwei Computer gleichzeitig aufwachen und beide denken, sie seien der Einzige? Beide lesen den Datensatz des Empfängers, beide sehen dasselbe und beide entscheiden, die E-Mail zu senden. Nun haben Sie ein „Double-Header“-Desaster.

Das Paper zeigt, dass es nicht ausreicht, die Computer dazu zu bringen, streng geordnet nacheinander zu arbeiten. Einer könnte die Arbeit halb unterbrechen und abstürzen, während der andere fertig wird, was zu einem Duplikat führt. Die Lösung ist ein „Claim“ (Anspruch). Bevor er etwas sendt, muss ein Computer rufen: „Ich bin jetzt der Boss!“ und die Tür abschließen. Er tut dies in einem einzigen, atomaren Schritt: Er beansprucht den Platz, liert den Datensatz und bereitet die Nachricht gleichzeitig vor. Wenn ein anderer Computer versucht, den Platz zu beanspruchen, wird er blockiert. Dies stellt sicher, dass immer nur ein Computer gleichzeitig an dem Problem arbeitet.

Die Haltbarkeit des Beweises

Schließlich fragt das Paper: Wie lange hält dieser Beweis an? Die „Quittungen“ und „Protokolle“, die die Computer verwenden, um ihre Arbeit zu überprüfen, halten nicht ewig. Wenn der Empfänger alte Quittungen nach 24 Stunden löscht und der Computer 48 Stunden lang ausgefallen ist, ist der Beweis dahin. Der Computer wacht auf, sieht keinen Datensatz der E-Mail und sendet sie erneut. Aber der Empfänger, der die alte Quittung gelöscht hat, betrachtet dies als eine neue E-Mail und akzeptiert sie. Nun haben Sie ein Duplikat.

Das Paper beweist, dass „Exactly-Once“ nur möglich ist, wenn Sie Ihre Beweise (die Protokolle und Quittungen) länger aufbewahren als den längstmöglichen Absturz. Wenn Sie die Beweise löschen, verlieren Sie die Garantie. Es ist wie der Versuch, die Zahlung der Steuern zu beweisen, indem man nach einer Quittung sucht, die man letzte Woche weggeworfen hat.

Das Fazit für die reale Welt

Dieses Paper sagt nicht nur „Seien Sie vorsichtig“. Es liefert eine strikte, maschinenprüfbare Regel. Es sagt Ingenieuren:

1. Vertrauen Sie Ihren eigenen Notizen nicht: Ihr Checkpoint kann Ihnen nicht sagen, ob die andere Seite die Nachricht erhalten hat.
2. Fragen Sie den Empfänger: Sie müssen den „akzeptierten Datensatz“ des Empfängers lesen.
3. Bauen Sie einen Zaun: Wenn alte Nachrichten noch eintreffen können, müssen Sie sie mit einem Generations-Fence blockieren.
4. Beanspruchen Sie Ihren Platz: Wenn mehrere Computer aufwachen könnten, müssen sie um einen „Claim“ kämpfen, bevor sie irgendwelche Arbeiten ausführen.
5. Bewahren Sie Ihre Quittungen auf: Sie müssen Ihre Protokolle und Quittungen länger aufbewahren als den längsten Ausfallzeitraum.

Der Autor verwendete ein mächtiges mathematisches Werkzeug namens Isabelle/HOL, um jeden einzelnen Schritt seiner Logik zu prüfen. Er hat nicht nur geraten; er hat bewiesen, dass ohne diese spezifischen Schritte Duplikate oder verlorene Nachrichten mathematisch unvermeidlich sind. Er hat auch bewiesen, dass gängige Abkürzungen, wie etwa nur die „Senke zu lesen“, ohne einen Zaun zu nutzen, oder die „Schritte zu ordnen“, ohne einen Claim zu nutzen, in spezifischen, kniffligen Szenarien scheitern werden.

Wenn Sie also das nächste Mal zwei E-Mails für eine Bestellung erhalten, geben Sie nicht der Datenbank die Schuld. Geben Sie dem Umstand die Schuld, dass das System nicht die richtige Frage gestellt, keinen richtigen Zaun gebaut oder die Quittung nicht lange genug aufbewahrt hat. Dieses Paper liefert uns den exakten Bauplan, um Systeme zu bauen, die diesen Fehler nie wieder machen.