Ha visszautazhatnánk az időben 1974-be, talán Leslie Lamportot a helyi pékségben találnánk, amint a következő problémával küzd. A pékségnek több pénztárosa volt, de ha egy pénztároshoz egyszerre többen is odaléptek, a pénztáros megpróbált mindannyiukkal egyszerre beszélni, és összezavarodott. Lamport rájött, hogy valamilyen módon garantálni kell, hogy az emberek egyszerre csak egy-egy pénztároshoz forduljanak. Ez a probléma Lamportot egy olyan problémára emlékeztette, amelyet Edsger Dijkstra informatikus egy korábbi cikkében egy másik hétköznapi kérdéssel kapcsolatban vetett fel: hogyan osszuk meg az evőeszközöket az étkezőasztalnál. Az egyik koordinációs kihívás annak garantálása volt, hogy minden egyes evőeszközt egyszerre legfeljebb egy étkező használjon, amit a kölcsönös kizárás problémájaként általánosítottak, pontosan azzal a kihívással, amellyel Lamportnak a pékségben kellett szembenéznie.

1974-ben egy reggel Lamportnak támadt egy ötlete, hogyan oldhatnák meg a pékség vásárlói a kölcsönös kizárást egymás között, anélkül, hogy a pékség segítségére szorulnának. Ez nagyjából így működött: az emberek számokat választanak, amikor belépnek a pékségbe, majd a pénztárnál a számrendelésüknek megfelelően kiszolgálják őket. A számválasztáshoz a vásárló megkérdezi a körülötte lévők számát, és az összes többinél magasabb számot választ.

Ez az egyszerű ötlet egy elegáns algoritmus lett a kölcsönös kizárási probléma megoldására anélkül, hogy alacsonyabb szintű oszthatatlan műveletekre lenne szükség. Emellett gazdag forrása volt a jövőbeli ötleteknek, mivel sok problémát kellett megoldani. Például egyes pékségi vásárlóknak sokáig tartott más számok ellenőrzése, és közben újabb vásárlók érkeztek, akik további számokat választottak ki. Egy másik alkalommal a pékség vezetője pillanatfelvételt akart kapni az összes vásárlói számról, hogy elegendő süteményt tudjon készíteni. Lamport később azt mondta: “A pékség algoritmusának felfedezése után néhány évig minden, amit az egyidejűségről tanultam, ennek tanulmányozásából származott”.

A Sütőalgoritmus és Lamport más úttörő munkái – sokuk vicces nevekkel és kapcsolódó példázatokkal – a számítástechnika pilléreivé váltak. Gyűjteménye az egyidejűség széles területeinek alapját képezi, és hatással volt az egyidejű rendszerek specifikációjára, fejlesztésére és verifikációjára.

Miután 1972-ben a Brandeis Egyetemen matematikából doktorált, Lamport 1970-től 1977-ig a Massachusetts Computer Associates, 1977-től 1985-ig az SRI International, majd 1985-től 2001-ig a Digital Equipment Corporation Systems Research Center (a későbbi Compaq tulajdonában) informatikusként dolgozott. 2001-ben csatlakozott a Microsoft Researchhez a kaliforniai Mountain View-ban.

Kutatói pályafutását nem véletlenül töltötte ipari kutatási környezetben. “Szeretek ipari kutatólaboratóriumban dolgozni, az input miatt” – mondta Lamport. “Ha csak magamban dolgoznék, és problémákat találnék ki, akkor kevés dologra jutnék, de ha kimegyek a világba, ahol emberek valódi számítógépes rendszereken dolgoznak, akkor ott milliónyi probléma van. Ha visszatekintek a legtöbb dologra, amin dolgoztam – Bizánci generálisok, Paxos -, azok valós problémákból eredtek.”

Munkái rávilágítottak az egyidejű programok alapvető kérdéseire, amelyekre akkoriban nem létezett formális elmélet. Olyan alapvető fogalmakkal birkózott meg, mint a kauzalitás és a logikai idő, az atomi és szabályos megosztott regiszterek, a szekvenciális konzisztencia, az állapotgépek replikációja, a bizánci megegyezés és a várakozás-szabadság. Olyan algoritmusokon dolgozott, amelyek a hibatűrő elosztott rendszerek szabványos mérnöki gyakorlatává váltak. Jelentős munkát végzett az egyidejű rendszerek formális specifikációjával és verifikációjával kapcsolatban is, és hozzájárult az ezeket a módszereket alkalmazó automatizált eszközök fejlesztéséhez. Hozzájárulásai közül csak néhányat érintünk.

1. Kölcsönös kizárási megoldások és a Bakery algoritmus

Lamport nagy hatású munkái az 1970-es és 1980-as években készültek, amikor még csak kevéssé voltak tisztában a több egyidejű processzorra történő programozás alapvető kérdéseivel.

Az például ismert volt, hogy a helyes végrehajtás megkövetelheti, hogy a párhuzamos tevékenységek kizárják egymást a “kritikus szakaszok” időszakaiban, amikor ugyanazokat az adatokat manipulálják, hogy a műveletek nemkívánatos átlapolódását megakadályozzák. Ennek a kölcsönös kizárási problémának az eredete Edsger Dijkstra úttörő munkájára vezethető vissza, amely az ő megoldását is tartalmazza. Dijkstra algoritmusa, bár helyes, attól függ, hogy a megosztott memória-hozzáférések atomikusak legyenek – hogy az egyik processzor, amelyik akkor olvas, amikor a másik éppen ír, várakozásra kényszerüljön, ahelyett, hogy egy esetlegesen torzított értéket adna vissza. Bizonyos értelemben magas szintű megoldást konstruál a hardver által már megvalósított alacsony szintű kölcsönös kizárásból.

Lamport figyelemre méltóan elegáns és intuitív “Sütőalgoritmusa” nem ezt teszi. Az ő megoldása a versengő folyamatokat egy implicit sorba rendezi érkezési sorrendjük szerint, hasonlóan a pékség várólistájához. Mégsem számít, ha egy másik processzor által frissített adatokat olvasó processzor szemetet kap. Az algoritmus ettől még működik.

Lamport felidézi a Bakery algoritmus felfedezését.

A Bakery algoritmus tankönyvi anyaggá vált, és a legtöbb informatika alapszakos hallgató találkozik vele tanulmányai során.

2. A konkurens programozás alapjai

A Bakery algoritmus munkájából számos fontos új fogalom származott, ami Lamport pályafutása során többször is megismétlődött. Az egyidejű algoritmusok kidolgozásának és a helyesség ellenőrzésének tapasztalata arra késztette, hogy azokra az alapvető alapokra összpontosítson, amelyek a többprocesszoros processzorokat olyan viselkedésre késztetik, amelyről a programozók matematikailag is tudnak gondolkodni. Miközben egy konkrét konkrét probléma megoldásán dolgozott, Lamport kitalált absztrakciókat és általános szabályokat, amelyek szükségesek a helyességgel kapcsolatos érveléshez, és ezek a fogalmi hozzájárulások aztán az egyidejű programozás elméleti pilléreivé váltak.

Hurokszabadság: A Bakery algoritmus munkája bevezetett egy fontos fogalmat, a “ciklusszabadságot”. Néhány kézenfekvő megoldás, amely a kölcsönös kizárás problémájára jut eszünkbe, előre kijelöli a `fordulókat’ a folyamatok között. Ez azonban arra kényszeríti a folyamatokat, hogy várjanak másokra, amelyek lassúak, és még el sem érték a vitapontot. A pékség analógiáját használva ez olyan lenne, mintha egy üres pékségbe érkeznénk, és arra kérnénk, hogy várjon egy olyan vevőre, aki még meg sem érkezett a pékségbe. Ezzel szemben a hurokszabadság azt fejezi ki, hogy a folyamatok képesek más folyamatok sebességétől függetlenül haladni. Mivel a pékségi algoritmus a folyamatokat az érkezésük sorrendjében sorolja be, hurokszabadsággal rendelkezik. Ez egy kulcsfontosságú fogalom, amelyet számos későbbi algoritmus tervezésénél és a memóriaarchitektúrák tervezésénél is felhasználtak. A várakozás-szabadság, amely a hibák ellenére is független előrehaladást igénylő feltétel, egyértelműen a hurokszabadság fogalmában és a Bakery átjáró koncepciójában gyökerezik. Később mások, köztük Maurice Herlihy is széleskörűen kutatták.

Szekvenciális konzisztencia: Egy olyan többmagos architektúrával való munka, amely elosztott gyorsítótár-memóriával rendelkezett, arra késztette Lamportot, hogy formális specifikációkat hozzon létre a többprocesszoros rendszerekben a gyorsítótárak koherens viselkedésére. Ez a munka rendet teremtett a terület káoszában a szekvenciális konzisztencia feltalálásával , amely a memóriakonzisztencia-modellek arany standardjává vált. Ez az egyszerű és intuitív fogalom éppen a megfelelő szintű “atomicitást” biztosítja a szoftverek működéséhez. Ma hardveres rendszereket tervezünk időbélyegrendezéssel vagy részleges tárolási rendezéssel, hozzáadott memória kerítés utasításokkal, ami lehetővé teszi a programozók számára, hogy a hardvert szekvenciálisan konzisztensnek tüntessék fel. A programozók ezután olyan algoritmusokat implementálhatnak, amelyek erős konzisztencia tulajdonságokat biztosítanak. Ez a Java és a C++ memóriakonzisztencia-modelljeinek kulcsa. Többmagos processzoraink ma a Leslie Lamport által 1979-ben leírt elvek alapján működnek.

Atomikus és szabályos regiszterek: A Bakery algoritmus arra is késztette Lamportot, hogy elgondolkodjon a memória pontos szemantikáján, amikor több folyamat interakcióban osztja meg az adatokat. Ennek formalizálása majdnem egy évtizedet vett igénybe, és az eredmény a szabályos és az atomi regiszterek absztrakciója .

Az elmélete minden egyes műveletnek egy megosztott regiszteren explicit időtartamot ad, amely a meghívással kezdődik és az eredménnyel végződik. A regisztereket különböző technikákkal lehet megvalósítani, például replikációval. Mindazonáltal a folyamatoknak egy atomi regiszterrel való kölcsönhatásai elvileg úgy “néznek ki”, mint a tényleges megosztott memóriához való soros hozzáférés. Az elmélet a kölcsönhatások gyengébb szemantikáját is tartalmazza, mint a hagyományos regiszterekét. A szabályos regiszter olyan helyzeteket ragad meg, amikor a folyamatok a regiszter különböző replikáit olvassák, miközben a regisztert frissítik. Bármelyik pillanatban előfordulhat, hogy egyes replikák frissülnek, míg mások nem, és végül az összes replika tartalmazza a frissített értéket. Fontos, hogy ezek a gyengébb szemantikák elegendőek a kölcsönös kizárás támogatásához: a Bakery algoritmus helyesen működik, ha egy írót átfedő olvasó bármilyen tetszőleges értéket visszakap.

Lamport leírja munkáját az atomi, szabályos és biztonságos regiszterek absztrakcióinak pontos meghatározására.

Ez a munka az elosztott számítástechnikában egy külön kutatási részterületet indított el, amely a mai napig virágzik. Lamport atomi objektumai csak olvasási és írási műveleteket támogattak, azaz atomi regiszterek voltak. A fogalmat Maurice Herlihy és Jeannette Wing általánosította más adattípusokra, és a “linearizálhatóság” kifejezésük az atomicitás szinonimájává vált. Ma már lényegében minden nem-relációs tárolórendszer, amelyet olyan vállalatok fejlesztettek ki, mint az Amazon, a Google és a Facebook, lineárisíthatóságot és szekvenciális konzisztenciát alkalmaz az adatok koherenciájának garantálására.

3. Az elosztott rendszerek alapjai

A konkurens rendszerek egy speciális típusa az elosztott rendszer, amelyet az jellemez, hogy a folyamatok üzenetek segítségével lépnek kapcsolatba egymással. Leslie Lamport nagy hatással volt arra, ahogyan az elosztott rendszerekről gondolkodunk, valamint a terület mérnöki gyakorlatára.

Logikai órák: Sokan felismerték, hogy az idő globális fogalma nem természetes egy elosztott rendszer számára. Lamport volt az első, aki pontosan meghatározta a “logikai órák” alternatív fogalmát, amelyek a rendszer egyik részéből a másikba küldött üzenetek által indukált oksági kapcsolaton alapuló részleges rendet szabnak meg az eseményeknek . Az “Time, Clocks, and the Ordering of Events in a Distributed System” (Idő, órák és az események rendezése egy elosztott rendszerben) című tanulmánya lett Lamport legtöbbet idézett munkája, és az informatikai szaknyelvben a logikai órákat gyakran Lamport időbélyegeknek nevezik. Dolgozata 2000-ben elnyerte a Principles of Distributed Computing Conference Influential Paper Award díját (később átnevezték Edsger W. Dijkstra Prize in Distributed Computing díjra), 2007-ben pedig elnyerte az ACM SIGOPS Hall of Fame Award díját.

Lamport ismerteti az “Time, Clocks…” című dolgozatát és annak kapcsolatát a speciális relativitáselmélettel.

Hogy megértsük, miért lett ez a munka olyan befolyásos, ismerjük fel, hogy a találmány idején nem volt más jó módszer az elosztott rendszerek kommunikációs késleltetésének megragadására, mint a valós idő használata. Lamport felismerte, hogy a kommunikációs késleltetés miatt ezek a rendszerek nagyon különböznek a megosztott memóriájú többprocesszoros rendszerektől. A felismerés akkor jött, amikor elolvasott egy replikált adatbázisokról szóló tanulmányt, és rájött, hogy a parancsok logikai sorrendje sértheti a kauzalitást.

Az események sorrendjének felhasználása a rendszer helyességének bizonyításának módjaként ma leginkább az, amit az emberek az egyidejű szinkronizációs algoritmusok intuitív bizonyítására használnak. Ennek a munkának egy másik erőteljes hozzájárulása az volt, hogy bemutatta, hogyan lehet egy állapotgépet logikai órák segítségével replikálni, amit alább ismertetünk.

Disztributált pillanatfelvételek: Ha egyszer definiáljuk az oksági rendet, a konzisztens globális állapotok fogalma természetesen következik. Ez egy másik éleslátó munkához vezetett. Lamport és Mani Chandy feltalálta az első algoritmust egy tetszőleges elosztott rendszer állapotának kiolvasására (egy `snapshot’ készítésére) . Ez egy olyan erős fogalom, hogy később mások is felhasználták különböző területeken, például a hálózatépítésben, az önstabilizálásban, a hibakeresésben és az elosztott rendszerekben. Ez a dolgozat 2013-ban elnyerte az ACM SIGOPS Hall of Fame Award díjat.

4. Hibatűrés és állapotgép-replikáció

“Az elosztott rendszer olyan rendszer, amelyben egy olyan számítógép meghibásodása, amelynek létezéséről nem is tudtál, használhatatlanná teheti a saját számítógépedet” – ez egy híres Lamport-vers. Munkájának nagy része a hibatűréssel foglalkozik.

State Machine Replication (SMR): Lamport számos hozzájárulása közül talán a legjelentősebb az állapotgép-replikációs paradigma, amelyet az “Time, Clocks, and the Ordering of Events in a Distributed System” című híres dolgozatában mutatott be, és nem sokkal később továbbfejlesztett. Az absztrakció bármely szolgáltatást egy központosított állapotgépként – egyfajta univerzális számítógéptípusként, a Turing-géphez hasonlóan – ábrázol. Van egy belső állapota, és sorban dolgozza fel a parancsokat, amelyek mindegyike új belső állapotot és választ eredményez. Lamport felismerte, hogy egy szolgáltatás több számítógépen történő replikálásának ijesztő feladata rendkívül egyszerűvé tehető, ha a bemeneti parancsok azonos sorozatát adjuk meg minden replikának, és azok az állapotok azonos egymásutánján haladnak keresztül.

Ez az éleslátó SMR-paradigma áll számos megbízható rendszer alapjául, és eleganciája miatt a replikált elosztott rendszerek építésének standard megközelítésének tekinthető. Mielőtt azonban Lamport az SMR-t használva teljes megoldást dolgozott volna ki, foglalkoznia kellett egy alapvető összetevővel, a megegyezéssel, amellyel a következő munkájában foglalkozott.

Byzantine Agreement: Míg az összeomlási hibákkal szemben ellenálló állapotgépes megközelítések sok alkalmazáshoz elegendőek, addig a kritikusabb rendszereknek, például az avionikának, még szélsőségesebb hibatűrési modellre van szükségük, amely áthatolhatatlan az olyan csomópontokkal szemben, amelyek belülről megzavarhatják a rendszert.

A Stanford Research Institute-ban (későbbi nevén SRI International) az 1970-es években Lamport tagja volt annak a csapatnak, amely segített a NASA-nak egy robusztus avionikai vezérlőrendszer tervezésében. A feladat küldetéskritikus jellege miatt a formális garanciák elengedhetetlenül szükségesek voltak. A biztonságot az elképzelhető legszélsőségesebb rendszerhiba ellen is garantálni kellett. Az SRI csapatának egyik első kihívása az volt, hogy a NASA által tervezett pilótafülke-irányítási rendszer helyességét három olyan számítógépes rendszerrel bizonyítsák, amelyek többségi szavazást alkalmaznak a hibás komponensek elfedésére.

A csoport munkájának eredménye számos alapkoncepció és felismerés volt a robusztus rendszerek e szigorú típusaira vonatkozóan. Ide tartozott a robusztusság alapvető definíciója ebben a környezetben, a koordinációs probléma absztrakciója, amely a mai napig minden replikált rendszer alapjául szolgál, és egy meglepő felfedezés, miszerint a három számítógéppel rendelkező rendszerek soha nem tudnak biztonságosan üzemeltetni egy küldetéskritikus pilótafülkét!

A csapat két alapvető munkájában (“LPS”), amelyet Pease és Shostakkal együtt publikáltak, először egy kissé sajátos sebezhetőséget azonosított. Az LPS azt állította, hogy “egy meghibásodott komponens olyan típusú viselkedést mutathat, amelyet gyakran figyelmen kívül hagynak — nevezetesen, hogy ellentmondó információkat küld a rendszer különböző részeinek”. Általánosabban fogalmazva, egy meghibásodott komponens az előírt viselkedésével teljesen ellentétes módon működhet, és szinte rosszindulatúnak tűnhet.

Az új hibamodellnek nevet kellett adni. Abban az időben létezett egy kapcsolódó klasszikus kihívás két kommunikáló számítógép összehangolásával kapcsolatban, amelyet egy 1975-ös tanulmányban mutattak be, és Jim Gray a “The Two Generals Paradox ” néven emlegetett. Ez arra késztette Lamportot, hogy úgy gondoljon a pilótafülkében lévő vezérlő számítógépekre, mint bizánci tábornokok hadseregére, ahol a hadsereg megpróbál összehangolt támadást kialakítani, miközben a belső árulók egymásnak ellentmondó jeleket küldenek. Erre a hibamodellre a “Bizánci meghibásodások” nevet fogadták el, és ezt tudományos munkák egész sora követte. A bizánci hibamodell a mai napig használatos a rendszerek legrosszabb fajta baleseteinek és biztonsági hibáinak megragadására.

Lamport a “bizánci tábornokokról” szóló történet felhasználását a hibatűrő elosztott rendszerek problémájának keretezésére magyarázza.

A bizánci hibák elemzik a rossz dolgokat, amelyek megtörténhetnek. De mi a helyzet a jó dolgokkal, amelyeknek meg kell történniük? Az LPS absztrakt megfogalmazását adta annak a problémának is, hogy a bizánci hibák ellenére is elérjük a koordinációt; ez a “bizánci megállapodás” problémája néven ismert. Ez a tömör megfogalmazás a vezérlési koordinációs feladatot úgy fejezi ki, mint az egyes komponensek bemenetére potenciálisan különböző bitekből kiindulva egy-egy bitre vonatkozó egyetértési döntés kialakításának problémáját. Ha már megvan a megállapodás egyetlen bitre vonatkozóan, akkor azt ismételten felhasználhatjuk egy egész komplex rendszer koordinációjának fenntartása érdekében. A dolgozat bemutatja, hogy egyetlen meghibásodás esetén négy számítógépre van szükség ahhoz, hogy egyetlen bitre vonatkozó megállapodást alakítsunk ki. Három nem elég, mert három egység esetén egy meghibásodott egység egymásnak ellentmondó értékeket küldhet a másik két egységnek, és mindegyiknél más-más többséget alakíthat ki. Általánosabban, kimutatták, hogy 3F+1 egységre van szükség ahhoz, hogy legyőzzük az F egyidejűleg hibás komponenseket. Ennek bizonyítására egy gyönyörű szimmetriaérvet használtak, amely a “hatszög érv” néven vált ismertté. Ez az archetípusos érv más felhasználási területeket is talált, amikor azzal érvelünk, hogy egy hibásan működő egység, amely ellentmondásos információt küld a rendszer különböző részeinek, megkülönböztethetetlennek tűnik egy szimmetrikus helyzettől, amelyben a helyes és a hibás szerepek felcserélődnek.

LPS azt is kimutatta, hogy 3F+1 egység elegendő, és bemutattak egy megoldást arra, hogy F+1 szinkron kommunikációs fordulóban 3F+1 egység között bizánci megállapodást érjünk el. Azt is megmutatták, hogy ha digitális aláírásokat használunk, akkor csak 2F+1 egység elegendő és szükséges.

A Bizánci Egyetértés problémája és annak megoldása a hibatűrő rendszerek védjegyévé vált. A legtöbb redundanciával felépített rendszer belső replikációra és koordinációra használja a redundanciát. Lamport maga is felhasználta később a következőkben tárgyalt állapotgép-replikációs paradigma kialakításakor, amely a replikáció algoritmikus alapját adja.

Az 1980-as dolgozatot 2005-ben Edsger W. Dijkstra-díjjal tüntették ki az elosztott számítástechnikában, az 1982-es pedig Jean-Claude Laprie-díjjal a megbízható számítástechnikában.

Paxos: Az elosztott számítástechnika egyetértési problémájának növekvő megértésével Lamport számára itt volt az ideje, hogy visszatérjen az állapotgép-replikációhoz, és ott foglalkozzon a hibákkal. Az első SMR-megoldás, amelyet 1978-as tanulmányában bemutatott, azt feltételezte, hogy nincsenek hibák, és a logikai időt használja fel arra, hogy a replikákat ugyanazon a parancssorozaton lépkedjen keresztül. 1989-ben Lamport megtervezte a Paxos nevű hibatűrő algoritmust. Folytatva a humoros példamondás trendjét, a dolgozat egy Paxosz nevű ókori görög szigeten lévő kormányparlament képzeletbeli történetét mutatja be, ahol bármelyik tagjának, vagy esetleg az összes tagnak a távolléte tolerálható a konzisztencia elvesztése nélkül.

Lamport leírja a hibatűrő elosztott számítástechnika Paxos algoritmusának eredetét.

Sajnos a görög példabeszédként való beállítás a dolgozatot a legtöbb olvasó számára nehezen érthetővé tette, és a benyújtástól az 1998-as publikálásig kilenc év telt el. A DEC 1989-es műszaki jelentésére azonban felfigyeltek. Lamport kollégája, Butler Lampson evangelizálta az ötletet az elosztott számítástechnikai közösségnek . Röviddel a Paxos publikálása után a Google Chubby rendszere és az Apache nyílt forráskódú ZooKeeperje külső, széles körben elterjedt szolgáltatásként kínálta az állapotgép-replikációt.

A Paxos optimalizált módon fűzi össze az egyetértési döntések sorozatát állapotgép-parancsok sorozatává. Fontos, hogy a Paxos-dokumentumban megadott megállapodási komponens első fázisa (az úgynevezett Synod) elkerülhető, ha ugyanaz a vezető elnököl több döntésben; ezt a fázist csak akkor kell végrehajtani, ha a vezetőt le kell cserélni. Ez az éleslátó áttörés nagyrészt a Paxos népszerűségének köszönhető, és később a Google csapata Multi-Paxosnak nevezte el. Lamport Paxos-dolgozata 2012-ben elnyerte az ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award díját.

Az SMR és a Paxos vált a konszenzus és replikációs módszerek tervezésének és érvelésének de facto szabványos keretrendszerévé. Számos kritikus információs rendszert építő vállalat, köztük a Google, a Yahoo, a Microsoft és az Amazon is átvette a Paxos alapjait.

5. Programok formális specifikációja és verifikációja

A párhuzamossági elmélet kezdeti időszakában felmerült az igény jó eszközökre a megoldások leírására és helyességük bizonyítására. Lamport központi szerepet játszott az egyidejű programok specifikációjának és verifikációjának elméletében. Például ő fogalmazta meg elsőként a biztonsági tulajdonságok és az életképességi tulajdonságok fogalmát az aszinkron elosztott algoritmusok számára. Ezek a korábban szekvenciális programokra definiált “részleges helyesség” és “teljes helyesség” tulajdonságok általánosítását jelentették. Ma a biztonsági és az életképességi tulajdonságok alkotják az aszinkron elosztott algoritmusok helyességi tulajdonságainak standard osztályozását.

Egy másik munka, Martin Abadival , bevezetett egy speciális absztrakciót, az úgynevezett prófécia-változókat egy algoritmusmodellbe, hogy kezelje azt a helyzetet, amikor egy algoritmus egy nemdeterminisztikus választást előbb old meg, mint a specifikáció. Abadi és Lamport rámutatott azokra a helyzetekre, amikor ilyen problémák merülnek fel, és kidolgozta az elmélet e kiterjesztésének támogatásához szükséges elméletet. Továbbá bebizonyították, hogy amikor egy elosztott algoritmus találkozik egy specifikációval, ahol mindkettő állapotgépként van kifejezve, a kettő közötti megfelelés bizonyítható a propozíciós változók és korábbi fogalmak, például a történeti változók kombinációjával. Ez a munka elnyerte a 2008-as LICS Test-Of-Time díjat.

Formális modellezési nyelvek és verifikációs eszközök: A fenti alapfogalmak kidolgozása mellett Lamport kifejlesztette a TLA (Temporal Logic of Actions) nyelvet és a TLA+ eszközkészletet, elosztott algoritmusok és rendszerek modellezésére és verifikálására.

Lamport leírja a TLA-t és annak kapcsolatát a finomítási leképezéssel.

A TLA és a TLA+ támogatja mind a biztonsági, mind az életképességi tulajdonságok specifikációját és bizonyítását, temporális logikán alapuló jelölés segítségével. Lamport felügyelte a TLA+-on alapuló verifikációs eszközök fejlesztését, nevezetesen a Yuan Yu által épített TLC modellellenőrzőt. A TLA+-t és a TLC-t valós rendszerek leírására és elemzésére használták. Ezeket az eszközöket például arra használták, hogy megtalálják a Microsoft Xbox 360 hardverében használt koherenciaprotokoll súlyos hibáját a 2005-ös megjelenés előtt. Az Intelnél a Nehalem magprocesszorban megvalósított Intel Quick Path Interconnect cache-koherencia protokolljának elemzésére használták. Hogy megtanítsa a mérnököknek, hogyan használják a formális specifikációs eszközeit, Lamport írt egy könyvet . Nemrégiben Lamport kifejlesztette a PlusCAL formális nyelvet és eszközöket elosztott algoritmusok verifikálásához; ez a munka a TLA+-ra épül.

6. LaTeX

A hatásos dolgozatok ilyen hatalmas gyűjteményének létrehozásakor természetes, hogy kényelmes szedőeszközre vágyunk. Lamport nem csak kívánta, hanem megalkotta az egész közösség számára. A párhuzamosság területén kívül Lamport Latex rendszere , egy makrókészlet Donald Knuth TeX szövegszerkesztő rendszerével való használatra. A LaTeX három fontos dolgot adott hozzá a TeX-hez:

1. A “szedési környezet” fogalmát, amely Brian Reid Scribe rendszeréből származott.
2. A szerkezeti és nem a tipográfiai jelölés erős hangsúlyozása.
3. Egy általános dokumentumtervezés, amely elég rugalmas ahhoz, hogy sokféle dokumentumhoz megfelelő legyen.

Lamport nem ezeknek az ötleteknek az eredetije, de a lehető legmesszebbmenőkig kitolva őket, olyan rendszert hozott létre, amely a TeX minőségét és annak rugalmasságából sokat nyújt, de sokkal könnyebben használható. A Latex a számítástechnikában és sok más területen a műszaki publikálás de facto szabványává vált.

Leslie Lamportnak sok más fontos írása is van — túl sok ahhoz, hogy itt leírjuk. Ezek időrendi sorrendben vannak felsorolva Lamport honlapján , történeti jegyzetekkel kísérve, amelyek leírják az egyes eredmények motivációját és kontextusát.

Minden alkalommal, amikor hozzáférünk egy modern számítógéphez, valószínűleg hatással lesznek ránk Leslie Lamport algoritmusai. És mindez a munka azzal a törekvéssel kezdődött, hogy megértse, hogyan lehet megszervezni egy sorban állást egy helyi pékségben.

Author: Dahlia Malkhi
Kiegészítő közreműködők: Dahlia Malkhi
További közreműködők: Dahlia Malkhi
További közreműködők: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese és Len Shustek

.