Fehlertolerante verteilte Algorithmen sind das Herzstück jedes verteilten Computersystems für kritische Anwendungen und implementieren grundlegende Services wie Uhrensynchronisation, Group Membership und Consensus. Derartige Algorithmen müssen ihre Spezifikation trotz der inhärenten Unsicherheit erfüllen, die in netzwerk- oder shared-memory-gekoppelten verteilten Systemen unvermeidbar ist. Quellen dieser Unsicherheit sind variable/unbekannte Ausführungs- und Nachrichtenübertragungszeiten und, insbesondere, Fehler von Subsystemen. Die daraus resultierende kombinatorische Explosion macht es in vielen Fällen unmöglich, die korrekte Operation solcher Algorithmen durch Model Checking (oder gar erschöpfendes Testing) zu verifizieren. Korrektheitsbeweise basierend auf einer geeigneten formal-mathematischen Modellierung stellen hier die einzig taugliche Alternative dar. Diese Master-level Basis-LVA bietet eine Einführung in verteilte Algorithmen und deren formal-mathematische Analyse. Neben der generellen Entwicklung formal-mathematischer Fertigkeiten soll sie es ihren Absolventen erlauben, (1) Modelle, Probleme, Algorithmen, Lower-Bounds, Impossibility-Resultate und Korrektheitsbeweise im Bereich Distributed Computing zu verstehen, (2) existierende Lower-Bounds und Impossibility-Resultate in neuen Situationen anzuwenden, (3) auf Basis der erlernten Algorithmen und Techniken neue verteilte Algorithmen für spezielle Problemstellungen zu entwickeln und deren Korrektheit zu beweisen, und (4) neue Lower-Bounds und Impossibility-Resultate zu finden.
Die LVA wird im "angloamerikanischen Modus" abgehalten, der auf kontinuierlicher Beschäftigung mit den Inhalten während des gesamten Semesters basiert: Mehrere Quizzes und Homework-Assignments stellen sicher, dass (1) die in Vorlesung vermittelten Inhalte effizient erlernt und (2) die individuelle Problemlösungskompetenz im formal-mathematischen Bereich trainiert werden.
Grundlagen: Execution runs, safety and liveness properties, causality and time; Modelle: Message passing vs. shared memory, synchronous vs. asynchronous, failure models; Algorithmen: Leader election, mutual exclusion, clock synchronization, consensus, distributed snapshots; Beweistechniken: Impossibility proofs, lower bounds, simulation, indistinguishability, bivalence.
Alle, die die nächste LVA besuchen möchten: Bitte möglichst bald die LVA im TISS LVA-Forum & News abonnieren. [Die eigentliche LVA-Anmeldung (via myTI) ist erst nach der Erfüllung der Zulassungsbedingungen erlaubt.]
Textbook: Hagit Attiya, Jennifer Welch. Distributed Computing: Fundamentals, Simulations and Advanced Topics (2nd ed.), John Wiley and Sons, 2004. ISBN 0-471-45324-2
Vertrautheit mit der Analyse von sequentiellen Algorithmen und elementarer diskreter Mathematik; ausreichende Fertigkeiten bei der Erstellung mathematischer Beweise. Hintergrundwissen über verteilte Systeme und fehlertolerante Systeme ist hilfreich, aber nicht notwendig.
