Dacă am fi putut călători în timp până în 1974, poate că l-am fi găsit pe Leslie Lamport la brutăria sa locală de cartier, foarte aglomerată, confruntându-se cu următoarea problemă. Brutăria avea mai mulți casieri, dar dacă mai multe persoane se apropiau de un singur casier în același timp, acel casier încerca să vorbească cu toți în același timp și devenea confuz. Lamport și-a dat seama că trebuie să existe o modalitate de a garanta că oamenii se apropie de casieri unul câte unul. Această problemă i-a amintit lui Lamport de o problemă care a fost pusă într-un articol anterior de către informaticianul Edsger Dijkstra cu privire la o altă problemă banală: cum se împart ustensilele de cină în jurul unei mese. Una dintre provocările de coordonare a fost garantarea faptului că fiecare ustensilă a fost folosită de cel mult un singur diner la un moment dat, care a ajuns să fie generalizată ca problemă de excludere reciprocă, exact provocarea cu care s-a confruntat Lamport la brutărie.

Într-o dimineață din 1974, lui Lamport i-a venit o idee despre cum clienții brutăriei ar putea rezolva excluderea reciprocă între ei, fără a se baza pe ajutorul brutăriei. Funcționa aproximativ în felul următor: oamenii aleg numere când intră în brutărie și apoi sunt serviți la casierie în funcție de numărul comandat. Pentru a alege un număr, un client cerea numărul tuturor celor din jurul său și alegea un număr mai mare decât toți ceilalți.

Această idee simplă a devenit un algoritm elegant pentru rezolvarea problemei excluderii reciproce fără a necesita operații indivizibile de nivel inferior. De asemenea, a fost o sursă bogată de idei viitoare, deoarece trebuiau rezolvate multe probleme. De exemplu, unii clienți ai brutăriei au avut nevoie de mult timp pentru a verifica alte numere și, între timp, alți clienți au sosit și au selectat numere suplimentare. Altă dată, managerul brutăriei a dorit să obțină o imagine instantanee a tuturor numerelor clienților pentru a pregăti suficiente produse de patiserie. Lamport a declarat mai târziu: „Timp de câțiva ani după ce am descoperit algoritmul brutăriei, tot ceea ce am învățat despre concurență a provenit din studierea acestuia.”

Algoritmul brutăriei și alte lucrări de pionierat ale lui Lamport – multe cu nume amuzante și parabole asociate – au devenit piloni ai informaticii. Colecția sa constituie fundamentul unor domenii largi în domeniul concurenței și a influențat specificarea, dezvoltarea și verificarea sistemelor concurente.

După ce a absolvit cu un doctorat în matematică la Universitatea Brandeis în 1972, Lamport a lucrat ca informatician la Massachusetts Computer Associates din 1970 până în 1977, la SRI International din 1977 până în 1985 și la Digital Equipment Corporation Systems Research Center (deținut ulterior de Compaq) din 1985 până în 2001. În 2001 s-a alăturat echipei Microsoft Research din Mountain View, California.

Să-și petreacă cariera de cercetător în medii de cercetare industrială nu a fost un accident. „Îmi place să lucrez într-un laborator de cercetare industrială, din cauza aportului”, a declarat Lamport. „Dacă aș lucra de unul singur și aș veni cu probleme, aș veni cu un număr mic de lucruri, dar dacă mă duc în lume, unde oamenii lucrează la sisteme informatice reale, există un milion de probleme. Când mă uit în urmă la majoritatea lucrurilor la care am lucrat – Byzantine Generals, Paxos – acestea au venit din probleme din lumea reală.”

Lucrările sale au aruncat lumină asupra problemelor fundamentale ale programelor concurente, pentru care nu exista o teorie formală la acea vreme. El s-a confruntat cu concepte fundamentale precum cauzalitatea și timpul logic, registrele partajate atomice și regulate, consistența secvențială, replicarea mașinilor de stare, acordul bizantin și libertatea de așteptare. A lucrat la algoritmi care au devenit o practică standard de inginerie pentru sistemele distribuite cu toleranță la erori. De asemenea, a dezvoltat un volum substanțial de lucrări privind specificarea și verificarea formală a sistemelor concurente și a contribuit la dezvoltarea de instrumente automate care aplică aceste metode. Ne vom referi doar la unele dintre contribuțiile sale.

1. Soluțiile de excludere reciprocă și algoritmul Bakery

Lucrările influente ale lui Lamport din anii 1970 și 1980 au apărut într-o perioadă în care exista doar o înțelegere redusă a problemelor fundamentale privind programarea pentru mai multe procesoare concurente.

De exemplu, se știa că execuția corectă poate necesita ca activitățile paralele să se excludă reciproc în timpul perioadelor din „secțiunile critice” în care manipulează aceleași date, pentru a preveni intercalarea nedorită a operațiilor. Originile acestei probleme de excludere reciprocă provin din activitatea de pionierat a lui Edsger Dijkstra, care include soluția sa. Algoritmul lui Dijkstra, deși este corect, depinde de faptul că accesele la memoria partajată sunt atomice – un procesor care citește atunci când un altul scrie va fi pus să aștepte, în loc să returneze o valoare posibil distorsionată. Într-un anumit sens, el construiește o soluție de nivel înalt din excluderea reciprocă de nivel scăzut deja implementată de hardware.

Lamport’s remarkably elegant and intuitive „Bakery Algorithm” nu face acest lucru. Soluția sa aranjează procesele concurente într-o coadă implicită în funcție de ordinea sosirii lor, la fel ca o coadă de așteptare într-o brutărie. Cu toate acestea, nu contează dacă un procesor care citește date care sunt actualizate de un alt procesor primește gunoi. Algoritmul funcționează în continuare.

Lamport își amintește de descoperirea sa a algoritmului Bakery.

Algoritmul Bakery a devenit material de manual, iar cei mai mulți absolvenți de licență în informatică îl întâlnesc în cursul studiilor lor.

2. Fundamentele programării concurente

Câteva concepte noi importante au emanat din lucrarea Algoritmul Bakery, o tendință care s-a repetat de mai multe ori în cariera lui Lamport. Experiența conceperii algoritmilor concurențiali și a verificării corectitudinii l-a determinat să se concentreze asupra fundamentelor de bază care ar face ca multiprocesoarele să se comporte într-un mod în care programatorii să poată raționa matematic. În timp ce lucra la o soluție pentru o anumită problemă concretă, Lamport a inventat abstracțiuni și reguli generale necesare pentru a raționa asupra corectitudinii acesteia, iar aceste contribuții conceptuale au devenit apoi piloni teoretici ai programării concurente.

Libertatea buclelor: Lucrarea Bakery Algorithm a introdus un concept important numit „libertate de buclă”. Unele soluții evidente care ne vin în minte pentru problema excluderii reciproce pre-atribuie `turnele’ în rotație între procese. Dar acest lucru forțează procesele să aștepte alte procese care sunt lente și care nici măcar nu au ajuns încă la punctul de dispută. Folosind analogia cu brutăria, ar fi ca și cum ai ajunge la o brutărie goală și ți s-ar cere să aștepți un client care nici măcar nu a ajuns încă la brutărie. În schimb, libertatea buclei exprimă capacitatea proceselor de a progresa independent de viteza altor procese. Deoarece Algoritmul brutăriei atribuie turele proceselor în ordinea sosirii lor, acesta dispune de libertate de buclă. Acesta este un concept crucial care a fost utilizat în proiectarea multor algoritmi ulteriori și în proiectarea arhitecturilor de memorie. Libertatea de așteptare, o condiție care necesită un progres independent în ciuda eșecurilor, își are rădăcinile clare în noțiunea de libertate de buclă și în conceptul de ușă Bakery. Ulterior a fost explorată pe larg de alții, inclusiv de Maurice Herlihy .

Coerența secvențială: Lucrul cu o arhitectură multi-core care avea memorie cache distribuită l-a determinat pe Lamport să creeze specificații formale pentru comportamentul coerent al cache-ului în sistemele multiprocesor. Această lucrare a adus puțină ordine în haosul din acest domeniu prin inventarea consistenței secvențiale , care a devenit standardul de aur pentru modelele de consistență a memoriei. Această noțiune simplă și intuitivă oferă exact nivelul potrivit de „atomicitate” pentru a permite software-ului să funcționeze. În prezent, proiectăm sisteme hardware cu ordine cronologică sau cu ordine de stocare parțială, la care se adaugă instrucțiuni de închidere a memoriei, ceea ce permite programatorilor să facă hardware-ul să pară coerent secvențial. Programatorii pot apoi să implementeze algoritmi care oferă proprietăți puternice de coerență. Acest lucru este esențial pentru modelele de consistență a memoriei din Java și C++. Procesoarele noastre multicore funcționează astăzi pe baza principiilor descrise de Leslie Lamport în 1979.

Registre atomice și regulate: Algoritmul Bakery l-a determinat, de asemenea, pe Lamport să se întrebe despre semantica precisă a memoriei atunci când mai multe procese interacționează pentru a partaja date. A fost nevoie de aproape un deceniu pentru a o formaliza, iar rezultatul este abstractizarea registrelor regulate și atomice .

Teoria sa dă fiecărei operații pe un registru partajat o durată explicită, începând cu o invocare și terminând cu un rezultat. Registrele pot fi implementate printr-o varietate de tehnici, cum ar fi replicarea. Cu toate acestea, se presupune că interacțiunile proceselor cu un registru atomic trebuie să „semene” cu accesările seriale la memoria partajată reală. Teoria include, de asemenea, o semantică mai slabă a interacțiunii, precum cea a unui registru obișnuit. Un registru obișnuit surprinde situațiile în care procesele citesc diferite replici ale registrului în timp ce acesta este actualizat. În orice moment, unele replici pot fi actualizate în timp ce altele nu sunt actualizate, iar în cele din urmă, toate replicile vor conține valoarea actualizată. În mod important, această semantică mai slabă este suficientă pentru a susține excluderea reciprocă: algoritmul Bakery funcționează corect dacă un cititor care se suprapune peste un scriitor obține înapoi orice valoare arbitrară.

Lamport descrie munca sa pentru a defini cu precizie abstracțiile pentru registrele atomice, regulate și sigure.

Această lucrare a inițiat un subdomeniu distinct de cercetare în informatica distribuită care este încă înfloritor. Obiectele atomice ale lui Lamport suportau numai operații de citire și scriere, adică erau registre atomice. Noțiunea a fost generalizată la alte tipuri de date de Maurice Herlihy și Jeannette Wing , iar termenul lor de „linearizabilitate” a devenit sinonim cu atomicitatea. Astăzi, în esență, toate sistemele de stocare non-relaționale dezvoltate de companii precum Amazon, Google și Facebook adoptă linearizabilitatea și consistența secvențială pentru garanțiile de coerență a datelor.

3. Fundamentele sistemelor distribuite

Un tip special de sistem concurent este un sistem distribuit, caracterizat prin faptul că are procese care utilizează mesaje pentru a interacționa între ele. Leslie Lamport a avut un impact uriaș asupra modului în care ne gândim la sistemele distribuite, precum și asupra practicilor inginerești din domeniu.

Încuietori logice: Mulți oameni și-au dat seama că o noțiune globală de timp nu este naturală pentru un sistem distribuit. Lamport a fost primul care a precizat o noțiune alternativă de „ceasuri logice”, care impun o ordine parțială a evenimentelor pe baza relației cauzale induse de trimiterea de mesaje de la o parte la alta a sistemului . Lucrarea sa intitulată „Time, Clocks, and the Ordering of Events in a Distributed System” (Timpul, ceasurile și ordonarea evenimentelor într-un sistem distribuit) a devenit cea mai citată lucrare a lui Lamport, iar în limbajul informaticii ceasurile logice sunt adesea supranumite timestamps Lamport. Lucrarea sa a câștigat premiul „Principles of Distributed Computing Conference Influential Paper Award” din 2000 (redenumit ulterior „Edsger W. Dijkstra Prize in Distributed Computing”) și a câștigat un premiu ACM SIGOPS Hall of Fame în 2007.

Lamport descrie lucrarea sa „Time, Clocks…” și relația sa cu relativitatea specială.

Pentru a înțelege de ce această lucrare a devenit atât de influentă, recunoașteți că la momentul invenției nu exista o modalitate bună de a capta întârzierea comunicațiilor în sistemele distribuite decât prin utilizarea timpului real. Lamport și-a dat seama că întârzierea comunicațiilor făcea ca aceste sisteme să fie foarte diferite de un sistem multiprocesor cu memorie partajată. Înțelegerea a venit atunci când a citit o lucrare despre bazele de date replicate și și-a dat seama că ordonarea logică a comenzilor sale ar putea încălca cauzalitatea.

Utilizarea ordonării evenimentelor ca modalitate de a dovedi corectitudinea sistemului este în mare parte ceea ce oamenii fac astăzi pentru dovezile intuitive ale algoritmilor de sincronizare concurentă. O altă contribuție puternică a acestei lucrări a fost demonstrarea modului de replicare a unei mașini de stare folosind ceasuri logice, care este explicată mai jos.

Distributed Snapshots: Odată ce se definește ordinea cauzală, noțiunea de stări globale coerente rezultă în mod natural. Aceasta a dus la o altă lucrare perspicace. Lamport și Mani Chandy au inventat primul algoritm pentru citirea stării (realizarea unui `snapshot’) a unui sistem distribuit arbitrar . Aceasta este o noțiune atât de puternică încât alții au folosit-o ulterior în diferite domenii, cum ar fi rețelele, auto-stabilizarea, depanarea și sistemele distribuite. Această lucrare a primit în 2013 premiul ACM SIGOPS Hall of Fame Award.

4. Fault tolerance and State Machine Replication

„Un sistem distribuit este un sistem în care defectarea unui calculator despre care nici măcar nu știai că există poate face ca propriul tău calculator să fie inutilizabil” este o glumă celebră a lui Lamport. O mare parte din munca sa se referă la toleranța la erori.

State Machine Replication (SMR): Poate cea mai semnificativă dintre numeroasele contribuții ale lui Lamport este paradigma State Machine Replication, care a fost introdusă în celebra lucrare „Time, Clocks, and the Ordering of Events in a Distributed System”, și dezvoltată în continuare la scurt timp după aceea . Această abstractizare surprinde orice serviciu ca o mașină de stare centralizată – un fel de motor de calcul universal asemănător unei mașini Turing. Acesta are o stare internă și procesează comenzile în secvență, fiecare având ca rezultat o nouă stare internă și producând un răspuns. Lamport și-a dat seama că sarcina descurajantă de a replica un serviciu pe mai multe calculatoare poate fi simplificată în mod remarcabil dacă prezentați aceeași secvență de comenzi de intrare tuturor replicilor și acestea trec printr-o succesiune identică de stări.

Această paradigmă SMR perspicace stă la baza multor sisteme fiabile și este considerată o abordare standard pentru construirea de sisteme distribuite replicate datorită eleganței sale. Dar înainte ca Lamport să dezvolte o soluție completă folosind pentru SMR, el trebuia să abordeze un ingredient de bază, acordul, care a fost abordat în următoarea sa lucrare.

Acord bizantin: În timp ce abordările mașinilor de stare care sunt rezistente la defecte de colaps sunt suficiente pentru multe aplicații, sistemele mai critice pentru misiune, cum ar fi cele pentru avionică, au nevoie de un model și mai extrem de toleranță la defecte, care să fie impenetrabil la nodurile care ar putea perturba sistemul din interior.

La Stanford Research Institute (numit ulterior SRI International) în anii 1970, Lamport a făcut parte dintr-o echipă care a ajutat NASA să proiecteze un sistem robust de control al avionicii. Garanțiile formale au fost o necesitate absolută din cauza naturii critice a misiunii. Siguranța trebuia să fie garantată împotriva celor mai extreme disfuncționalități de sistem care se puteau imagina. Una dintre primele provocări pe care echipa de la SRI a fost rugată să le accepte a fost aceea de a dovedi corectitudinea unei scheme de control a cabinei de pilotaj, pe care NASA o proiectase, cu ajutorul a trei sisteme informatice care utilizează votul majoritar pentru a masca orice componentă defectă.

Rezultatul muncii echipei a fost reprezentat de câteva concepte fundamentale și perspective privind aceste tipuri stringente de sisteme robuste. Acestea au inclus o definiție fundamentală a robusteții în acest context, o abstractizare a problemei de coordonare care stă la baza oricărui sistem replicat până în prezent și o revelație surprinzătoare că sistemele cu trei calculatoare nu pot niciodată să gestioneze în siguranță un cockpit critic pentru o misiune!

De fapt, în două lucrări fundamentale („LPS”) publicate împreună cu Pease și Shostak , echipa a identificat pentru prima dată o vulnerabilitate oarecum ciudată. LPS a postulat că „o componentă defectă poate prezenta un tip de comportament care este adesea trecut cu vederea – și anume, trimiterea de informații conflictuale către diferite părți ale sistemului”. Mai general, o componentă defectă ar putea funcționa într-o manieră complet inconsecventă cu comportamentul său prescris și ar putea părea aproape malițioasă.

Noul model de defect avea nevoie de un nume. La acea vreme exista o provocare clasică legată de coordonarea a două calculatoare care comunică, introdusă într-o lucrare din 1975 și menționată de Jim Gray în ca „Paradoxul celor doi generali „. Acest lucru l-a determinat pe Lamport să se gândească la computerele de control dintr-o cabină de pilotaj ca la o armată de generali bizantini, armata încercând să formeze un atac coordonat în timp ce trădătorii din interior trimiteau semnale contradictorii. Pentru acest model de defecțiune a fost adoptată denumirea de „eșecuri bizantine” și a urmat o avalanșă de lucrări academice. Modelul de defecte bizantine este încă folosit pentru a surprinde cele mai grave tipuri de incidente și defecte de securitate în sisteme.

Lamport explică folosirea de către el a unei povești despre „Byzantine Generals” pentru a încadra o problemă în sistemele distribuite tolerante la defecte.

Byzantine Failures analizează lucrurile rele care se pot întâmpla. Dar cum rămâne cu lucrurile bune care trebuie să se întâmple? LPS a oferit, de asemenea, o formulare abstractă a problemei de a ajunge la coordonare în ciuda eșecurilor bizantine; aceasta este cunoscută sub numele de problema „acordului bizantin”. Această formulare succintă exprimă sarcina de coordonare a controlului ca problemă de formare a unei decizii de acord pentru un bit individual, pornind de la biți potențial diferiți introduși în fiecare componentă. Odată ce ați ajuns la un acord asupra unui singur bit, este posibil să îl utilizați în mod repetat pentru a menține coordonat un întreg sistem complex. Lucrarea arată că sunt necesare patru calculatoare pentru a forma un acord asupra unui singur bit în fața unei singure defecțiuni. Trei nu sunt suficiente, deoarece cu trei unități, o unitate defectă poate trimite valori contradictorii celorlalte două unități și poate forma o majoritate diferită cu fiecare dintre ele. Mai general, ei au arătat că sunt necesare 3F+1 unități pentru a depăși F componente defecte simultan. Pentru a demonstra acest lucru, ei au folosit un argument de simetrie frumos, care a devenit cunoscut sub numele de „argumentul hexagonului”. Acest argument arhetip a găsit și alte utilizări ori de câte ori se argumentează că o unitate defectă care trimite informații conflictuale către diferite părți ale sistemului nu se deosebește de o situație simetrică în care rolurile corecte și defecte sunt inversate.

LPS a demonstrat, de asemenea, că 3F+1 unități sunt suficiente și au prezentat o soluție pentru a ajunge la un acord bizantin între cele 3F+1 unități în F+1 runde de comunicare sincronă. Ei au arătat, de asemenea, că, dacă se folosesc semnături digitale, doar 2F+1 unități sunt suficiente și necesare.

Problema acordului bizantin și soluțiile sale au devenit semnul distinctiv al sistemelor tolerante la erori. Cele mai multe sisteme construite cu redundanță se folosesc de aceasta pe plan intern pentru replicare și pentru coordonare. Lamport însuși a folosit-o mai târziu pentru a forma paradigma State Machine Replication discutată în continuare, care oferă fundamentul algoritmic al replicării.

Articolul din 1980 a primit premiul Edsger W. Dijkstra Prize in Distributed Computing din 2005, iar cel din 1982 a primit premiul Jean-Claude Laprie Award in Dependable Computing.

Paxos: Cu o înțelegere din ce în ce mai bună a problemei acordului pentru calculul distribuit, era timpul ca Lamport să se întoarcă la replicarea mașinilor de stat și să abordeze eșecurile acolo. Prima soluție SMR pe care a prezentat-o în lucrarea sa din 1978 presupunea că nu există eșecuri și se folosește de timpul logic pentru a trece replicile prin aceeași secvență de comenzi. În 1989, Lamport a conceput un algoritm de toleranță la erori numit Paxos . Continuând tendința sa de a povesti parabole pline de umor, lucrarea prezintă povestea imaginară a unui parlament guvernamental de pe o insulă grecească antică numită Paxos, unde absența oricărui număr de membri, sau eventual a tuturor, poate fi tolerată fără a se pierde coerența.

Lamport descrie originile algoritmului său Paxos pentru calcul distribuit cu toleranță la erori.

Din păcate, amplasarea ca o parabolă grecească a făcut ca lucrarea să fie dificil de înțeles pentru majoritatea cititorilor și a durat nouă ani de la depunere până la publicare în 1998. Dar raportul tehnic DEC din 1989 a fost remarcat. Colegul lui Lamport, Butler Lampson, a evanghelizat ideea în comunitatea de calcul distribuit . La scurt timp după publicarea lui Paxos, sistemul Chubby al Google și sistemul open-source ZooKeeper al Apache au oferit State Machine Replication ca un serviciu extern, implementat pe scară largă.

Paxos coase o succesiune de decizii de acord într-o secvență de comenzi ale mașinii de stat într-o manieră optimizată. În mod important, prima fază a componentei de acord prezentată în documentul Paxos (numită Synod) poate fi evitată atunci când același lider prezidează mai multe decizii; această fază trebuie realizată numai atunci când un lider trebuie înlocuit. Această descoperire perspicace explică o mare parte din popularitatea Paxos și a fost numită ulterior Multi-Paxos de către echipa Google . Lucrarea Paxos a lui Lamport a câștigat premiul ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award în 2012.

SMR și Paxos au devenit cadrul standard de facto pentru proiectarea și raționamentul privind metodele de consens și replicare. Multe companii care construiesc sisteme de informații critice, inclusiv Google, Yahoo, Microsoft și Amazon, au adoptat bazele Paxos.

5. Specificarea și verificarea formală a programelor

În primele zile ale teoriei concurenței a apărut necesitatea unor instrumente bune pentru a descrie soluțiile și a demonstra corectitudinea lor. Lamport a avut contribuții centrale la teoria specificării și verificării programelor concurente. De exemplu, el a fost primul care a articulat noțiunile de proprietăți de siguranță și proprietăți de vivacitate pentru algoritmii distribuiți asincroni. Acestea au fost generalizarea proprietăților de „corectitudine parțială” și „corectitudine totală” definite anterior pentru programele secvențiale. Astăzi, proprietățile de siguranță și de vivacitate formează clasificarea standard pentru proprietățile de corectitudine ale algoritmilor distribuiți asincroni.

O altă lucrare, împreună cu Martin Abadi , a introdus o abstracțiune specială numită variabile de profeție la un model de algoritm, pentru a gestiona o situație în care un algoritm rezolvă o alegere nedeterministă înainte ca specificația să o facă. Abadi și Lamport au evidențiat situațiile în care apar astfel de probleme și au dezvoltat teoria necesară pentru a susține această extensie a teoriei. Mai mult, ei au demonstrat că, ori de câte ori un algoritm distribuit se întâlnește cu o specificație, unde ambele sunt exprimate ca mașini de stare, corespondența dintre ele poate fi dovedită folosind o combinație de variabile de profeție și noțiuni anterioare, cum ar fi variabilele istorice. Această lucrare a câștigat premiul LICS Test-Of-Time 2008.

Limbaje de modelare formală și instrumente de verificare: În plus față de dezvoltarea noțiunilor de bază de mai sus, Lamport a dezvoltat limbajul TLA (Logica temporală a acțiunilor) și setul de instrumente TLA+, pentru modelarea și verificarea algoritmilor și sistemelor distribuite.

Lamport descrie TLA și legătura sa cu cartografierea de rafinament.

TLA și TLA+ suportă specificarea și demonstrarea atât a proprietăților de siguranță, cât și a celor de vivacitate, folosind o notație bazată pe logica temporală. Lamport a supravegheat dezvoltarea de instrumente de verificare bazate pe TLA+, în special verificatorul de modele TLC construit de Yuan Yu. TLA+ și TLC au fost utilizate pentru a descrie și analiza sisteme reale. De exemplu, aceste instrumente au fost utilizate pentru a găsi o eroare majoră în protocolul de coerență utilizat în hardware-ul pentru Xbox 360 de la Microsoft înainte de lansarea sa în 2005. La Intel, a fost utilizat pentru analiza unui protocol de coerență a memoriei cache a Intel Quick Path Interconnect, așa cum a fost implementat în procesorul de bază Nehalem. Pentru a-i învăța pe ingineri cum să utilizeze instrumentele sale de specificații formale, Lamport a scris o carte . Mai recent, Lamport a dezvoltat limbajul formal PlusCAL și instrumente pentru utilizarea în verificarea algoritmilor distribuiți; această lucrare se bazează pe TLA+.

6. LaTeX

Când se creează o colecție atât de vastă de lucrări de impact, este firesc să se dorească un instrument de tipărire convenabil. Lamport nu și-a dorit doar unul, ci l-a creat pentru întreaga comunitate. În afara domeniului concurenței se află sistemul Latex al lui Lamport , un set de macrocomenzi pentru utilizare cu sistemul de tipărire TeX al lui Donald Knuth. LaTeX a adăugat trei lucruri importante la TeX:

1. Conceptul de „mediu de tipărire”, care își avusese originea în sistemul Scribe al lui Brian Reid.
2. Un accent puternic pe marcajul structural mai degrabă decât pe cel tipografic.
3. Un design generic al documentelor, suficient de flexibil pentru a fi adecvat pentru o mare varietate de documente.

Lamport nu a fost la originea acestor idei, dar împingându-le cât mai departe posibil a creat un sistem care oferă calitatea TeX și o mare parte din flexibilitatea acestuia, dar este mult mai ușor de utilizat. Latex a devenit standardul de facto pentru publicarea tehnică în informatică și în multe alte domenii.

Există multe alte lucrări importante ale lui Leslie Lamport – prea multe pentru a le descrie aici. Ele sunt enumerate în ordine cronologică pe pagina de start a lui Lamport , însoțite de note istorice care descriu motivația și contextul fiecărui rezultat.

De fiecare dată când accesați un calculator modern, este posibil să fiți influențat de algoritmii lui Leslie Lamport. Și toată această muncă a început cu încercarea de a înțelege cum să organizeze o coadă la o brutărie locală.

Autor: Prof. dr: Dahlia Malkhi
Contribuitori suplimentari: Dahlia Malkhi: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese și Len Shustek

.