Vorlesung Verteilte Algorithmen

Ein Algorithmus heißt verteilt, wenn er auf einer physikalisch oder logisch verteilten Architektur arbeitet. Solche Algorithmen werden praktisch zunehmend wichtiger. In der Vorlesung wird eine Reihe solcher Algorithmen vorgestellt und ihre Korrektheit bewiesen. Mit Vorlesungen zu Methoden und Modellen des Systementwurfes oder zur Computergestützten Verifikation ergänzt sich dieser Halbkurs zu einem Ganzkurs.

Aktuell

Dozent

• Prof. Dr. Wolfgang Reisig

Telefon:	+49-30-2093-3065 (Sekretariat)
	+49-30-2093-3065 (Büro)
Raum:	RUD 25, 4.416
E-Mail:	reisig @ informatik.hu-berlin.de

Termin

Die erste Vorlesung und Übung findet am Dienstag, den 18. Oktober statt.

Material

Literatur

• Wolfgang Reisig. Elements of Distributed Algorithms: Modeling and Analysis with Petri Nets. Springer-Verlag, September 1998.
• Nancy Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, San Mateo, CA, 1996.

Vorlesungen

I. Grundlagen und elementare Fallstudien

• Lektion 01: Einführung, Beispiele, Organisation der Vorlesung (erneut aktualisiert)
• Lektion 02: Wie formulieren wir Verteilte Algorithmen? (aktualisiert)
• Lektion 03: Sequentielle und parallele Puffer
• Lektion 04: Der Crosstalk-Algorithmus
• Lektion 05: Wechselseitiger Ausschluss

II. Eigenschaften verteilter Systeme

• Lektion 06: Korrektheit
• Lektion 07: Einschub: Induktive Invarianten
• Lektion 08: Gleichungen und Ungleichungen elementarer Algorithmen
• Lektion 09: Platz-Invarianten und Fallen (aktualisiert)
• Lektion 10: Progress (aktualisiert)
• Lektion 11: Fairness (aktualisiert)
• Lektion 12: Leads-to (aktualisiert)
• Lektion 13: Die Pick-up Regel (aktualisiert)
• Lektion 14: Beweisgraphen (aktualisiert)
• Lektion 15: Fairness ablesen (aktualisiert)
• Lektion 16: Evolution von Mutex-Algorithmen (aktualisiert)

III. Systemnetze

• Lektion 17: Erste Beispiele für Systemnetze
• Lektion 18: Multimengen
• Lektion 19: Symbolische Darstellung
• Lektion 20: Die Mathematik hinter Systemnetzen (aktualisiert)
• Lektion 21: Varianten des Philosophenproblems
• Lektion 22: Weitere Beispiele
• Lektion 23: Verteilte Constraint-Algorithmen, verteilte Online-Algorithmen
• Lektion 24: Noch mehr Beispiele
• Lektion 25: Selbststabilisierende Algorithmen

IV. Nachrichtenbasierte Algorithmen

• Lektion 26: Alternating Bit und Sliding Window
• Lektion 27: Nachrichten schicken und bestätigen
• Lektion 28: Modellierung von Netzwerkalgorithmen; Leader Election & Echo-Algorithmus
• Lektion 29: Wechselseitiger Ausschluß in Netzwerken
• Lektion 30: Konsens, Phasensynchronisation, Selbststabilisierung

V. Zustandseigenschaften von Systemnetzen

• Lektion 31: Gleichungen und Ungleichungen von Systemnetzen
• Lektion 32: Platz-Invarianten von Systemnetzen
• Lektion 33: Zustandseigenschaften einiger verteilter Algorithmen

VI. Progress verteilter Abläufe

• Lektion 34: Verteilte Abläufe (aktualisiert)
• Lektion 35: Progress auf verteilten Abläufen (aktualisiert)
• Lektion 36: Grundformeln (aktualisiert)
• Lektion 37: Ablese-Muster für Systemnetze
• Lektion 38: Fallstudien
• Lektion 39: Der Algorithmus von Gallenger, Humblett und Spira , Systemnetz:
• Lektion 40: Kontrollfluß, Datenfluß, Datenreplikation
• Lektion 41: Weitere Ausdrucksmittel

Übungen

• Übung zu Lektion 01
• Übung zu Lektion 02
• Übung zu Lektion 03 (Puffer)
• Übung zu Lektion 04 (Crosstalk)
• Übung zu Lektion 05 (Mutex)
• Übung zu Lektion 07 (Induktive Invarianten)
• Übung zu Lektion 08 (Glch. & Unglch. elementarer Algorithmen)
• Übung zu Lektion 09 (Zustandseigenschaften aus Platzinvarianten)
• Übung zu Lektion 10 (Progress)
• Übung zu Lektion 12
• Übung zu Lektion 13 (Die Pick-up Regel)
• Übung zu Lektion 14 (Beweisgraphen)
• Übung zu Lektion 15 (Fairness ablesen)
• Übung zu Lektion 16 (Evolution von Mutex-Algorithmen)
• Übung zu Lektion 28 (Leader election)
• Übung zu Lektion 29 (Globaler Mutex)
• Übung zu Lektion 32 (Platz-Invarianten Systemnetze) (geändert!)
• Übung zu Lektion 34 (Verteilte Abläufe)

Prüfung

Die mündlichen Prüfungen finden am 3. & 6. März statt.