Hvis vi kunne rejse tilbage i tiden til 1974, ville vi måske have fundet Leslie Lamport i sit travle lokale bageri, hvor han kæmpede med følgende spørgsmål. Bageriet havde flere kasserere, men hvis flere personer henvendte sig til en enkelt kasserer på samme tid, ville kassereren forsøge at tale med dem alle på en gang og blive forvirret. Lamport indså, at der måtte være en måde at garantere, at folk henvendte sig til kassererne én ad gangen. Dette problem mindede Lamport om et problem, som datalog Edsger Dijkstra havde rejst i en tidligere artikel om et andet banalt problem, nemlig hvordan man deler spisebordets redskaber ved et spisebord. En af koordineringsudfordringerne bestod i at sikre, at hvert redskab højst blev brugt af én gæst ad gangen, hvilket blev generaliseret som et gensidigt udelukkelsesproblem, præcis den udfordring, som Lamport stod over for i bageriet.

En morgen i 1974 fik Lamport en idé om, hvordan bageriets kunder kunne løse problemet med gensidig udelukkelse indbyrdes, uden at de skulle have hjælp fra bageriet. Det fungerede nogenlunde sådan her: Folk vælger numre, når de kommer ind i bageriet, og bliver derefter betjent ved kassen i overensstemmelse med deres nummerbestilling. For at vælge et nummer spørger en kunde efter nummeret for alle omkring sig og vælger et nummer, der er højere end alle de andres.

Denne enkle idé blev til en elegant algoritme til løsning af problemet med gensidig udelukkelse uden at kræve uadskillelige operationer på lavere niveau. Den var også en rig kilde til fremtidige ideer, da der var mange problemer, der skulle udarbejdes. F.eks. tog det lang tid for nogle bagerikunder at tjekke andre numre, og i mellemtiden kom der flere kunder til og valgte yderligere numre. En anden gang ønskede bageriets leder at få et øjebliksbillede af alle kundernes numre for at kunne forberede nok kager. Lamport sagde senere: “I et par år efter min opdagelse af bageri-algoritmen kom alt, hvad jeg lærte om samtidighed, ved at studere den.”

Bageri-algoritmen og Lamports andre banebrydende værker – mange med morsomme navne og tilhørende lignelser – er blevet grundpiller i datalogien. Hans samling danner grundlaget for brede områder inden for samtidighed og har haft indflydelse på specifikation, udvikling og verifikation af samtidige systemer.

Efter at have taget en ph.d. i matematik fra Brandeis University i 1972 arbejdede Lamport som datalog hos Massachusetts Computer Associates fra 1970 til 1977, hos SRI International fra 1977 til 1985 og hos Digital Equipment Corporation Systems Research Center (senere ejet af Compaq) fra 1985 til 2001. I 2001 blev han ansat hos Microsoft Research i Mountain View, Californien.

Det var ikke tilfældigt, at han tilbragte sin forskerkarriere i industrielle forskningsmiljøer. “Jeg kan godt lide at arbejde i et industrielt forskningslaboratorium på grund af input”, sagde Lamport. “Hvis jeg bare arbejdede alene og fandt på problemer, ville jeg finde på et lille antal ting, men hvis jeg går ud i verden, hvor folk arbejder på rigtige computersystemer, er der en million problemer derude. Når jeg ser tilbage på de fleste af de ting, jeg har arbejdet på – Bysantine Generals, Paxos – så kom de fra virkelige problemer i den virkelige verden.”

Hans arbejde kastede lys over grundlæggende spørgsmål om samtidige programmer, som der ikke fandtes nogen formel teori for på det tidspunkt. Han beskæftigede sig med grundlæggende begreber som kausalitet og logisk tid, atomare og regelmæssige delte registre, sekventiel konsistens, replikation af tilstandsmaskiner, Byzantine Agreement og wait-freedom. Han arbejdede på algoritmer, som er blevet standardteknisk praksis for fejltolerante distribuerede systemer. Han har også udviklet en betydelig mængde arbejde om formel specifikation og verifikation af samtidige systemer og har bidraget til udviklingen af automatiserede værktøjer, der anvender disse metoder. Vi vil kun berøre nogle af hans bidrag.

1. Mutual Exclusion-løsninger og Bakery-algoritmen

Lamports indflydelsesrige værker fra 1970’erne og 1980’erne kom på et tidspunkt, hvor der kun var en ringe forståelse af de grundlæggende spørgsmål om programmering for flere samtidige processorer.

For eksempel vidste man, at korrekt udførelse kan kræve, at parallelle aktiviteter udelukker hinanden i perioder i “kritiske afsnit”, hvor de manipulerer de samme data, for at forhindre uønsket sammenfletning af operationer. Oprindelsen af dette problem med gensidig udelukkelse stammer fra Edsger Dijkstras banebrydende arbejde, som omfatter hans løsning. Dijkstras algoritme er ganske vist korrekt, men den er afhængig af, at adgangen til den fælles hukommelse er atomar – at en processor, der læser, mens en anden skriver, skal vente, i stedet for at returnere en eventuelt forvrænget værdi. På en måde konstruerer den en løsning på højt niveau ud fra gensidig udelukkelse på lavt niveau, som allerede er implementeret af hardwaren.

Lamports bemærkelsesværdigt elegante og intuitive “Bakery Algorithm” gør ikke dette. Hans løsning arrangerer konkurrerende processer i en implicit kø i henhold til deres ankomstrækkefølge, ligesom en ventekø i et bageri. Alligevel er det ligegyldigt, om en processor, der læser data, som er ved at blive opdateret af en anden processor, får skrald. Algoritmen virker stadig.

Lamport husker sin opdagelse af Bakery-algoritmen.

Bakery-algoritmen er blevet lærebogsmateriale, og de fleste bachelorstuderende i datalogi støder på den i løbet af deres studietid.

2. Grundlaget for samtidig programmering

Flere vigtige nye begreber udsprang af arbejdet med Bakery-algoritmen, en tendens, der gentog sig flere gange i Lamports karriere. Erfaringen med at udtænke samtidige algoritmer og verificere korrekthed fik ham til at fokusere på de grundlæggende fundamenter, der kunne få multiprocessorer til at opføre sig på en måde, som programmører kan ræsonnere matematisk om. Mens Lamport arbejdede på en løsning til et specifikt konkret problem, opfandt han abstraktioner og generelle regler, der var nødvendige for at kunne ræsonnere om dens korrekthed, og disse konceptuelle bidrag blev derefter teoretiske søjler i concurrent programming.

Loop-frihed: Bakery Algorithm-arbejdet introducerede et vigtigt begreb kaldet “loop-frihed”. Nogle indlysende løsninger, der falder mig ind for problemet med gensidig udelukkelse, tildeler på forhånd `turns’ i rotation mellem processerne. Men det tvinger processerne til at vente på andre processer, der er langsomme og endnu ikke engang er nået frem til det punkt, hvor der er stridigheder. Hvis man bruger bagerianalogien, ville det svare til at ankomme til et tomt bageri og blive bedt om at vente på en kunde, som ikke engang er ankommet til bageriet endnu. I modsætning hertil udtrykker loop-frihed processernes evne til at gøre fremskridt uafhængigt af andre processers hastighed. Da bagerialgoritmen tildeler processerne turer i den rækkefølge, de ankommer, har den loop-frihed. Dette er et afgørende begreb, som er blevet anvendt ved udformningen af mange efterfølgende algoritmer og ved udformningen af hukommelsesarkitekturer. Vent-frihed, som er en betingelse, der kræver uafhængig fremgang på trods af fejl, har sine klare rødder i begrebet loop-frihed og i Bakery-dørløbsbegrebet. Det blev senere udforsket indgående af andre, bl.a. Maurice Herlihy.

Sekventiel konsistens: Arbejdet med en arkitektur med flere kerner, der havde distribueret cachehukommelse, fik Lamport til at skabe formelle specifikationer for sammenhængende cacheadfærd i multiprocessorsystemer. Dette arbejde bragte noget orden i kaoset på dette område ved at opfinde sekventiel konsistens , som er blevet den gyldne standard for hukommelseskonsistensmodeller. Dette enkle og intuitive begreb giver lige det rette niveau af “atomicitet”, så software kan fungere. I dag designer vi hardwaresystemer med timestamp-ordning eller partial-store-ordning med tilføjede memory fence-instruktioner, som giver programmørerne mulighed for at få hardwaren til at fremstå sekventielt konsistent. Programmører kan derefter implementere algoritmer, der giver stærke konsistensegenskaber. Dette er nøglen til hukommelseskonsistensmodellerne i Java og C++. Vores multicore-processorer kører i dag på grundlag af principper, der blev beskrevet af Leslie Lamport i 1979.

Atomiske og regelmæssige registre: Bakery-algoritmen førte også til, at Lamport undrede sig over den præcise semantik af hukommelsen, når flere processer interagerer for at dele data. Det tog næsten et årti at formalisere det, og resultatet er abstraktionen af regulære og atomare registre.

Hans teori giver hver operation på et delt register en eksplicit varighed, der starter med et påkald og slutter med et resultat. Registrene kan implementeres ved hjælp af en række forskellige teknikker, f.eks. replikation. Ikke desto mindre er det meningen, at processernes interaktioner med et atomisk register skal “ligne” serielle adganger til den faktiske delte hukommelse. Teorien omfatter også en svagere semantik for interaktion, som den, der gælder for et almindeligt register. Et regulært register omfatter situationer, hvor processer læser forskellige replikaer af registret, mens det opdateres. På et hvilket som helst tidspunkt kan nogle replikaer være opdateret, mens andre ikke er det, og i sidste ende vil alle replikaer indeholde den opdaterede værdi. Det er vigtigt, at denne svagere semantik er tilstrækkelig til at understøtte gensidig udelukkelse: Bakery-algoritmen fungerer korrekt, hvis en læser, der overlapper en skriver, får en vilkårlig værdi tilbage.

Lamport beskriver sit arbejde med præcist at definere abstraktioner for atomare, regelmæssige og sikre registre.

Dette arbejde indledte et særskilt delområde af forskning inden for distribueret databehandling, som stadig er blomstrende. Lamports atomiske objekter understøttede kun læse- og skriveoperationer, dvs. de var atomiske registre. Begrebet blev generaliseret til andre datatyper af Maurice Herlihy og Jeannette Wing , og deres begreb “linearizability” blev synonymt med atomicitet. I dag anvender stort set alle ikke-relationelle lagringssystemer, der er udviklet af virksomheder som Amazon, Google og Facebook, linearizability og sekventiel konsistens som garanti for datakohærens.

3. Grundlag for distribuerede systemer

En særlig type af samtidige systemer er et distribueret system, der er kendetegnet ved at have processer, der bruger meddelelser til at interagere med hinanden. Leslie Lamport har haft en enorm indflydelse på den måde, vi tænker om distribuerede systemer, samt på den tekniske praksis på området.

Logiske ure: Mange mennesker indså, at et globalt tidsbegreb ikke er naturligt for et distribueret system. Lamport var den første til at præcisere et alternativt begreb om “logiske ure”, som pålægger begivenhederne en delvis rækkefølge baseret på den kausale relation, der fremkaldes ved at sende meddelelser fra en del af systemet til en anden . Hans artikel om “Time, Clocks, and the Ordering of Events in a Distributed System” er blevet det mest citerede af Lamports værker, og i datalogisk sprogbrug kaldes logiske ure ofte Lamport-timestamps. Hans artikel vandt i 2000 Principles of Distributed Computing Conference Influential Paper Award (senere omdøbt til Edsger W. Dijkstra Prize in Distributed Computing), og den vandt en ACM SIGOPS Hall of Fame Award i 2007.

Lamport beskriver sin artikel “Time, Clocks…” og dens relation til den specielle relativitetsteori.

For at forstå, hvorfor dette arbejde er blevet så indflydelsesrigt, skal man erkende, at der på det tidspunkt, hvor det blev opfundet, ikke var nogen god måde at indfange kommunikationsforsinkelsen i distribuerede systemer på, undtagen ved at bruge realtid. Lamport indså, at kommunikationsforsinkelsen gjorde disse systemer meget forskellige fra et multiprocessorsystem med delt hukommelse. Indsigten kom, da han læste et dokument om replikerede databaser og indså, at dets logiske rækkefølge af kommandoer kunne krænke kausaliteten.

Anvendelse af rækkefølge af begivenheder som en måde at bevise systemkorrekthed på er for det meste det, man i dag gør for intuitive beviser for samtidige synkroniseringsalgoritmer. Et andet stærkt bidrag fra dette arbejde var at demonstrere, hvordan man replikerer en tilstandsmaskine ved hjælp af logiske ure, hvilket forklares nedenfor.

Distributed Snapshots: Når man først har defineret kausal orden, følger begrebet konsistente globale tilstande naturligt. Det førte til et andet indsigtsfuldt arbejde. Lamport og Mani Chandy opfandt den første algoritme til at læse tilstanden (tage et “snapshot”) af et vilkårligt distribueret system . Dette er et så stærkt begreb, at andre senere har brugt det inden for forskellige områder som f.eks. netværk, selvstabilisering, fejlfinding og distribuerede systemer. Denne artikel modtog 2013 ACM SIGOPS Hall of Fame Award.

4. Fejltolerance og replikation af tilstandsmaskiner

“`Et distribueret system er et system, hvor fejl på en computer, som du ikke engang vidste eksisterede, kan gøre din egen computer ubrugelig” er en berømt Lamport-kvip. En stor del af hans arbejde drejer sig om fejltolerance.

State Machine Replication (SMR): Det måske vigtigste af Lamports mange bidrag er paradigmet State Machine Replication, som blev introduceret i den berømte artikel om “Time, Clocks, and the Ordering of Events in a Distributed System” og videreudviklet kort efter . Abstraktionen indfanger enhver tjeneste som en centraliseret tilstandsmaskine – en slags universel datamaskine svarende til en Turing-maskine. Den har en intern tilstand, og den behandler kommandoer i rækkefølge, som hver især resulterer i en ny intern tilstand og giver et svar. Lamport indså, at den skræmmende opgave med at replikere en tjeneste over flere computere kan gøres bemærkelsesværdigt enkel, hvis man præsenterer den samme sekvens af inputkommandoer for alle replikaer, og de fortsætter gennem en identisk rækkefølge af tilstande.

Dette indsigtsfulde SMR-paradigme ligger til grund for mange pålidelige systemer og betragtes på grund af sin elegance som en standardtilgang til opbygning af replikerede distribuerede systemer. Men før Lamport udviklede en fuld løsning ved hjælp af SMR, var han nødt til at tage fat på en central ingrediens, nemlig aftale, som han tog fat på i sit næste arbejde.

Byzantine Agreement: Mens tilstandsmaskinetilgange, der er modstandsdygtige over for nedbrud, er tilstrækkelige til mange anvendelser, har mere missionskritiske systemer, f.eks. til flyelektronik, brug for en endnu mere ekstrem fejltolerancemodel, der er uimodtagelig over for knudepunkter, der kan forstyrre systemet indefra.

På Stanford Research Institute (senere kaldet SRI International) i 1970’erne var Lamport en del af et hold, der hjalp NASA med at designe et robust flyelektronikstyresystem. Formelle garantier var en absolut nødvendighed på grund af opgavens missionskritiske karakter. Sikkerheden skulle garanteres mod de mest ekstreme systemfejl, man kunne forestille sig. En af de første udfordringer, som holdet på SRI blev bedt om at tage på sig, var at bevise korrektheden af et cockpitkontrolsystem, som NASA havde designet, med tre computersystemer, der bruger flertalsafstemning til at maskere enhver defekt komponent.

Resultatet af holdets arbejde var flere grundlæggende koncepter og indsigter vedrørende disse strenge typer af robuste systemer. Det omfattede en grundlæggende definition af robusthed i denne sammenhæng, en abstraktion af det koordinationsproblem, der ligger til grund for ethvert replikeret system til dato, og en overraskende afsløring af, at systemer med tre computere aldrig sikkert kan drive et missionskritisk cockpit!

I to grundlæggende værker (“LPS”), der blev offentliggjort sammen med Pease og Shostak , identificerede holdet først en noget besynderlig sårbarhed. I LPS blev det hævdet, at “en defekt komponent kan udvise en type adfærd, som ofte overses – nemlig at den sender modstridende oplysninger til forskellige dele af systemet”. Mere generelt kunne en defekt komponent fungere på en måde, der var helt uforenelig med dens foreskrevne adfærd, og den kunne nærmest virke ondsindet.

Den nye fejlmodel havde brug for et navn. På det tidspunkt var der en beslægtet klassisk udfordring med at koordinere to kommunikerende computere, som blev introduceret i en artikel fra 1975 og omtalt af Jim Gray i som “The Two Generals Paradox “. Dette fik Lamport til at tænke på kontrolcomputerne i et cockpit som en hær af byzantinske generaler, hvor hæren forsøgte at danne et koordineret angreb, mens forrædere indeni sendte modstridende signaler. Navnet “Byzantine Failures” blev vedtaget for denne fejlmodel, og der fulgte en strøm af akademisk arbejde. Den byzantinske fejlmodel bruges stadig til at indfange den værste form for uheld og sikkerhedsbrister i systemer.

Lamport forklarer sin brug af en historie om “Byzantine Generals” til at indramme et problem i fejltolerante distribuerede systemer.

Byzantine Failures analyserer de dårlige ting, der kan ske. Men hvad med de gode ting, der skal ske? LPS gav også en abstrakt formulering af problemet med at opnå koordinering på trods af byzantinske fejl; dette er kendt som “Byzantine Agreement”-problemet. Denne kortfattede formulering udtrykker kontrolkoordineringsopgaven som problemet med at træffe en beslutning om en aftale for en enkelt bit, idet der tages udgangspunkt i potentielt forskellige bits, som hver komponent kan have forskellige input til hver enkelt komponent. Når man først har opnået enighed om en enkelt bit, er det muligt at bruge den gentagne gange for at holde et helt komplekst system koordineret. Af artiklen fremgår det, at der skal fire computere til for at nå til enighed om en enkelt bit i forbindelse med en enkelt fejlfunktion. Tre er ikke nok, for med tre enheder kan en fejlbehæftet enhed sende modstridende værdier til de to andre enheder og danne et forskelligt flertal med hver enhed. Mere generelt viste de, at der er behov for 3F+1 enheder for at overvinde F samtidigt fejlbehæftede komponenter. For at bevise dette brugte de et smukt symmetriargument, som er blevet kendt som “hexagon-argumentet”. Dette arketypeargument har fundet andre anvendelser, når man argumenterer for, at en defekt enhed, der sender modstridende oplysninger til forskellige dele af systemet, ikke kan skelnes fra en symmetrisk situation, hvor de korrekte og defekte roller er byttet om.

LPS viste også, at 3F+1 enheder er nok, og de præsenterede en løsning til at opnå Byzantine Agreement blandt de 3F+1 enheder i F+1 synkrone kommunikationsrunder. De viste også, at hvis man anvender digitale signaturer, er kun 2F+1 enheder tilstrækkelige og nødvendige.

Det byzantinske aftaleproblem og dets løsninger er blevet kendetegnende for fejltolerante systemer. De fleste systemer, der er konstrueret med redundans, gør brug af den internt til replikation og til koordinering. Lamport selv brugte det senere til at danne paradigmet State Machine Replication, der behandles i det følgende, og som giver det algoritmiske grundlag for replikation.

Afhandlingen fra 1980 blev tildelt Edsger W. Dijkstra Prize in Distributed Computing i 2005, og afhandlingen fra 1982 modtog Jean-Claude Laprie-prisen i Dependable Computing.

Paxos: Med en voksende forståelse af aftaleproblemet for distribueret databehandling var det på tide for Lamport at gå tilbage til State Machine Replication og behandle fejl der. Den første SMR-løsning, som han præsenterede i sin artikel fra 1978, antog, at der ikke er nogen fejl, og den gør brug af logisk tid til at lade replikaer gennemgå den samme kommandosekvens. I 1989 udviklede Lamport en fejltolerant algoritme kaldet Paxos . I forlængelse af hans tendens til humoristisk parabelfortælling præsenteres i artiklen en imaginær historie om et regeringsparlament på en gammel græsk ø ved navn Paxos, hvor fraværet af et vilkårligt antal medlemmer, eller muligvis alle medlemmer, kan tolereres uden at miste konsistens.

Lamport beskriver oprindelsen til sin Paxos-algoritme til fejltolerant distribueret databehandling.

Uheldigvis gjorde indstillingen som en græsk parabel oplægget svært forståeligt for de fleste læsere, og der gik ni år fra indsendelse til offentliggørelse i 1998. Men den tekniske rapport fra DEC fra 1989 blev bemærket. Lamports kollega Butler Lampson udbreder ideen til det distribuerede computerfællesskab . Kort efter offentliggørelsen af Paxos tilbød Googles Chubby-system og Apaches open source ZooKeeper State Machine Replication som en ekstern, bredt implementeret tjeneste.

Paxos syr en række aftalebeslutninger sammen til en sekvens af state-machine-kommandoer på en optimeret måde. Det er vigtigt, at den første fase af den aftalekomponent, der er angivet i Paxos-papiret (kaldet Synode), kan undgås, når den samme leder er formand for flere beslutninger; denne fase skal kun udføres, når en leder skal udskiftes. Dette indsigtsfulde gennembrud er årsagen til en stor del af Paxos’ popularitet og blev senere kaldt Multi-Paxos af Google-holdet . Lamports Paxos-papir vandt ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award i 2012.

SMR og Paxos er blevet de facto-standardrammen for udformning af og ræsonnementer om konsensus- og replikationsmetoder. Mange virksomheder, der opbygger kritiske informationssystemer, herunder Google, Yahoo, Microsoft og Amazon, har vedtaget Paxos-grundlaget.

5. Formel specifikation og verifikation af programmer

I samtidighedsteoriens tidlige dage opstod der et behov for gode værktøjer til at beskrive løsninger og bevise deres korrekthed. Lamport har ydet centrale bidrag til teorien om specifikation og verifikation af samtidige programmer. Han var f.eks. den første til at formulere begreberne sikkerhedsegenskaber og liveness-egenskaber for asynkrone distribuerede algoritmer. Disse var en generalisering af egenskaberne “partiel korrekthed” og “total korrekthed”, som tidligere var defineret for sekventielle programmer. I dag udgør sikkerheds- og liveness-egenskaberne standardklassifikationen for korrekthedsegenskaber for asynkrone distribuerede algoritmer.

Et andet arbejde, udført sammen med Martin Abadi , introducerede en særlig abstraktion kaldet profetivariabler til en algoritmemodel for at håndtere en situation, hvor en algoritme løser et ikke-deterministisk valg, før specifikationen gør det. Abadi og Lamport pegede på situationer, hvor sådanne problemer opstår, og udviklede den teori, der er nødvendig for at understøtte denne udvidelse af teorien. Desuden beviste de, at når en distribueret algoritme møder en specifikation, hvor begge er udtrykt som tilstandsmaskiner, kan korrespondancen mellem dem bevises ved hjælp af en kombination af profetivariabler og tidligere begreber som f.eks. historikvariabler. Dette arbejde vandt 2008 LICS Test-Of-Time-prisen.

Formelle modelleringssprog og verificeringsværktøjer: Ud over at udvikle de grundlæggende begreber ovenfor har Lamport udviklet sproget TLA (Temporal Logic of Actions) og TLA+-værktøjssættet til modellering og verifikation af distribuerede algoritmer og systemer.

Lamport beskriver TLA og dets forbindelse til refinement mapping.

TLA og TLA+ understøtter specifikation og bevisførelse af både sikkerheds- og liveness-egenskaber ved hjælp af notation baseret på temporal logik. Lamport har ført tilsyn med udviklingen af verifikationsværktøjer baseret på TLA+, navnlig TLC-modelkontrollen, der er udviklet af Yuan Yu. TLA+ og TLC er blevet anvendt til at beskrive og analysere virkelige systemer. Disse værktøjer blev f.eks. brugt til at finde en stor fejl i den kohærensprotokol, der blev anvendt i hardwaren til Microsofts Xbox 360 inden dens udgivelse i 2005. Hos Intel blev det brugt til analyse af en cache-kohærensprotokol i Intel Quick Path Interconnect som implementeret i Nehalem-kernens processor. Lamport har skrevet en bog for at lære ingeniører at bruge sine formelle specifikationsværktøjer . For nylig har Lamport udviklet det formelle sprog PlusCAL og værktøjer til brug ved verificering af distribuerede algoritmer; dette arbejde bygger på TLA+.

6. LaTeX

Når man skaber en så stor samling af slagkraftige artikler, er det naturligt at ønske sig et praktisk sætningsværktøj. Lamport ønskede sig ikke bare et sådant, han skabte et til hele samfundet. Uden for samtidighedsområdet er Lamports Latex-system , et sæt makroer til brug sammen med Donald Knuths TeX-sættesystem . LaTeX tilføjede tre vigtige ting til TeX:

1. Begrebet “sættemiljø”, som havde sin oprindelse i Brian Reids Scribe-system.
2. En stærk vægt på strukturel snarere end typografisk markup.
3. Et generisk dokumentdesign, der er fleksibelt nok til at være passende til en lang række forskellige dokumenter.

Lamport var ikke ophavsmand til disse ideer, men ved at skubbe dem så langt som muligt skabte han et system, der giver samme kvalitet som TeX og en stor del af dets fleksibilitet, men som er meget lettere at bruge. Latex blev de facto-standard for teknisk publicering inden for datalogi og mange andre områder.

Der er mange andre vigtige artikler af Leslie Lamport — for mange til at beskrive dem her. De er opført i kronologisk rækkefølge på Lamports hjemmeside , ledsaget af historiske noter, der beskriver motivationen og konteksten for hvert resultat.

Hver gang du har adgang til en moderne computer, vil du sandsynligvis blive berørt af Leslie Lamports algoritmer. Og alt dette arbejde startede med en søgen efter at forstå, hvordan man organiserer en kø hos en lokal bager.

Author: Dahlia Malkhi
Oplysende bidragydere:: Dahlia Malkhi
Oplysende bidragydere:: Dahlia Malkhi Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese og Len Shustek