Se potessimo viaggiare indietro nel tempo al 1974, forse avremmo trovato Leslie Lamport nella sua affollata panetteria di quartiere, alle prese con il seguente problema. La panetteria aveva diversi cassieri, ma se più di una persona si avvicinava ad un singolo cassiere allo stesso tempo, il cassiere cercava di parlare con tutti contemporaneamente e si confondeva. Lamport si rese conto che ci doveva essere un modo per garantire che le persone si avvicinassero ai cassieri uno alla volta. Questo problema ha ricordato a Lamport un problema che è stato posto in un precedente articolo dell’informatico Edsger Dijkstra su un altro problema banale: come condividere gli utensili da cena intorno ad un tavolo da pranzo. Una delle sfide di coordinazione era di garantire che ogni utensile fosse usato da un solo commensale alla volta, il che è stato generalizzato come il problema dell’esclusione reciproca, esattamente la sfida che Lamport ha affrontato nella panetteria.

Una mattina del 1974, a Lamport venne un’idea su come i clienti della panetteria potessero risolvere l’esclusione reciproca tra di loro, senza fare affidamento sull’aiuto della panetteria. Funzionava più o meno così: le persone scelgono dei numeri quando entrano nella panetteria, e poi vengono servite alla cassa in base al numero che hanno ordinato. Per scegliere un numero, una cliente chiede il numero di tutti quelli che la circondano e sceglie un numero più alto di tutti gli altri.

Questa semplice idea divenne un elegante algoritmo per risolvere il problema della mutua esclusione senza richiedere alcuna operazione indivisibile di livello inferiore. Fu anche una ricca fonte di idee future, poiché molti problemi dovevano essere risolti. Per esempio, alcuni clienti della panetteria impiegavano molto tempo per controllare altri numeri, e nel frattempo arrivavano altri clienti e selezionavano altri numeri. Un’altra volta, il direttore della panetteria voleva avere un’istantanea di tutti i numeri dei clienti per preparare abbastanza pasticcini. Lamport disse in seguito: “Per un paio d’anni dopo la mia scoperta dell’algoritmo della panetteria, tutto ciò che ho imparato sulla concorrenza è venuto dallo studio di questo algoritmo”.

L’algoritmo della panetteria e gli altri lavori pionieristici di Lamport — molti con nomi divertenti e parabole associate — sono diventati pilastri dell’informatica. La sua collezione costituisce la base di ampie aree di concorrenza, e ha influenzato la specifica, lo sviluppo e la verifica dei sistemi concorrenti.

Dopo essersi laureato con un dottorato in matematica alla Brandeis University nel 1972, Lamport ha lavorato come informatico alla Massachusetts Computer Associates dal 1970 al 1977, alla SRI International dal 1977 al 1985, e al Digital Equipment Corporation Systems Research Center (poi di proprietà della Compaq) dal 1985 al 2001. Nel 2001 è entrato in Microsoft Research a Mountain View, California.

Spendere la sua carriera di ricerca in ambienti di ricerca industriale non è stato un caso. “Mi piace lavorare in un laboratorio di ricerca industriale, a causa degli input”, ha detto Lamport. “Se lavorassi da solo e mi venissero in mente dei problemi, mi verrebbe in mente un piccolo numero di cose, ma se vado fuori nel mondo, dove la gente sta lavorando su sistemi informatici reali, ci sono un milione di problemi là fuori. Quando guardo indietro alla maggior parte delle cose su cui ho lavorato -yzantine generals, Paxos- provengono da problemi del mondo reale”.

I suoi lavori hanno fatto luce su questioni fondamentali dei programmi concorrenti, per i quali non esisteva una teoria formale all’epoca. Ha affrontato concetti fondamentali come la causalità e il tempo logico, i registri condivisi atomici e regolari, la coerenza sequenziale, la replica delle macchine a stati, l’accordo bizantino e la libertà di attesa. Ha lavorato su algoritmi che sono diventati una pratica ingegneristica standard per i sistemi distribuiti tolleranti agli errori. Ha anche sviluppato un corpo sostanziale di lavoro sulla specifica formale e la verifica dei sistemi concorrenti, e ha contribuito allo sviluppo di strumenti automatici che applicano questi metodi. Toccheremo solo alcuni dei suoi contributi.

1. Soluzioni di mutua esclusione e l’algoritmo Bakery

Le influenti opere di Lamport degli anni ’70 e ’80 sono arrivate in un momento in cui c’era solo una piccola comprensione delle questioni fondamentali sulla programmazione per più processori concorrenti.

Per esempio, si sapeva che la corretta esecuzione può richiedere che le attività parallele si escludano a vicenda durante i periodi in “sezioni critiche” quando manipolano gli stessi dati, al fine di prevenire un indesiderato interleaving di operazioni. Le origini di questo problema di esclusione reciproca provengono dal lavoro pionieristico di Edsger Dijkstra, che include la sua soluzione. L’algoritmo di Dijkstra, sebbene corretto, dipende dal fatto che gli accessi alla memoria condivisa siano atomici – che un processore che legge quando un altro sta scrivendo sarà fatto aspettare, piuttosto che restituire un valore possibilmente confuso. In un certo senso, costruisce una soluzione di alto livello sulla mutua esclusione di basso livello già implementata dall’hardware.

Il “Bakery Algorithm” di Lamport, notevolmente elegante e intuitivo, non lo fa. La sua soluzione organizza i processi contendenti in una coda implicita secondo il loro ordine di arrivo, proprio come una coda di attesa in una panetteria. Eppure non importa se un processore che legge dati che vengono aggiornati da un altro processore ottiene spazzatura. L’algoritmo funziona ancora.

Lamport ricorda la sua scoperta dell’algoritmo Bakery.

L’algoritmo Bakery è diventato materiale da manuale, e la maggior parte dei laureandi in informatica lo incontrano nel corso dei loro studi.

2. Fondamenti della programmazione concorrente

Dal lavoro sull’algoritmo Bakery sono scaturiti diversi nuovi concetti importanti, una tendenza che si è ripetuta più volte nella carriera di Lamport. L’esperienza di ideare algoritmi concorrenti e verificarne la correttezza lo portò a concentrarsi sui fondamenti di base che avrebbero fatto sì che i multiprocessori si comportassero in un modo su cui i programmatori potessero ragionare matematicamente. Mentre lavorava ad una soluzione per uno specifico problema concreto, Lamport inventò astrazioni e regole generali necessarie per ragionare sulla sua correttezza, e questi contributi concettuali divennero poi pilastri teorici della programmazione concorrente.

Loop-freedom: Il lavoro sull’algoritmo Bakery ha introdotto un concetto importante chiamato “libertà di loop”. Alcune soluzioni ovvie che vengono in mente per il problema dell’esclusione reciproca pre-assegnano `giri’ a rotazione tra i processi. Ma questo costringe i processi ad aspettare altri che sono lenti e non hanno ancora raggiunto il punto di contesa. Usando l’analogia della panetteria, sarebbe come arrivare in una panetteria vuota ed essere invitati ad aspettare un cliente che non è ancora arrivato in panetteria. Al contrario, la libertà del ciclo esprime la capacità dei processi di fare progressi indipendentemente dalla velocità degli altri processi. Poiché l’algoritmo della panetteria assegna i turni ai processi nell’ordine del loro arrivo, ha la libertà di loop. Questo è un concetto cruciale che è stato utilizzato nella progettazione di molti algoritmi successivi, e nella progettazione di architetture di memoria. Wait-freedom, una condizione che richiede un progresso indipendente nonostante i fallimenti, ha le sue chiare radici nella nozione di loop-freedom e nel concetto di Bakery doorway. È stato poi ampiamente esplorato da altri, tra cui Maurice Herlihy.

Consistenza sequenziale: Lavorare con un’architettura multi-core che aveva una memoria cache distribuita ha portato Lamport a creare specifiche formali per il comportamento coerente della cache nei sistemi multiprocessore. Quel lavoro ha portato un po’ di ordine nel caos di questo campo inventando la coerenza sequenziale, che è diventata il gold standard per i modelli di coerenza della memoria. Questa nozione semplice e intuitiva fornisce il giusto livello di “atomicità” per permettere al software di funzionare. Oggi progettiamo sistemi hardware con l’ordinamento timestamp o l’ordinamento partial-store, con l’aggiunta di istruzioni di recinzione della memoria, che permette ai programmatori di far apparire l’hardware coerente in modo sequenziale. I programmatori possono quindi implementare algoritmi che forniscono forti proprietà di coerenza. Questa è la chiave per i modelli di coerenza della memoria di Java e C++. I nostri processori multicore funzionano oggi sulla base dei principi descritti da Leslie Lamport nel 1979.

Registri atomici e regolari: L’algoritmo Bakery ha anche portato Lamport a interrogarsi sulla semantica precisa della memoria quando più processi interagiscono per condividere dati. Ci volle quasi un decennio per formalizzarla, e il risultato è l’astrazione dei registri regolari e atomici.

La sua teoria dà ad ogni operazione su un registro condiviso una durata esplicita, iniziando con una invocazione e finendo con un risultato. I registri possono essere implementati con una varietà di tecniche, come la replica. Tuttavia, si suppone che le interazioni dei processi con un registro atomico “assomiglino” ad accessi seriali alla memoria condivisa reale. La teoria include anche semantiche di interazione più deboli, come quelle di un registro regolare. Un registro regolare cattura situazioni in cui i processi leggono diverse repliche del registro mentre viene aggiornato. In qualsiasi momento, alcune repliche possono essere aggiornate mentre altre no, e alla fine, tutte le repliche terranno il valore aggiornato. È importante notare che questa semantica debole è sufficiente per supportare la mutua esclusione: l’algoritmo Bakery funziona correttamente se un lettore che si sovrappone a uno scrittore ottiene indietro qualsiasi valore arbitrario.

Lamport descrive il suo lavoro per definire con precisione le astrazioni per i registri atomici, regolari e sicuri.

Questo lavoro ha iniziato un sottocampo distinto di ricerca nel calcolo distribuito che è ancora fiorente. Gli oggetti atomici di Lamport supportavano solo operazioni di lettura e scrittura, cioè erano registri atomici. La nozione fu generalizzata ad altri tipi di dati da Maurice Herlihy e Jeannette Wing, e il loro termine “linearizzabilità” divenne sinonimo di atomicità. Oggi, essenzialmente tutti i sistemi di archiviazione non relazionali sviluppati da aziende come Amazon, Google e Facebook adottano la linearizzabilità e la coerenza sequenziale per le loro garanzie di coerenza dei dati.

3. Fondamenti dei sistemi distribuiti

Un tipo speciale di sistema concorrente è un sistema distribuito, caratterizzato dall’avere processi che usano messaggi per interagire tra loro. Leslie Lamport ha avuto un enorme impatto sul modo in cui pensiamo al sistema distribuito, così come sulle pratiche di ingegneria del campo.

Gli orologi logici: Molte persone hanno capito che una nozione globale di tempo non è naturale per un sistema distribuito. Lamport fu il primo a precisare una nozione alternativa di “orologi logici”, che impongono un ordine parziale agli eventi basato sulla relazione causale indotta dall’invio di messaggi da una parte all’altra del sistema. Il suo articolo su “Time, Clocks, and the Ordering of Events in a Distributed System” è diventato il più citato dei lavori di Lamport, e nel linguaggio informatico gli orologi logici sono spesso soprannominati Lamport timestamps. Il suo articolo ha vinto il Principles of Distributed Computing Conference Influential Paper Award nel 2000 (successivamente rinominato Edsger W. Dijkstra Prize in Distributed Computing), e ha vinto un ACM SIGOPS Hall of Fame Award nel 2007.

Lamport descrive il suo articolo “Time, Clocks…” e la sua relazione con la relatività speciale.

Per capire perché quel lavoro è diventato così influente, bisogna riconoscere che all’epoca dell’invenzione non c’era un buon modo per catturare il ritardo di comunicazione nei sistemi distribuiti se non usando il tempo reale. Lamport si rese conto che il ritardo di comunicazione rendeva quei sistemi molto diversi da un sistema multiprocessore a memoria condivisa. L’intuizione venne quando lesse un articolo sui database replicati e si rese conto che il suo ordinamento logico dei comandi poteva violare la causalità.

Utilizzare l’ordinamento degli eventi come un modo per dimostrare la correttezza del sistema è per lo più ciò che si fa oggi per le prove intuitive degli algoritmi di sincronizzazione simultanea. Un altro potente contributo di questo lavoro è stato quello di dimostrare come replicare una macchina a stati usando orologi logici, che è spiegato di seguito.

Schede distribuite: Una volta definito l’ordine causale, la nozione di stati globali coerenti segue naturalmente. Questo ha portato ad un altro lavoro perspicace. Lamport e Mani Chandy hanno inventato il primo algoritmo per leggere lo stato (prendere un `snapshot’) di un sistema distribuito arbitrario. Questa è una nozione così potente che altri l’hanno poi usata in diversi domini, come il networking, l’auto-stabilizzazione, il debug e i sistemi distribuiti. Questo articolo ha ricevuto il 2013 ACM SIGOPS Hall of Fame Award.

4. Tolleranza ai guasti e replica delle macchine di stato

“Un sistema distribuito è un sistema in cui il fallimento di un computer che non sapevi nemmeno esistesse può rendere il tuo computer inutilizzabile” è una famosa battuta di Lamport. Gran parte del suo lavoro riguarda la tolleranza agli errori.

State Machine Replication (SMR): Forse il più significativo dei molti contributi di Lamport è il paradigma State Machine Replication, che è stato introdotto nel famoso documento su “Time, Clocks, and the Ordering of Events in a Distributed System”, e ulteriormente sviluppato subito dopo. L’astrazione cattura qualsiasi servizio come una macchina a stati centralizzata — una specie di motore di calcolo universale simile ad una macchina di Turing. Ha uno stato interno, ed elabora comandi in sequenza, ognuno dei quali risulta in un nuovo stato interno e produce una risposta. Lamport si rese conto che l’arduo compito di replicare un servizio su più computer può essere reso notevolmente semplice se si presenta la stessa sequenza di comandi in ingresso a tutte le repliche e queste procedono attraverso una identica successione di stati.

Questo perspicace paradigma SMR è alla base di molti sistemi affidabili, ed è considerato un approccio standard per la costruzione di sistemi distribuiti replicati grazie alla sua eleganza. Ma prima che Lamport sviluppasse una soluzione completa utilizzando l’SMR, aveva bisogno di affrontare un ingrediente fondamentale, l’accordo, che fu affrontato nel suo lavoro successivo.

Accordo bizantino: Mentre gli approcci alle macchine a stati che sono resistenti ai guasti di crash sono sufficienti per molte applicazioni, i sistemi più mission-critical, come quelli avionici, hanno bisogno di un modello ancora più estremo di fault-tolerance che sia impermeabile ai nodi che potrebbero interrompere il sistema dall’interno.

Al Stanford Research Institute (poi chiamato SRI International) negli anni ’70, Lamport ha fatto parte di un team che ha aiutato la NASA a progettare un robusto sistema di controllo avionico. Le garanzie formali erano una necessità assoluta a causa della natura mission-critical del compito. La sicurezza doveva essere garantita contro i malfunzionamenti di sistema più estremi che si possano immaginare. Una delle prime sfide che il team dello SRI ha dovuto affrontare è stata quella di dimostrare la correttezza di uno schema di controllo della cabina di pilotaggio, che la NASA aveva progettato, con tre sistemi di computer che utilizzano il voto a maggioranza per mascherare qualsiasi componente difettoso.

Il risultato del lavoro del team è stato diversi concetti e intuizioni fondamentali riguardanti questi tipi di sistemi robusti. Includeva una definizione fondamentale di robustezza in questo ambiente, un’astrazione del problema di coordinazione che è alla base di qualsiasi sistema replicato fino ad oggi, e una sorprendente rivelazione che i sistemi con tre computer non possono mai eseguire in sicurezza una cabina di pilotaggio mission critical! LPS postulava che “un componente guasto può esibire un tipo di comportamento che è spesso trascurato – vale a dire, l’invio di informazioni contrastanti a diverse parti del sistema”. Più in generale, un componente malfunzionante potrebbe funzionare in un modo completamente incoerente con il suo comportamento prescritto, e potrebbe apparire quasi maligno.

Il nuovo modello di guasto aveva bisogno di un nome. All’epoca c’era una sfida classica correlata di coordinare due computer comunicanti, introdotta in un articolo del 1975 e a cui Jim Gray si riferiva come il “Paradosso dei due generali”. Questo portò Lamport a pensare ai computer di controllo in una cabina di pilotaggio come un esercito di generali bizantini, con l’esercito che cerca di formare un attacco coordinato mentre i traditori interni inviano segnali contrastanti. Il nome “Byzantine Failures” è stato adottato per questo modello di guasto, ed è seguita una raffica di lavoro accademico. Il modello di guasto bizantino è ancora in uso per catturare il peggior tipo di incidenti e difetti di sicurezza nei sistemi.

Lamport spiega il suo uso di una storia sui “generali bizantini” per inquadrare un problema nei sistemi distribuiti tolleranti ai guasti.

I guasti bizantini analizzano le cose brutte che possono accadere. Ma che dire delle cose buone che devono accadere? LPS ha anche dato una formulazione astratta del problema di raggiungere la coordinazione nonostante i fallimenti bizantini; questo è noto come il problema “Accordo bizantino”. Questa succinta formulazione esprime il compito di coordinazione del controllo come il problema di formare una decisione di accordo per un singolo bit, partendo da bit potenzialmente diversi in ingresso ad ogni componente. Una volta che si ha accordo su un singolo bit, è possibile usarlo ripetutamente per mantenere coordinato un intero sistema complesso. L’articolo mostra che sono necessari quattro computer per formare un accordo su un singolo bit di fronte a un singolo malfunzionamento. Tre non sono sufficienti, perché con tre unità, un’unità difettosa può inviare valori contrastanti alle altre due unità, e formare una maggioranza diversa con ciascuna di esse. Più in generale, hanno dimostrato che sono necessarie 3F+1 unità per superare F componenti simultaneamente difettose. Per dimostrare questo, hanno usato un bellissimo argomento di simmetria che è diventato noto come “argomento dell’esagono”. Questo argomento archetipo ha trovato altri usi ogni volta che si sostiene che un’unità malfunzionante che invia informazioni contrastanti a diverse parti del sistema sembra indistinguibile da una situazione simmetrica in cui i ruoli corretti e difettosi sono invertiti.

LPS ha anche dimostrato che 3F+1 unità sono sufficienti, e hanno presentato una soluzione per raggiungere l’accordo bizantino tra le 3F+1 unità in F+1 turni di comunicazione sincrona. Hanno anche dimostrato che se si usano le firme digitali, solo 2F+1 unità sono sufficienti e necessarie.

Il problema dell’Accordo Bizantino e le sue soluzioni sono diventati il segno distintivo dei sistemi tolleranti agli errori. La maggior parte dei sistemi costruiti con ridondanza ne fanno uso internamente per la replica e per il coordinamento. Lamport stesso lo usò in seguito per formare il paradigma State Machine Replication discusso in seguito, che dà il fondamento algoritmico della replica.

L’articolo del 1980 è stato premiato con il 2005 Edsger W. Dijkstra Prize in Distributed Computing, e quello del 1982 ha ricevuto il Jean-Claude Laprie Award in Dependable Computing.

Paxos: Con una crescente comprensione del problema dell’accordo per il calcolo distribuito, era tempo per Lamport di tornare alla State Machine Replication e affrontare i fallimenti lì. La prima soluzione SMR che presentò nel suo articolo del 1978 presupponeva che non ci fossero fallimenti, e faceva uso del tempo logico per far passare le repliche attraverso la stessa sequenza di comandi. Nel 1989, Lamport ha progettato un algoritmo tollerante ai guasti chiamato Paxos. Continuando la sua tendenza a raccontare parabole umoristiche, l’articolo presenta la storia immaginaria di un parlamento governativo su un’antica isola greca chiamata Paxos, dove l’assenza di qualsiasi numero dei suoi membri, o forse di tutti, può essere tollerata senza perdere consistenza.

Lamport descrive le origini del suo algoritmo Paxos per il calcolo distribuito tollerante ai guasti.

Purtroppo l’impostazione come parabola greca ha reso l’articolo difficile da comprendere per la maggior parte dei lettori, e ci sono voluti nove anni dalla presentazione alla pubblicazione nel 1998. Ma il rapporto tecnico del DEC del 1989 è stato notato. Il collega di Lamport, Butler Lampson, evangelizzò l’idea alla comunità del calcolo distribuito. Poco dopo la pubblicazione di Paxos, il sistema Chubby di Google e l’open-source ZooKeeper di Apache hanno offerto State Machine Replication come servizio esterno, ampiamente distribuito.

Paxos mette insieme una successione di decisioni di accordo in una sequenza di comandi di state-machine in modo ottimizzato. È importante notare che la prima fase della componente di accordo data nel documento di Paxos (chiamata Sinodo) può essere evitata quando lo stesso leader presiede a più decisioni; questa fase deve essere eseguita solo quando un leader deve essere sostituito. Questa svolta perspicace rappresenta gran parte della popolarità di Paxos, ed è stata successivamente chiamata Multi-Paxos dal team di Google. Il documento Paxos di Lamport ha vinto il premio ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame nel 2012.

SMR e Paxos sono diventati il quadro standard de facto per progettare e ragionare sui metodi di consenso e replica. Molte aziende che costruiscono sistemi informativi critici, tra cui Google, Yahoo, Microsoft e Amazon, hanno adottato i fondamenti di Paxos.

5. Specificazione formale e verifica dei programmi

Nei primi giorni della teoria della concorrenza è emersa la necessità di buoni strumenti per descrivere le soluzioni e dimostrare la loro correttezza. Lamport ha dato contributi centrali alla teoria della specificazione e della verifica dei programmi concorrenti. Per esempio, è stato il primo ad articolare le nozioni di proprietà di sicurezza e proprietà di liveness per algoritmi distribuiti asincroni. Queste erano la generalizzazione delle proprietà di “correttezza parziale” e “correttezza totale” precedentemente definite per i programmi sequenziali. Oggi, le proprietà di sicurezza e di liveness formano la classificazione standard per le proprietà di correttezza degli algoritmi distribuiti asincroni.

Un altro lavoro, con Martin Abadi , ha introdotto un’astrazione speciale chiamata variabili di profezia in un modello di algoritmo, per gestire una situazione in cui un algoritmo risolve una scelta non deterministica prima della specifica. Abadi e Lamport hanno evidenziato le situazioni in cui sorgono tali problemi, e hanno sviluppato la teoria necessaria per sostenere questa estensione della teoria. Inoltre, hanno dimostrato che ogni volta che un algoritmo distribuito incontra una specifica, dove entrambi sono espressi come macchine a stati, la corrispondenza tra loro può essere dimostrata utilizzando una combinazione di variabili di profezia e nozioni precedenti come le variabili di storia. Questo lavoro ha vinto il premio LICS Test-Of-Time 2008.

Linguaggi di modellazione formale e strumenti di verifica: Oltre a sviluppare le nozioni di base di cui sopra, Lamport ha sviluppato il linguaggio TLA (Temporal Logic of Actions) e il set di strumenti TLA+, per la modellazione e la verifica di algoritmi e sistemi distribuiti.

Lamport descrive TLA e la sua connessione al refinement mapping.

TLA e TLA+ supportano la specifica e la dimostrazione di proprietà di sicurezza e liveness, usando una notazione basata sulla logica temporale. Lamport ha supervisionato lo sviluppo di strumenti di verifica basati su TLA+, in particolare il TLC model checker costruito da Yuan Yu. TLA+ e TLC sono stati usati per descrivere e analizzare sistemi reali. Per esempio, questi strumenti sono stati usati per trovare un grave errore nel protocollo di coerenza usato nell’hardware della Xbox 360 di Microsoft prima del suo rilascio nel 2005. Alla Intel, è stato usato per l’analisi di un protocollo di cache-coerenza dell’Intel Quick Path Interconnect come implementato nel processore core Nehalem. Per insegnare agli ingegneri come usare i suoi strumenti di specificazione formale, Lamport ha scritto un libro. Più recentemente, Lamport ha sviluppato il linguaggio formale PlusCAL e gli strumenti per l’uso nella verifica di algoritmi distribuiti; questo lavoro si basa su TLA+.

6. LaTeX

Quando si crea una così vasta collezione di documenti di impatto, è naturale desiderare un comodo strumento di composizione. Lamport non ne ha solo desiderato uno, ne ha creato uno per l’intera comunità. Fuori dal campo della concorrenza è il sistema Latex di Lamport, un insieme di macro da usare con il sistema di composizione TeX di Donald Knuth. LaTeX aggiunse tre cose importanti a TeX:

1. Il concetto di ‘ambiente di composizione’, che aveva avuto origine nel sistema Scribe di Brian Reid.
2. Una forte enfasi sul markup strutturale piuttosto che tipografico.
3. Un design di documento generico, abbastanza flessibile da essere adeguato ad un’ampia varietà di documenti.

Lamport non ha originato queste idee, ma spingendole il più lontano possibile ha creato un sistema che fornisce la qualità di TeX e molta della sua flessibilità, ma è molto più facile da usare. Latex divenne lo standard de facto per la pubblicazione tecnica in informatica e in molti altri campi.

Ci sono molti altri importanti articoli di Leslie Lamport — troppi per essere descritti qui. Sono elencati in ordine cronologico sulla home page di Lamport, accompagnati da note storiche che descrivono la motivazione e il contesto di ogni risultato.

Ogni volta che accedete a un computer moderno, è probabile che siate influenzati dagli algoritmi di Leslie Lamport. E tutto questo lavoro è iniziato con la ricerca di capire come organizzare una coda in una panetteria locale.

Autore: Dahlia Malkhi
Altri collaboratori: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese, e Len Shustek