Dieses Dokument ist eine wissenschaftliche Autobiografie und bibliografische Übersicht des Informatikers Leslie Lamport (Stand: Mai 2026). Es verzeichnet sein akademisches Werk von ersten mathematischen Arbeiten aus den lateinischen 1950er-Jahren bis hin zu Fachbüchern und Publikationen im Jahr 2026. Lamport beschreibt darin die Entstehungsgeschichte, den historischen Kontext und die Publikationshürden seiner Veröffentlichungen in den Bereichen verteilte Systeme, Nebenläufigkeit, formale Methoden und Dokumentensatz.
Zu seinen zentralen wissenschaftlichen Beiträgen zählen der Bäckerei-Algorithmus für wechselseitigen Ausschluss, die Definition logischer Uhren und kausaler Ordnungen in verteilten Systemen, grundlegende Arbeiten zur byzantinischen Fehlertoleranz, das Konsensprotokoll Paxos, das Textverarbeitungssystem LaTeX sowie die Spezifikationssprache TLA+ (Temporal Logic of Actions). Das Werk skizziert zudem seinen beruflichen Werdegang – unter anderem bei SRI International, Digital Equipment Corporation und Microsoft Research – sowie seine Auszeichnungen, darunter den ACM Turing Award 2013.
Wichtigste Punkte
Akademischer und beruflicher Werdegang: Lamport erwarb 1960 seinen B.S. am M.I.T. sowie 1963 seinen M.A. und 1972 seinen Ph.D. in Mathematik an der Brandeis University. Seine beruflichen Stationen umfassen Massachusetts Computer Associates, SRI International (1977–1985), Digital Equipment Corporation/Compaq (1985–2001) und Microsoft Research (ab 2001).
Höchste Auszeichnungen: Ausgezeichnet unter anderem mit dem ACM Turing Award (2013/2014), der IEEE John von Neumann Medal (2008), dem Edsger W. Dijkstra Prize in Distributed Computing (2005, 2014) sowie Aufnahme in die National Academy of Engineering (1991) und die National Academy of Sciences (2011).
Bäckerei-Algorithmus (1974): Erfindung eines grundlegenden Algorithmus für wechselseitigen Ausschluss (Mutual Exclusion), der nachweist, dass Synchronisation ohne unterlagerte atomare Speicherzugriffe oder atomare Register realisierbar ist.
Logische Uhren und Kausalität (1978): In seiner meistzitierten Arbeit („Time, Clocks and the Ordering of Events in a Distributed System“) überträgt Lamport Prinzipien der Speziellen Relativitätstheorie auf Informatiksysteme und definiert die kausale Ordnung von Ereignissen über logische Uhren.
Byzantinische Fehlertoleranz (1980/1982): Mathematischer Nachweis, dass in Systemen mit willkürlichen (byzantinischen) Ausfällen mindestens $3n+1$ Prozessoren erforderlich sind, um $n$ Fehler ohne digitale Signaturen zu tolerieren (mit Signaturen reichen $2n+1$).
Entwicklung von LaTeX (1986): Konstruktion des Makropakets LaTeX auf Basis von Donald Knuths TeX-Satzsystem sowie Publikation des Standard-Handbuchs zur logischen Dokumentstrukturierung.
Paxos-Konsensalgorithmus (1998): Formulierung des Drei-Phasen-Konsensprotokolls Paxos zur zustandssicheren Replikation in fehlertoleranten asynchronen Netzwerken (ursprünglich 1990 verfasst). Spätere Verfeinerungen umfassen Disk Paxos, Cheap Paxos, Fast Paxos und Vertical Paxos.
Temporal Logic of Actions (TLA / TLA+): Entwicklung eines mathematischen Formalismus, der Aktionen als Prädikate über geprimte und ungeprimte Zustandsvariablen ausdrückt, um nebenläufige und verteilte Soft- und Hardware ohne die Inkonsistenzen klassischer Programmiersprachen zu spezifizieren und zu verifizieren.
Formalisierung von Safety und Liveness: Grundlegende Differenzierung und mathematische Begriffsprägung von Sicherheitseigenschaften („etwas Schlechtes passiert nie“) und Lebendigkeitseigenschaften („etwas Gutes passiert schließlich“) für nebenläufige Programme.
Hierarchische Beweismethodik: Entwicklung und Verfechter einer strukturierten, hierarchischen Beweisführung für mathematische Theoreme und Programmbeweise zur Vermeidung von Fehlern in unstrukturierten Prosabeweisen.
Glossar
Bakery Algorithm (Bäckerei-Algorithmus): Ein nebenläufiger Algorithmus zur Garantie des wechselseitigen Ausschlusses, der korrekt funktioniert, selbst wenn Speicherlese- und Speicherschreibvorgänge zeitlich überlappen und nicht-atomar sind.
Byzantine Fault (Byzantinischer Fehler): Ein Fehlerzustand in verteilten Systemen, bei dem eine Komponente völlig unvorhersehbar oder böswillig agiert und verschiedenen Systemknoten widersprüchliche Daten übermittelt.
Consensus (Konsens): Das fundamentale Problem in der verteilten Informatik, bei dem sich mehrere autonome Prozessoren trotz Netzwerkverzögerungen oder Knotenausfällen auf einen einzelnen Datenwert einigen müssen.
LaTeX: Ein Softwaresystem zum Erstellen qualitativ hochwertiger Typografien und mathematischer Dokumente, das Inhalte und semantische Struktur von der visuellen Formatierung trennt.
Liveness (Lebendigkeitseigenschaft): Eine formale Zusicherung in der Verifikation, dass ein System im Laufe der Zeit einen gewünschten Zielzustand erreicht oder einen Fortschritt macht.
Mutual Exclusion (Wechselseitiger Ausschluss): Eine Eigenschaft der Nebenläufigkeitssteuerung, die verhindert, dass mehr als ein Prozess gleichzeitig auf einen kritischen Speicherbereich oder eine Ressource zugreift.
Paxos: Eine Protokollfamilie zur Erreichung von Konsens in einem Netzwerk aus potenziell unzuverlässigen Knoten, bildet die Basis für verteilte Zustandsmaschinen und Datenbankreplikationen.
Safety (Sicherheitseigenschaft): Eine formale Systemeigenschaft, die garantiert, dass das System zu keinem Zeitpunkt in einen unzulässigen oder fehlerhaften Zustand gerät.
Sequential Consistency (Sequenzielle Konsistenz): Ein Konsistenzmodell für Mehrprozessorsysteme, das fordert, dass das Ausführungsergebnis dem entspricht, als ob alle Operationen aller Prozessoren in einer einzigen sequenziellen Reihenfolge abgearbeitet worden wären.
TLA+ (Temporal Logic of Actions): Eine auf der modalen Temporallogik und Mengenlehre basierende formale Spezifikationssprache zur mathematischen Modellierung und Prüfung komplexer Soft- und Hardwaresysteme.