Wenn wir in das Jahr 1974 zurückreisen könnten, hätten wir Leslie Lamport vielleicht in seiner belebten Bäckerei in der Nachbarschaft gefunden, wo er sich mit folgendem Problem auseinandersetzte. Die Bäckerei hatte mehrere Kassierer, aber wenn sich mehrere Personen gleichzeitig an einen Kassierer wandten, versuchte dieser, mit allen gleichzeitig zu sprechen, was zu Verwirrung führte. Lamport erkannte, dass es eine Möglichkeit geben musste, um zu gewährleisten, dass sich die Leute nur einzeln an die Kassierer wenden. Dieses Problem erinnerte Lamport an ein Problem, das der Informatiker Edsger Dijkstra in einem früheren Artikel über ein anderes alltägliches Problem aufgeworfen hatte: die Frage, wie man die Essensutensilien an einem Esstisch verteilt. Eine der Koordinationsaufgaben bestand darin, zu gewährleisten, dass jedes Utensil jeweils nur von einem Gast benutzt wurde, was später als das Problem des gegenseitigen Ausschlusses verallgemeinert wurde – genau die Herausforderung, mit der Lamport in der Bäckerei konfrontiert war.

Eines Morgens im Jahr 1974 kam Lamport eine Idee, wie die Kunden der Bäckerei das Problem des gegenseitigen Ausschlusses untereinander lösen könnten, ohne sich auf die Hilfe der Bäckerei zu verlassen. Es funktionierte in etwa so: Die Kunden wählten beim Betreten der Bäckerei Nummern aus und wurden dann an der Kasse entsprechend ihrer Nummernbestellung bedient. Um eine Nummer zu wählen, fragt eine Kundin nach der Nummer aller um sie herum und wählt eine Nummer, die höher ist als alle anderen.

Aus dieser einfachen Idee wurde ein eleganter Algorithmus zur Lösung des Problems des gegenseitigen Ausschlusses, ohne dass irgendwelche unteilbaren Operationen auf niedrigerer Ebene erforderlich waren. Sie war auch eine reiche Quelle für zukünftige Ideen, da viele Probleme gelöst werden mussten. Zum Beispiel brauchten einige Bäckereikunden sehr lange, um andere Nummern zu prüfen, und in der Zwischenzeit kamen weitere Kunden und wählten zusätzliche Nummern aus. Ein anderes Mal wollte der Leiter der Bäckerei eine Momentaufnahme aller Kundennummern erhalten, um genügend Gebäck vorbereiten zu können. Lamport sagte später: „Ein paar Jahre lang nach meiner Entdeckung des Bäckerei-Algorithmus habe ich alles, was ich über Parallelität gelernt habe, aus dem Studium dieses Algorithmus gelernt.“

Der Bäckerei-Algorithmus und Lamports andere bahnbrechende Werke – viele mit amüsanten Namen und zugehörigen Gleichnissen – sind zu Säulen der Informatik geworden. Seine Sammlung bildet die Grundlage für weite Bereiche der Nebenläufigkeit und hat die Spezifikation, Entwicklung und Verifikation von nebenläufigen Systemen beeinflusst.

Nach seinem Doktortitel in Mathematik an der Brandeis University im Jahr 1972 arbeitete Lamport von 1970 bis 1977 als Informatiker bei Massachusetts Computer Associates, von 1977 bis 1985 bei SRI International und von 1985 bis 2001 im Digital Equipment Corporation Systems Research Center (später im Besitz von Compaq). Im Jahr 2001 wechselte er zu Microsoft Research in Mountain View, Kalifornien.

Es war kein Zufall, dass er seine Forschungskarriere in einer industriellen Forschungsumgebung verbrachte. „Ich arbeite gerne in einem industriellen Forschungslabor, weil ich so viele Anregungen bekomme“, sagt Lamport. „Wenn ich alleine arbeite und mir Probleme ausdenke, komme ich nur auf eine kleine Anzahl von Dingen, aber wenn ich in die Welt hinausgehe, wo Leute an echten Computersystemen arbeiten, gibt es eine Million Probleme da draußen. Wenn ich auf die meisten Dinge zurückblicke, an denen ich gearbeitet habe – Byzantinische Generäle, Paxos -, dann sind sie aus realen Problemen entstanden.“

Seine Arbeiten beleuchteten grundlegende Fragen der nebenläufigen Programme, für die es damals noch keine formale Theorie gab. Er beschäftigte sich mit grundlegenden Konzepten wie Kausalität und logischer Zeit, atomaren und regulären gemeinsamen Registern, sequenzieller Konsistenz, Replikation von Zustandsautomaten, byzantinischer Vereinbarung und Wartefreiheit. Er arbeitete an Algorithmen, die zum Standardverfahren für fehlertolerante verteilte Systeme geworden sind. Er hat auch ein umfangreiches Werk über die formale Spezifikation und Verifikation von nebenläufigen Systemen entwickelt und zur Entwicklung automatisierter Werkzeuge beigetragen, die diese Methoden anwenden. Wir werden nur einige seiner Beiträge erwähnen.

1. Lösungen für den gegenseitigen Ausschluss und der Bakery-Algorithmus

Lamports einflussreiche Arbeiten aus den 1970er und 1980er Jahren kamen zu einer Zeit, als man die grundlegenden Probleme der Programmierung für mehrere nebenläufige Prozessoren nur wenig verstand.

Zum Beispiel war bekannt, dass eine korrekte Ausführung erfordern kann, dass sich parallele Aktivitäten während der Zeiträume in „kritischen Abschnitten“, in denen sie dieselben Daten manipulieren, gegenseitig ausschließen, um unerwünschte Verschachtelungen von Operationen zu verhindern. Die Ursprünge dieses Problems des gegenseitigen Ausschlusses gehen auf die bahnbrechende Arbeit von Edsger Dijkstra zurück, die auch seine Lösung beinhaltet. Dijkstras Algorithmus ist zwar korrekt, hängt aber davon ab, dass die Zugriffe auf den gemeinsamen Speicher atomar sind – dass ein Prozessor, der liest, während ein anderer schreibt, warten muss, anstatt einen möglicherweise verstümmelten Wert zurückzugeben. In gewissem Sinne konstruiert er eine High-Level-Lösung aus dem bereits von der Hardware implementierten Low-Level-Verfahren des gegenseitigen Ausschlusses.

Lamports bemerkenswert eleganter und intuitiver „Bakery Algorithm“ tut dies nicht. Seine Lösung ordnet konkurrierende Prozesse in einer impliziten Warteschlange entsprechend ihrer Ankunftsreihenfolge an, ähnlich wie eine Warteschlange in einer Bäckerei. Dabei spielt es keine Rolle, ob ein Prozessor, der Daten liest, die gerade von einem anderen Prozessor aktualisiert werden, Müll bekommt. Der Algorithmus funktioniert trotzdem.

Lamport erinnert sich an seine Entdeckung des Bakery-Algorithmus.

Der Bakery-Algorithmus ist zum Lehrbuchmaterial geworden, und die meisten Studenten der Informatik begegnen ihm im Laufe ihres Studiums.

2. Grundlagen der nebenläufigen Programmierung

Aus der Arbeit am Bakery-Algorithmus gingen mehrere wichtige neue Konzepte hervor, ein Trend, der sich in Lamports Karriere mehrfach wiederholte. Die Erfahrung mit der Entwicklung von nebenläufigen Algorithmen und der Überprüfung ihrer Korrektheit veranlasste ihn, sich auf die Grundlagen zu konzentrieren, die das Verhalten von Multiprozessoren in einer für Programmierer mathematisch nachvollziehbaren Weise ermöglichen würden. Während er an einer Lösung für ein bestimmtes konkretes Problem arbeitete, erfand Lamport Abstraktionen und allgemeine Regeln, die benötigt wurden, um über die Korrektheit des Problems nachzudenken, und diese konzeptionellen Beiträge wurden dann zu theoretischen Säulen der nebenläufigen Programmierung.

Schleifenfreiheit: Die Arbeit am Bakery-Algorithmus führte ein wichtiges Konzept namens „Schleifenfreiheit“ ein. Einige offensichtliche Lösungen, die für das Problem des gegenseitigen Ausschlusses in Frage kommen, weisen den Prozessen im Voraus „Schleifen“ im Wechsel zu. Dies zwingt jedoch Prozesse dazu, auf andere zu warten, die langsam sind und noch nicht einmal den Punkt erreicht haben, an dem sie sich streiten. In Anlehnung an die Bäckerei wäre es so, als würde man in eine leere Bäckerei kommen und gebeten werden, auf einen Kunden zu warten, der noch gar nicht in der Bäckerei angekommen ist. Im Gegensatz dazu drückt die Schleifenfreiheit die Fähigkeit von Prozessen aus, unabhängig von der Geschwindigkeit anderer Prozesse voranzukommen. Da der Bäckerei-Algorithmus die Prozesse in der Reihenfolge ihres Eintreffens abarbeitet, verfügt er über Schleifenfreiheit. Dies ist ein entscheidendes Konzept, das bei der Entwicklung vieler nachfolgender Algorithmen und bei der Entwicklung von Speicherarchitekturen verwendet wurde. Die Wartefreiheit, eine Bedingung, die ein unabhängiges Fortschreiten trotz Fehlern erfordert, hat ihre eindeutigen Wurzeln im Begriff der Schleifenfreiheit und dem Bakery-Doorway-Konzept. Sie wurde später von anderen, darunter Maurice Herlihy, ausgiebig erforscht.

Sequentielle Konsistenz: Die Arbeit mit einer Multi-Core-Architektur mit verteiltem Cache-Speicher veranlasste Lamport, formale Spezifikationen für kohärentes Cache-Verhalten in Multiprozessorsystemen zu erstellen. Diese Arbeit brachte etwas Ordnung in das Chaos auf diesem Gebiet, indem sie die sequentielle Konsistenz erfand, die zum Goldstandard für Speicherkonsistenzmodelle geworden ist. Dieser einfache und intuitive Begriff bietet genau das richtige Maß an „Atomarität“, damit Software funktionieren kann. Heute entwerfen wir Hardwaresysteme mit Zeitstempel- oder Partial-Store-Ordnung und zusätzlichen Speicherzaunanweisungen, die es Programmierern ermöglichen, die Hardware als sequentiell konsistent erscheinen zu lassen. Die Programmierer können dann Algorithmen implementieren, die starke Konsistenzeigenschaften bieten. Dies ist der Schlüssel zu den Speicherkonsistenzmodellen von Java und C++. Unsere Multicore-Prozessoren laufen heute auf der Grundlage von Prinzipien, die Leslie Lamport 1979 beschrieben hat.

Atomische und regelmäßige Register: Der Bakery-Algorithmus brachte Lamport auch dazu, sich über die genaue Semantik des Speichers Gedanken zu machen, wenn mehrere Prozesse interagieren und Daten gemeinsam nutzen. Es dauerte fast ein Jahrzehnt, diese Frage zu formalisieren, und das Ergebnis ist die Abstraktion von regulären und atomaren Registern.

Seine Theorie gibt jeder Operation auf einem gemeinsam genutzten Register eine explizite Dauer, die mit einem Aufruf beginnt und mit einem Ergebnis endet. Die Register können durch eine Vielzahl von Techniken implementiert werden, z. B. durch Replikation. Dennoch sollen die Interaktionen von Prozessen mit einem atomaren Register „wie“ serielle Zugriffe auf den tatsächlichen gemeinsamen Speicher aussehen. Die Theorie umfasst auch eine schwächere Semantik der Interaktion, wie die eines regulären Registers. Ein reguläres Register erfasst Situationen, in denen Prozesse verschiedene Repliken des Registers lesen, während es aktualisiert wird. Zu jedem Zeitpunkt können einige Replikate aktualisiert werden, während andere nicht aktualisiert werden, und schließlich werden alle Replikate den aktualisierten Wert enthalten. Wichtig ist, dass diese schwächere Semantik ausreicht, um den gegenseitigen Ausschluss zu unterstützen: Der Bakery-Algorithmus funktioniert korrekt, wenn ein Leser, der sich mit einem Schreiber überschneidet, einen beliebigen Wert zurückerhält.

Lamport beschreibt seine Arbeit zur präzisen Definition von Abstraktionen für atomare, reguläre und sichere Register.

Diese Arbeit initiierte ein eigenes Teilgebiet der Forschung im Bereich des verteilten Rechnens, das immer noch floriert. Lamports atomare Objekte unterstützten nur Lese- und Schreiboperationen, das heißt, sie waren atomare Register. Der Begriff wurde von Maurice Herlihy und Jeannette Wing auf andere Datentypen verallgemeinert, und ihr Begriff „Linearisierbarkeit“ wurde zum Synonym für Atomarität. Heute verwenden im Wesentlichen alle nicht-relationalen Speichersysteme, die von Unternehmen wie Amazon, Google und Facebook entwickelt wurden, Linearisierbarkeit und sequentielle Konsistenz für ihre Datenkohärenzgarantien.

3. Grundlagen verteilter Systeme

Ein spezieller Typ von nebenläufigen Systemen ist ein verteiltes System, das dadurch gekennzeichnet ist, dass es über Prozesse verfügt, die Nachrichten verwenden, um miteinander zu interagieren. Leslie Lamport hatte einen großen Einfluss auf die Art und Weise, wie wir über verteilte Systeme denken, sowie auf die technische Praxis in diesem Bereich.

Logische Uhren: Viele Menschen erkannten, dass ein globaler Zeitbegriff für ein verteiltes System nicht natürlich ist. Lamport war der erste, der einen alternativen Begriff von „logischen Uhren“ präzisierte, die eine partielle Ordnung der Ereignisse auf der Grundlage der kausalen Beziehung auferlegen, die durch das Senden von Nachrichten von einem Teil des Systems zu einem anderen entsteht. Seine Abhandlung über „Time, Clocks, and the Ordering of Events in a Distributed System“ ist die am häufigsten zitierte Arbeit von Lamport, und in der Informatik werden logische Uhren oft als Lamport-Zeitstempel bezeichnet. Seine Arbeit wurde im Jahr 2000 mit dem Principles of Distributed Computing Conference Influential Paper Award (später umbenannt in Edsger W. Dijkstra Prize in Distributed Computing) ausgezeichnet und erhielt 2007 einen ACM SIGOPS Hall of Fame Award.

Lamport beschreibt seine Arbeit „Time, Clocks…“ und ihre Beziehung zur speziellen Relativitätstheorie.

Um zu verstehen, warum diese Arbeit so einflussreich geworden ist, muss man sich vergegenwärtigen, dass es zum Zeitpunkt der Erfindung keine gute Möglichkeit gab, die Kommunikationsverzögerung in verteilten Systemen zu erfassen, außer durch Verwendung von Echtzeit. Lamport erkannte, dass sich diese Systeme durch die Kommunikationsverzögerung stark von einem Multiprozessorsystem mit gemeinsamem Speicher unterscheiden. Die Einsicht kam ihm, als er eine Abhandlung über replizierte Datenbanken las und feststellte, dass die logische Reihenfolge der Befehle die Kausalität verletzen könnte.

Die Verwendung der Reihenfolge von Ereignissen zum Nachweis der Korrektheit eines Systems wird heute meist für intuitive Beweise von gleichzeitigen Synchronisationsalgorithmen verwendet. Ein weiterer wichtiger Beitrag dieser Arbeit war die Demonstration der Replikation eines Zustandsautomaten mit logischen Uhren, die im Folgenden erläutert wird.

Verteilte Schnappschüsse: Sobald man die kausale Ordnung definiert, folgt der Begriff der konsistenten globalen Zustände von selbst. Dies führte zu einer weiteren aufschlussreichen Arbeit. Lamport und Mani Chandy erfanden den ersten Algorithmus, um den Zustand eines beliebigen verteilten Systems zu lesen (einen „Schnappschuss“ zu machen). Dieses Konzept ist so mächtig, dass andere es später in verschiedenen Bereichen wie Netzwerken, Selbststabilisierung, Fehlersuche und verteilten Systemen verwendeten. Diese Arbeit wurde 2013 mit dem ACM SIGOPS Hall of Fame Award ausgezeichnet.

4. Fault tolerance and State Machine Replication

„Ein verteiltes System ist ein System, in dem der Ausfall eines Computers, von dem man nicht einmal wusste, dass er existiert, den eigenen Computer unbrauchbar machen kann“ ist ein berühmtes Lamport-Witzchen. Ein Großteil seiner Arbeit befasst sich mit Fehlertoleranz.

State Machine Replication (SMR): Der vielleicht bedeutendste von Lamports vielen Beiträgen ist das Paradigma der State Machine Replication, das in dem berühmten Papier „Time, Clocks, and the Ordering of Events in a Distributed System“ eingeführt und bald darauf weiterentwickelt wurde. Die Abstraktion fasst jeden Dienst als zentralisierte Zustandsmaschine auf – eine Art universelle Rechenmaschine, ähnlich einer Turing-Maschine. Er hat einen internen Zustand und verarbeitet Befehle nacheinander, wobei jeder Befehl zu einem neuen internen Zustand führt und eine Antwort erzeugt. Lamport erkannte, dass die schwierige Aufgabe der Replikation eines Dienstes über mehrere Computer hinweg bemerkenswert einfach zu bewältigen ist, wenn man allen Replikaten dieselbe Abfolge von Eingabebefehlen vorgibt und sie eine identische Abfolge von Zuständen durchlaufen.

Dieses aufschlussreiche SMR-Paradigma liegt vielen zuverlässigen Systemen zugrunde und gilt aufgrund seiner Eleganz als Standardansatz für den Aufbau replizierter verteilter Systeme. Bevor Lamport jedoch eine vollständige Lösung für SMR entwickelte, musste er sich mit einem Kernbestandteil, der Vereinbarung, befassen, die in seiner nächsten Arbeit behandelt wurde.

Byzantinische Vereinbarung: Während Zustandsautomatenansätze, die gegen Absturzfehler resistent sind, für viele Anwendungen ausreichen, benötigen unternehmenskritischere Systeme, wie z.B. für die Avionik, ein noch extremeres Modell der Fehlertoleranz, das unempfindlich gegenüber Knoten ist, die das System von innen heraus stören könnten.

Am Stanford Research Institute (später SRI International) gehörte Lamport in den 1970er Jahren zu einem Team, das der NASA bei der Entwicklung eines robusten Avionik-Steuerungssystems half. Formale Garantien waren eine absolute Notwendigkeit, da es sich um eine missionskritische Aufgabe handelte. Die Sicherheit musste gegen die extremsten Systemstörungen, die man sich vorstellen konnte, garantiert werden. Eine der ersten Aufgaben, mit denen das SRI-Team betraut wurde, bestand darin, die Korrektheit eines von der NASA entwickelten Cockpit-Steuerungssystems mit drei Computersystemen zu beweisen, die mit Hilfe von Mehrheitsentscheidungen jede fehlerhafte Komponente ausblenden.

Das Ergebnis der Arbeit des Teams waren mehrere grundlegende Konzepte und Erkenntnisse in Bezug auf diese strengen Arten von robusten Systemen. Dazu gehörten eine grundlegende Definition von Robustheit in diesem Umfeld, eine Abstraktion des Koordinationsproblems, das bis heute jedem replizierten System zugrunde liegt, und die überraschende Erkenntnis, dass Systeme mit drei Computern niemals ein missionskritisches Cockpit sicher betreiben können!

In zwei bahnbrechenden Arbeiten („LPS“), die zusammen mit Pease und Shostak veröffentlicht wurden, identifizierte das Team erstmals eine etwas merkwürdige Schwachstelle. LPS stellte fest, dass „eine ausgefallene Komponente ein Verhalten zeigen kann, das oft übersehen wird, nämlich das Senden widersprüchlicher Informationen an verschiedene Teile des Systems“. Allgemeiner ausgedrückt, könnte eine fehlerhafte Komponente auf eine Art und Weise funktionieren, die mit ihrem vorgeschriebenen Verhalten völlig unvereinbar ist und fast bösartig erscheinen könnte.

Das neue Fehlermodell brauchte einen Namen. Zu dieser Zeit gab es ein verwandtes klassisches Problem der Koordination von zwei kommunizierenden Computern, das 1975 in einer Arbeit vorgestellt und von Jim Gray als „The Two Generals Paradox“ bezeichnet wurde. Dies veranlasste Lamport dazu, sich die Kontrollcomputer in einem Cockpit als eine Armee byzantinischer Generäle vorzustellen, wobei die Armee versucht, einen koordinierten Angriff durchzuführen, während Verräter im Inneren widersprüchliche Signale senden. Der Name „Byzantinische Fehler“ wurde für dieses Fehlermodell gewählt, und es folgten zahlreiche wissenschaftliche Arbeiten. Das byzantinische Fehlermodell wird immer noch verwendet, um die schlimmsten Arten von Pannen und Sicherheitslücken in Systemen zu erfassen.

Lamport erklärt, dass er eine Geschichte über „byzantinische Generäle“ verwendet, um ein Problem in fehlertoleranten verteilten Systemen zu formulieren.

Byzantinische Fehler analysieren die schlechten Dinge, die passieren können. Aber was ist mit den guten Dingen, die passieren müssen? LPS hat auch eine abstrakte Formulierung für das Problem der Koordinierung trotz byzantinischer Fehlschläge gefunden, die als „Byzantinische Vereinbarung“ bekannt ist. Diese prägnante Formulierung drückt die Aufgabe der Kontrollkoordination als das Problem aus, eine Einigungsentscheidung für ein einzelnes Bit zu treffen, wobei jede Komponente mit potenziell unterschiedlichen Bits beginnt. Sobald man sich auf ein einzelnes Bit geeinigt hat, kann man es wiederholt verwenden, um ein ganzes komplexes System koordiniert zu halten. Das Papier zeigt, dass vier Computer benötigt werden, um sich bei einer einzigen Störung auf ein einziges Bit zu einigen. Drei reichen nicht aus, denn bei drei Einheiten kann eine fehlerhafte Einheit widersprüchliche Werte an die beiden anderen Einheiten senden und mit jeder eine andere Mehrheit bilden. Ganz allgemein zeigten sie, dass 3F+1 Einheiten erforderlich sind, um F gleichzeitig fehlerhafte Komponenten zu überwinden. Um dies zu beweisen, verwendeten sie ein schönes Symmetrieargument, das als „Hexagon-Argument“ bekannt geworden ist. Dieses Archetyp-Argument hat weitere Verwendungen gefunden, wenn man argumentiert, dass eine fehlerhafte Einheit, die widersprüchliche Informationen an verschiedene Teile des Systems sendet, nicht von einer symmetrischen Situation zu unterscheiden ist, in der die korrekten und fehlerhaften Rollen vertauscht sind.

LPS zeigte auch, dass 3F+1 Einheiten ausreichen, und sie präsentierten eine Lösung für das Erreichen einer byzantinischen Vereinbarung zwischen den 3F+1 Einheiten in F+1 synchronen Kommunikationsrunden. Sie zeigten auch, dass bei Verwendung digitaler Signaturen nur 2F+1 Einheiten ausreichend und notwendig sind.

Das Problem der Byzantinischen Vereinbarung und seine Lösungen sind zum Markenzeichen fehlertoleranter Systeme geworden. Die meisten Systeme, die mit Redundanz aufgebaut sind, nutzen sie intern zur Replikation und zur Koordination. Lamport selbst verwendete es später bei der Entwicklung des State Machine Replication Paradigmas, das im Folgenden besprochen wird und das die algorithmische Grundlage für die Replikation bildet.

Die Arbeit von 1980 wurde mit dem Edsger W. Dijkstra Prize in Distributed Computing 2005 ausgezeichnet, und die Arbeit von 1982 erhielt den Jean-Claude Laprie Award in Dependable Computing.

Paxos: Mit dem wachsenden Verständnis des Vereinbarungsproblems für verteiltes Rechnen war es für Lamport an der Zeit, zur State Machine Replication zurückzukehren und sich dort mit Fehlern zu befassen. Die erste SMR-Lösung, die er in seiner Arbeit von 1978 vorstellte, ging davon aus, dass es keine Ausfälle gibt, und sie nutzt die logische Zeit, um die Replikate durch dieselbe Befehlssequenz zu führen. 1989 entwarf Lamport einen fehlertoleranten Algorithmus namens Paxos. In Fortführung seines Trends zu humorvollen Gleichniserzählungen stellt das Papier die imaginäre Geschichte eines Regierungsparlaments auf einer altgriechischen Insel namens Paxos dar, in der die Abwesenheit einer beliebigen Anzahl von Mitgliedern oder möglicherweise aller Mitglieder toleriert werden kann, ohne dass die Konsistenz verloren geht.

Lamport beschreibt die Ursprünge seines Paxos-Algorithmus für fehlertolerantes verteiltes Rechnen.

Unglücklicherweise machte das Setting als griechische Parabel das Papier für die meisten Leser schwer verständlich, und es dauerte neun Jahre von der Einreichung bis zur Veröffentlichung im Jahr 1998. Aber der technische Bericht der DEC von 1989 wurde dennoch wahrgenommen. Lamports Kollege Butler Lampson verkündete die Idee in der Distributed-Computing-Gemeinschaft. Kurz nach der Veröffentlichung von Paxos boten Googles Chubby-System und Apaches quelloffener ZooKeeper State Machine Replication als externen, weit verbreiteten Dienst an.

Paxos fügt eine Abfolge von Zustimmungsentscheidungen auf optimierte Weise zu einer Folge von State-Machine-Befehlen zusammen. Wichtig ist, dass die erste Phase der in dem Paxos-Papier beschriebenen Vereinbarungskomponente (Synode genannt) vermieden werden kann, wenn derselbe Anführer mehrere Entscheidungen leitet; diese Phase muss nur durchgeführt werden, wenn ein Anführer ersetzt werden muss. Dieser aufschlussreiche Durchbruch macht einen Großteil der Popularität von Paxos aus und wurde später vom Google-Team Multi-Paxos genannt. Das Paxos-Papier von Lamport wurde 2012 mit dem ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award ausgezeichnet.

SMR und Paxos haben sich zum De-facto-Standard-Framework für den Entwurf und die Argumentation von Konsens- und Replikationsmethoden entwickelt. Viele Unternehmen, die kritische Informationssysteme aufbauen, darunter Google, Yahoo, Microsoft und Amazon, haben die Paxos-Grundlagen übernommen.

5. Formale Spezifikation und Verifikation von Programmen

In den Anfängen der Nebenläufigkeitstheorie entstand der Bedarf an guten Werkzeugen, um Lösungen zu beschreiben und ihre Korrektheit zu beweisen. Lamport hat zentrale Beiträge zur Theorie der Spezifikation und Verifikation von nebenläufigen Programmen geleistet. Er war zum Beispiel der erste, der die Begriffe Sicherheitseigenschaften und Liveness-Eigenschaften für asynchrone verteilte Algorithmen formulierte. Dabei handelte es sich um die Verallgemeinerung der Eigenschaften „partielle Korrektheit“ und „vollständige Korrektheit“, die zuvor für sequenzielle Programme definiert worden waren. Heute bilden Sicherheits- und Liveness-Eigenschaften die Standardklassifikation für Korrektheitseigenschaften asynchroner verteilter Algorithmen.

In einer weiteren Arbeit mit Martin Abadi wurde eine spezielle Abstraktion, die so genannten Prophezeiungsvariablen, in ein Algorithmusmodell eingeführt, um eine Situation zu behandeln, in der ein Algorithmus eine nicht-deterministische Wahl auflöst, bevor die Spezifikation dies tut. Abadi und Lamport wiesen auf Situationen hin, in denen solche Probleme auftreten, und entwickelten die Theorie, die zur Unterstützung dieser Erweiterung der Theorie erforderlich ist. Darüber hinaus bewiesen sie, dass immer dann, wenn ein verteilter Algorithmus auf eine Spezifikation trifft, bei der beide als Zustandsautomaten ausgedrückt sind, die Übereinstimmung zwischen ihnen durch eine Kombination von Prophezeiungsvariablen und früheren Begriffen wie Geschichtsvariablen nachgewiesen werden kann. Diese Arbeit wurde 2008 mit dem LICS-Test-Of-Time-Preis ausgezeichnet.

Formale Modellierungssprachen und Verifikationswerkzeuge: Zusätzlich zur Entwicklung der oben genannten grundlegenden Begriffe hat Lamport die Sprache TLA (Temporal Logic of Actions) und das TLA+-Toolset entwickelt, um verteilte Algorithmen und Systeme zu modellieren und zu verifizieren.

Lamport beschreibt TLA und seine Verbindung zur Verfeinerungsabbildung.

TLA und TLA+ unterstützen die Spezifikation und den Beweis von Sicherheits- und Liveness-Eigenschaften unter Verwendung einer Notation, die auf temporaler Logik basiert. Lamport hat die Entwicklung von Verifikationswerkzeugen auf der Grundlage von TLA+ beaufsichtigt, insbesondere den von Yuan Yu entwickelten TLC Model Checker. TLA+ und TLC wurden zur Beschreibung und Analyse realer Systeme eingesetzt. So wurden diese Tools beispielsweise eingesetzt, um einen großen Fehler im Kohärenzprotokoll zu finden, das in der Hardware der Xbox 360 von Microsoft vor deren Veröffentlichung im Jahr 2005 verwendet wurde. Bei Intel wurde es für die Analyse eines Cache-Kohärenzprotokolls des Intel Quick Path Interconnect verwendet, das im Nehalem-Kernprozessor implementiert ist. Um Ingenieuren den Umgang mit seinen formalen Spezifikationswerkzeugen zu vermitteln, hat Lamport ein Buch geschrieben. In jüngerer Zeit hat Lamport die formale Sprache PlusCAL und Werkzeuge für die Verifizierung verteilter Algorithmen entwickelt; diese Arbeit baut auf TLA+ auf.

6. LaTeX

Wenn man eine so umfangreiche Sammlung eindrucksvoller Arbeiten erstellt, ist es nur natürlich, dass man sich ein bequemes Satzwerkzeug wünscht. Lamport wünschte sich nicht nur eines, er schuf eines für die gesamte Gemeinschaft. Außerhalb des Bereichs der Gleichzeitigkeit ist Lamports Latex-System, eine Reihe von Makros zur Verwendung mit Donald Knuths TeX-Satzsystem. LaTeX fügte TeX drei wichtige Dinge hinzu:

1. Das Konzept der „Satzumgebung“, das seinen Ursprung im Scribe-System von Brian Reid hatte.
2. Eine starke Betonung der strukturellen statt der typografischen Auszeichnung.
3. Ein generisches Dokumentendesign, das flexibel genug ist, um für eine Vielzahl von Dokumenten geeignet zu sein.

Lamport hat diese Ideen nicht entwickelt, aber indem er sie so weit wie möglich vorangetrieben hat, hat er ein System geschaffen, das die Qualität von TeX und viel von dessen Flexibilität bietet, aber viel einfacher zu benutzen ist. Latex wurde zum De-facto-Standard für das technische Publizieren in der Informatik und in vielen anderen Bereichen.

Es gibt viele weitere wichtige Arbeiten von Leslie Lamport – zu viele, um sie hier zu beschreiben. Sie sind in chronologischer Reihenfolge auf der Homepage von Lamport aufgelistet, begleitet von historischen Anmerkungen, die die Motivation und den Kontext jedes Ergebnisses beschreiben.

Jedes Mal, wenn Sie auf einen modernen Computer zugreifen, werden Sie wahrscheinlich mit den Algorithmen von Leslie Lamport in Berührung kommen. Und all diese Arbeit begann mit dem Versuch zu verstehen, wie man eine Warteschlange in einer örtlichen Bäckerei organisiert.

Autorin: Dahlia Malkhi
Weitere Mitwirkende: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, und Len Shustek