Jos voisimme matkustaa ajassa taaksepäin vuoteen 1974, olisimme ehkä löytäneet Leslie Lamportin vilkkaasta paikallisesta leipomosta pohtimassa seuraavaa ongelmaa. Leipomossa oli useita kassatyöntekijöitä, mutta jos useampi kuin yksi henkilö lähestyi yhtä kassatyöntekijää samanaikaisesti, kassatyöntekijä yritti puhua kaikille yhtä aikaa ja meni sekaisin. Lamport tajusi, että oli oltava jokin tapa taata, että ihmiset lähestyivät kassoja yksi kerrallaan. Tämä ongelma toi Lamportille mieleen kysymyksen, jonka tietotekniikan tutkija Edsger Dijkstra oli esittänyt aiemmassa artikkelissaan toisesta arkipäiväisestä asiasta: miten ruokailuvälineet jaetaan ruokapöydässä. Yksi koordinoinnin haasteista oli taata, että kutakin ruokailuvälinettä käytti korkeintaan yksi ruokailija kerrallaan, mikä yleistyi vastavuoroisen poissulkemisen ongelmaksi (mutual exclusion problem), joka on juuri se haaste, jonka Lamport kohtasi leipomossa.

Eräänä aamuna vuonna 1974 Lamportille tuli ajatus siitä, miten leipomon asiakkaat voisivat ratkaista keskinäisen poissulkemisen keskenään turvautumatta leipomon apuun. Se toimi suunnilleen näin: ihmiset valitsevat numerot tullessaan leipomoon ja saavat sitten kassalla palvelua numerotilauksensa mukaisesti. Valitakseen numeron asiakas kysyy numeron kaikilta ympärillään olevilta ja valitsee numeron, joka on korkeampi kuin kaikkien muiden.

Tästä yksinkertaisesta ideasta tuli tyylikäs algoritmi keskinäisen poissulkemisen ongelman ratkaisemiseksi ilman, että tarvitaan mitään alemman tason jakamattomia operaatioita. Se oli myös runsas tulevien ideoiden lähde, koska monia kysymyksiä oli selvitettävä. Esimerkiksi joillakin leipomon asiakkailla kesti kauan tarkistaa muita numeroita, ja sillä välin saapui lisää asiakkaita, jotka valitsivat lisää numeroita. Toisella kerralla leipomon johtaja halusi saada tilannekuvan kaikista asiakasnumeroista, jotta hän voisi valmistaa riittävästi leivonnaisia. Lamport sanoi myöhemmin: ”Parin vuoden ajan sen jälkeen, kun löysin leipomoalgoritmin, kaikki, mitä opin samanaikaisuudesta, tuli sen tutkimisesta.”

Leipomoalgoritmista ja Lamportin muista uraauurtavista teoksista – joista monilla on huvittavia nimiä ja niihin liittyviä vertauksia – on tullut tietojenkäsittelytieteen tukipilareita. Hänen kokoelmansa muodostaa perustan samanaikaisuuden laajoille alueille, ja se on vaikuttanut samanaikaisten järjestelmien määrittelyyn, kehittämiseen ja verifiointiin.

Valmistuttuaan matematiikan tohtoriksi Brandeisin yliopistosta vuonna 1972 Lamport työskenteli tietojenkäsittelytieteilijänä Massachusetts Computer Associatesissa vuosina 1970-1977, SRI Internationalissa vuosina 1977-1985 ja Digital Equipment Corporation Systems Research Centerissä (jonka Compaq myöhemmin omisti) vuosina 1985-2001. Vuonna 2001 hän siirtyi Microsoft Researchin palvelukseen Mountain View’hen, Kaliforniaan.

Tutkijanuransa viettäminen teollisissa tutkimusympäristöissä ei ollut sattumaa. ”Pidän työskentelystä teollisessa tutkimuslaboratoriossa, koska siellä on panos”, Lamport sanoi. ”Jos työskentelisin vain yksin ja keksisin ongelmia, keksisin jonkin pienen määrän asioita, mutta jos menen ulos maailmaan, jossa ihmiset työskentelevät oikeiden tietokonejärjestelmien parissa, siellä on miljoona ongelmaa. Kun katson taaksepäin useimpia asioita, joiden parissa olen työskennellyt – Bysantin kenraalit, Paxos – ne ovat lähtöisin todellisista ongelmista.”

Hänen työnsä valaisivat rinnakkaisohjelmien peruskysymyksiä, joille ei tuolloin ollut olemassa muodollista teoriaa. Hän käsitteli peruskäsitteitä, kuten kausaalisuutta ja loogista aikaa, atomisia ja säännöllisiä jaettuja rekistereitä, sekventiaalista konsistenssia, tilakoneiden replikointia, Bysanttilaista sopimista ja odottelunvapautta. Hän työskenteli algoritmien parissa, joista on tullut vikasietoisten hajautettujen järjestelmien vakiokäytäntö. Hän on myös kehittänyt huomattavan määrän työtä samanaikaisten järjestelmien muodollisen määrittelyn ja verifioinnin alalla ja osallistunut näitä menetelmiä soveltavien automaattisten työkalujen kehittämiseen. Käsittelemme vain joitakin hänen panoksistaan.

1. Mutual Exclusion -ratkaisut ja Bakery-algoritmi

Lamportin vaikutusvaltaiset työt 1970- ja 1980-luvuilla syntyivät aikana, jolloin oli vain vähän ymmärrystä perustavanlaatuisista kysymyksistä, jotka koskivat ohjelmointia useille samanaikaisille prosessoreille.

Esimerkiksi tiedettiin, että oikeanlainen suoritus voi vaatia rinnakkaisten toimintojen poissulkemista toisistaan ”kriittisten osioiden” ajanjaksoina, jolloin ne manipuloivat samoja datatiedostoja, jotta estettäisiin operaatioiden ei-toivottu lomittuminen toistensa kanssa. Tämän keskinäisen poissulkemisen ongelman juuret ovat Edsger Dijkstran uraauurtavassa työssä, joka sisältää hänen ratkaisunsa. Vaikka Dijkstran algoritmi on oikea, se riippuu siitä, että jaetun muistin käyttö on atomaattista eli että prosessori, joka lukee, kun toinen kirjoittaa, joutuu odottamaan sen sijaan, että se palauttaisi mahdollisesti vääristyneen arvon. Tavallaan se rakentaa korkean tason ratkaisun matalan tason vastavuoroisesta poissulkemisesta, jonka laitteisto on jo toteuttanut.

Lamportin hämmästyttävän tyylikäs ja intuitiivinen ”Bakery Algorithm” ei tee niin. Hänen ratkaisunsa järjestää kilpailevat prosessit implisiittiseen jonoon niiden saapumisjärjestyksen mukaan, aivan kuten odotusjono leipomossa. Silti ei ole väliä, jos prosessori, joka lukee tietoja, joita toinen prosessori päivittää, saa roskaa. Algoritmi toimii silti.

Lamport muistelee löytäneensä Bakery-algoritmin.

Bakery-algoritmista on tullut oppikirjamateriaalia, ja useimmat tietojenkäsittelytieteen perustutkinto-opiskelijat törmäävät siihen opintojensa aikana.

2. Rinnakkaisohjelmoinnin perusteet

Bakeryn algoritmityöstä lähti useita tärkeitä uusia käsitteitä, mikä toistui Lamportin uran aikana useita kertoja. Kokemus rinnakkaisten algoritmien laatimisesta ja niiden oikeellisuuden todentamisesta sai hänet keskittymään niihin peruslähtökohtiin, jotka saisivat moniprosessorit käyttäytymään tavalla, josta ohjelmoijat voivat järkeillä matemaattisesti. Työskennellessään ratkaisun parissa tiettyyn konkreettiseen ongelmaan Lamport keksi abstraktioita ja yleisiä sääntöjä, joita tarvittiin sen oikeellisuuden päättelyyn, ja näistä käsitteellisistä panoksista tuli sitten rinnakkaisohjelmoinnin teoreettisia tukipilareita.

Silmukan vapaus: Leipurin algoritmityö esitteli tärkeän käsitteen nimeltä ”silmukanvapaus”. Jotkin ilmeiset ratkaisut, jotka tulevat mieleen keskinäisen poissulkemisen ongelmaan, määräävät ennalta `kierrokset’ kiertoon prosessien kesken. Tämä kuitenkin pakottaa prosessit odottamaan muita prosesseja, jotka ovat hitaita ja jotka eivät ole vielä edes saavuttaneet kiistakohtaa. Leipomoanalogiaa käyttäen se olisi kuin saapuisi tyhjään leipomoon ja joutuisi odottamaan asiakasta, joka ei ole vielä edes saapunut leipomoon. Silmukan vapaus sen sijaan ilmaisee prosessien kykyä edetä muiden prosessien nopeudesta riippumatta. Koska leipomoalgoritmi jakaa vuorot prosesseille niiden saapumisjärjestyksessä, se on silmukkavapaa. Tämä on keskeinen käsite, jota on käytetty monien myöhempien algoritmien suunnittelussa ja muistiarkkitehtuurien suunnittelussa. Odotusvapaus, ehto, joka edellyttää itsenäistä etenemistä epäonnistumisista huolimatta, juontaa juurensa silmukanvapauden käsitteeseen ja Bakery-käytävän käsitteeseen. Sitä ovat myöhemmin tutkineet laajasti muut, kuten Maurice Herlihy .

Sekventiaalinen johdonmukaisuus: Työskentely moniydinarkkitehtuurin kanssa, jossa oli hajautettua välimuistia, sai Lamportin luomaan muodolliset määrittelyt koherentille välimuistikäyttäytymiselle moniprosessorijärjestelmissä. Tämä työ toi järjestystä alan kaaokseen keksimällä sekventiaalisen johdonmukaisuuden , josta on tullut muistin johdonmukaisuusmallien kultainen standardi. Tämä yksinkertainen ja intuitiivinen käsite tarjoaa juuri oikean tason ”atomisuutta”, jotta ohjelmistot voivat toimia. Nykyään suunnittelemme laitteistojärjestelmiä, joissa on timestamp ordering tai partial-store ordering, johon on lisätty muistin aitaamiskäskyjä, joiden avulla ohjelmoijat voivat saada laitteiston näyttämään sekvenssikonsistentilta. Ohjelmoijat voivat sitten toteuttaa algoritmeja, jotka tarjoavat vahvat johdonmukaisuusominaisuudet. Tämä on avainasemassa Javan ja C++:n muistin johdonmukaisuusmalleissa. Moniydinprosessorimme toimivat nykyään Leslie Lamportin vuonna 1979 kuvaamien periaatteiden mukaisesti.

Atomiset ja säännölliset rekisterit: Bakery Algorithm sai Lamportin myös pohtimaan muistin tarkkaa semantiikkaa, kun useat prosessit vuorovaikutuksessa jakavat tietoja. Sen formalisointi kesti lähes vuosikymmenen, ja tuloksena on säännöllisten ja atomisten rekisterien abstraktio .

Hänen teoriansa antaa jokaiselle jaettuun rekisteriin kohdistuvalle operaatiolle eksplisiittisen keston, joka alkaa kutsusta ja päättyy tulokseen. Rekisterit voidaan toteuttaa erilaisilla tekniikoilla, kuten replikoinnilla. Prosessien vuorovaikutuksen atomirekisterin kanssa on kuitenkin tarkoitus ”näyttää” sarjakäynneiltä todelliseen jaettuun muistiin. Teoria sisältää myös heikompaa vuorovaikutuksen semantiikkaa, kuten tavallisessa rekisterissä. Säännöllinen rekisteri kuvaa tilanteita, joissa prosessit lukevat rekisterin eri kopioita, kun rekisteriä päivitetään. Millä tahansa hetkellä jotkin replikaatiot voivat olla päivitettyinä, kun taas toiset eivät, ja lopulta kaikilla replikaatioilla on päivitetty arvo. Tärkeää on, että nämä heikommat semantiikat riittävät tukemaan keskinäistä poissulkemista: Bakery-algoritmi toimii oikein, jos kirjoittajan päällekkäin oleva lukija saa takaisin minkä tahansa mielivaltaisen arvon.

Lamport kuvailee työtään, jonka avulla hän pyrkii määrittelemään täsmällisesti abstraktiot atomaarisille, säännönmukaisille ja turvallisille rekistereille.

Tämä työ aloitti erillisen hajautetun tietojenkäsittelyn tutkimuskohteen, joka kukoistaa edelleen. Lamportin atomiobjektit tukivat vain luku- ja kirjoitusoperaatioita, eli ne olivat atomirekistereitä. Maurice Herlihy ja Jeannette Wing yleistivät käsitteen muihin tietotyyppeihin, ja heidän termistään ”linearisoituvuus” tuli atomisuuden synonyymi. Nykyään käytännössä kaikki ei-relationaaliset tallennusjärjestelmät, joita Amazonin, Googlen ja Facebookin kaltaiset yritykset ovat kehittäneet, käyttävät linearisoituvuutta ja sekventiaalista johdonmukaisuutta tietojensa yhtenäisyystakuita varten.

3. Hajautettujen järjestelmien perusteet

Erikoistyyppinen rinnakkaisjärjestelmä on hajautettu järjestelmä, jolle on ominaista, että siinä on prosesseja, jotka käyttävät viestejä vuorovaikutukseen toistensa kanssa. Leslie Lamportilla on ollut valtava vaikutus tapaan, jolla ajattelemme hajautetuista järjestelmistä, sekä alan suunnittelukäytäntöihin.

Logiikan kellot: Monet tajusivat, että globaali aikakäsitys ei ole luonteva hajautetussa järjestelmässä. Lamport oli ensimmäinen, joka täsmensi vaihtoehtoisen käsitteen ”loogiset kellot”, jotka asettavat tapahtumille osittaisen järjestyksen, joka perustuu kausaalisuhteeseen, joka syntyy lähettämällä viestejä järjestelmän yhdestä osasta toiseen . Hänen artikkelistaan ”Time, Clocks, and the Ordering of Events in a Distributed System” (Aika, kellot ja tapahtumien järjestys hajautetussa järjestelmässä) on tullut Lamportin teoksista eniten siteerattu, ja tietojenkäsittelytieteen kielenkäytössä loogisia kelloja kutsutaan usein nimellä Lamportin aikaleimat. Hänen artikkelinsa voitti vuonna 2000 Principles of Distributed Computing -konferenssin Influential Paper Award -palkinnon (joka myöhemmin nimettiin uudelleen Edsger W. Dijkstra Prize in Distributed Computing -palkinnoksi), ja se voitti ACM SIGOPS Hall of Fame -palkinnon vuonna 2007.

Lamport kuvailee artikkeliaan ”Time, Clocks…” ja sen suhdetta suhteellisuusteoriaan.

Ymmärtääksesi, miksi tuosta työstä tuli niin vaikutusvaltainen, tunnusta, että keksinnön aikaan ei ollut mitään hyvää tapaa kuvata tiedonsiirtoviivettä hajautetuissa järjestelmissä muuten kuin käyttämällä reaaliaikaa. Lamport tajusi, että kommunikaatioviive teki näistä järjestelmistä hyvin erilaisia kuin jaetun muistin moniprosessorijärjestelmistä. Oivallus tuli, kun hän luki replikoituja tietokantoja käsittelevää artikkelia ja tajusi, että sen käskyjen looginen järjestys saattoi rikkoa kausaalisuutta.

Tapahtumien järjestyksen käyttäminen tapana todistaa järjestelmän oikeellisuus on enimmäkseen sitä, mitä nykyään tehdään rinnakkaisten synkronointialgoritmien intuitiivisiin todistuksiin. Toinen tämän työn voimakas kontribuutio oli sen osoittaminen, miten tilakonetta voidaan replikoida loogisten kellojen avulla, mikä selitetään jäljempänä.

Distributed Snapshots: Kun kausaalijärjestys on määritelty, siitä seuraa luonnollisesti käsite johdonmukaiset globaalitilat. Tämä johti toiseen oivaltavaan työhön. Lamport ja Mani Chandy keksivät ensimmäisen algoritmin mielivaltaisen hajautetun järjestelmän tilan lukemiseen (tilannekuvan ottamiseen) . Tämä on niin voimakas käsite, että muut käyttivät sitä myöhemmin eri aloilla, kuten verkottumisessa, itsestabiloinnissa, virheenkorjauksessa ja hajautetuissa järjestelmissä. Tämä artikkeli sai vuonna 2013 ACM SIGOPS Hall of Fame -palkinnon.

4. Vikasietoisuus ja tilakoneiden replikointi

”Hajotettu järjestelmä on sellainen, jossa sellaisen tietokoneen vikaantuminen, jonka olemassaolosta et edes tiennyt, voi tehdä oman tietokoneesi käyttökelvottomaksi” on kuuluisa Lamportin sutkaus. Suuri osa hänen työstään koskee vikasietoisuutta.

State Machine Replication (SMR): Se esiteltiin kuuluisassa artikkelissa ”Time, Clocks, and the Ordering of Events in a Distributed System”, ja sitä kehitettiin edelleen pian sen jälkeen. Tämä abstraktio kuvaa minkä tahansa palvelun keskitettynä tilakoneena – eräänlaisena universaalina laskentakoneena, joka muistuttaa Turingin konetta. Sillä on sisäinen tila, ja se käsittelee käskyjä peräkkäin, joista jokainen johtaa uuteen sisäiseen tilaan ja tuottaa vastauksen. Lamport oivalsi, että pelottava tehtävä palvelun replikoimisesta useille tietokoneille voidaan tehdä huomattavan yksinkertaiseksi, jos kaikille replikaattoreille esitetään sama tulokäskyjen sarja ja ne käyvät läpi identtisen tilojen peräkkäisyyden.

Tämä oivaltava SMR-paradigma on monien luotettavien järjestelmien perustana, ja sitä pidetään tyylikkyytensä vuoksi vakiolähestymistapana replikoitujen hajautettujen järjestelmien rakentamisessa. Mutta ennen kuin Lamport kehitti SMR:n avulla täydellisen ratkaisun, hänen oli käsiteltävä keskeistä ainesosaa, sopimusta, jota hän käsitteli seuraavassa teoksessaan.

Byzantine Agreement: Vaikka tilakoneisiin perustuvat lähestymistavat, jotka kestävät törmäysvirheitä, riittävät moniin sovelluksiin, tehtäväkriittisemmät järjestelmät, kuten ilmailutekniikka, tarvitsevat vielä äärimmäisemmän vikasietoisuuden mallin, joka on läpäisemätön solmuille, jotka saattavat häiritä järjestelmää sen sisältä käsin.

Stanfordin tutkimuslaitoksessa (myöhemmin SRI International) 1970-luvulla Lamport kuului ryhmään, joka auttoi NASA:ta suunnittelemaan vankan avioniikan ohjausjärjestelmän. Muodolliset takeet olivat ehdoton välttämättömyys tehtävän kriittisen luonteen vuoksi. Turvallisuus oli taattava kaikkein äärimmäisimpiä kuviteltavissa olevia järjestelmähäiriöitä vastaan. Yksi ensimmäisistä haasteista, joihin SRI:n tiimiä pyydettiin vastaamaan, oli todistaa NASA:n suunnitteleman ohjaamon ohjausjärjestelmän oikeellisuus kolmella tietokonejärjestelmällä, jotka käyttävät enemmistöäänestystä peittääkseen kaikki vialliset komponentit.

Työryhmän työn tuloksena saatiin useita perustavanlaatuisia käsitteitä ja oivalluksia, jotka koskivat näitä tiukkoja robustien järjestelmien tyyppejä. Siihen sisältyi robustiuden perustavanlaatuinen määritelmä tässä ympäristössä, koordinaatio-ongelman abstraktio, joka on kaikkien toistettujen järjestelmien perustana tähän mennessä, ja yllättävä paljastus, että järjestelmät, joissa on kolme tietokonetta, eivät koskaan voi turvallisesti käyttää operaatiokriittistä ohjaamoa!

Kahdessa perimmäisessä teoksessa (”LPS”), jotka julkaistiin yhdessä Peasen ja Shostakin kanssa , tiimi havaitsi ensimmäisenä hieman erikoisen haavoittuvuuden. LPS esitti, että ”vikaantunut komponentti voi osoittaa sellaista käyttäytymistä, joka jätetään usein huomiotta – nimittäin ristiriitaisten tietojen lähettämistä järjestelmän eri osiin”. Yleisemmin sanottuna vikaantunut komponentti saattoi toimia tavalla, joka oli täysin ristiriidassa sille määrätyn käyttäytymisen kanssa, ja se saattoi vaikuttaa lähes pahantahtoiselta.

Uusi vikamalli tarvitsi nimen. Siihen aikaan oli olemassa siihen liittyvä klassinen haaste kahden kommunikoivan tietokoneen koordinoinnista, joka esiteltiin vuonna 1975 julkaistussa artikkelissa ja johon Jim Gray viittasi vuonna ”The Two Generals Paradox ”. Tämä sai Lamportin ajattelemaan ohjaamon ohjaustietokoneita Bysantin kenraalien armeijana, jossa armeija yrittää muodostaa koordinoidun hyökkäyksen, kun taas sisällä olevat petturit lähettävät ristiriitaisia signaaleja. Tälle vikamallille otettiin käyttöön nimi ”Byzantine Failures”, ja sitä seurasi akateemisen työn tulva. Bysantin vikamalli on edelleen käytössä, kun halutaan kuvata järjestelmissä esiintyviä pahimpia vahinkoja ja tietoturva-aukkoja.

Lamport selittää käyttäneensä ”Bysantin kenraaleista” kertovaa tarinaa kehystääkseen ongelmaa vikasietoisissa hajautetuissa järjestelmissä.

Byzantin vikaantumiset (Byzantin vikaantumiset)

Byzantin vikaantumiset (Byzantin vikaantumiset)

Analysoi pahoja asioita, jotka voivat tapahtua. Mutta entä ne hyvät asiat, joiden on tapahduttava? LPS antoi myös abstraktin muotoilun ongelmasta, joka koskee koordinaation saavuttamista Bysantin vioista huolimatta; tämä tunnetaan nimellä ”Bysantin sopimuksen” ongelma. Tämä ytimekäs muotoilu ilmaisee ohjauksen koordinointitehtävän ongelmana, joka koskee sopimuspäätöksen tekemistä yksittäiselle bitille, kun lähtökohtana ovat mahdollisesti erilaiset bitit, jotka syötetään kuhunkin komponenttiin. Kun on päästy yhteisymmärrykseen yksittäisestä bitistä, sitä on mahdollista käyttää toistuvasti koko monimutkaisen järjestelmän koordinoinnin ylläpitämiseksi. Artikkelissa osoitetaan, että tarvitaan neljä tietokonetta muodostamaan yhteisymmärrys yhdestä bitistä yksittäisen toimintahäiriön sattuessa. Kolme ei riitä, koska kolmella yksiköllä vikaantunut yksikkö voi lähettää ristiriitaisia arvoja kahdelle muulle yksikölle ja muodostaa eri enemmistön jokaisen yksikön kanssa. Yleisemmin he osoittivat, että tarvitaan 3F+1 yksikköä, jotta voidaan voittaa F samanaikaisesti vialliset komponentit. Todistaakseen tämän he käyttivät kaunista symmetria-argumenttia, joka on tullut tunnetuksi nimellä ”kuusikulmioargumentti”. Tämä arkkityyppinen argumentti on löytänyt muitakin käyttökohteita aina, kun väitetään, että toimintahäiriöinen yksikkö, joka lähettää ristiriitaista tietoa järjestelmän eri osiin, näyttää erottamattomalta symmetrisestä tilanteesta, jossa oikeat ja vialliset roolit ovat päinvastaiset.

LPS osoitti myös, että 3F+1 yksikköä riittää, ja he esittelivät ratkaisun, jolla voidaan saavuttaa bysanttilainen yhteisymmärrys (Byzantine Agreement) 3F+1:n yksikön kesken F+1:ssä synkronisessa kommunikaatiokierroksessa. He osoittivat myös, että jos käytetään digitaalisia allekirjoituksia, vain 2F+1 yksikköä on riittävä ja tarpeellinen.

Bysantin sopimuksen ongelmasta ja sen ratkaisuista on tullut vikasietoisten järjestelmien tunnusmerkki. Useimmat redundanssilla rakennetut järjestelmät hyödyntävät sitä sisäisesti replikointiin ja koordinointiin. Lamport itse käytti sitä myöhemmin muodostaessaan seuraavaksi käsiteltävän tilakoneiden replikointiparadigman, joka antaa replikoinnille algoritmisen perustan.

Vuoden 1980 paperille myönnettiin vuoden 2005 Edsger W. Dijkstra -palkinto hajautetun tietojenkäsittelyn alalta ja vuoden 1982 paperille Jean-Claude Laprie -palkinto luotettavan tietojenkäsittelyn alalta.

Paxos: Kun ymmärrys hajautetun tietojenkäsittelyn sopimusongelmasta kasvoi, Lamportin oli aika palata takaisin tilakoneiden replikointiin ja puuttua vikoihin siellä. Ensimmäisessä SMR-ratkaisussa, jonka hän esitteli vuonna 1978 julkaistussa artikkelissaan, oletettiin, että vikoja ei ole, ja siinä käytetään loogista aikaa, jotta replikaatiot kävisivät läpi saman komentosarjan. Vuonna 1989 Lamport suunnitteli vikasietoisen algoritmin nimeltä Paxos . Lamport jatkoi humoristista vertauskertomustaan ja esitti kuvitteellisen tarinan Paxos-nimisellä muinaiskreikkalaisella saarella sijaitsevasta hallituksen parlamentista, jossa voidaan sietää minkä tahansa jäsenmäärän tai mahdollisesti kaikkien jäsenten poissaoloa ilman, että johdonmukaisuus heikkenee.

Lamport kuvaa Paxos-algoritminsa alkuperää vikasietoiselle hajautetulle tietojenkäsittelylle.

Valitettavasti asetelma kreikkalaisena vertauskuvana teki paperista vaikeasti ymmärrettävän useimmille lukijoille, ja paperin jättämisestä julkaisuun vuonna 1998 kului yhdeksän vuotta. DEC:n tekninen raportti vuodelta 1989 sai kuitenkin huomiota. Lamportin kollega Butler Lampson evankelioi ajatusta hajautetun tietojenkäsittelyn yhteisölle . Pian Paxosin julkaisemisen jälkeen Googlen Chubby-järjestelmä ja Apachen avoimen lähdekoodin ZooKeeper tarjosivat tilakoneiden replikointia ulkoisena, laajalti käytössä olevana palveluna.

Paxos nivoo peräkkäiset sopimuspäätökset optimoidusti yhteen tilakoneiden komentojen sarjaksi. Tärkeää on, että Paxos-paperissa esitetyn sopimuskomponentin ensimmäinen vaihe (nimeltään Synod) voidaan välttää, kun sama johtaja johtaa useita päätöksiä; tämä vaihe on suoritettava vain silloin, kun johtaja on vaihdettava. Tämä oivaltava läpimurto selittää suuren osan Paxosin suosiosta, ja Googlen tiimi kutsui sitä myöhemmin nimellä Multi-Paxos . Lamportin Paxos-paperi voitti ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame -palkinnon vuonna 2012.

SMR:stä ja Paxosista on tullut de facto standardikehys konsensus- ja replikointimenetelmien suunnitteluun ja päättelyyn. Monet kriittisiä tietojärjestelmiä rakentavat yritykset, kuten Google, Yahoo, Microsoft ja Amazon, ovat omaksuneet Paxosin perusteet.

5. Ohjelmien muodollinen spesifiointi ja verifiointi

Rinnakkaisteorian alkuaikoina ilmaantui tarve hyville työkaluille ratkaisujen kuvaamiseen ja niiden oikeellisuuden todistamiseen. Lamport on antanut keskeisen panoksen samanaikaisten ohjelmien spesifioinnin ja verifioinnin teoriaan. Hän esimerkiksi artikuloi ensimmäisenä asynkronisten hajautettujen algoritmien turvallisuusominaisuuksien ja elävyysominaisuuksien käsitteet. Nämä olivat aiemmin sekventiaalisille ohjelmille määriteltyjen ”osittaisen oikeellisuuden” ja ”täydellisen oikeellisuuden” ominaisuuksien yleistyksiä. Nykyään turvallisuus- ja elinvoimaisuusominaisuudet muodostavat vakioluokituksen asynkronisten hajautettujen algoritmien oikeellisuusominaisuuksille.

Toisessa yhdessä Martin Abadin kanssa tehdyssä työssä otettiin algoritmimalliin käyttöön erityinen abstraktio, jota kutsutaan ennustemuuttujiksi, jotta voidaan käsitellä tilannetta, jossa algoritmi ratkaisee epädeterministisen valinnan ennen kuin määrittely tekee sen. Abadi ja Lamport osoittivat tilanteita, joissa tällaisia ongelmia esiintyy, ja kehittivät teoriaa, jota tarvitaan tämän teorian laajennuksen tukemiseksi. Lisäksi he osoittivat, että aina kun hajautettu algoritmi kohtaa spesifikaation, jossa molemmat ilmaistaan tilakoneina, niiden välinen vastaavuus voidaan todistaa käyttämällä yhdistelmää ennustemuuttujista ja aiemmista käsitteistä, kuten historiamuuttujista. Tämä työ voitti vuoden 2008 LICS Test-Of-Time -palkinnon.

Formal Modeling Languages and Verification Tools: Edellä mainittujen peruskäsitteiden kehittämisen lisäksi Lamport on kehittänyt kielen TLA (Temporal Logic of Actions) ja TLA+-työkalupaketin hajautettujen algoritmien ja järjestelmien mallintamiseen ja verifiointiin.

Lamport kuvailee TLA:ta ja sen yhteyttä hienosäätökartoitukseen.

TLA ja TLA+ tukevat sekä turvallisuus- että elinvoimaisuusominaisuuksien spesifikaatioita ja todentamisia temporaalilogiikkalogiikkaan pohjautuvalla notaatiolla. Lamport on valvonut TLA+:aan perustuvien verifiointityökalujen kehittämistä, erityisesti Yuan Yun rakentaman TLC-mallin tarkistusohjelman. TLA+:a ja TLC:tä on käytetty todellisten järjestelmien kuvaamiseen ja analysointiin. Näitä työkaluja käytettiin esimerkiksi Microsoftin Xbox 360:n laitteistossa käytetyn koherenssiprotokollan merkittävän virheen löytämiseen ennen sen julkaisua vuonna 2005. Intelillä niitä käytettiin Nehalem-ydinprosessorissa toteutetun Intel Quick Path Interconnectin välimuistin koherenssiprotokollan analysointiin. Opettaakseen insinöörejä käyttämään formaaleja määrittelytyökalujaan Lamport on kirjoittanut kirjan . Viime aikoina Lamport on kehittänyt PlusCAL-formaalisen kielen ja työkalut käytettäväksi hajautettujen algoritmien verifioinnissa; tämä työ perustuu TLA+:aan.

6. LaTeX

Kun luodaan näin laaja kokoelma vaikuttavia artikkeleita, on luonnollista toivoa kätevää kirjasintekotyökalua. Lamport ei vain toivonut sellaista, hän loi sellaisen koko yhteisölle. Rinnakkaisalan ulkopuolella on Lamportin Latex-järjestelmä , joukko makroja käytettäväksi Donald Knuthin TeX-kirjoitusjärjestelmän kanssa. LaTeX lisäsi TeX:iin kolme tärkeää asiaa:

1. Käsitteen ’kirjoitusympäristö’, joka oli peräisin Brian Reidin Scribe-järjestelmästä.
2. Suuren painotuksen rakenteelliseen eikä typografiseen merkkaukseen.
3. Yleinen dokumenttisuunnittelu, joka on tarpeeksi joustava, jotta se soveltuu monenlaisiin dokumentteihin.

Lamport ei ollut näiden ideoiden alullepanija, mutta viemällä niitä mahdollisimman pitkälle hän loi järjestelmän, joka tarjoaa TeX:n laadun ja suuren osan sen joustavuudesta, mutta on paljon helpompi käyttää. Latexista tuli de facto standardi tekniselle julkaisemiselle tietojenkäsittelytieteessä ja monilla muilla aloilla.

Leslie Lamportilta on monia muitakin tärkeitä artikkeleita — liian monia kuvailtavaksi tässä. Ne on lueteltu aikajärjestyksessä Lamportin kotisivulla , ja niihin liittyy historiallisia huomautuksia, joissa kuvataan kunkin tuloksen motivaatio ja konteksti.

Aina kun käytät nykyaikaista tietokonetta, Leslie Lamportin algoritmit todennäköisesti vaikuttavat sinuun. Ja kaikki tämä työ alkoi pyrkimyksestä ymmärtää, miten järjestää jono paikallisessa leipomossa.

Tekijä: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese ja Len Shustek

.