Einige der gefährlichsten Systemfehler lassen sich erkennen, bevor Code geschrieben wird, wenn das Design selbst als analysierbares System behandelt wird. Darum geht es im Vortrag von Hillel Wayne, der erläutert, wie Prinzipien formaler Methoden dabei helfen, zukünftige Systeme zu untersuchen und Probleme bei Robustheit, Nebenläufigkeit und Fehlern zu erkennen, bevor sie sich in Betriebsfehler verwandeln.
Wayne beginnt mit einem vereinfachten Beispiel für das, was er „Task Runner“ nennt: Das System prüft, ob die Aufgabe erledigt wurde, markiert sie anschließend als erledigt und führt danach die Aufgabe aus. Die Abfolge wirkt logisch, bricht jedoch zusammen, wenn während der Ausführung ein Fehler auftritt. Nach der Markierung der Aufgabe als abgeschlossen kann ein erneuter Versuch erfolgen, sodass die Aufgabe tatsächlich nicht ausgeführt wird. Wird die Markierung des Abschlusses dagegen bis nach der Ausführung verschoben, entsteht ein weiteres Problem: Zwei nebenläufige Runner können dieselbe Aufgabe zweimal ausführen, bevor einer von ihnen ihre Erledigung registriert.
Das ist nicht nur ein theoretisches Problem. Der Vortrag verknüpft es mit Beispielen wie Paketversandsystemen, die eine Bestellung zweimal versenden können, Planungssystemen, die denselben Termin für zwei Personen buchen können, und Mechanismen zur Installation von Anwendungen, die bei einer Wiederholung der Anfrage in destruktives Verhalten geraten können.
Beginne damit zu definieren, was „korrekt“ bedeutet
Wayne schlägt vor, Systemanforderungen als binäre Eigenschaften zu formulieren: Sie sind entweder wahr oder falsch. Beispiele sind, dass eine Aufgabe nicht mehr als einmal ausgeführt wird – eine Sicherheitseigenschaft, die das Eintreten eines unerwünschten Ereignisses verhindert – und dass eine Aufgabe mindestens einmal ausgeführt wird – eine Lebendigkeitseigenschaft, die das Eintreten eines gewünschten Ereignisses sicherstellt.
Der Vortrag betont, dass Eigenschaften nicht gleich stark sind. Ein System, das 10.000 Abfragen pro Sekunde verarbeiten kann, erfüllt automatisch auch die Eigenschaft, zwei Abfragen pro Sekunde zu verarbeiten; umgekehrt gilt das nicht. Daher kann das Bestehen einer starken Eigenschaft ein Hinweis auf die Korrektheit einer Gruppe schwächerer Eigenschaften sein, während das Scheitern einer schwächeren Eigenschaft dabei hilft, den möglichen Fehlerbereich einzugrenzen. Wayne verbindet diese Idee mit der Testpyramide: Viele Unit-Tests können bei der Diagnose eines Fehlers nützlicher sein als eine begrenzte Zahl von End-to-End-Tests.
Das vereinfachte Modell macht das Grundproblem sichtbar
Statt das System mit all seinen Details abzubilden, fordert Wayne dazu auf, ein abstraktes Modell zu erstellen, das nur das notwendige Minimum an Zustand enthält: die aktuelle Phase des Algorithmus, die Information, ob die Aufgabe als abgeschlossen markiert ist, und die Anzahl ihrer Ausführungen. Dadurch lassen sich mögliche Zustände und die Pfade erkunden, die das System nehmen kann, einschließlich Fehlerzuständen und Wiederholungsversuchen.
In formalen Methoden können dieses Modell und die Eigenschaften mithilfe logischer Formeln codiert und anschließend mit Werkzeugen wie Model-Checkern und SMT-Solvern geprüft werden. Der praktische Gedanke des Vortrags erfordert jedoch nicht, diese Werkzeuge direkt einzusetzen; Ingenieure können dieselbe Denkweise übernehmen, indem sie mögliche Zustände und Übergänge verfolgen.
Der Faktor „Gegner“ bei Nebenläufigkeit und Fehlern
Wayne schlägt vor, jede Quelle von Nichtdeterminismus – etwa Benutzereingaben, Nebenläufigkeit, Zufall, Zeitüberschreitungen und Serverausfälle – als einen „Gegner“ zu betrachten, der stets das schlechtestmögliche Ergebnis auswählt. Wenn das System unendlich oft einen erneuten Versuch durchführen kann, wird dieser Gegner bei jedem Mal den Fehler auswählen. Dadurch zeigt sich, dass die Lebendigkeitseigenschaft selbst dann nicht garantiert ist, wenn ein Erfolg theoretisch möglich wäre.
Er erläutert außerdem, dass bei zwei nebenläufigen Runnern einige Variablen als für jeden Prozess lokal und andere als zwischen dem System und der Außenwelt gemeinsam genutzt modelliert werden müssen. Durch die Erkundung verschiedener Ausführungsreihenfolgen lässt sich ein Zustand erreichen, in dem die Aufgabe zweimal ausgeführt wird, selbst wenn jeder Runner für sich betrachtet fehlerfrei erscheint.
Annahmen sind Teil des Designs
Die Korrektheit eines Systems hängt nicht nur von seinen Eigenschaften ab, sondern auch von den Annahmen über die Umgebung, in der es arbeitet. Ein Design kann die starke Annahme erfordern, dass der Prozess überhaupt nicht ausfällt, während ein anderes Design funktionieren kann, wenn der Ausfall nur begrenzt oft auftritt. Wayne weist darauf hin, dass eine Umordnung der Schritte die Lebendigkeitsannahmen abschwächen kann, zugleich aber die Sicherheitsanforderungen erhöhen kann, etwa durch die Notwendigkeit sicherzustellen, dass sich zu jedem Zeitpunkt nur ein Runner im Einsatz befindet.
Die Lage verändert sich ebenfalls, wenn sich die Betriebsumgebung ändert. Die Abhängigkeit von starker Konsistenz in einer Datenbank und der anschließende Wechsel zu letztendlicher Konsistenz können dazu führen, dass zuvor korrekte Eigenschaften nicht mehr garantiert sind, selbst wenn sich der Systemcode nicht geändert hat. Daher sollten Annahmen über den Dienstanbieter oder die Datenbank nicht als externe Details betrachtet werden; sie sind unmittelbare Bedingungen für die Korrektheit des Designs.
Was ändert sich in der Praxis?
Der praktische Wert der Methode liegt nicht darin, Tests zu ersetzen oder den Einsatz formaler Werkzeuge in jedem Projekt zu fordern, sondern darin, Designfragen strenger zu machen: Welche Zustände sind möglich? Welche Ereignisreihenfolge ist die schlechteste? Was können wir tatsächlich kontrollieren? Und welche Annahmen kann das Team nicht garantieren? Je stärker die geforderte Eigenschaft oder je weniger vorhersehbar die Umgebung ist, desto komplexer muss das System gestaltet werden – oder die geforderte Eigenschaft muss abgeschwächt werden, etwa indem die Bedingung „jede Nachricht verarbeiten“ in „Nachrichten verarbeiten oder an eine Dead-Letter-Queue senden“ umgewandelt wird.
Wayne präsentiert diese Ideen als Denkwerkzeuge aus den formalen Methoden und nicht als fertigen Ersatz für ingenieurtechnisches Urteilsvermögen. Die offene Frage jedes Systems bleibt, wie genau das verwendete Modell und die zugrunde gelegten Annahmen sind. Wenn ein Zustand übersehen wird oder das Team ein Verhalten voraussetzt, das die Umgebung nicht garantiert, kann die Analyse die Korrektheit eines Modells nachweisen, das dem realen System nicht ähnelt.