Als we terug in de tijd konden reizen naar 1974, dan zouden we Leslie Lamport misschien hebben aangetroffen in zijn drukke buurtbakkerij, worstelend met het volgende probleem. De bakkerij had verschillende caissières, maar als meer dan één persoon tegelijkertijd een enkele caissière benaderde, zou die caissière proberen om met allemaal tegelijk te praten en in de war raken. Lamport realiseerde zich dat er een manier moest zijn om te garanderen dat mensen de kassiers één voor één benaderden. Dit probleem deed Lamport denken aan een vraagstuk dat in een eerder artikel van computerwetenschapper Edsger Dijkstra over een ander alledaags vraagstuk aan de orde is gesteld: hoe eetgerei rond een eettafel te verdelen. Een van de coördinatie-uitdagingen was om te garanderen dat elk gebruiksvoorwerp werd gebruikt door ten hoogste een diner tegelijk, wat werd veralgemeend als het wederzijdse uitsluitingsprobleem, precies de uitdaging Lamport geconfronteerd in de bakkerij.

Op een ochtend in 1974 kreeg Lamport een idee over hoe de klanten van de bakkerij wederzijdse uitsluiting onderling konden oplossen, zonder de hulp van de bakkerij in te roepen. Het werkte ongeveer als volgt: mensen kiezen nummers als ze de bakkerij binnenkomen, en worden dan bij de kassa bediend volgens hun nummerbestelling. Om een nummer te kiezen, vraagt een klant naar het nummer van iedereen om haar heen en kiest een nummer dat hoger is dan alle anderen.

Dit eenvoudige idee werd een elegant algoritme voor het oplossen van het wederzijdse uitsluitingsprobleem zonder dat daarvoor ondeelbare bewerkingen op een lager niveau nodig waren. Het was ook een rijke bron van toekomstige ideeën, omdat veel kwesties moesten worden uitgewerkt. Bijvoorbeeld, sommige klanten van de bakkerij deden er lang over om andere nummers te controleren, en ondertussen kwamen er meer klanten bij en kozen extra nummers. Een andere keer wilde de manager van de bakkerij een momentopname van alle klantnummers krijgen om genoeg gebakjes te kunnen bereiden. Lamport zei later “Gedurende een paar jaar na mijn ontdekking van het algoritme van de bakkerij, kwam alles wat ik leerde over concurrency voort uit het bestuderen ervan.”

The Bakery Algorithm en Lamport’s andere baanbrekende werken — vele met grappige namen en bijbehorende parabels — zijn pijlers van de computerwetenschap geworden. Zijn verzameling vormt de basis van brede gebieden in gelijktijdigheid, en heeft de specificatie, ontwikkeling, en verificatie van gelijktijdige systemen beïnvloed.

Na in 1972 te zijn gepromoveerd in de wiskunde aan de Brandeis University, werkte Lamport van 1970 tot 1977 als computerwetenschapper bij Massachusetts Computer Associates, van 1977 tot 1985 bij SRI International, en van 1985 tot 2001 bij het Systems Research Center van Digital Equipment Corporation (later eigendom van Compaq). In 2001 trad hij in dienst bij Microsoft Research in Mountain View, Californië.

Het doorbrengen van zijn onderzoekscarrière in industriële onderzoeksomgevingen was geen toeval. “Ik werk graag in een industrieel onderzoekslab, vanwege de input”, zei Lamport. “Als ik alleen zou werken en problemen zou bedenken, zou ik met een klein aantal dingen op de proppen komen, maar als ik de wereld in ga, waar mensen aan echte computersystemen werken, zijn er een miljoen problemen. Als ik terugkijk op de meeste dingen waar ik aan gewerkt heb – Byzantijnse Generaals, Paxos – die kwamen voort uit echte wereldproblemen.”

Zijn werk wierp licht op fundamentele kwesties van gelijktijdige programma’s, waarvoor er in die tijd geen formele theorie was. Hij worstelde met fundamentele concepten als causaliteit en logische tijd, atomaire en regelmatige gedeelde registers, sequentiële consistentie, replicatie van toestandsmachines, Byzantijnse overeenkomst en wacht-vrijheid. Hij werkte aan algoritmen die de standaard engineering praktijk zijn geworden voor fouttolerante gedistribueerde systemen. Hij heeft ook veel werk verricht op het gebied van de formele specificatie en verificatie van gelijktijdige systemen, en heeft bijgedragen aan de ontwikkeling van geautomatiseerde hulpmiddelen voor de toepassing van deze methoden. Wij zullen slechts enkele van zijn bijdragen bespreken.

1. Mutual Exclusion solutions and the Bakery algorithm

Lamport’s invloedrijke werk uit de jaren zeventig en tachtig kwam in een tijd dat er nog maar weinig bekend was over de fundamentele problemen rond het programmeren voor meervoudige gelijktijdige processoren.

Het was bijvoorbeeld bekend dat een correcte uitvoering kan vereisen dat parallelle activiteiten elkaar uitsluiten tijdens perioden in “kritieke secties” wanneer zij dezelfde gegevens manipuleren, om ongewenste interleaving van bewerkingen te voorkomen. De oorsprong van dit probleem van wederzijdse uitsluiting ligt in het baanbrekende werk van Edsger Dijkstra, dat ook zijn oplossing bevat. Dijkstra’s algoritme is weliswaar correct, maar is ervan afhankelijk dat gedeelde geheugentoegang atomair is – dat een processor die leest terwijl een andere schrijft, zal moeten wachten, in plaats van een mogelijk verminkte waarde terug te geven. In zekere zin construeert het een oplossing op hoog niveau uit een wederzijdse uitsluiting op laag niveau die al door de hardware is geïmplementeerd.

Lamport’s opmerkelijk elegante en intuïtieve “Bakery Algorithm” doet dat niet. Zijn oplossing rangschikt tegenstrijdige processen in een impliciete wachtrij volgens hun aankomstvolgorde, zoals een wachtrij in een bakkerij. Toch maakt het niet uit of een processor die gegevens leest die door een andere processor worden bijgewerkt, vuilnis krijgt. Het algoritme werkt nog steeds.

Lamport herinnert zich zijn ontdekking van het algoritme van de bakkerij.

Het algoritme van de bakkerij is lesmateriaal geworden, en de meeste studenten computerwetenschappen komen het tijdens hun studie tegen.

2. Grondslagen van het gelijktijdig programmeren

Er zijn verschillende belangrijke nieuwe concepten voortgekomen uit het werk aan het Bakery-algoritme, een trend die zich in Lamports loopbaan verschillende malen heeft voorgedaan. De ervaring van het bedenken van concurrerende algoritmen en het verifiëren van de juistheid ervan deed hem zich concentreren op de basisprincipes die multiprocessoren zich zouden laten gedragen op een wijze waarover programmeurs wiskundig kunnen redeneren. Terwijl hij werkte aan een oplossing voor een specifiek concreet probleem, vond Lamport abstracties en algemene regels uit die nodig waren om te redeneren over de juistheid ervan, en deze conceptuele bijdragen werden vervolgens theoretische pijlers van gelijktijdig programmeren.

Lus-vrijheid: Het Bakery Algorithm werk introduceerde een belangrijk concept genaamd “loop freedom”. Sommige voor de hand liggende oplossingen die in gedachten komen voor het wederzijdse uitsluitingsprobleem wijzen vooraf `draaibeurten’ toe tussen de processen. Maar dit dwingt processen te wachten op andere die traag zijn en nog niet eens het twistpunt hebben bereikt. Als we de analogie met de bakkerij gebruiken, zou dat hetzelfde zijn als aankomen bij een lege bakkerij en gevraagd worden te wachten op een klant die nog niet eens bij de bakkerij is aangekomen. Lusvrijheid daarentegen drukt de mogelijkheid uit van processen om vooruitgang te boeken onafhankelijk van de snelheid van andere processen. Omdat het bakkerij-algoritme beurten toekent aan processen in de volgorde van hun aankomst, heeft het lusvrijheid. Dit is een cruciaal concept dat is gebruikt in het ontwerp van vele volgende algoritmen en in het ontwerp van geheugenarchitecturen. Wait-freedom, een voorwaarde die onafhankelijke voortgang vereist ondanks mislukkingen, heeft zijn duidelijke wortels in het begrip loop-freedom en het Bakery doorway concept. Het werd later uitgebreid onderzocht door anderen, waaronder Maurice Herlihy.

Sequentiële consistentie: Het werken met een multi-core architectuur met gedistribueerd cache geheugen bracht Lamport ertoe formele specificaties te maken voor coherent cache gedrag in multiprocessor systemen. Dat werk bracht enige orde in de chaos op dit gebied door sequentiële consistentie uit te vinden, wat de gouden standaard is geworden voor geheugenconsistentiemodellen. Dit eenvoudige en intuïtieve begrip biedt precies het juiste niveau van “atomiciteit” om software te laten werken. Tegenwoordig ontwerpen we hardwaresystemen met tijdstempel- of partiële-store-ordening, met toegevoegde geheugenhek-instructies, waardoor programmeurs de hardware sequentieel consistent kunnen laten lijken. Programmeurs kunnen dan algoritmen implementeren die sterke consistentie-eigenschappen bieden. Dit is de sleutel tot de geheugenconsistentie-modellen van Java en C++. Onze multicore processoren draaien vandaag de dag op basis van principes beschreven door Leslie Lamport in 1979.

Atomische en regelmatige registers: Het Bakery Algoritme leidde er ook toe dat Lamport zich afvroeg wat de precieze semantiek van het geheugen zou moeten zijn wanneer meerdere processen met elkaar samenwerken om gegevens te delen. Het kostte bijna tien jaar om het te formaliseren, en het resultaat is de abstractie van reguliere en atomaire registers.

Zijn theorie geeft elke bewerking op een gedeeld register een expliciete duur, beginnend met een aanroep en eindigend met een resultaat. De registers kunnen worden geïmplementeerd door een verscheidenheid van technieken, zoals replicatie. Niettemin worden de interacties van processen met een atomair register verondersteld er “uit te zien” als seriële toegangen tot werkelijk gedeeld geheugen. De theorie omvat ook zwakkere semantiek van interactie, zoals die van een regulier register. Een regulier register vangt situaties op waarin processen verschillende replica’s van het register lezen terwijl het wordt bijgewerkt. Op elk moment kunnen sommige replica’s worden bijgewerkt en andere niet, en uiteindelijk zullen alle replica’s de bijgewerkte waarde bevatten. Belangrijk is dat deze zwakkere semantiek volstaat om wederzijdse uitsluiting te ondersteunen: het Bakery-algoritme werkt correct als een lezer die een schrijver overlapt een willekeurige waarde terugkrijgt.

Lamport beschrijft zijn werk om abstracties voor atomaire, reguliere en veilige registers nauwkeurig te definiëren.

Dit werk gaf de aanzet tot een apart subgebied van onderzoek op het gebied van gedistribueerde gegevensverwerking dat nog steeds bloeit. Lamport’s atomaire objecten ondersteunden alleen lees- en schrijfbewerkingen, dat wil zeggen dat het atomaire registers waren. Dit begrip werd door Maurice Herlihy en Jeannette Wing veralgemeend tot andere gegevenstypen, en hun term “linearizability” werd synoniem met atomiciteit. Tegenwoordig gebruiken vrijwel alle niet-relationele opslagsystemen van bedrijven als Amazon, Google en Facebook lineariseerbaarheid en sequentiële consistentie voor de coherentie van hun gegevens.

3. Grondslagen van gedistribueerde systemen

Een speciaal type concurrent systeem is een gedistribueerd systeem, dat wordt gekenmerkt door processen die berichten gebruiken om met elkaar te interageren. Leslie Lamport heeft een enorme invloed gehad op de manier waarop wij over gedistribueerde systemen denken, en ook op de engineeringpraktijken van het vakgebied.

Logische klokken: Veel mensen realiseerden zich dat een globale notie van tijd niet natuurlijk is voor een gedistribueerd systeem. Lamport was de eerste die een alternatief begrip van “logische klokken” preciseerde, die een gedeeltelijke orde opleggen aan gebeurtenissen op basis van de causale relatie die wordt geïnduceerd door het zenden van berichten van het ene deel van het systeem naar het andere. Zijn paper over “Time, Clocks, and the Ordering of Events in a Distributed System” is het meest geciteerde werk van Lamport geworden, en in de computerwetenschap worden logische klokken vaak Lamport timestamps genoemd. Zijn paper won in 2000 de Principles of Distributed Computing Conference Influential Paper Award (later omgedoopt tot de Edsger W. Dijkstra Prize in Distributed Computing), en het won in 2007 een ACM SIGOPS Hall of Fame Award.

Lamport beschrijft zijn paper “Time, Clocks…” en de relatie met speciale relativiteit.

Om te begrijpen waarom dat werk zo invloedrijk is geworden, moet je beseffen dat er ten tijde van de uitvinding geen goede manier was om de communicatievertraging in gedistribueerde systemen vast te leggen, behalve door gebruik te maken van realtime. Lamport realiseerde zich dat de communicatievertraging die systemen heel anders maakte dan een gedeeld-memory multiprocessor systeem. Het inzicht kwam toen hij een artikel las over gerepliceerde databases en zich realiseerde dat de logische volgorde van commando’s in strijd zou kunnen zijn met causaliteit.

Het gebruiken van de volgorde van gebeurtenissen als een manier om de correctheid van een systeem te bewijzen is wat men tegenwoordig meestal doet voor intuïtieve bewijzen van gelijktijdige synchronisatie-algoritmen. Een andere krachtige bijdrage van dit werk was het aantonen hoe je een toestandsmachine kunt repliceren met behulp van logische klokken, wat hieronder wordt uitgelegd.

Distributed Snapshots: Zodra je causale orde definieert, volgt de notie van consistente globale toestanden vanzelf. Dat leidde tot een ander inzichtelijk werk. Lamport en Mani Chandy vonden het eerste algoritme uit voor het lezen van de toestand (het nemen van een `snapshot’) van een willekeurig gedistribueerd systeem. Dit is zo’n krachtig begrip dat anderen het later gebruikten in verschillende domeinen, zoals netwerken, zelfstabilisatie, debugging, en gedistribueerde systemen. Deze paper ontving de 2013 ACM SIGOPS Hall of Fame Award.

4. Fouttolerantie en replicatie van State Machine

“Een gedistribueerd systeem is er een waarin het falen van een computer waarvan je niet eens wist dat hij bestond, je eigen computer onbruikbaar kan maken”, is een beroemde Lamport-kwinkslag. Veel van zijn werk heeft betrekking op fouttolerantie.

State Machine Replication (SMR): Misschien wel de belangrijkste van Lamports vele bijdragen is het State Machine Replication paradigma, dat werd geïntroduceerd in de beroemde paper “Time, Clocks, and the Ordering of Events in a Distributed System”, en kort daarna verder werd ontwikkeld. De abstractie vat elke dienst op als een gecentraliseerde toestandsmachine — een soort universele rekenmachine vergelijkbaar met een Turing machine. Het heeft een interne toestand, en het verwerkt commando’s in volgorde, elk resulterend in een nieuwe interne toestand en een antwoord producerend. Lamport realiseerde zich dat de ontmoedigende taak van het repliceren van een dienst over meerdere computers opmerkelijk eenvoudig kan worden gemaakt als je alle replica’s dezelfde volgorde van invoeropdrachten voorlegt en zij een identieke opeenvolging van toestanden doorlopen.

Dit inzichtelijke SMR-paradigma ligt ten grondslag aan veel betrouwbare systemen, en wordt vanwege zijn elegantie beschouwd als een standaardbenadering voor het bouwen van gerepliceerde gedistribueerde systemen. Maar voordat Lamport een volledige oplossing ontwikkelde met behulp van SMR, moest hij een kernbestanddeel aanpakken, overeenkomst, dat in zijn volgende werk werd aangepakt.

Byzantijnse overeenkomst: Terwijl state machine benaderingen die bestand zijn tegen crash fouten voldoende zijn voor veel toepassingen, meer missie-kritische systemen, zoals voor avionica, hebben behoefte aan een nog extremer model van fouttolerantie die ongevoelig is voor knooppunten die het systeem van binnenuit zou kunnen verstoren.

Aan het Stanford Research Institute (later SRI International geheten) maakte Lamport in de jaren zeventig deel uit van een team dat de NASA hielp bij het ontwerpen van een robuust avionica-besturingssysteem. Formele garanties waren een absolute noodzaak vanwege de missie-kritische aard van de taak. De veiligheid moest worden gegarandeerd tegen de meest extreme systeemstoringen die men zich kon voorstellen. Een van de eerste uitdagingen die het team van het SRI moest aangaan, was het bewijzen van de juistheid van een cockpitbesturingssysteem, dat de NASA had ontworpen, met drie computersystemen die meerderheidsbesluiten gebruiken om elk defect onderdeel te maskeren.

Het resultaat van het werk van het team was een aantal fundamentele concepten en inzichten met betrekking tot deze strenge types van robuuste systemen. Het omvatte een fundamentele definitie van robuustheid in deze setting, een abstractie van het coördinatieprobleem dat ten grondslag ligt aan elk gerepliceerd systeem tot op heden, en een verrassende openbaring dat systemen met drie computers nooit veilig een missiekritieke cockpit kunnen besturen!

Inderdaad, in twee baanbrekende werken (“LPS”) gepubliceerd met Pease en Shostak , identificeerde het team eerst een enigszins eigenaardige kwetsbaarheid. LPS stelde dat “een defect onderdeel een soort gedrag kan vertonen dat vaak over het hoofd wordt gezien — namelijk het zenden van tegenstrijdige informatie naar verschillende delen van het systeem”. Meer in het algemeen zou een defecte component kunnen functioneren op een manier die volledig in strijd is met zijn voorgeschreven gedrag, en bijna kwaadaardig kunnen overkomen.

Het nieuwe foutmodel had een naam nodig. In die tijd was er een verwante klassieke uitdaging van het coördineren van twee communicerende computers, geïntroduceerd in een artikel uit 1975 en door Jim Gray de “The Two Generals Paradox” genoemd. Dit bracht Lamport ertoe om de controlecomputers in een cockpit te zien als een leger van Byzantijnse generaals, waarbij het leger een gecoördineerde aanval probeert te vormen terwijl binnen verraders tegenstrijdige signalen uitzenden. De naam “Byzantijnse storingen” werd voor dit storingsmodel aangenomen, en een vlaag van academisch werk volgde. Het Byzantijnse foutenmodel wordt nog steeds gebruikt om de ergste ongelukken en veiligheidslekken in systemen vast te leggen.

Lamport legt uit hoe hij een verhaal over “Byzantijnse generaals” gebruikt om een probleem in fouttolerante gedistribueerde systemen te kaderen.

Byzantijnse mislukkingen analyseren de slechte dingen die kunnen gebeuren. Maar hoe zit het met de goede dingen die moeten gebeuren? LPS heeft ook een abstracte formulering gegeven van het probleem van het bereiken van coördinatie ondanks Byzantijnse mislukkingen; dit staat bekend als het probleem van de “Byzantijnse overeenkomst”. Deze beknopte formulering drukt de coördinatieopdracht van de besturing uit als het probleem van het vormen van een akkoordbeslissing voor een individuele bit, te beginnen met potentieel verschillende bits die aan elke component worden ingevoerd. Als je eenmaal overeenstemming hebt over één bit, is het mogelijk om die herhaaldelijk te gebruiken om een heel complex systeem gecoördineerd te houden. Het artikel toont aan dat vier computers nodig zijn om overeenstemming te bereiken over één bit bij één enkele storing. Drie zijn niet genoeg, want met drie eenheden kan een defecte eenheid tegenstrijdige waarden naar de andere twee eenheden sturen, en met elke eenheid een andere meerderheid vormen. Meer algemeen toonden zij aan dat 3F+1 eenheden nodig zijn om F gelijktijdig defecte componenten te overwinnen. Om dit te bewijzen gebruikten zij een prachtig symmetrie-argument dat bekend is geworden als het `hexagon argument’. Dit archetype argument heeft andere toepassingen gevonden wanneer men betoogt dat een defecte eenheid die tegenstrijdige informatie naar verschillende delen van het systeem stuurt, niet te onderscheiden lijkt van een symmetrische situatie waarin de correcte en defecte rollen zijn omgedraaid.

LPS toonden ook aan dat 3F+1 eenheden genoeg zijn, en zij presenteerden een oplossing voor het bereiken van Byzantijns Akkoord tussen de 3F+1 eenheden in F+1 synchrone communicatierondes. Zij toonden ook aan dat als je digitale handtekeningen gebruikt, slechts 2F+1 eenheden voldoende en noodzakelijk zijn.

Het Byzantijnse Overeenstemmingsprobleem en zijn oplossingen zijn het kenmerk geworden van fouttolerante systemen. De meeste systemen die met redundantie zijn opgebouwd, maken er intern gebruik van voor replicatie en voor coördinatie. Lamport zelf gebruikte het later bij het vormen van het State Machine Replication paradigma dat hierna wordt besproken en dat de algoritmische basis vormt voor replicatie.

De paper uit 1980 werd bekroond met de 2005 Edsger W. Dijkstra Prize in Distributed Computing, en de paper uit 1982 ontving de Jean-Claude Laprie Award in Dependable Computing.

Paxos: Met een groeiend begrip van het overeenkomstprobleem voor gedistribueerde gegevensverwerking, was het tijd voor Lamport om terug te gaan naar State Machine Replication en storingen daar aan te pakken. De eerste SMR oplossing die hij presenteerde in zijn paper uit 1978 ging ervan uit dat er geen fouten waren, en het maakt gebruik van logische tijd om replica’s door dezelfde commando-sequentie te laten lopen. In 1989 ontwierp Lamport een fouttolerant algoritme genaamd Paxos. Voortbordurend op zijn trend om op humoristische wijze parabels te vertellen, presenteert hij het denkbeeldige verhaal van een regeringsparlement op een oud Grieks eiland genaamd Paxos, waar de afwezigheid van een willekeurig aantal leden, of mogelijk zelfs van alle leden, kan worden getolereerd zonder dat de consistentie verloren gaat.

Lamport beschrijft de oorsprong van zijn Paxos-algoritme voor fouttolerante gedistribueerde computers.

Helaas maakte de setting als een Griekse parabel het artikel voor de meeste lezers moeilijk te begrijpen, en het duurde negen jaar van indiening tot publicatie in 1998. Maar het technisch rapport van DEC uit 1989 werd wel opgemerkt. Lamport’s collega Butler Lampson bracht het idee over aan de distributed computing gemeenschap. Kort na de publicatie van Paxos, boden Google’s Chubby systeem en Apache’s open-source ZooKeeper State Machine Replication aan als een externe, wijd verspreide dienst.

Paxos voegt een opeenvolging van overeenkomstbeslissingen samen in een opeenvolging van state-machine commando’s op een geoptimaliseerde manier. Belangrijk is dat de eerste fase van de overeenkomstcomponent die in het Paxos-paper wordt gegeven (synode genoemd) kan worden vermeden wanneer dezelfde leider meerdere beslissingen leidt; die fase hoeft alleen te worden uitgevoerd wanneer een leider moet worden vervangen. Deze inzichtelijke doorbraak verklaart veel van de populariteit van Paxos, en werd later Multi-Paxos genoemd door het Google team. Lamport’s Paxos paper won de ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award in 2012.

SMR en Paxos zijn de facto het standaardraamwerk geworden voor het ontwerpen van en redeneren over consensus- en replicatiemethoden. Veel bedrijven die kritieke informatiesystemen bouwen, waaronder Google, Yahoo, Microsoft en Amazon, hebben de grondslagen van Paxos overgenomen.

5. Formele specificatie en verificatie van programma’s

In de begindagen van de concurrency theorie ontstond de behoefte aan goede gereedschappen om oplossingen te beschrijven en hun juistheid te bewijzen. Lamport heeft centrale bijdragen geleverd aan de theorie van specificatie en verificatie van gelijktijdige programma’s. Hij was bijvoorbeeld de eerste die de begrippen veiligheidseigenschappen en liviteitseigenschappen voor asynchrone gedistribueerde algoritmen formuleerde. Dit waren de veralgemeningen van de eigenschappen “gedeeltelijke juistheid” en “totale juistheid” die eerder voor sequentiële programma’s waren gedefinieerd. Tegenwoordig vormen veiligheid en liveness de standaard classificatie voor correctheidseigenschappen van asynchrone gedistribueerde algoritmen.

Een ander werk, met Martin Abadi , introduceerde een speciale abstractie, prophecy variabelen genaamd, in een algoritme model, om een situatie te behandelen waarin een algoritme een nondeterministische keuze oplost voordat de specificatie dat doet. Abadi en Lamport wezen op situaties waarin dergelijke problemen zich voordoen, en ontwikkelden de theorie die nodig is om deze uitbreiding van de theorie te ondersteunen. Bovendien bewezen zij dat wanneer een gedistribueerd algoritme voldoet aan een specificatie, waarbij beide worden uitgedrukt als toestandsmachines, de correspondentie tussen beide kan worden bewezen met behulp van een combinatie van prophecy variabelen en eerdere noties zoals geschiedenisvariabelen. Dit werk won de LICS Test-Of-Time award 2008.

Formal Modeling Languages and Verification Tools: Naast de ontwikkeling van bovenstaande basisnoties heeft Lamport de taal TLA (Temporal Logic of Actions) en de TLA+-toolset ontwikkeld, voor het modelleren en verifiëren van gedistribueerde algoritmen en systemen.

Lamport beschrijft TLA en het verband met refinement mapping.

TLA en TLA+ ondersteunen de specificatie en het bewijs van zowel veiligheids- als liviteitseigenschappen, met behulp van notatie die is gebaseerd op temporele logica. Lamport heeft toezicht gehouden op de ontwikkeling van verificatie-instrumenten op basis van TLA+, met name de TLC-modelchecker die is gebouwd door Yuan Yu. TLA+ en TLC zijn gebruikt om echte systemen te beschrijven en te analyseren. Deze hulpmiddelen zijn bijvoorbeeld gebruikt om een grote fout te vinden in het coherentieprotocol dat werd gebruikt in de hardware voor Microsofts Xbox 360, voordat die in 2005 op de markt kwam. Bij Intel werd het gebruikt voor de analyse van een cache-coherentieprotocol van de Intel Quick Path Interconnect zoals geïmplementeerd in de Nehalem core processor. Om ingenieurs te leren hoe ze zijn formele specificatiegereedschappen kunnen gebruiken, heeft Lamport een boek geschreven. Meer recentelijk heeft Lamport de PlusCAL formele taal en gereedschappen ontwikkeld voor gebruik bij het verifiëren van gedistribueerde algoritmen; dit werk bouwt voort op TLA+.

6. LaTeX

Bij het maken van zo’n grote verzameling invloedrijke papers is het vanzelfsprekend dat men een handig zetgereedschap wenst. Lamport wenste er niet alleen een, hij creëerde er een voor de hele gemeenschap. Buiten het gebied van concurrency is Lamport’s Latex systeem , een set macro’s voor gebruik met Donald Knuth’s TeX typesetting systeem. LaTeX voegde drie belangrijke dingen toe aan TeX:

1. Het concept van ‘zetomgeving’, dat zijn oorsprong had in Brian Reid’s Scribe systeem.
2. Een sterke nadruk op structurele in plaats van typografische markup.
3. Een generiek document ontwerp, flexibel genoeg om geschikt te zijn voor een grote verscheidenheid aan documenten.

Lamport is niet de bedenker van deze ideeën, maar door ze zo ver mogelijk door te voeren creëerde hij een systeem dat de kwaliteit van TeX en veel van zijn flexibiliteit biedt, maar veel gemakkelijker in gebruik is. Latex werd de de facto standaard voor technisch publiceren in computerwetenschappen en vele andere gebieden.

Er zijn nog vele andere belangrijke papers van Leslie Lamport — te veel om hier te beschrijven. Ze staan in chronologische volgorde op Lamport’s home page , vergezeld van historische aantekeningen die de motivatie en context van elk resultaat beschrijven.

Telkens wanneer u een moderne computer gebruikt, zult u waarschijnlijk te maken krijgen met de algoritmen van Leslie Lamport. En al dit werk begon met de zoektocht om te begrijpen hoe je een rij bij een plaatselijke bakker moet organiseren.

Auteur: Dahlia Malkhi
Aanvragers: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, en Len Shustek