Das Internet und die Dienste, die es bereitstellt, sind ein omnipräsenter Teil unseres Lebens geworden, und asynchrone verteilte Systeme bilden die Basis dieser Dienste. Eine wichtige Eigenschaft von verteilten Systemen ist, dass sie robust mit partiellen Fehlern umgehen. Diese Eigenschaft ermöglicht den verteilten Systemen, trotz Fehlern in mehreren Komponenten, weiterhin den Anforderungen entsprechende Fortschritte zu machen. Das Programmieren von verteilten Systemen wird durch die Notwendigkeit mit partiellen Fehlern umzugehen, sehr anspruchsvoll und fehleranfällig. Insbesondere das Sicherstellen der Anforderungen, unter Berücksichtigung von Asynchronität und möglichen Fehlern, ist eine Herausforderung. Multiparty Session Types (MPSTs) ist eine Klasse von Typsystemen für parallele Prozesse, die wünschenswerte Eigenschaften, wie beispielsweise die Abwesenheit von Empfangsfehlern und Deadlocks, statisch sicherstellt. Daher können MPSTs das Programmieren von verteilten Anwendungen vereinfachen. Bisher existierende MPSTs-Ansätze können nicht auf eine signifikante Klasse von verteilten Systemen angewendet werden, da diese die Spezifikation und Verifikation von Crash-Stopp-Fehlerbehandlung nicht ermöglichen. Weiterhin bieten existierende MPSTs-Ansätze nicht die nötigen Abstraktionen zur Spezifikation und Verifikation von praxistauglichen Protokollen, die partielle Fehler behandeln und tolerieren.

Diese Ausarbeitung stellt unseren Artikel “A Typing Discipline for Statically Verified Crash Failure Handling in Distributed Systems” [VCE+ 18] vor, der die erste MPSTs Formulierung für Crash-Stopp-Fehlerbehandlung in asynchronen verteilten Systemen ist. Diese Arbeit verwendet ein leichtgewichtiges Koordinatormodell, inspiriert durch die weit verbreiteten Systeme wie Apache ZooKeeper und Cubby. Für dieses Modell haben wir ein MPSTs-Typsystem entwickelt, dass das Spezifizieren und Verifizieren von Protokollen mit expliziter Fehlerbehandlung von partiellen Fehlern ermöglicht. Der Koordinator ist nur in der kritischen Behandlung von partiellen Fehlern involviert, daher bewahrt die Arbeit die verteilte Struktur von MPSTs. Wir zeigen, dass das Typsystem Subject-Reduction erfüllt, trotz des möglichen Auftretens von Fehlern während der Laufzeit. Wir haben einen Prototypen in Scala entwickelt, der Apache Zookeeper als Koordinator verwendet und demonstrieren damit die praktische Einsetzbarkeit unserer MPSTs Formulierung zur Entwicklung und Verifikation von verteilten Anwendungen, die robust mit partiellen Fehlern umgehen können. In der durchgeführten Evaluation hat der entwickelte Prototyp außerhalb der Fehlerbehandlung keinen relevanten Performance Overhead.

Weiterhin stellen wir unseren Artikel “A Multiparty Session Typing Discipline for Fault-tolerant Event-driven Distributed Programming” [VHEZ21] vor, dies ist die erste Formulierung von MPSTs für die praxistaugliche Programmierung von fehlertoleranten verteilten Anwendungen in asynchronen verteilten Systemen. Wir beantworten eine offene Frage im Bereich von Session Types; wie können wir Kommunikationsmustern, die Asynchronität und parallele Fehler beinhalten eine Struktur geben und gleichzeitig die nötigen Funktionen bereitstellen, die für praxistaugliche fehlertolerante Protokolle nötig sind. Diese Protokolle benötigen Funktionen, wie das dynamische Ersetzten von fehlerhaften Teilnehmern, das Wiederholen von Protokollsegmenten, die wegen Fehlern gescheitert sind und das Tolerieren von nicht perfekten Fehlerdetektoren (da eine perfekte Fehlererkennung in asynchronen System nicht möglich ist). Kern unseres Ansatzes ist, dass wir das erste Modell für eine eventbasierte Nebenläufigkeit für MPSTs entwickelt haben. Dieses Modell behandelt normale IO-Nachrichten und Fehlerbenachrichtigungen uniform. Dies ermöglicht es uns, nicht nur eine Vielzahl an Funktionen zu realisieren, sondern ist auch Grundlage für unser Global Progress Resultat, was traditionell nicht in MPSTs gilt. Um die praktische Einsetzbarkeit unseres Ansatzes aufzuzeigen, haben wir eine Toolchain in Scala entwickelt. In dieser haben wir einen Session typisierten Cluster Manager (CM) für Apache Spark entwickelt. Unsere Session typisierter CM interagiert mit Apache Spark Komponenten und ergibt eine funktionierende Apache Spark Laufzeitumgebung. Der CM kann existierende und unmodifizierte Spark Anwendungen, auch von Dritten, ausführen. In einem Standardbenchmark hat Apache Spark, wenn es den Session typisierten CM anstelle des Standard CM verwendet, einen durchschnittlich Overhead von unter 10%.

Die entwickelten neuartigen MPSTs basierten Typsysteme und Frameworks ermöglichen die Spezifikation und Verifikation von praxistauglichen verteilten Anwendungen, die partielle Fehler behandeln. Wir ermöglichen damit eine leichtgewichtige Verifikation, stellen wünschenswerte Eigenschaften sicher und unterstützen damit die Entwicklung von robusten verteilten Anwendungen.