Modeling and verification of distributed algorithms in theorem proving environments
Küfner, Philipp
Mit dem wachsenden Markt für Netzwerkanwendungen gewinnt das Anwendungsgebiet von verteilten Algorithmen immer mehr an Bedeutung. Sobald ein globales Ziel durch ein koordiniertes Zusammenwirken mehrerer Prozesse erreicht werden muss, müssen lokale Berechnungen auf die einzelnen Teilnehmer verteilt und Kommunikationsprotokolle festgelegt werden. Dies erfordert die Entwicklung eines verteilten Algorithmus. In asynchronen Umgebungen müssen verteilte Algorithmen so konstruiert sein, dass sie das globale Ziel trotz unterschiedlicher Laufzeiten der Teilnehmer und verzögert ausgelieferter Nachrichten erreichen. Oft ist es eine zusätzliche Anforderung, dass verteilte Algorithmen auch in Hinblick auf den Ausfall einzelner Teilnehmer fehlertolerant sind. Die zusätzliche Komplexität, die durch die nebenläufige Ausführung der Prozesse in verteilten Systemen entsteht, macht den Einsatz konventioneller Methoden zur Modellierung und Verifikation der verteilten Algorithmen häufig unmöglich. Obwohl es viele verschiedene formale Ansätze, wie z.B. I/O Automaten und Prozesskalküle, zur Modellierung fehlertoleranter verteilter Algorithmen gibt, ist das verbreitete Mittel zur Darstellung neuer Algorithmen Pseudocode. Diese wenig formale Modellierung ermöglicht keine formale Verifikation und daher ist die Beweisführung zur Korrektheit der Algorithmen meist eher eine unpräzise Argumentation, die durch die Vielzahl der möglichen Ausführungsszenarien von verteilten Algorithmen häufig nicht nachvollziehbar ist. Inhalt dieser Arbeit ist die Erarbeitung neuer formaler Strategien zur Modellierung und Verifikation verteilter Algorithmen unter besonderer Berücksichtigung zweier Ziele: Zum einen neue Methoden zur Verfügung zu stellen, die den Ansprüchen eines Algorithmendesigners genügen, d.h. möglichst einfach zu verstehen und aufwandsarm anzuwenden sind. Auf der anderen Seite sollen diese Methoden formal genug sein, um die Anwendung maschineller Verifikation in Form von Theorembeweisern und damit eine mechanische Beweisführung für die Korrektheit zu ermöglichen. Um das erste Ziel zu erreichen verwenden wir Methoden, die bisherigen praxisnahen Modellierungsmethoden, wie z.B. Leslie Lamports Spezifikationssprache/-logik TLA+ oder Gurevichs Abstract State Machines sehr ähnlich sind. Zur formalen Modellierung von Algorithmen verwenden wir viele Abstraktionen, die der Arbeit von Fuzzati entnommen sind. Fuzzatis Arbeit untersucht zwei sehr ähnliche Algorithmen auf der Basis einer formalen prädikatenlogischen Modellierung. Diese Arbeit greift diese Abstraktionen auf und verallgemeinert sie so, dass sie zur passend und wiederverwendbar für eine Vielzahl von Algorithmen sind. Zusätzlich stellt diese Arbeit eine neue Methode vor, wie lokal beschriebene Berechnungsschritte auf einfache Weise in einen globalen Ausführungskontext übertragen werden können. Der Vorteil dieser Methode ist, dass Schritte, die lokal vollzogen werden, lokal beschrieben werden, aber dennoch in der Beweisführung für ein globales Ziel im globalen Kontext eingebettet werden können. Entsprechend ist die Modellierung aufwandsärmer, da lokale Berechnungsschritte, ähnlich wie im Pseudocode, ohne die Beschreibung des weiteren globalen Rahmens modelliert werden können. Gleichzeitig ermöglicht die formal korrekte Einbettung in den globalen Kontext formale Beweise zum Nachweis globaler Systemeigenschaften. Unser Modell umfasst dabei mehrere verschiedene Kommunikationsmechanismen wie Punkt-zu-Punkt Nachrichten, Broadcasts und Kommunikation über gemeinsam genutzte Speichersegmente. Erweiterungen dieser Möglichkeiten um weitere mögliche Kommunikationsinfrastrukturen zu unterstützen können einfach in das Modell integriert werden. Neben der Modellierung ist ein weiterer Schwerpunkt dieser Arbeit die Analyse verschiedener Strategien zum formalen Nachweis von Systemeigenschaften. Dazu müssen diese Eigenschaften zunächst in unserem Modell beschrieben werden. Diese Arbeit stellt Methoden zur Formulierung und Verifikation der beiden wesentlichen Klassen von Eigenschaften (Safety- und Livenesseigenschaften) vor. Für den Theorembeweiser Isabelle/HOL stellen wir ausserdem eine Bibliothek zur Verfügung, die die vorgestellten Abstraktionen und ebenso die Strategien zur Beweisführung in Form von Definitionen und Theoremen kapselt und dadurch wiederverwendbar macht. Der letzte Teil der Arbeit erbringt dann anhand mehrerer Fallstudien den Nachweis der Anwendbarkeit der vorgestellten Strategien. Vier bekannte verteilte Algorithmen werden in unserem Framework in Isabelle/HOL untersucht und verifiziert. Die vier Algorithmen variieren dabei in mehreren Aspekten, wie Komplexität, Kommunikationsinfrastruktur, Fehlermodell und Annahmen über die Synchronität des Systems und veranschaulicht daher viele wesentliche Modellierungs- und Verifikationsaspekte.
The field of application for distributed algorithms is growing with the ongoing demand for new network applications. Wherever a global goal must be achieved by a number of peers, a distributed algorithm consisting of local computations and communication protocols must be developed. In asynchronous environments the design of a distributed algorithm must respect the fact that processes may vary in speed and that messages might be delayed for an arbitrarily long time. Moreover, it is often required that the distributed algorithm still works in the presence of crash failures, i.e., in scenarios, where some processes stop working at some time. The complex nature of concurrent executions in distributed systems often hinder the application of common methods for modeling and verification. Although many different formal approaches for modeling fault tolerant distributed algorithms, like e.g. I/O automata and process calculi have been proposed, many works in the field of distributed systems use informal pseudo-code representations to introduce new distributed algorithms. On most cases this leads to informal and crude arguments for correctness, which usually become incomprehensible if all race conditions must be taken into account. This work proposes new formal strategies to model and verify distributed algorithms, whereas we focus on two main goals. Firstly, we introduce a means to satisfy a designer's demands by using methods that are easy to understand and to work with and which are very similar to common applied methods as e.g. TLA+ and Abstract State Machines. Secondly, our strategies are suitable for the formal use in a theorem proving environment. This enables mechanical verification of our distributed algorithms and therefore, we are able to produce machine-checked proofs for correctness.
Our model adopts abstractions from the work of Fuzzati, which examines two similar distributed algorithms in a logical framework. We lifted these abstractions to a more general level to make them suitable and reusable for as many distributed algorithms as possible. Furthermore, we present a new method to place local computation steps in the respective global context. The advantage of our method is that, on the on hand, like with pseudo code, computations can be described as local steps, but, on the other hand, it is possible to formally reason over global system states. Our model for communication mechanisms comprises modules for different kinds of message passing, broadcasts, and shared memory access. We are convinced that our model can easily be extended to support almost all kinds of communication infrastructures that can formally be described. We show how properties that have to be verified can be expressed in terms of our model to enable formal reasoning. Furthermore, we present appropriate strategies to verify different classes of properties. For the theorem proving environment Isabelle/HOL we provide a library which incorporates all introduced abstractions and can, therefore, be reused and extended for further applications, new algorithms, and further verification projects. Finally, we present case studies for the verification of different distributed algorithms to demonstrate the applicability of our strategies. Four known algorithms are verified in our model using our framework for Isabelle/HOL. The algorithms vary in complexity, the used communication infrastructure, the failure model, and other constraints, so that many different modeling and verification aspects are exemplified.
