Complete Characterization of Stabilizing Consensus in Distributed Systems

Abstract

Das terminating consensus Problem ist eines der fundamentalsten Probleme in derTheorie verteilter Systeme da es die Grundlage unzähliger Anwendungen darstellt. Seit seiner Einführung haben sich eine Vielzahl an Arbeiten mit der (nicht-) Existenz von Protokollen für verschiedene distributed computing models beschäftigt. Diese zentrale Rolle motivierte auch zahlreiche Problemvariationen, eine davon ist das stabilizing consensus Problem. Während Prozessoren in der terminierenden Variante irgendwann final entscheiden müssen, können sie in der stabilisierenden Variante finit oft ihre Meinung ändern, solange alle irgendwann übereinstimmen. Dieser kleine, aber wichtige Unterschied erlaubt es, stabilizing consensus in Modellen zu lösen, in denen terminating consensus erwiesenermaßen unmöglich ist. Die Frage, wo genau man stabilizing consensus erreichen kann und wo nicht, wurde von Charron-Bost und Moran in [CM21] gestellt, und ist das umfassende Thema dieser Dissertation. Lange Zeit wusste man nicht viel über stabilizing consesus. Nachdem das Problem von Angluin, Fischer und Jiang in [AFJ06] definiert und hinsichtlich seiner Lösbarkeit in klassischen Modellen untersucht wurde, gab es bis auf die erwähnte Arbeit von Charron-Bost und Moran keinen signifikanten Fortschritt - bis zu dieser Dissertation. Wir betrachten stabilizing consensus aus 3 verschiedenen Blickwinkeln: Wir starten in Chapter 2 damit, eine offene Frage von [CM21] negativ zu beantworten, indem wir zeigen, dass ein permanenter Broadcaster nicht ausreicht, um stabilizing consensuszu lösen. Im Zuge dessen verwenden wir eine neue Beweistechnik, die den bekannten Bivalence Argumenten ähnelt, aber mit nicht-terminierenden Protokollen arbeiten kann. Die entscheidende Entdeckung sind so genannte patient protocols, auf die jedes andere Protokoll reduziert werden kann. In Chapter 3 modellieren wir den Raum der infiniten Executions von stabilizing consensus über eine point-set topology, für jedes verteilte Modell mit Kommunikations- und nichtbyzantinischen Prozessfehlern. Verglichen mit der topologischen Characterisierung von terminating consensus stellt sich heraus, dass die Entscheidungsmengen nicht geschlossenund offen sondern nur semi-offen sein müssen und dass die Entscheidungsfunktion für stabilizing consensus nicht stetig sondern nur semi-stetig ist. Diese Begriffe wurden von Levine [Lev63] definiert, wobei hier entscheidend ist, dass jede geschlossene und offene Menge auch semi-offen ist, und dass eine semi-stetige Funktion eine zusammenhängende Menge auf nicht-zusammenhängende Mengen abbilden kann. Weiters beweisen wir, dass stabilizing consensus mit strong und weak validity äquivalent sind, und unterstreichen unsere Resultate mit mehreren Beispielen. Abschließend charakterisieren wir stabilizing consensus in epistemischer Logik im "Runs and Systems" framework, das von Fagin, Halpern, Moses und Vardi [FHMV95] entwickelt und popularisiert wurde. Ausgehend von einer neuen Charakterisierung von dynamic common knowledge von Gonczarowski und Moses [GM24] entwickeln eine neue Modalität, die wir Vorahnung nennen. Wir beweisen, dass gemeinsame Vorahnung, definiert über einenFixpunkt in der Semantik, sowohl notwendig als auch hinreichend für stabilizing consensus ist. Darüber hinaus etablieren wir eine Verbindung zu den beiden vorhergegangenen Kapitel und komplettieren damit unsere Charakterisierung.Die vorliegende Dissertation charakterisiert somit vollständig den bis dato unbekannten Lösungsraum des stabilizing consensus Problems und leistet damit einen signifikanten Beitrag zum wissenschaftlichen state-of-the-art.

Terminating consensus is the canonical problem in distributed computing, as mutual agreement on a common value is at the core of many real-world applications. Countlessworks analyze solvability and impossibility in different models, characterizing many aspects of the task since its introduction. Its prominence has also sparked many variations, one of which is the stabilizing consensus problem - instead of irrevocably deciding once, processes are allowed to update their decision values and only need to reach agreement eventually.This relaxation in the termination condition allows stabilizing consensus to be solved in models where terminating consensus is already impossible. Characterizing where exactly stabilizing consensus is solvable was stated as an open question by Charron-Bost and Moran in [CM21], and is the topic of this thesis. Relatively little was known about stabilizing consensus for decades. After its introductionby Angluin, Fischer and Jiang in [AFJ06], only the aforementioned paper by Charron-Bost and Moran focused on this problem - until this thesis. We approach the solvability boundaries of stabilizing consensus from three different directions: In Chapter 2, we negatively answer the open question in [CM21] about whether a perpetual broadcaster is sufficient for stabilizing consensus, by utilizing a novel combinatorial proof technique where we reduce the decision of any protocol to its decision in the limit. Crucially, we introduce a novel delayed lossy link model which admits unbounded periods of no communication, and show how to map any protocol to a so-called patient protocol, which exploits such unbounded periods of silence. In Chapter 3, we completely capture the solvability conditions for stabilizing consensus by defining a point-set topology on the set of infinite runs generated by any given distributed computing model with non-byzantine failures and communication faults. Contrary to terminating consensus, where the run space needs to separate into clopen sets, we show that the run space for stabilizing consensus needs to just separate into semi-open sets together with a semi-continuous decision function, as introduced by Levine in [Lev63]. Crucially, a semi-continuous function can map a connected space into a disconnected one. We also prove that stabilizing consensus with weak and strong validity is equivalent, and apply our results to illustrative examples ranging from synchronous message passing to asynchronous distributed systems. Finally, Chapter 4 uses temporal epistemic logic in the runs and systems framework introduced by Fagin, Halpern, Moses and Vardi in [FHMV95] for characterizing the necessary and sufficient knowledge for solving stabilizing consensus. Starting from the newly introduced dynamic common knowledge by Gonczarowski and Moses [GM24], which allows to circumvent the "Halpern-Moses paradox", we formally develop a new knowledge modality called foreknowledge and show that common foreknowledge, defined as a greatest fixed point in the underlying semantics, is mandatory for stabilizing consensus. We also establish a relation to the topological results developed in Chapter 3, thus complementing our characterization.This thesis therefore completely characterizes the so-far unknown solvability boundariesof stabilizing consensus and thus significantly contributes to expanding the scientific state-of-the-art.