In diesem Artikel simulieren und untersuchen wir ein Zwei-Phasen-Festschreibungsprotokoll mit TLA +.
Das Zwei-Phasen-Festschreibungsprotokoll ist praktisch und wird heute in vielen verteilten Systemen verwendet. Trotzdem ist es eher kurz. Daher können wir es schnell modellieren und viel lernen. In der Tat werden wir anhand dieses Beispiels veranschaulichen, welches Ergebnis in verteilten Systemen
grundsätzlich unmöglich ist .
Das Biphase-Commit-Problem
Die Transaktion wird über
Ressourcenmanager (RM) geleitet . Alle RMs müssen vereinbaren, ob die Transaktion
abgeschlossen oder
abgebrochen wird .
Der Transaction Manager (TM) trifft die endgültige Entscheidung:
Festschreiben oder
Abbrechen . Voraussetzung für das Commit ist die Bereitschaft, alle RMs zu verpflichten. Andernfalls sollte die Transaktion abgebrochen werden.
Einige Hinweise zur Modellierung
Der Einfachheit halber führen wir Simulationen in einem Shared-Memory-Modell durch, nicht in einem Messaging-System. Es bietet auch eine schnelle Modellvalidierung. Wir werden den Aktionen „Lesen vom benachbarten Knoten und Aktualisieren des Status“ jedoch eine Nichtatomarität hinzufügen, um ein interessantes Verhalten beim Senden von Nachrichten zu erfassen.
RM kann nur den TM-Status lesen und seinen eigenen Status lesen / aktualisieren. Der Status eines anderen Ressourcenmanagers kann nicht gelesen werden. Ein TM kann den Status aller RM-Knoten lesen und seinen eigenen Status lesen / aktualisieren.
Definitionen
In den Zeilen 9-10 wird der anfängliche
rmState für jeden RM auf "
working und TM auf "
init .
Das
canCommit Prädikat ist
true wenn alle RMs "vorbereitet" sind (bereit zum Festschreiben). Wenn RM im
canAbort wird das
canAbort Prädikat
canAbort .
Das Modellieren von TM ist einfach. Der Transaktionsmanager prüft die Möglichkeit eines Commits oder einer Stornierung - und aktualisiert
tmState .
Es besteht die Möglichkeit, dass TM
tmState "unzugänglich" machen kann, sondern nur, wenn die
TMMAYFAIL Konstante vor der Validierung des Modells auf
true ist. In TLA + bestimmen Markierungen den Atomizitätsgrad, dh die Granularität. Mit den Bezeichnungen F1 und F2 bezeichnen wir, dass die entsprechenden Operatoren in Bezug auf die vorherigen Operatoren nichtatomisch (nach einer unbestimmten Zeit) ausgeführt werden.
RM-Modell
Das RM-Modell ist auch einfach. Da die Zustände "Arbeiten" und "Vorbereitet" nicht endgültig sind, wählt RM nicht deterministisch zwischen den Aktionen aus, bis sie den Endzustand erreichen. Ein "funktionierender" RM kann in einen "unterbrochenen" oder "vorbereiteten" Zustand übergehen. "Vorbereitet" RM erwartet ein Commit / Cancel von TM - und handelt entsprechend. Die folgende Abbildung zeigt die möglichen Zustandsübergänge für einen RM. Beachten Sie jedoch, dass wir mehrere RMs haben, von denen jeder seinen Status in seinem eigenen Tempo durchläuft, ohne den Status der anderen RMs zu kennen.
Zwei-Phasen-Commit-Modell
Wir müssen die Konsistenz unseres zweiphasigen Commits überprüfen: damit es keine unterschiedlichen RMs gibt, von denen einer "Commit" und der andere "Abtreibung" sagt.
Das Prädikat "
Completed überprüft, ob das Protokoll nicht für immer hängt: Am Ende erreicht jeder RM den endgültigen Status "
committed oder "
aborted .
Jetzt können wir das Protokollmodell testen. Zunächst setzen wir
TMMAYFAIL=FALSE, RM=1..3 , um das Protokoll mit drei RM und einem TM zu starten,
TMMAYFAIL=FALSE, RM=1..3 in einer zuverlässigen Konfiguration. Das Testen des Modells dauert 15 Sekunden und zeigt an, dass keine Fehler vorliegen. Sowohl
Consistency als auch
Completed mit jeder möglichen Protokollausführung mit einem Wechsel von RM-Aktionen und TM-Aktionen zufrieden.
Setzen
TMMAYFAIL=TRUE nun
TMMAYFAIL=TRUE und starten Sie die Prüfung neu. Das Programm führt schnell zu dem gegenteiligen Ergebnis, bei dem RM nicht weiterkommt und auf eine Antwort von einem nicht verfügbaren TM wartet.
Wir sehen, dass bei
State=4 Übergänge RM2 unterbrochen werden, bei
State=7 Übergänge RM3 unterbrochen werden, bei
State=8 geht
State=8 TM in den Zustand "Auflegen" und fällt auf
State=9 . Bei
State=10 friert
State=10 System ein, da RM1 für immer in einem vorbereiteten Zustand bleibt und auf eine Entscheidung eines gefallenen TM wartet.
BTM-Simulation
Um ein Einfrieren von Transaktionen zu vermeiden, fügen wir ein Backup-TM (BTM) hinzu, das schnell die Kontrolle übernimmt, wenn das Haupt-TM nicht verfügbar ist. BTM verwendet dieselbe Logik wie TM, um Entscheidungen zu treffen. Der Einfachheit halber gehen wir davon aus, dass das BTM niemals abstürzt.
Wenn wir das Modell mit dem hinzugefügten BTM-Prozess testen, erhalten wir eine neue Fehlermeldung.
BTM kann kein Commit akzeptieren, da unsere ursprüngliche Bedingung
canCommit besagt, dass alle
RMstates Zustände „vorbereitet“ sein müssen, und nicht die Bedingung berücksichtigt, dass einige RMs bereits eine Commit-Entscheidung vom ursprünglichen TM erhalten haben, bevor das TMB die Kontrolle übernimmt. Es ist notwendig, die Bedingungen von
canCommit unter Berücksichtigung einer solchen Situation neu zu schreiben.
Erfolg! Wenn wir das Modell testen, erreichen wir sowohl Konsistenz als auch Vollständigkeit, da das BTM die Kontrolle übernimmt und die Transaktion abschließt, wenn das TM fällt.
Hier ist das 2PCwithBTM-Modell in TLA + (BTM und die zweite Zeile von canCommit sind anfangs nicht kommentiert) und das
entsprechende PDF .
Was ist, wenn RM auch ausfällt?
Wir gingen davon aus, dass RM zuverlässig ist. Brechen Sie nun diesen Zustand ab und sehen Sie, wie sich das Protokoll verhält, wenn RM ausfällt. Fügen Sie dem Fehlermodell den Status "unzugänglich" hinzu. Um das Verhalten zu untersuchen und einen zeitweiligen Verfügbarkeitsverlust zu simulieren, lassen Sie den Notfall-RM wiederherstellen und arbeiten Sie weiter, indem Sie seinen Status aus dem Protokoll lesen. Hier ist ein weiteres RM-Zustandsübergangsdiagramm mit dem hinzugefügten "unzugänglichen" Zustand und rot markierten Übergängen. Und unten ist das überarbeitete Modell für RM.
Es ist auch notwendig,
canAbort unter Berücksichtigung des Nichtverfügbarkeitszustands zu verfeinern. TM kann die Entscheidung „auflegen“, wenn sich einer der Dienste in einem unterbrochenen oder unzugänglichen Zustand befindet. Wenn diese Bedingung weggelassen wird, unterbricht ein gefallener und nicht wiederhergestellter RM den Fortschritt der Transaktion. Natürlich sollten Sie auch hier den RM berücksichtigen, der die Entscheidung zum Abschluss der Transaktion aus dem Quell-TM gelernt hat.
Modellprüfung
Wenn wir das Modell testen, gibt es ein Problem der Inkonsistenz! Wie konnte das passieren? Wir verfolgen die Spur.
Mit
State=6 alle RMs in einem vorbereiteten Zustand. TM hat eine Entscheidung zum Abschluss der Transaktion getroffen. RM1 hat diese Entscheidung getroffen und auf das RC-Label umgestellt. Dies bedeutet, dass die Bereitschaft besteht, den Status in "abgeschlossen" zu ändern. (Denken Sie daran, RM1, diese Waffe wird im letzten Akt feuern). Leider fällt das TM bei
State=7 und RM2 wird bei
State=8 nicht mehr verfügbar. Im neunten Schritt übernimmt das Backup-BTM die Kontrolle und liest den Status der drei RMs als "vorbereitet, unzugänglich, vorbereitet" - und beschließt, die Transaktion im zehnten Schritt abzubrechen. Erinnerst du dich an RM1? Er beschließt, die Transaktion abzuschließen, da er eine solche Entscheidung vom ursprünglichen TM erhalten hat, und tritt in Schritt 11 in den
committed Zustand ein. In
State=13 erfüllt RM3 die Entscheidung, die Transaktion von BTM abzubrechen, und wechselt in den
aborted Zustand - und jetzt haben wir die Koordination mit RM1 unterbrochen.
In diesem Fall traf das BTM eine Entscheidung, die gegen die
Konsistenz verstieß. Wenn Sie andererseits das BTM warten lassen, bis der RM den unzugänglichen Zustand verlässt, kann es im Falle eines Unfalls am Knoten für immer einfrieren, was die
Erfüllungsbedingung (Fortschrittsbedingung) verletzt.
Eine aktualisierte TLA + -Modelldatei sowie das
entsprechende PDF finden Sie hier .
Unmöglichkeit FLP
Also, was ist passiert? Wir stießen auf den
Satz von Fisher, Lynch, Paterson (FLP) über die Unmöglichkeit eines Konsenses in einem asynchronen System mit Fehlern.
In unserem Beispiel kann BTM nicht richtig entscheiden, ob sich RM2 in einem fehlgeschlagenen Zustand befindet oder nicht - und entscheidet fälschlicherweise, die Transaktion abzubrechen. Wenn nur das ursprüngliche TM die Entscheidung treffen würde, wäre eine solche Ungenauigkeit beim Erkennen eines Fehlers kein Problem. RM wird jeder TM-Entscheidung gehorchen, damit Konsistenz und Fortschritt erhalten bleiben.
Das Problem ist, dass wir zwei Objekte haben, die Entscheidungen treffen: TM und BTM. Sie betrachten den Zustand von RM zu unterschiedlichen Zeiten und treffen unterschiedliche Entscheidungen. Eine solche Informationsasymmetrie ist die Wurzel allen Übels in verteilten Systemen.
Das Problem verschwindet auch bei der Erweiterung auf ein dreiphasiges Commit nicht.
Hier ist ein in TLA + modelliertes dreiphasiges Commit (
PDF-Version ). Im Folgenden finden Sie eine Fehlerverfolgung, die zeigt, dass dieser Zeitverlauf verletzt wurde (auf
der Wikipedia-Seite zu einem dreiphasigen Commit wird eine Situation beschrieben, in der RM1 nach Erhalt einer Entscheidung vor dem Commit einfriert und RM2 und RM3 festschreiben festschreiben, was die Konsistenz verletzt).
Paxos versucht, die Welt zu einem besseren Ort zu machen.
Aber nicht alles ist verloren, die Hoffnung ist nicht gestorben.
Wir haben Paxos . Es wirkt ordentlich im Rahmen des FLP-Theorems. Die Innovation von Paxos besteht darin, dass es
immer sicher ist (auch bei ungenauen Detektoren, asynchroner Ausführung und Fehlern) und
die Transaktion schließlich abschließt, wenn ein Konsens möglich wird.
Sie können TM in einem Cluster mit drei Paxos-Knoten emulieren. Dadurch wird das TM / BTM-Inkonsistenzproblem gelöst. Oder, wie Gray und Lampport in einem
wissenschaftlichen Artikel über den Konsens beim Transaktions-Commit gezeigt haben , wenn RM den Paxos-Container verwendet, um ihre Entscheidungen gleichzeitig mit der TM-Antwort zu speichern, entfällt ein zusätzlicher Schritt im Standardprotokollalgorithmus.