Kdybychom se mohli vrátit v čase do roku 1974, možná bychom Leslieho Lamporta našli v jeho rušné místní pekárně, kde by řešil následující problém. Pekárna měla několik pokladních, ale pokud se k jedné pokladní přiblížilo více lidí najednou, snažila se pokladní mluvit se všemi najednou a byla zmatená. Lamport si uvědomil, že je třeba nějakým způsobem zajistit, aby lidé přistupovali k pokladnám po jednom. Tento problém Lamportovi připomněl otázku, kterou si v dřívějším článku položil počítačový vědec Edsger Dijkstra v souvislosti s jiným prozaickým problémem: jak rozdělit příbory k večeři u jídelního stolu. Jedním z koordinačních problémů bylo zaručit, aby každé náčiní používal vždy nejvýše jeden strávník, což se začalo zobecňovat jako problém vzájemného vyloučení, tedy přesně ten problém, kterému Lamport čelil v pekárně.
Jednoho rána v roce 1974 přišel Lamport na nápad, jak by zákazníci pekárny mohli vyřešit vzájemné vyloučení mezi sebou, aniž by se museli spoléhat na pomoc pekárny. Fungovalo to zhruba takto: lidé si při vstupu do pekárny zvolí čísla a pak je u pokladny obslouží podle jejich objednaného čísla. Při výběru čísla se zákazník zeptá na číslo všech kolem sebe a vybere si číslo vyšší než všichni ostatní.
Tato jednoduchá myšlenka se stala elegantním algoritmem pro řešení problému vzájemného vyloučení, aniž by vyžadovala nějaké nedělitelné operace nižší úrovně. Byl to také bohatý zdroj budoucích nápadů, protože bylo třeba vyřešit mnoho problémů. Například některým zákazníkům pekárny trvalo dlouho, než zkontrolovali další čísla, a mezitím přišli další zákazníci a vybrali další čísla. Jindy zase chtěl vedoucí pekárny získat přehled o všech zákaznických číslech, aby mohl připravit dostatek pečiva. Lamport později řekl: „Několik let po mém objevu algoritmu pekárny jsem se vše, co jsem se naučil o souběhu, odvíjel od jeho studia.“
Algoritmus pekárny a další Lamportovy průkopnické práce – mnohé s vtipnými názvy a souvisejícími přirovnáními – se staly pilíři informatiky. Jeho sbírka tvoří základ širokých oblastí souběžnosti a ovlivnila specifikaci, vývoj a verifikaci souběžných systémů.
Po získání doktorátu z matematiky na Brandeisově univerzitě v roce 1972 pracoval Lamport v letech 1970-1977 jako počítačový vědec ve společnosti Massachusetts Computer Associates, v letech 1977-1985 ve společnosti SRI International a v letech 1985-2001 ve společnosti Digital Equipment Corporation Systems Research Center (později vlastněné společností Compaq). V roce 2001 nastoupil do společnosti Microsoft Research v kalifornském Mountain View.
Pobyt v průmyslovém výzkumném prostředí nebyl náhodný. „Práce v průmyslové výzkumné laboratoři se mi líbí kvůli vstupním informacím,“ řekl Lamport. „Kdybych pracoval jen sám a vymýšlel problémy, přišel bych na nějaký malý počet věcí, ale když jdu do světa, kde lidé pracují na skutečných počítačových systémech, je tam milión problémů. Když se podívám zpět na většinu věcí, na kterých jsem pracoval – byzantské generály, Paxos – tak ty vznikly na základě problémů reálného světa.“
Jeho práce vrhly světlo na základní problémy souběžných programů, pro které v té době neexistovala žádná formální teorie. Zabýval se základními pojmy, jako je kauzalita a logický čas, atomické a regulární sdílené registry, sekvenční konzistence, replikace stavových strojů, byzantská dohoda a svoboda čekání. Pracoval na algoritmech, které se staly standardní inženýrskou praxí pro distribuované systémy odolné vůči poruchám. Vypracoval také rozsáhlé dílo v oblasti formální specifikace a verifikace souběžných systémů a přispěl k vývoji automatizovaných nástrojů aplikujících tyto metody. Zmíníme se pouze o některých jeho příspěvcích.
1. Řešení vzájemného vyloučení a algoritmus Bakery
Lamportovy vlivné práce ze 70. a 80. let 20. století vznikly v době, kdy existovalo jen malé porozumění základním otázkám programování pro více souběžných procesorů.
Například bylo známo, že správné provádění může vyžadovat vzájemné vyloučení paralelních činností v obdobích „kritických úseků“, kdy manipulují se stejnými daty, aby se zabránilo nežádoucímu prolínání operací. Počátky tohoto problému vzájemného vylučování pocházejí z průkopnické práce Edsgera Dijkstry, jejíž součástí je i jeho řešení. Dijkstrův algoritmus je sice správný, ale závisí na tom, že přístupy do sdílené paměti jsou atomické – že jeden procesor, který čte, když jiný zapisuje, bude muset čekat, místo aby vracel případně zkomolenou hodnotu. V jistém smyslu konstruuje vysokoúrovňové řešení z nízkoúrovňového vzájemného vyloučení již implementovaného hardwarem.
Lamportův pozoruhodně elegantní a intuitivní „algoritmus pekárny“ to nedělá. Jeho řešení řadí soupeřící procesy do implicitní fronty podle pořadí jejich příchodu, podobně jako čekací fronta v pekárně. Přesto nevadí, když procesor, který čte data aktualizovaná jiným procesorem, dostane smetí. Algoritmus stále funguje.
Lamport vzpomíná na svůj objev algoritmu Bakery.
Algoritmus Bakery se stal učebnicovým materiálem a většina vysokoškolských studentů informatiky se s ním setkává v průběhu studia.
2. Základy souběžného programování
Z práce na Bakeryho algoritmu vzešlo několik nových důležitých konceptů, což se v Lamportově kariéře několikrát opakovalo. Zkušenosti s vymýšlením souběžných algoritmů a ověřováním jejich správnosti způsobily, že se zaměřil na základní základy, které by umožnily, aby se víceprocesorové systémy chovaly způsobem, o němž mohou programátoři matematicky uvažovat. Při práci na řešení konkrétního problému Lamport vymyslel abstrakce a obecná pravidla potřebná k odůvodnění jeho správnosti a tyto koncepční příspěvky se pak staly teoretickými pilíři souběžného programování.
Svoboda cyklu: V práci Bakery Algorithm byl zaveden důležitý pojem zvaný „volnost smyčky“. Některá zřejmá řešení, která přicházejí v úvahu pro problém vzájemného vyloučení, předřazují ´otáčky´ v rotaci mezi procesy. To však nutí procesy čekat na ostatní, které jsou pomalé a ještě ani nedosáhly sporného bodu. Použijeme-li analogii s pekárnou, bylo by to podobné, jako kdybychom přišli do prázdné pekárny a byli požádáni, aby počkali na zákazníka, který do pekárny ještě ani nedorazil. Naproti tomu volnost smyčky vyjadřuje schopnost procesů postupovat nezávisle na rychlosti ostatních procesů. Vzhledem k tomu, že algoritmus pekárny přiděluje procesy v pořadí jejich příchodu, má volnost smyčky. Jedná se o klíčový koncept, který byl použit při návrhu mnoha následných algoritmů a při návrhu paměťových architektur. Svoboda čekání, podmínka vyžadující nezávislý postup navzdory selháním, má své jasné kořeny v pojmu svobody smyčky a v konceptu Bakeryho dveří. Později ji hojně zkoumali i další, včetně Maurice Herlihyho .
Sekvenční konzistence: Práce s vícejádrovou architekturou, která měla distribuovanou paměť cache, vedla Lamporta k vytvoření formálních specifikací pro koherentní chování cache ve víceprocesorových systémech. Tato práce vnesla do chaosu v této oblasti určitý řád tím, že vynalezla sekvenční konzistenci , která se stala zlatým standardem pro modely konzistence paměti. Tento jednoduchý a intuitivní pojem poskytuje tu správnou úroveň „atomicity“, která umožňuje fungování softwaru. Dnes navrhujeme hardwarové systémy s uspořádáním časových značek nebo s uspořádáním částečných úložišť s přidanými instrukcemi pro ohrazení paměti, což programátorům umožňuje, aby se hardware jevil jako sekvenčně konzistentní. Programátoři pak mohou implementovat algoritmy, které poskytují silné konzistentní vlastnosti. To je klíčové pro modely konzistence paměti v jazycích Java a C++. Naše vícejádrové procesory dnes pracují na principech, které popsal Leslie Lamport v roce 1979.
Atomické a regulární registry: Algoritmus Bakery vedl Lamporta také k úvahám o přesné sémantice paměti při interakci více procesů, které sdílejí data. Formalizace trvala téměř deset let a jejím výsledkem je abstrakce regulárních a atomárních registrů .
Jeho teorie dává každé operaci na sdíleném registru explicitní trvání, počínaje voláním a konče výsledkem. Registry lze implementovat různými technikami, například replikací. Nicméně interakce procesů s atomickým registrem mají „vypadat“ jako sériové přístupy do skutečné sdílené paměti. Teorie zahrnuje i slabší sémantiku interakcí, podobně jako u běžného registru. Běžný registr zachycuje situace, kdy procesy čtou různé repliky registru během jeho aktualizace. V každém časovém okamžiku mohou být některé repliky aktualizovány, zatímco jiné nikoli, a nakonec budou všechny repliky obsahovat aktualizovanou hodnotu. Důležité je, že tato slabší sémantika postačuje k podpoře vzájemného vyloučení: algoritmus Bakery funguje správně, pokud čtenář překrývající zapisovatele získá zpět libovolnou hodnotu.
Lamport popisuje svou práci na přesné definici abstrakcí pro atomické, regulární a bezpečné registry.
Tato práce iniciovala samostatnou podoblast výzkumu v oblasti distribuovaných výpočtů, která se stále rozvíjí. Lamportovy atomické objekty podporovaly pouze operace čtení a zápisu, to znamená, že se jednalo o atomické registry. Tento pojem zobecnili Maurice Herlihy a Jeannette Wing na další datové typy a jejich termín „linearizovatelnost“ se stal synonymem pro atomicitu. Dnes v podstatě všechny nerelační úložné systémy vyvinuté společnostmi jako Amazon, Google a Facebook přijímají linearizovatelnost a sekvenční konzistenci jako záruku koherence dat.
3. Základy distribuovaných systémů
Speciálním typem souběžného systému je distribuovaný systém, který se vyznačuje tím, že má procesy, které k vzájemné interakci používají zprávy. Leslie Lamportová měla obrovský vliv na způsob, jakým přemýšlíme o distribuovaném systému, a také na inženýrskou praxi v této oblasti.
Logické hodiny: Mnoho lidí si uvědomilo, že globální pojetí času není pro distribuovaný systém přirozené. Lamport jako první zpřesnil alternativní pojem „logických hodin“, které ukládají událostem částečný řád na základě kauzálního vztahu vyvolaného odesíláním zpráv z jedné části systému do druhé . Jeho článek „Time, Clocks, and the Ordering of Events in a Distributed System“ se stal nejcitovanější Lamportovou prací a v řeči informatiky se logickým hodinám často přezdívá Lamportovy časové značky. Jeho článek získal v roce 2000 na konferenci Principles of Distributed Computing Influential Paper Award (později přejmenovanou na Edsger W. Dijkstra Prize in Distributed Computing) a v roce 2007 získal cenu ACM SIGOPS Hall of Fame Award.
Lamport popisuje svůj článek „Time, Clocks…“ a jeho vztah ke speciální teorii relativity.
Chceme-li pochopit, proč se tato práce stala tak vlivnou, uvědomme si, že v době vynálezu neexistoval žádný dobrý způsob, jak zachytit komunikační zpoždění v distribuovaných systémech jinak než pomocí reálného času. Lamport si uvědomil, že komunikační zpoždění tyto systémy velmi odlišuje od víceprocesorového systému se sdílenou pamětí. Prozření přišlo při čtení článku o replikovaných databázích a uvědomil si, že jeho logické řazení příkazů může porušovat kauzalitu.
Použití řazení událostí jako způsobu důkazu správnosti systému je většinou to, co dnes lidé dělají pro intuitivní důkazy souběžných synchronizačních algoritmů. Dalším silným přínosem této práce bylo ukázat, jak replikovat stavový stroj pomocí logických hodin, což je vysvětleno níže.
Distribuované snímky: Jakmile definujete kauzální uspořádání, přirozeně z toho vyplývá pojem konzistentních globálních stavů. To vedlo k další pronikavé práci. Lamport a Mani Chandy vynalezli první algoritmus pro čtení stavu (pořízení `snímku‘) libovolného distribuovaného systému . Tento pojem je tak mocný, že jej později použili i další autoři v různých oblastech, jako jsou sítě, samostabilizace, ladění a distribuované systémy. Tento článek získal v roce 2013 ocenění ACM SIGOPS Hall of Fame Award.
4. Fault tolerance and State Machine Replication
„A distributed system is one in which the failure of a computer you didn’t even know thereed thereed can make your own computer unusable“ je známý Lamportův vtip. Velká část jeho práce se zabývá odolností proti chybám.
Replikace stavového stroje (SMR): Snad nejvýznamnějším z mnoha Lamportových příspěvků je paradigma State Machine Replication, které bylo představeno ve slavném článku „Time, Clocks, and the Ordering of Events in a Distributed System“ a brzy poté dále rozvíjeno. Tato abstrakce zachycuje jakoukoli službu jako centralizovaný stavový stroj – jakýsi univerzální výpočetní stroj podobný Turingovu stroji. Má vnitřní stav a postupně zpracovává příkazy, z nichž každý vede k novému vnitřnímu stavu a vytváří odpověď. Lamport si uvědomil, že náročný úkol replikovat službu na více počítačích lze pozoruhodně zjednodušit, pokud všem replikám předložíte stejnou posloupnost vstupních příkazů a ony projdou identickou posloupností stavů.
Toto pronikavé paradigma SMR je základem mnoha spolehlivých systémů a díky své eleganci je považováno za standardní přístup pro budování replikovaných distribuovaných systémů. Než však Lamport vyvinul úplné řešení využívající pro SMR, potřeboval se zabývat základní složkou, dohodou, kterou se zabýval ve své další práci.
Byzantská dohoda: Zatímco přístupy založené na stavových strojích, které jsou odolné vůči poruchám při havárii, jsou pro mnoho aplikací dostačující, kritičtější systémy, například pro avioniku, potřebují ještě extrémnější model odolnosti vůči poruchám, který je odolný vůči uzlům, které by mohly narušit systém zevnitř.
Lamport byl v 70. letech minulého století ve Stanfordském výzkumném institutu (později pod názvem SRI International) členem týmu, který pomáhal NASA navrhnout odolný systém řízení avioniky. Formální záruky byly naprostou nutností kvůli kritické povaze úkolu. Bezpečnost musela být zaručena proti nejextrémnějším poruchám systému, jaké si lze představit. Jedním z prvních úkolů, který měl tým SRI přijmout, bylo prokázat správnost systému řízení pilotní kabiny, který NASA navrhla, pomocí tří počítačových systémů, které používají většinové hlasování k zamaskování jakékoli vadné součásti.
Výsledkem práce týmu bylo několik základních konceptů a poznatků týkajících se těchto přísných typů robustních systémů. Patřila k nim základní definice robustnosti v tomto prostředí, abstrakce koordinačního problému, který je dodnes základem každého replikovaného systému, a překvapivé odhalení, že systémy se třemi počítači nikdy nemohou bezpečně provozovat kritický kokpit!“
Ve dvou zásadních pracích („LPS“) publikovaných společně s Peasem a Shostakem , tým poprvé identifikoval poněkud zvláštní zranitelnost. LPS předpokládal, že „selhávající součást může vykazovat typ chování, který je často přehlížen – totiž vysílání konfliktních informací do různých částí systému“. Obecněji řečeno, porouchaná komponenta by mohla fungovat způsobem zcela neodpovídajícím jejímu předepsanému chování a mohla by se jevit téměř jako škodlivá.
Nový model poruchy potřeboval název. V té době existoval související klasický problém koordinace dvou komunikujících počítačů, představený v článku z roku 1975 a označovaný Jimem Grayem v jako „Paradox dvou generálů „. To vedlo Lamporta k představě řídicích počítačů v kokpitu jako armády byzantských generálů, přičemž armáda se snaží vytvořit koordinovaný útok, zatímco zrádci uvnitř vysílají protichůdné signály. Pro tento model poruchy se vžil název „byzantské poruchy“ a následovala lavina akademických prací. Model byzantských poruch se stále používá pro zachycení nejhoršího druhu neštěstí a bezpečnostních chyb v systémech.
Lamport vysvětluje své použití příběhu o „byzantských generálech“ k zarámování problému v distribuovaných systémech odolných proti poruchám.
Byzantské poruchy analyzují špatné věci, které se mohou stát. Ale co dobré věci, které se musí stát? LPS také podal abstraktní formulaci problému dosažení koordinace navzdory byzantským selháním; tento problém je znám jako problém „byzantské dohody“. Tato stručná formulace vyjadřuje úlohu koordinace řízení jako problém vytvoření rozhodnutí o dohodě pro jednotlivý bit, počínaje potenciálně různými bity na vstupu každé komponenty. Jakmile jednou získáte dohodu o jednom bitu, je možné ji opakovaně použít k udržení koordinace celého složitého systému. Článek ukazuje, že k vytvoření dohody o jediném bitu tváří v tvář jediné poruše jsou zapotřebí čtyři počítače. Tři nestačí, protože při třech jednotkách může vadná jednotka poslat konfliktní hodnoty zbylým dvěma jednotkám a s každou z nich vytvořit jinou většinu. Obecněji ukázali, že k překonání F současně vadných komponent je zapotřebí 3F+1 jednotek. K důkazu použili krásný argument symetrie, který se stal známým jako ´hexagonální argument´. Tento archetypální argument našel další využití vždy, když někdo tvrdí, že nefunkční jednotka, která vysílá konfliktní informace do různých částí systému, vypadá k nerozeznání od symetrické situace, v níž jsou správné a chybné role obrácené.
LPS také ukázali, že stačí 3F+1 jednotek, a představili řešení pro dosažení byzantské dohody mezi 3F+1 jednotkami v F+1 synchronních komunikačních kolech. Ukázali také, že při použití digitálních podpisů stačí a jsou nutné pouze 2F+1 jednotky.
Problém byzantské dohody a jeho řešení se stal charakteristickým znakem systémů odolných proti poruchám. Většina systémů konstruovaných s redundancí ji využívá interně pro replikaci a pro koordinaci. Sám Lamport ji později použil při tvorbě paradigmatu State Machine Replication, o kterém bude řeč dále a který dává algoritmický základ replikaci.
Příspěvek z roku 1980 byl oceněn v roce 2005 cenou Edsgera W. Dijkstry v oblasti distribuovaných počítačů a příspěvek z roku 1982 získal cenu Jeana-Clauda Laprieho v oblasti spolehlivých počítačů.
Paxos: S rostoucím pochopením problému dohody pro distribuované výpočty nastal čas, aby se Lamport vrátil k replikaci stavových strojů a řešil selhání tam. První řešení SMR, které představil ve svém článku z roku 1978, předpokládalo, že k žádným selháním nedochází, a využívalo logický čas k tomu, aby repliky postupně procházely stejnou posloupností příkazů. V roce 1989 Lamport navrhl algoritmus odolný proti poruchám nazvaný Paxos . Pokračoval v trendu vyprávění humorných podobenství a v článku představil imaginární příběh vládního parlamentu na starověkém řeckém ostrově jménem Paxos, kde lze tolerovat nepřítomnost libovolného počtu jeho členů, případně všech, aniž by došlo ke ztrátě konzistence.
Lamport popisuje vznik svého algoritmu Paxos pro distribuované výpočty odolné vůči poruchám.
Naneštěstí zasazení do podobenství o Řecku způsobilo, že článek byl pro většinu čtenářů obtížně srozumitelný, a od jeho odevzdání do vydání v roce 1998 uplynulo devět let. Technická zpráva DEC z roku 1989 však vzbudila pozornost. Lamportův kolega Butler Lampson tuto myšlenku evangelizoval komunitě distribuovaných počítačů . Krátce po zveřejnění Paxosu nabídl systém Chubby od Googlu a open-source ZooKeeper od Apache replikaci stavového stroje jako externí, široce rozšířenou službu.
Paxos sešívá posloupnost rozhodnutí o dohodě do posloupnosti příkazů stavového stroje optimalizovaným způsobem. Důležité je, že první fázi součásti dohody uvedené v článku Paxos (nazvané Synod) se lze vyhnout, pokud stejný vůdce předsedá více rozhodnutím; tuto fázi je třeba provést pouze tehdy, když je třeba vůdce vyměnit. Tento pronikavý objev stojí z velké části za popularitou systému Paxos, který byl později týmem Google nazván Multi-Paxos . Lamportův článek o systému Paxos získal v roce 2012 cenu ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award.
SMR a Paxos se staly de facto standardním rámcem pro navrhování a zdůvodňování metod konsensu a replikace. Základy Paxosu přijalo mnoho společností vytvářejících kritické informační systémy, včetně společností Google, Yahoo, Microsoft a Amazon.
5. Formální specifikace a verifikace programů
V počátcích teorie souběhu se objevila potřeba dobrých nástrojů pro popis řešení a důkaz jejich správnosti. Lamport zásadním způsobem přispěl k teorii specifikace a verifikace souběžných programů. Například jako první formuloval pojmy bezpečnostních vlastností a vlastností živosti pro asynchronní distribuované algoritmy. Ty byly zobecněním vlastností „částečné správnosti“ a „úplné správnosti“, které byly dříve definovány pro sekvenční programy. Dnes tvoří vlastnosti bezpečnosti a živosti standardní klasifikaci vlastností správnosti asynchronních distribuovaných algoritmů.
Další práce, spolu s Martinem Abadim , zavedla do modelu algoritmu speciální abstrakci zvanou proměnné proroctví, která řeší situaci, kdy algoritmus vyřeší nedeterministickou volbu dříve než specifikace. Abadi a Lamport poukázali na situace, kdy takové problémy vznikají, a vyvinuli teorii potřebnou k podpoře tohoto rozšíření teorie. Navíc dokázali, že kdykoli se distribuovaný algoritmus setká se specifikací, kde jsou oba vyjádřeny jako stavové stroje, lze korespondenci mezi nimi dokázat pomocí kombinace proměnných proroctví a předchozích pojmů, jako jsou proměnné historie. Tato práce získala v roce 2008 cenu LICS Test-Of-Time.
Formální modelovací jazyky a verifikační nástroje: Kromě vývoje výše uvedených základních pojmů Lamport vyvinul jazyk TLA (Temporal Logic of Actions) a sadu nástrojů TLA+ pro modelování a ověřování distribuovaných algoritmů a systémů.
Lamport popisuje jazyk TLA a jeho spojení s mapováním upřesnění.
Jazyky TLA a TLA+ podporují specifikaci a důkaz vlastností bezpečnosti i živosti pomocí notace založené na časové logice. Lamport dohlížel na vývoj verifikačních nástrojů založených na TLA+, zejména na TLC model checker, který vytvořil Yuan Yu. TLA+ a TLC byly použity k popisu a analýze reálných systémů. Tyto nástroje byly například použity k nalezení závažné chyby v koherenčním protokolu použitém v hardwaru pro Xbox 360 společnosti Microsoft před jeho vydáním v roce 2005. Ve společnosti Intel byly použity pro analýzu koherenčního protokolu mezipaměti Intel Quick Path Interconnect implementovaného v procesoru s jádrem Nehalem. Aby naučil inženýry používat své formální specifikační nástroje, napsal Lamport knihu . Nedávno Lamport vyvinul formální jazyk a nástroje PlusCAL pro použití při ověřování distribuovaných algoritmů; tato práce navazuje na TLA+.
6. LaTeX
Při tvorbě tak rozsáhlé sbírky impaktovaných článků je přirozené přát si vhodný nástroj pro sazbu. Lamport si ho nejen přál, ale vytvořil ho pro celou komunitu. Mimo oblast souběhu je Lamportův systém Latex , sada maker pro použití se systémem pro sazbu TeX Donalda Knutha. LaTeX přidal do TeXu tři důležité věci:
- Koncept „typografického prostředí“, který měl původ v systému Scribe Briana Reida.
- Silný důraz na strukturální, nikoli typografické značky.
- Všeobecný design dokumentu, dostatečně flexibilní, aby byl vhodný pro širokou škálu dokumentů.
Lamport nebyl původcem těchto myšlenek, ale jejich maximálním prosazením vytvořil systém, který poskytuje kvalitu TeXu a velkou část jeho flexibility, ale je mnohem jednodušší na používání. Latex se stal de facto standardem pro technické publikování v informatice a mnoha dalších oborech.
Existuje mnoho dalších důležitých prací Leslieho Lamporta – je jich příliš mnoho na to, abychom je zde popisovali. Jsou uvedeny v chronologickém pořadí na Lamportově domovské stránce , doplněné historickými poznámkami, které popisují motivaci a kontext každého výsledku.
Každý přístup k modernímu počítači pravděpodobně ovlivní algoritmy Leslieho Lamporta. A celá tato práce začala snahou pochopit, jak organizovat frontu v místní pekárně.
Autor: Dahlia Malkhiová
Další přispěvatelé: Dahlia Malkhiová
Další přispěvatelé: Dalšími autory jsou Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese a Len Shustek
.