Gdybyśmy mogli cofnąć się w czasie do roku 1974, być może zastalibyśmy Leslie Lamporta w jego ruchliwej, lokalnej piekarni, zmagającego się z następującym problemem. Piekarnia miała kilku kasjerów, ale jeśli więcej niż jedna osoba podchodziła do jednego kasjera w tym samym czasie, kasjer próbował rozmawiać z nimi wszystkimi na raz i stawał się zdezorientowany. Lamport zdał sobie sprawę, że musi być jakiś sposób, aby zagwarantować, że ludzie będą podchodzić do kasjerów pojedynczo. Ten problem przypomniał Lamportowi o zagadnieniu, które zostało postawione we wcześniejszym artykule informatyka Edsgera Dijkstry na temat innej prozaicznej kwestii: jak dzielić naczynia przy stole. Jednym z wyzwań koordynacyjnych było zagwarantowanie, że każdy przyrząd był używany przez co najwyżej jednego gościa w tym samym czasie, co zostało uogólnione jako problem wzajemnego wykluczania, dokładnie takie samo wyzwanie, przed jakim stanął Lamport w piekarni.

Jednego ranka w 1974, pomysł przyszedł do Lamport na jak klienci piekarni może rozwiązać wzajemnego wykluczenia między sobą, bez polegania na piekarni o pomoc. Działało to mniej więcej tak: ludzie wybierają numery, gdy wchodzą do piekarni, a następnie zostają obsłużeni przy kasie zgodnie z zamówionym numerem. Aby wybrać numer, klient pyta o numer wszystkich wokół siebie i wybiera numer wyższy niż wszystkie inne.

Ten prosty pomysł stał się eleganckim algorytmem do rozwiązywania problemu wzajemnego wykluczania, nie wymagając żadnych niepodzielnych operacji niższego rzędu. Był on również bogatym źródłem przyszłych pomysłów, ponieważ wiele kwestii musiało zostać dopracowanych. Na przykład, niektórzy klienci piekarni długo sprawdzali inne numery, a w międzyczasie przychodzili kolejni klienci i wybierali dodatkowe numery. Innym razem kierownik piekarni chciał mieć wgląd we wszystkie numery klientów, aby przygotować wystarczającą ilość ciastek. Lamport powiedział później „Przez kilka lat po moim odkryciu algorytmu piekarni wszystko, czego nauczyłem się o współbieżności, pochodziło z jego studiowania.”

Algorytm piekarni i inne pionierskie prace Lamporta — wiele o zabawnych nazwach i związanych z nimi przypowieściach — stały się filarami informatyki. Jego zbiór stanowi podstawę szerokich obszarów współbieżności i wpłynął na specyfikację, rozwój i weryfikację systemów współbieżnych.

Po ukończeniu studiów z tytułem doktora matematyki na Brandeis University w 1972 roku, Lamport pracował jako informatyk w Massachusetts Computer Associates w latach 1970-1977, w SRI International w latach 1977-1985 oraz w Digital Equipment Corporation Systems Research Center (później własność Compaq) w latach 1985-2001. W 2001 roku dołączył do Microsoft Research w Mountain View w Kalifornii.

Spędzenie kariery naukowej w przemysłowych środowiskach badawczych nie było przypadkiem. „Lubię pracować w przemysłowym laboratorium badawczym, ze względu na wkład”, powiedział Lamport. „Gdybym pracował sam i wymyślał problemy, wymyśliłbym niewielką liczbę rzeczy, ale jeśli wyjdę do świata, gdzie ludzie pracują nad prawdziwymi systemami komputerowymi, jest tam milion problemów. Kiedy patrzę wstecz na większość rzeczy, nad którymi pracowałem – bizantyjskie generały, Paxos – wzięły się one z problemów świata rzeczywistego.”

Jego prace rzuciły światło na fundamentalne zagadnienia programów współbieżnych, dla których nie istniała wówczas żadna formalna teoria. Zmagał się z podstawowymi pojęciami, takimi jak przyczynowość i czas logiczny, atomowe i regularne rejestry współdzielone, spójność sekwencyjna, replikacja maszyn stanowych, bizantyjskie porozumienie i wait-freedom. Pracował nad algorytmami, które stały się standardową praktyką inżynierską dla systemów rozproszonych odpornych na błędy. Rozwinął również znaczny zakres prac nad formalną specyfikacją i weryfikacją systemów współbieżnych, a także przyczynił się do rozwoju zautomatyzowanych narzędzi stosujących te metody. Poruszymy tu tylko niektóre z jego prac.

1. Rozwiązania wzajemnego wykluczania i algorytm Bakery

Wpływowe prace Lamporta z lat 70. i 80. powstały w czasie, gdy zrozumienie podstawowych zagadnień programowania dla wielu procesorów współbieżnych było niewielkie.

Na przykład wiadomo było, że poprawne wykonanie może wymagać, aby równoległe działania wykluczały się wzajemnie podczas okresów w „sekcjach krytycznych”, gdy manipulują tymi samymi danymi, aby zapobiec niepożądanemu przeplataniu się operacji. Początki tego problemu wzajemnego wykluczania wywodzą się z pionierskiej pracy Edsgera Dijkstry, która zawiera jego rozwiązanie. Algorytm Dijkstry, choć poprawny, zależy od tego, czy dostęp do wspólnej pamięci jest atomowy – że jeden procesor czytający, gdy inny pisze, będzie musiał poczekać, zamiast zwracać potencjalnie zniekształconą wartość. W pewnym sensie konstruuje on wysokopoziomowe rozwiązanie z niskopoziomowego wzajemnego wykluczania już zaimplementowanego przez sprzęt.

Niezwykle elegancki i intuicyjny „Algorytm piekarni” Lamporta nie robi tego. Jego rozwiązanie porządkuje rywalizujące procesy w ukrytej kolejce zgodnie z ich kolejnością przybycia, podobnie jak kolejka oczekujących w piekarni. Jednak nie ma znaczenia, czy procesor czytający dane, które są aktualizowane przez inny procesor, dostanie śmieci. Algorytm nadal działa.

Lamport wspomina swoje odkrycie algorytmu Bakery.

Algorytm Bakery stał się materiałem podręcznikowym, a większość studentów informatyki styka się z nim w trakcie studiów.

2. Podstawy programowania współbieżnego

Kilka ważnych nowych koncepcji wyrosło z pracy nad algorytmem Bakery’ego, a tendencja ta powtarzała się kilkakrotnie w karierze Lamporta. Doświadczenie z opracowywaniem algorytmów współbieżnych i weryfikacją poprawności sprawiło, że skupił się na podstawowych podstawach, które sprawiłyby, że wieloprocesory zachowywałyby się w sposób, o którym programiści mogliby rozumować matematycznie. Pracując nad rozwiązaniem konkretnego problemu, Lamport wymyślił abstrakcje i ogólne reguły potrzebne do rozumowania o jego poprawności, a te koncepcyjne wkłady stały się następnie teoretycznymi filarami programowania współbieżnego.

Loop-freedom: Praca Bakery Algorithm wprowadziła ważne pojęcie zwane „wolnością pętli”. Niektóre oczywiste rozwiązania, które przychodzą na myśl dla problemu wzajemnego wykluczania, wstępnie przydzielają `obroty’ w rotacji pomiędzy procesami. Ale to zmusza procesy do czekania na inne, które są wolne i jeszcze nie osiągnęły punktu spornego. Używając analogii z piekarnią, byłoby to podobne do przybycia do pustej piekarni i bycia poproszonym o czekanie na klienta, który nawet nie przybył jeszcze do piekarni. W przeciwieństwie do tego, swoboda pętli wyraża zdolność procesów do robienia postępów niezależnie od szybkości innych procesów. Ponieważ Algorytm Piekarni przydziela kolejki procesom w kolejności ich przybycia, posiada on swobodę pętli. Jest to kluczowe pojęcie, które zostało wykorzystane przy projektowaniu wielu kolejnych algorytmów, a także przy projektowaniu architektur pamięci. Wait-freedom, czyli warunek wymagający niezależnego postępu pomimo niepowodzeń, ma swoje wyraźne korzenie w pojęciu loop-freedom i koncepcji Bakery doorway. Została ona później szeroko zbadana przez innych, w tym Maurice’a Herlihy’ego .

Sekwencyjna spójność: Praca z architekturą wielordzeniową, która miała rozproszoną pamięć podręczną, doprowadziła Lamporta do stworzenia formalnej specyfikacji dla spójnego zachowania pamięci podręcznej w systemach wieloprocesorowych. Praca ta wniosła trochę porządku do chaosu tej dziedziny poprzez wynalezienie spójności sekwencyjnej, która stała się złotym standardem dla modeli spójności pamięci. To proste i intuicyjne pojęcie zapewnia właściwy poziom „atomowości”, pozwalający na działanie oprogramowania. Dziś projektujemy systemy sprzętowe z porządkowaniem timestamp lub partial-store, z dodanymi instrukcjami ogrodzenia pamięci, co pozwala programistom sprawić, że sprzęt wydaje się sekwencyjnie spójny. Programiści mogą następnie zaimplementować algorytmy, które zapewniają silne właściwości spójności. Jest to klucz do modeli spójności pamięci w Javie i C++. Nasze wielordzeniowe procesory działają dziś w oparciu o zasady opisane przez Leslie Lamport w 1979 roku.

Rejestry atomowe i regularne: Algorytm Bakery doprowadził również Lamporta do zastanowienia się nad dokładną semantyką pamięci, gdy wiele procesów wchodzi w interakcje, aby dzielić się danymi. Zajęło to prawie dekadę, aby sformalizować, a wynikiem jest abstrakcja rejestrów regularnych i atomowych .

Jego teoria daje każdej operacji na wspólnym rejestrze wyraźny czas trwania, zaczynając od wywołania i kończąc wynikiem. Rejestry mogą być implementowane za pomocą różnych technik, takich jak replikacja. Niemniej jednak, interakcje procesów z rejestrem atomowym mają „wyglądać” jak szeregowe dostępy do rzeczywistej pamięci współdzielonej. Teoria ta zawiera również słabsze semantyki interakcji, jak w przypadku rejestru regularnego. Rejestr regularny pozwala uchwycić sytuacje, w których procesy czytają różne repliki rejestru podczas jego aktualizacji. W dowolnym momencie, niektóre repliki mogą być aktualizowane, podczas gdy inne nie, a ostatecznie wszystkie repliki będą posiadały zaktualizowaną wartość. Co ważne, ta słabsza semantyka wystarcza do obsługi wzajemnego wykluczania: algorytm Bakery działa poprawnie, jeśli czytelnik zachodzący na pisarza uzyskuje z powrotem dowolną arbitralną wartość.

Lamport opisuje swoją pracę nad precyzyjnym zdefiniowaniem abstrakcji dla rejestrów atomowych, regularnych i bezpiecznych.

Ta praca zapoczątkowała odrębną subdziedzinę badań w informatyce rozproszonej, która wciąż kwitnie. Obiekty atomowe Lamporta obsługiwały tylko operacje odczytu i zapisu, czyli były rejestrami atomowymi. Pojęcie to zostało uogólnione na inne typy danych przez Maurice’a Herlihy’ego i Jeannette Wing, a ich termin „liniowość” stał się synonimem atomowości. Obecnie zasadniczo wszystkie nierelacyjne systemy pamięci masowej opracowane przez firmy takie jak Amazon, Google i Facebook przyjmują liniowość i spójność sekwencyjną dla swoich gwarancji spójności danych.

3. Podstawy systemów rozproszonych

Specjalnym rodzajem systemu współbieżnego jest system rozproszony, charakteryzujący się posiadaniem procesów, które używają wiadomości do interakcji między sobą. Leslie Lamport miała ogromny wpływ na sposób, w jaki myślimy o systemie rozproszonym, jak również na praktyki inżynierskie w tej dziedzinie.

Zegary logiczne: Wiele osób zdawało sobie sprawę, że globalne pojęcie czasu nie jest naturalne dla systemu rozproszonego. Lamport był pierwszym, który sprecyzował alternatywne pojęcie „zegarów logicznych”, które nakładają częściowy porządek na zdarzenia w oparciu o związek przyczynowy wywołany przez wysyłanie wiadomości z jednej części systemu do drugiej. Jego praca na temat „Time, Clocks, and the Ordering of Events in a Distributed System” stała się najczęściej cytowaną pracą Lamporta, a w języku informatyki logiczne zegary są często nazywane timestampami Lamporta. Jego praca zdobyła w 2000 roku nagrodę Principles of Distributed Computing Conference Influential Paper Award (później przemianowaną na Edsger W. Dijkstra Prize in Distributed Computing), a w 2007 roku zdobyła nagrodę ACM SIGOPS Hall of Fame Award.

Lamport opisuje swoją pracę „Time, Clocks…” i jej związek ze szczególną względnością.

Aby zrozumieć, dlaczego ta praca stała się tak wpływowa, należy uznać, że w momencie jej wynalezienia nie było dobrego sposobu na uchwycenie opóźnienia komunikacyjnego w systemach rozproszonych, z wyjątkiem użycia czasu rzeczywistego. Lamport zdał sobie sprawę, że opóźnienie komunikacyjne czyni te systemy bardzo różnymi od systemów wieloprocesorowych z pamięcią wspólną. Spostrzeżenie przyszło podczas czytania pracy na temat replikowanych baz danych i uświadomienia sobie, że logiczne uporządkowanie poleceń może naruszać przyczynowość.

Używanie uporządkowania zdarzeń jako sposobu na udowodnienie poprawności systemu jest w większości tym, co ludzie robią dzisiaj dla intuicyjnych dowodów współbieżnych algorytmów synchronizacji. Innym potężnym wkładem tej pracy było zademonstrowanie jak replikować maszynę stanów używając logicznych zegarów, co jest wyjaśnione poniżej.

Distributed Snapshots: Kiedy już zdefiniujesz porządek przyczynowy, pojęcie spójnych stanów globalnych naturalnie z niego wynika. To doprowadziło do kolejnej wnikliwej pracy. Lamport i Mani Chandy wymyślili pierwszy algorytm odczytywania stanu (robienia `zrzutu’) dowolnego systemu rozproszonego. Jest to tak potężne pojęcie, że inni później wykorzystali je w różnych domenach, takich jak sieci, samostabilizacja, debugowanie i systemy rozproszone. Praca ta otrzymała nagrodę 2013 ACM SIGOPS Hall of Fame Award.

4. Odporność na błędy i replikacja maszyn stanowych

„System rozproszony to taki, w którym awaria komputera, o którego istnieniu nawet nie wiedziałeś, może sprawić, że twój własny komputer stanie się bezużyteczny” – to słynny dowcip Lamporta. Duża część jego pracy dotyczy odporności na błędy.

State Machine Replication (SMR): Być może najbardziej znaczącym z wielu wkładów Lamporta jest paradygmat State Machine Replication, który został wprowadzony w słynnym artykule „Time, Clocks, and the Ordering of Events in a Distributed System” i dalej rozwijany wkrótce potem. Abstrakcja ta ujmuje dowolną usługę jako scentralizowaną maszynę stanów – rodzaj uniwersalnego silnika obliczeniowego podobnego do maszyny Turinga. Posiada ona stan wewnętrzny i przetwarza polecenia w sekwencji, z których każde skutkuje nowym stanem wewnętrznym i wytworzeniem odpowiedzi. Lamport zdał sobie sprawę, że trudne zadanie replikacji usługi na wielu komputerach można uczynić niezwykle prostym, jeśli przedstawi się wszystkim replikom tę samą sekwencję poleceń wejściowych, a one same przejdą przez identyczny ciąg stanów.

Ten wnikliwy paradygmat SMR leży u podstaw wielu niezawodnych systemów i jest uważany za standardowe podejście do budowania replikowanych systemów rozproszonych ze względu na swoją elegancję. Ale zanim Lamport opracował pełne rozwiązanie wykorzystujące SMR, musiał zająć się kluczowym składnikiem, umową, którą zajął się w swojej następnej pracy.

Umowa bizantyjska: Podczas gdy podejścia maszyny stanów, które są odporne na błędy zderzeniowe są wystarczające dla wielu zastosowań, bardziej krytyczne systemy, takie jak w awionice, potrzebują jeszcze bardziej ekstremalnego modelu odporności na błędy, który jest odporny na węzły, które mogą zakłócić system od wewnątrz.

W Stanford Research Institute (później nazwanym SRI International) w latach 70-tych, Lamport był częścią zespołu, który pomógł NASA zaprojektować solidny system kontroli awioniki. Gwarancje formalne były absolutną koniecznością ze względu na krytyczny charakter zadania. Bezpieczeństwo musiało być zagwarantowane przed najbardziej ekstremalnymi awariami systemu, jakie można sobie wyobrazić. Jednym z pierwszych wyzwań, o których podjęcie poproszono zespół z SRI, było udowodnienie poprawności schematu sterowania kokpitem, zaprojektowanego przez NASA, za pomocą trzech systemów komputerowych, które wykorzystują głosowanie większością głosów, aby zamaskować każdy wadliwy element.

Wynikiem pracy zespołu było kilka fundamentalnych koncepcji i spostrzeżeń dotyczących tych rygorystycznych typów systemów odpornych. Obejmowały one fundamentalną definicję odporności w tym środowisku, abstrakcję problemu koordynacji, który leży u podstaw każdego systemu replikowanego do tej pory, oraz zaskakujące odkrycie, że systemy z trzema komputerami nigdy nie będą w stanie bezpiecznie obsługiwać kokpitu krytycznego dla misji!

W dwóch przełomowych pracach („LPS”) opublikowanych wraz z Pease’em i Shostakiem, zespół po raz pierwszy zidentyfikował nieco osobliwą podatność. LPS stwierdził, że „uszkodzony komponent może wykazywać typ zachowania, który jest często pomijany – mianowicie, wysyłanie sprzecznych informacji do różnych części systemu”. Bardziej ogólnie, wadliwie działający komponent może funkcjonować w sposób całkowicie niezgodny z jego zalecanym zachowaniem i może wydawać się niemal złośliwy.

Nowy model usterki potrzebował nazwy. W tym czasie nie było związane klasyczne wyzwanie koordynowania dwóch komunikujących się komputerów, wprowadzone w 1975 papieru i określone przez Jima Graya w jako „The Two Generals Paradox”. To doprowadziło Lamporta do myślenia o komputerach sterujących w kokpicie jako o armii bizantyjskich generałów, z armią próbującą sformować skoordynowany atak, podczas gdy wewnętrzni zdrajcy wysyłali sprzeczne sygnały. Dla tego modelu usterek przyjęto nazwę „Byzantine Failures”, a następnie rozpoczęto intensywną pracę naukową. Model błędu bizantyjskiego jest nadal używany do uchwycenia najgorszego rodzaju błędów i wad bezpieczeństwa w systemach.

Lamport wyjaśnia swoje wykorzystanie historii o „bizantyjskich generałach” do ujęcia w ramy problemu w systemach rozproszonych tolerujących błędy.

Byzantine Failures analizują złe rzeczy, które mogą się zdarzyć. Ale co z dobrymi rzeczami, które muszą się wydarzyć? LPS podał również abstrakcyjne sformułowanie problemu osiągania koordynacji pomimo bizantyjskich niepowodzeń; jest to znane jako problem „bizantyjskiego porozumienia”. To zwięzłe sformułowanie wyraża zadanie koordynacji sterowania jako problem formowania decyzji o porozumieniu dla pojedynczego bitu, zaczynając od potencjalnie różnych bitów wejściowych do każdego komponentu. Po uzyskaniu porozumienia co do pojedynczego bitu, możliwe jest wielokrotne wykorzystywanie go w celu utrzymania koordynacji całego złożonego systemu. W artykule pokazano, że do osiągnięcia porozumienia w sprawie jednego bitu w obliczu pojedynczej awarii potrzebne są cztery komputery. Trzy nie wystarczą, ponieważ przy trzech jednostkach, uszkodzona jednostka może wysyłać sprzeczne wartości do pozostałych dwóch jednostek i z każdą z nich tworzyć inną większość. Ogólniej, pokazali, że potrzeba 3F+1 jednostek, aby pokonać F jednocześnie wadliwych elementów. Aby to udowodnić, użyli oni pięknego argumentu symetrii, który stał się znany jako „argument sześciokąta”. Ten archetypowy argument znalazł inne zastosowania, gdy argumentuje się, że źle działająca jednostka, która wysyła sprzeczne informacje do różnych części systemu, wygląda nieodróżnialnie od symetrycznej sytuacji, w której prawidłowe i wadliwe role są odwrócone.

LPS wykazali również, że 3F+1 jednostek jest wystarczające, i przedstawili rozwiązanie na osiągnięcie bizantyjskiego porozumienia pomiędzy 3F+1 jednostkami w F+1 rundach synchronicznej komunikacji. Pokazali również, że jeśli używamy podpisów cyfrowych, to wystarczy 2F+1 jednostek.

Problem Byzantine Agreement i jego rozwiązania stały się znakiem rozpoznawczym systemów odpornych na błędy. Większość systemów zbudowanych z redundancji wykorzystuje ją wewnętrznie do replikacji i koordynacji. Sam Lamport wykorzystał go później w tworzeniu omawianego dalej paradygmatu State Machine Replication, który daje algorytmiczne podstawy replikacji.

Praca z 1980 roku została nagrodzona w 2005 roku Edsger W. Dijkstra Prize in Distributed Computing, a praca z 1982 roku otrzymała Jean-Claude Laprie Award in Dependable Computing.

Paxos: Wraz z rosnącym zrozumieniem problemu umowy dla obliczeń rozproszonych, nadszedł czas, aby Lamport powrócił do State Machine Replication i zajął się tam awariami. Pierwsze rozwiązanie SMR, które przedstawił w swojej pracy z 1978 roku zakłada, że nie ma żadnych awarii i wykorzystuje czas logiczny do przejścia replik przez tę samą sekwencję poleceń. W 1989 roku Lamport zaprojektował algorytm odporny na błędy o nazwie Paxos . Kontynuując swój trend humorystycznego opowiadania przypowieści, praca przedstawia wyimaginowaną historię parlamentu rządowego na starożytnej greckiej wyspie o nazwie Paxos, gdzie nieobecność dowolnej liczby jego członków, lub ewentualnie wszystkich, może być tolerowana bez utraty spójności.

Lamport opisuje pochodzenie swojego algorytmu Paxos dla odpornych na błędy obliczeń rozproszonych.

Niestety ustawienie w formie greckiej przypowieści sprawiło, że praca była trudna do zrozumienia dla większości czytelników, a od złożenia do publikacji w 1998 roku minęło dziewięć lat. Jednak raport techniczny DEC z 1989 roku został zauważony. Kolega Lamporta, Butler Lampson, ewangelizował ten pomysł wśród społeczności zajmującej się obliczeniami rozproszonymi. Wkrótce po opublikowaniu Paxosa, system Chubby firmy Google oraz open-source’owy ZooKeeper firmy Apache zaoferowały Replikację Maszyn Stanowych jako zewnętrzną, szeroko stosowaną usługę.

Paxos zszywa w zoptymalizowany sposób sekwencję decyzji umownych w sekwencję poleceń maszyny stanowej. Co ważne, pierwsza faza komponentu porozumienia podana w dokumencie Paxos (zwana Synod) może zostać pominięta, gdy ten sam lider przewodniczy wielu decyzjom; faza ta musi zostać wykonana tylko wtedy, gdy lider musi zostać zastąpiony. Ten wnikliwy przełom odpowiada za dużą część popularności Paxosa i został później nazwany Multi-Paxos przez zespół Google. Artykuł Lamporta o Paxosie zdobył nagrodę ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award w 2012 roku.

SMR i Paxos stały się de facto standardowymi ramami do projektowania i rozumowania o metodach konsensusu i replikacji. Wiele firm budujących krytyczne systemy informacyjne, w tym Google, Yahoo, Microsoft i Amazon, przyjęło fundamenty Paxos.

5. Formalna specyfikacja i weryfikacja programów

W początkach teorii współbieżności pojawiła się potrzeba dobrych narzędzi do opisywania rozwiązań i udowadniania ich poprawności. Lamport wniósł główny wkład do teorii specyfikacji i weryfikacji programów współbieżnych. Na przykład, jako pierwszy wyartykułował pojęcia własności bezpieczeństwa i własności trwałości dla asynchronicznych algorytmów rozproszonych. Były one uogólnieniem własności „częściowej poprawności” i „całkowitej poprawności” zdefiniowanych wcześniej dla programów sekwencyjnych. Dzisiaj własności bezpieczeństwa i liveness tworzą standardową klasyfikację własności poprawności asynchronicznych algorytmów rozproszonych.

Inna praca, z Martinem Abadim, wprowadziła do modelu algorytmu specjalną abstrakcję zwaną zmiennymi przepowiedni, aby obsłużyć sytuację, w której algorytm rozwiązuje nondeterministyczny wybór, zanim zrobi to specyfikacja. Abadi i Lamport wskazali sytuacje, w których pojawiają się takie problemy, i rozwinęli teorię potrzebną do wsparcia tego rozszerzenia teorii. Co więcej, udowodnili, że gdy rozproszony algorytm spotyka się ze specyfikacją, gdzie oba są wyrażone jako maszyny stanów, korespondencja między nimi może być udowodniona przy użyciu kombinacji zmiennych przepowiedni i wcześniejszych pojęć, takich jak zmienne historii. Praca ta zdobyła nagrodę LICS Test-Of-Time 2008.

Formalne języki modelowania i narzędzia weryfikacji: Oprócz rozwijania powyższych podstawowych pojęć, Lamport opracował język TLA (Temporal Logic of Actions) i zestaw narzędzi TLA+, do modelowania i weryfikacji rozproszonych algorytmów i systemów.

Lamport opisuje TLA i jego związek z refinement mapping.

TLA i TLA+ wspierają specyfikację i dowód zarówno własności bezpieczeństwa jak i liveness, używając notacji opartej na logice temporalnej. Lamport nadzorował rozwój narzędzi weryfikacyjnych opartych na TLA+, w szczególności TLC model checker zbudowany przez Yuan Yu. TLA+ i TLC zostały użyte do opisu i analizy rzeczywistych systemów. Na przykład, narzędzia te zostały użyte do znalezienia poważnego błędu w protokole koherencji zastosowanym w sprzęcie dla konsoli Xbox 360 firmy Microsoft przed jej premierą w 2005 roku. W firmie Intel wykorzystano je do analizy protokołu koherencji pamięci podręcznej Intel Quick Path Interconnect zaimplementowanego w procesorze Nehalem. Aby nauczyć inżynierów, jak korzystać z jego narzędzi formalnej specyfikacji, Lamport napisał książkę . Ostatnio Lamport opracował język formalny PlusCAL i narzędzia do weryfikacji algorytmów rozproszonych; praca ta bazuje na TLA+.

6. LaTeX

Przy tworzeniu tak obszernej kolekcji wpływowych prac, naturalnym jest, że chciałoby się mieć wygodne narzędzie do składu. Lamport nie tylko sobie tego życzył, on stworzył je dla całej społeczności. Poza dziedziną współbieżności jest system Latex Lamporta, zestaw makr do użycia z systemem składu TeX Donalda Knutha. LaTeX dodał do TeX-a trzy ważne rzeczy:

1. Pojęcie „środowiska składu”, które powstało w systemie Scribe Briana Reida.
2. Silny nacisk na znaczniki strukturalne, a nie typograficzne.
3. Ogólny projekt dokumentu, na tyle elastyczny, by był odpowiedni dla szerokiej gamy dokumentów.

Lamport nie zapoczątkował tych idei, ale posuwając je tak daleko, jak to tylko możliwe, stworzył system, który zapewnia jakość TeX-a i dużą część jego elastyczności, ale jest znacznie łatwiejszy w użyciu. Latex stał się de facto standardem dla publikacji technicznych w informatyce i wielu innych dziedzinach.

Istnieje wiele innych ważnych prac Leslie Lamporta — zbyt wiele, by je tu opisać. Są one wymienione w porządku chronologicznym na stronie domowej Lamporta, wraz z notkami historycznymi, które opisują motywację i kontekst każdego wyniku.

Za każdym razem, gdy uzyskujesz dostęp do nowoczesnego komputera, możesz być pod wpływem algorytmów Leslie Lamporta. A cała ta praca zaczęła się od dążenia do zrozumienia, jak zorganizować kolejkę w lokalnej piekarni.

Autor: Dahlia Malkhi
Dodatkowi współautorzy: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, and Len Shustek

.