Engineering-Philosophie: Leslie Lamport – Erst denken, dann programmieren

Die wichtigsten Erkenntnisse

• Erst denken, dann programmieren – und das Gedachte aufschreiben. Eine Spezifikation ist das Software-Äquivalent zum Bauplan eines Architekten – „Nicht zu denken garantiert”, dass wir Fehler machen werden.
• Zeit ist nicht global; Kausalität ist das eigentlich Reale. Ohne eine verlässliche gemeinsame Uhr hört man auf zu fragen, wann ein Ereignis eintrat, und fragt stattdessen, was was verursacht hat.
• Happened-before und logische Uhren formalisieren Kausalität. Lamports partielle Ordnung – und der prozesseigene Zähler, der sie umsetzt – ist der Keim für Vektoruhren und moderne Konfliktauflösung.
• Korrektheit präzise definieren, dann beweisen. Safety und Liveness, der Paxos-Konsens, die byzantinische Fehlertoleranz und die Spezifikationssprache TLA+ entspringen alle dem Ansatz, verteiltes Rechnen als Mathematik zu behandeln, nicht als überliefertes Erfahrungswissen.

Das Prinzip

„Ein verteiltes System ist eines, in dem der Ausfall eines Computers, von dessen Existenz Sie nicht einmal wussten, Ihren eigenen Computer unbenutzbar machen kann.” – Leslie Lamport¹

Diesen Satz schickte er 1987 an ein schwarzes Brett in seinem Labor, und er ist der meistzitierte Satz der verteilten Datenverarbeitung, weil er genau das benennt, was die Intuition partout nicht glauben will.¹ Sie meinen, Sie führten ein Programm auf Ihrem Computer aus. Tun Sie aber nicht. Sie führen es über eine ganze Population von Maschinen aus, deren Existenz Sie nie aufgezählt haben, deren Uhren voneinander abweichen und von denen jede einzelne genau in dem Moment ausfallen kann, in dem es darauf ankommt. Das System, das Sie im Kopf behalten können, und das System, das tatsächlich läuft, sind zwei verschiedene Systeme – und in der Lücke dazwischen wohnt jeder Fehler verteilter Systeme.

Lamports Lebenswerk ist die Weigerung, diese Lücke mit Optimismus zu übertünchen. Seine Überzeugung lautet: Nebenläufige und verteilte Systeme sind zu subtil, um sie mit Intuition zu durchdenken – also durchdenkt man sie mit Mathematik, auf dem Papier, bevor man eine einzige Zeile Code schreibt. „Denken garantiert nicht, dass wir keine Fehler machen”, sagte er 2013 gegenüber Wired. „Aber nicht zu denken garantiert, dass wir welche machen.”² Das Denken muss aufgeschrieben werden, denn beim Schreiben tritt schludriges Denken zutage: „Um zu denken, muss man schreiben. Wenn Sie denken, ohne zu schreiben, denken Sie nur, dass Sie denken.”³ Architekten zeichnen einen Bauplan, bevor ein Stein gesetzt wird; das Software-Äquivalent ist eine Spezifikation, und Lamport verbrachte die zweite Hälfte seiner Laufbahn mit dem Argument, dass unsere Systeme deshalb kaputtgehen, weil wir genau diesen Schritt überspringen.⁴

Der tiefere Gedanke betrifft die Zeit selbst. In der physikalischen Welt gibt es keine globale Uhr, der man vertrauen könnte, um Ereignisse über Maschinen hinweg zu ordnen – also müssen Sie aufhören zu fragen, wann etwas geschah, und anfangen zu fragen, was was verursacht hat. Die Kausalität, nicht die Wanduhr, ist die eigentliche Struktur einer verteilten Berechnung.⁵ Fast alles, was Lamport schuf, folgt daraus, diese eine Tatsache ernst zu nehmen – und es ist dieselbe Überzeugung, die unter der Beweisschwelle liegt: Sie dürfen die Ordnung, die Sie sich wünschen, nicht einfach voraussetzen; Sie müssen sie nachweisen.

Kontext

Leslie Lamport wurde am 7. Februar 1941 in New York City geboren.⁶ 1960 erwarb er einen B.S. in Mathematik am MIT, danach einen M.A. und – 1972 – einen Doktortitel in Mathematik an der Brandeis University, mit einer Dissertation über Singularitäten in partiellen Differentialgleichungen.⁶ Er wurde nicht zum Informatiker ausgebildet. Er wurde zum Mathematiker ausgebildet, und er hörte nie auf, sich wie einer zu verhalten. Das bestimmende Merkmal seiner Laufbahn ist, dass er die Maßstäbe der Mathematik – präzise Definitionen, ausgesprochene Annahmen, Beweise statt Tests – in ein Feld einbrachte, in dem überwiegend nach Gefühl programmiert wurde.

Die Arbeit verteilte sich auf vier Institutionen. Bei Massachusetts Computer Associates leistete er in den 1970er-Jahren die grundlegende Denkarbeit zur Ordnung von Ereignissen. Bei SRI International (1977–1985) entstand die Arbeit zu den byzantinischen Generälen. Am Systems Research Center der Digital Equipment Corporation (ab 1985, fortgeführt über die Übernahme durch Compaq bis 2001) schrieb er Paxos und begann mit der Spezifikationsarbeit. Von 2001 bis zu seinem Ruhestand Anfang 2025 war er bei Microsoft Research.⁶ Über all das hinweg blieb die Methode konstant: ein Problem in der verteilten oder nebenläufigen Datenverarbeitung finden, das alle als überliefertes Erfahrungswissen behandelten, es präzise genug definieren, um einen Satz zu formulieren, und diesen Satz dann beweisen.

Das Werk

Zeit, Uhren und die Happened-before-Relation

„Time, Clocks, and the Ordering of Events in a Distributed System” erschien 1978 in den Communications of the ACM und gehört zu den meistzitierten Arbeiten der gesamten Informatik – sie gewann im Jahr 2000 den Dijkstra-Preis für die einflussreichste Arbeit der verteilten Datenverarbeitung.⁵⁶ Die Erkenntnis ist täuschend schlicht. In einem verteilten System gibt es keine gemeinsame, verlässliche Uhr, also können Sie zwei Ereignisse nicht durch den Vergleich von Zeitstempeln ordnen. Was Sie wissen können, ist, ob ein Ereignis ein anderes hätte verursachen können: Ereignis A happened-before Ereignis B, wenn A und B im selben Prozess liegen und A zuerst kommt, oder wenn A das Senden einer Nachricht und B ihr Empfang ist. Verketten Sie diese Beziehungen, und Sie erhalten die Happened-before-Relation – formalisierte Kausalität.⁵

Die entscheidende, kontraintuitive Konsequenz ist, dass happened-before nur eine partielle Ordnung ist, keine totale. Zwei Ereignisse in verschiedenen Prozessen, zwischen denen keine Kette von Nachrichten verläuft, sind echt nebenläufig: Es gibt keine Tatsache darüber, welches zuerst kam, und jedes System, das etwas anderes behauptet, erfindet eine Ordnung, die nicht existiert.⁵ Lamport lieferte daraufhin den Algorithmus, der heute allgemein Lamport-Uhr genannt wird: Jeder Prozess führt einen Zähler, erhöht ihn bei jedem Ereignis und versieht jede ausgehende Nachricht damit; ein Empfänger setzt seinen Zähler auf eins mehr als das Maximum aus seinem eigenen Wert und dem Zeitstempel der Nachricht.⁷ Diese einfache Regel erzeugt Zeitstempel, die mit der Kausalität im Einklang stehen, und sie ist der Keim für Vektoruhren, Versionsvektoren und die gesamte Maschinerie der Konfliktauflösung moderner verteilter Datenbanken.

Über seinen Algorithmus hinaus ist diese Arbeit deshalb bedeutsam, weil sie die Fragestellung veränderte. Vor Lamport galt „Zu welcher Zeit ist das passiert?” als eine Frage, die sich in einem verteilten System beantworten ließe. Nach Lamport lautete die ehrliche Antwort: „Falsche Frage – fragen Sie, was es verursacht hat.” Diese Neuformulierung ist der Grund, warum ihm zugeschrieben wird, die verteilte Datenverarbeitung von einem Handwerk zu einer Wissenschaft gemacht zu haben.

Paxos, Konsens und replizierte Zustandsautomaten

Wenn es keine globale Uhr gibt und Maschinen ausfallen, wie kommt dann eine Gruppe von Computern überhaupt jemals überein – darüber, welche Transaktion committet wurde, wer die Sperre hält, was der nächste Eintrag im Log ist? Diese Frage ist das Konsensproblem, und Lamports Antwort ist Paxos, der Algorithmus im Herzen nahezu jedes fehlertoleranten Systems, das seither gebaut wurde. Er kombinierte ihn mit dem Ansatz des replizierten Zustandsautomaten: Wenn jede Replik im selben Zustand startet und dieselbe Folge von Befehlen in derselben Reihenfolge anwendet, bleiben sie identisch – sodass sich das gesamte Problem, ein verteiltes System konsistent zu halten, auf die Einigung über die Reihenfolge der Befehle reduziert, und genau das liefert Paxos.⁶

Die Geschichte, wie Paxos veröffentlicht wurde, ist die berühmteste Warngeschichte des Feldes. Lamport schrieb ihn als „The Part-Time Parliament” auf und stellte den Algorithmus als das Gesetzgebungsverfahren einer fiktiven antiken griechischen Insel namens Paxos dar, samt Abgeordneten, die pseudo-griechische Transliterationen der Namen seiner Kollegen trugen.⁸ Der Scherz wurde zur Katastrophe. Gutachter dachten, er meine es nicht ernst; die Arbeit wurde als unbedeutend abgelehnt; Leute, die seine Vorträge besuchten, erinnerten sich an die Indiana-Jones-Inszenierung, nicht an den Algorithmus.⁸ Sie blieb jahrelang unveröffentlicht. Der Herausgeber der Communications of the ACM veröffentlichte sie schließlich 1998 in den ACM Transactions on Computer Systems – immer noch in das Gleichnis gehüllt.⁸ Als das Feld sie weiterhin ignorierte, kapitulierte Lamport endlich und schrieb 2001 „Paxos Made Simple”, streifte das Griechische ab und legte den, wie er beharrte, tatsächlich einfachen Algorithmus darunter frei.⁸ Die Lehre, die er daraus zog, war nicht „Die Leute sind dumm.” Sie lautete: Selbst eine korrekte, wichtige Idee scheitert, wenn man das Denken dahinter verschleiert – die Darstellung ist Teil der Arbeit, nicht von ihr getrennt.

Das Problem der byzantinischen Generäle

1982 veröffentlichte Lamport gemeinsam mit Robert Shostak und Marshall Pease „The Byzantine Generals Problem”, das dem Feld seine Sprache für die schwierigste Art des Versagens gab.⁶ Eine abgestürzte Komponente ist leicht im Vergleich zu einer byzantinischen – einer Komponente, die nicht stehen bleibt, sondern lügt und unterschiedliche, widersprüchliche Informationen an verschiedene Gegenstellen sendet, sei es durch einen Fehler, durch Korruption oder durch Böswilligkeit. Die Rahmenerzählung der Arbeit: Divisionen einer Armee, jede von einem General geführt, müssen sich per Boten auf einen einzigen Plan einigen – Angriff oder Rückzug –, während eine unbekannte Teilmenge der Generäle Verräter sind, die aktiv versuchen, eine Einigung zu verhindern. Lamport bewies die exakte Schwelle dafür, wie viele Verräter ein System tolerieren und dennoch zu einer Einigung gelangen kann, und machte so aus „Was, wenn ein Knoten lügt?” statt einer vagen Sorge einen Satz mit einer ausgesprochenen Schranke.

Dieser Satz ist die intellektuelle Wurzel jedes Systems, das weiterarbeiten muss, während einige seiner Teilnehmer feindselig agieren – und er ist der Grund, warum das Wort byzantinisch Jahrzehnte später im Zentrum des Blockchain-Konsenses steht. Lamport machte sich nicht daran, Kryptowährungen zu ermöglichen; er machte sich daran, exakt zu definieren, was Fehlertoleranz bedeutet, wenn „Fehler” auch Verrat einschließt.

TLA+ und Spezifikation (und ja, LaTeX)

Der rote Faden in Lamports Laufbahn ist die Überzeugung, dass man spezifizieren muss, bevor man programmiert, und TLA+ ist diese Überzeugung, gegossen in ein Werkzeug. Die Temporal Logic of Actions ist eine Sprache, um eine präzise mathematische Beschreibung dessen zu schreiben, was ein System tun soll – seine Zustände, die Schritte dazwischen und die Eigenschaften, die es stets erfüllen muss (Safety: nie passiert etwas Schlechtes) und schließlich erreichen muss (Liveness: irgendwann passiert etwas Gutes), zwei Konzepte, die er formalisierte.⁶ Sie schreiben die Spezifikation, und ein Model Checker durchsucht den Zustandsraum nach der subtilen Verschränkung, die Ihre Invariante bricht – jenem Fehler, den Sie durch Testen niemals gefunden hätten, weil er nur auftritt, wenn drei Maschinen drei Dinge in einer Reihenfolge tun, die Sie sich nie vorgestellt haben. Sein Argument ist der Bauplan des Architekten: Man zeichnet das Gebäude, bevor man Beton gießt, und eine Software-Spezifikation ist derselbe Bauplan, geschrieben in Mathematik, weil Mathematik die präziseste Sprache ist, die wir haben.⁴

Und es gibt ein stilleres Denkmal. In den frühen 1980er-Jahren schrieb Lamport, aufbauend auf Donald Knuths TeX, LaTeX – das Makrosystem, das zur Standardmethode wurde, mit der Wissenschaftler und Mathematiker Dokumente setzen, der Grund, warum eine Generation von Arbeiten und Dissertationen so aussieht, wie sie aussieht.⁶ Es ist ein charakteristisches Lamport-Artefakt: Er musste seine eigene Arbeit präzise niederschreiben, also baute er das Werkzeug, das es allen ermöglichte, dasselbe zu tun. Der Instinkt, der TLA+ hervorbrachte – eine Notation, die Präzision erzwingt –, ist derselbe Instinkt, der LaTeX hervorbrachte.

Die Methode

Die Methode ist eine einzige Idee, fünfzig Jahre lang unerbittlich angewandt: Das Denken ist die Arbeit, und das Denken muss vor dem Code aufgeschrieben werden.

Über Kausalität nachdenken, nicht über Zeit. Es gibt keine globale Uhr, der man trauen kann, also hören Sie auf, Ereignisse danach zu ordnen, wann sie geschahen, und ordnen Sie sie danach, was was verursacht hat. Die Happened-before-Relation, nicht die Wanduhr, ist die eigentliche Struktur – und zu akzeptieren, dass zwei Ereignisse echt nebenläufig sind, ist ehrlicher, als eine Ordnung zu erfinden.⁵

Spezifizieren, bevor Sie programmieren. Für alles, wofür es keine etablierte Lösung gibt, halten Sie inne und denken Sie zuerst nach, und das Denken ist unabhängig vom Programmieren. Schreiben Sie den Bauplan – die Spezifikation – in Mathematik, denn Mathematik ist einfach und präzise, wo Prosa vage ist.⁴ „Nicht zu denken garantiert”, dass wir Fehler machen werden.²

Schreiben, um herauszufinden, ob Sie denken. Schreiben ist die Probe darauf, ob ein Gedanke real ist. „Wenn Sie denken, ohne zu schreiben, denken Sie nur, dass Sie denken.”³ Eine Spezifikation, die Sie nicht aufschreiben können, ist eine Idee, die Sie noch gar nicht haben.

Das Versagen exakt definieren. „Was, wenn ein Knoten lügt?” bleibt überliefertes Erfahrungswissen, bis Sie es als das Problem der byzantinischen Generäle formulieren und die Toleranzschranke beweisen. Präzise Definitionen verwandeln Sorgen in Sätze.⁶

Darstellung ist Teil der Korrektheit. Paxos war jahrelang korrekt, bevor irgendjemand es nutzen konnte, weil das griechische Gleichnis die Idee begrub. Ein korrektes Ergebnis, das niemand verstehen kann, ist als technische Arbeit noch nicht fertig.⁸

Einflusskette

Wer ihn prägte

Die Mathematik selbst. Lamports Ausbildung war ein Doktortitel in Mathematik, nicht in Informatik, und die gesamte Gestalt seines Beitrags ist die Einführung mathematischer Maßstäbe – Definitionen, Axiome, Beweise – in ein Feld, in dem nach Intuition programmiert worden war.⁶ (Prägender Einfluss)

Die Fehlertoleranzprobleme realer Systeme der 1970er-Jahre. Die Arbeit von SRI an zuverlässigen Systemen für Flugzeuge und der praktische Schrecken von Maschinen, die mitten in einem Protokoll ausfallen, lieferten ihm konkrete Probleme – byzantinische Fehler, Konsens –, die genau die formale Behandlung verlangten, für die er gemacht war.⁶ (Direkter Einfluss)

Edsger Dijkstra. Die Überzeugung, dass Korrektheit durch Beweis statt durch Testen hergestellt wird und dass über nebenläufige Programme formal zu räsonieren ist, gehörte Dijkstra, bevor sie Lamport gehörte. Der Preis, den Lamport für seine Arbeit zu Uhren gewann, trägt Dijkstras Namen. (Direkter Einfluss)

Wen er prägte

Jede verteilte Datenbank, jede Cloud-Plattform und jede Blockchain. Logische Uhren tragen die Konfliktauflösung in verteilten Speichern; Paxos (und sein Abkömmling Raft) ist der Konsenskern von Googles Chubby und Spanner, von ZooKeeper, etcd und der Koordinationsschicht praktisch jeder Cloud. Das Ergebnis zu den byzantinischen Generälen ist der theoretische Boden unter Bitcoin und jedem fehlertoleranten Konsensprotokoll seither.

Formale Methoden in der Industrie. Amazon Web Services nutzt bekanntermaßen TLA+, um S3, DynamoDB und andere Kerndienste zu spezifizieren und zu prüfen, bevor sie ausgeliefert werden – und findet so subtile Fehler im Design, nicht in der Produktion. Lamports Bauplan-Argument ging von der Ketzerei in die Praxis über.

Das Vokabular des Feldes. Happened-before, Safety und Liveness, replizierte Zustandsautomaten, sequenzielle Konsistenz, byzantinischer Fehler – das sind nicht Lamports Beiträge zur Sprache der verteilten Systeme; sie sind weitgehend diese Sprache.

Der rote Faden

Edsger Dijkstra argumentierte, dass man ein Programm als korrekt beweist, bevor man es ausführt – dass Testen die Anwesenheit von Fehlern zeigt, niemals ihre Abwesenheit –, und Lamport ist der unmittelbare Erbe, der den Beweis-vor-Ausführung aus sequenziellen Programmen in die weit schwierigere Welt der Nebenläufigkeit trägt, in der der Fehler, auf den man nicht testen kann, die Regel und nicht die Ausnahme ist. Barbara Liskov machte das formale Räsonieren über das Verhalten von Programmen mit Datenabstraktion und Ersetzbarkeit zu einem praktischen Grundbaustein; Lamport machte das formale Räsonieren über das Verhalten eines Systems über die Zeit zum Standard und spezifizierte nicht, was ein Objekt garantiert, sondern was ein ganzes nebenläufiges System stets und schließlich tun muss. Und Donald Knuth brachte mathematische Strenge in die Analyse von Algorithmen und baute, fast nebenbei, TeX, damit sich diese Arbeit präzise niederschreiben ließ – ein nahezu exakter Reim auf Lamport, der LaTeX aus demselben Grund darauf aufbaute und die Spezifikation selbst zu einem mathematischen Akt machte. Drei Mathematiker, die sich weigerten, „es scheint zu funktionieren” als Wissen gelten zu lassen. (Brücke der Serie)

Was ich daraus mitnehme

Die Lehre, die ich behalte, lautet: Das Denken ist die Arbeit, und das Denken ist nicht real, solange es nicht aufgeschrieben ist. Lamports Bauplan-Argument ist unbequem, weil es richtig ist: Der Grund, warum ein System in der Produktion kaputtgeht, ist fast nie, dass der Code falsch getippt wurde – es ist, dass niemand spezifiziert hat, was das System unter Nebenläufigkeit und Ausfall eigentlich tun sollte, sodass es keine Aussage gab, gegen die man den Code prüfen konnte. Die Disziplin besteht darin, die Spezifikation vor der Implementierung zu schreiben, in einer Sprache, die präzise genug ist, dass ihre Widersprüche sichtbar werden. Das ist derselbe Maßstab wie Qualität ist die einzige Variable: Die Frage lautet nie „Besteht das den Happy Path?”, sondern „Habe ich exakt formuliert, was stets wahr sein muss – und bewiesen, dass das Design es einhält?” Deshalb stütze ich mich so stark darauf, die PRD vor dem Code zu schreiben; eine PRD ist eine Lamport-Spezifikation in Arbeitskleidung.

In der Welt, in der ich heute baue – Agenten, Tool-Schleifen, Multi-Agenten-Systeme –, ist Lamports Lehre genau die, die fast jeder überspringt und dafür bezahlt. Ein Agentensystem ist ein verteiltes System: unabhängige Prozesse, keine globale Uhr, Nachrichten, die in falscher Reihenfolge oder gar nicht ankommen, und Komponenten, die stillschweigend ausfallen oder, schlimmer, lügen. Die Fehler stecken nie im Prompt; sie stecken in der Reihenfolge – zwei Agenten, die auf veraltetem Zustand handeln, ein Tool-Aufruf, dessen Ergebnis nach der Entscheidung eintrifft, die es brauchte, ein „nebenläufiges” Ereignispaar, das der Orchestrator vorgab zu ordnen. Lamports Disziplin besteht darin, der Wanduhr-Intuition nicht mehr zu trauen, explizit über Kausalität und Ausfall zu räsonieren und niederzuschreiben, was stets wahr sein muss, bevor man irgendetwas zusammenschaltet. Die Überzeugung, dass man spezifiziert, bevor man baut, dass man über ein System räsoniert, statt daran herumzustochern – das ist der rote Faden von einer Arbeit über Uhren aus dem Jahr 1978 bis zu einem Agentenrahmen des Jahres 2026, und genau deshalb behandle ich die Performance und Korrektheit eines Systems als eine Eigenschaft, die man hineinkonstruiert, niemals als eine, die man hinterher zurückzudebuggen hofft.

FAQ

Was ist Leslie Lamports Engineering-Philosophie?

Lamports Überzeugung lautet: Nebenläufige und verteilte Systeme sind zu subtil, um sie mit Intuition zu durchdenken – also muss man mit Mathematik denken, auf dem Papier, bevor man Code schreibt, so wie ein Architekt einen Bauplan zeichnet, bevor ein Stein gesetzt wird. Der Software-Bauplan ist eine Spezifikation, geschrieben in Mathematik, weil Mathematik die präziseste verfügbare Sprache ist.⁴ Darunter liegt eine Haltung zur Zeit: In einem verteilten System gibt es keine globale Uhr, der man trauen kann, also ist die eigentliche Struktur einer Berechnung die Kausalität – was was verursacht hat –, nicht der Zeitpunkt der Geschehnisse.⁵ „Denken garantiert nicht, dass wir keine Fehler machen”, sagte er, „aber nicht zu denken garantiert, dass wir welche machen.”²

Was ist eine Lamport-Uhr und die Happened-before-Relation?

Die Happened-before-Relation ist Lamports Formalisierung der Kausalität in einem verteilten System: Ereignis A happened-before Ereignis B, wenn sie im selben Prozess liegen und A zuerst kommt, oder wenn A eine Nachricht sendet und B sie empfängt, oder durch Verkettung dieser Fälle.⁵ Sie ist nur eine partielle Ordnung – zwei Ereignisse in verschiedenen Prozessen ohne verbindende Nachricht sind echt nebenläufig, und kein korrektes System kann behaupten, eines sei zuerst gekommen.⁵ Eine Lamport-Uhr setzt das mit einem Zähler pro Prozess um: bei jedem Ereignis erhöhen, jede ausgehende Nachricht damit versehen und beim Empfang den eigenen Zähler auf eins über dem Maximum aus dem eigenen Wert und dem Zeitstempel der Nachricht setzen.⁷ Das Ergebnis ist eine Menge von Zeitstempeln, die mit der Kausalität im Einklang stehen – die Grundlage für Vektoruhren und moderne verteilte Konfliktauflösung.

Was sind Paxos und das Problem der byzantinischen Generäle?

Paxos ist Lamports Algorithmus für Konsens – eine Gruppe unzuverlässiger, womöglich ausfallender Maschinen dazu zu bringen, sich auf einen einzigen Wert zu einigen, etwa den nächsten Befehl in einem replizierten Log –, und er trägt die Koordinationsschicht nahezu jedes modernen verteilten Systems. Bekanntlich veröffentlichte er ihn zunächst als Gleichnis über ein fiktives griechisches Parlament („The Part-Time Parliament”, ACM TOCS 1998); der Scherz verschleierte die Idee so sehr, dass er sie schließlich 2001 als „Paxos Made Simple” neu schrieb.⁸ Das Problem der byzantinischen Generäle (Lamport, Shostak und Pease, 1982) definiert die schwierigste Versagensart – Komponenten, die nicht bloß abstürzen, sondern lügen und widersprüchliche Informationen senden – als Generäle, die sich auf einen Plan einigen wollen, während Verräter unter ihnen die Einigung sabotieren, und beweist, wie viele Verräter ein System tolerieren kann.⁶ Es ist die theoretische Wurzel des Blockchain-Konsenses.

Warum gewann Leslie Lamport den Turing Award?

Die ACM verlieh Lamport 2013 den A.M. Turing Award „für grundlegende Beiträge zur Theorie und Praxis verteilter und nebenläufiger Systeme, insbesondere die Erfindung von Konzepten wie Kausalität und logischen Uhren, Safety und Liveness, replizierten Zustandsautomaten und sequenzieller Konsistenz”.⁶ Die Begründung erfasst die Breite seiner Arbeit: Er verwandelte die verteilte Datenverarbeitung von überliefertem Erfahrungswissen in eine Wissenschaft mit präzisen Definitionen und Beweisen, gab dem Feld einen Großteil seines Vokabulars, schuf die Spezifikationssprache TLA+, um „spezifizieren, bevor du programmierst” zu einer praktischen Disziplin zu machen, und schrieb – aufbauend auf Knuths TeX – LaTeX, das Satzsystem, das in Wissenschaft und Mathematik zum Standard wurde.⁶

Quellen