Si pudiéramos viajar en el tiempo hasta 1974, tal vez encontraríamos a Leslie Lamport en la concurrida panadería de su barrio, lidiando con el siguiente problema. La panadería tenía varios cajeros, pero si más de una persona se acercaba a un solo cajero al mismo tiempo, éste intentaba hablar con todos a la vez y se confundía. Lamport se dio cuenta de que tenía que haber alguna forma de garantizar que la gente se acercara a los cajeros de uno en uno. Este problema le recordó a Lamport una cuestión planteada en un artículo anterior del informático Edsger Dijkstra sobre otra cuestión mundana: cómo compartir los cubiertos en una mesa de comedor. Uno de los retos de coordinación era garantizar que cada utensilio fuera utilizado como máximo por un comensal a la vez, lo que llegó a generalizarse como el problema de exclusión mutua, exactamente el reto al que se enfrentó Lamport en la panadería.

Una mañana de 1974, a Lamport se le ocurrió una idea sobre cómo los clientes de la panadería podían resolver la exclusión mutua entre ellos, sin depender de la ayuda de la panadería. Funcionaba más o menos así: la gente elegía números al entrar en la panadería, y luego se les servía en la caja según el número que habían pedido. Para elegir un número, un cliente pide el número de todos los que le rodean y elige un número superior a todos los demás.

Esta sencilla idea se convirtió en un elegante algoritmo para resolver el problema de exclusión mutua sin requerir ninguna operación indivisible de nivel inferior. También fue una rica fuente de ideas futuras, ya que había que resolver muchas cuestiones. Por ejemplo, algunos clientes de la panadería tardaban en comprobar otros números, y mientras tanto llegaban más clientes y seleccionaban números adicionales. En otra ocasión, el director de la panadería quería obtener una instantánea de todos los números de los clientes para poder preparar suficientes pasteles. Lamport dijo más tarde: «Durante un par de años después de mi descubrimiento del algoritmo de la panadería, todo lo que aprendí sobre concurrencia provino de su estudio.»

El Algoritmo de la Panadería y otros trabajos pioneros de Lamport -muchos con nombres divertidos y parábolas asociadas- se han convertido en pilares de la informática. Su colección constituye la base de amplias áreas en concurrencia, y ha influido en la especificación, desarrollo y verificación de sistemas concurrentes.

Después de graduarse con un doctorado en matemáticas por la Universidad de Brandeis en 1972, Lamport trabajó como informático en Massachusetts Computer Associates de 1970 a 1977, en SRI International de 1977 a 1985, y en el Centro de Investigación de Sistemas de Digital Equipment Corporation (posteriormente propiedad de Compaq) de 1985 a 2001. En 2001 se incorporó a Microsoft Research en Mountain View, California.

Pasar su carrera investigadora en entornos de investigación industrial no fue un accidente. «Me gusta trabajar en un laboratorio de investigación industrial, por la aportación que supone», afirma Lamport. «Si sólo trabajara por mi cuenta y se me ocurrieran problemas, se me ocurriría un pequeño número de cosas, pero si salgo al mundo, donde la gente está trabajando en sistemas informáticos reales, hay un millón de problemas ahí fuera. Cuando miro hacia atrás, la mayoría de las cosas en las que trabajé -Generales Bizantinos, Paxos- surgieron de problemas del mundo real.»

Sus trabajos arrojaron luz sobre cuestiones fundamentales de los programas concurrentes, para los que no existía una teoría formal en aquel momento. Trató conceptos fundamentales como la causalidad y el tiempo lógico, los registros compartidos atómicos y regulares, la consistencia secuencial, la replicación de máquinas de estado, el acuerdo bizantino y la libertad de espera. Trabajó en algoritmos que se han convertido en una práctica de ingeniería estándar para los sistemas distribuidos tolerantes a fallos. También ha desarrollado un importante cuerpo de trabajo sobre la especificación formal y la verificación de sistemas concurrentes, y ha contribuido al desarrollo de herramientas automatizadas que aplican estos métodos. Sólo mencionaremos algunas de sus contribuciones.

1. Soluciones de exclusión mutua y el algoritmo Bakery

Los influyentes trabajos de Lamport de las décadas de 1970 y 1980 se produjeron en un momento en el que se comprendían poco los problemas fundamentales de la programación para múltiples procesadores concurrentes.

Por ejemplo, se sabía que la ejecución correcta puede requerir que las actividades paralelas se excluyan unas a otras durante los periodos de las «secciones críticas» en los que manipulan los mismos datos, con el fin de evitar el intercalado indeseado de operaciones. Los orígenes de este problema de exclusión mutua provienen del trabajo pionero de Edsger Dijkstra, que incluye su solución. El algoritmo de Dijkstra, aunque es correcto, depende de que los accesos a la memoria compartida sean atómicos, es decir, que un procesador que lea cuando otro esté escribiendo tenga que esperar, en lugar de devolver un valor posiblemente confuso. En cierto sentido, construye una solución de alto nivel a partir de la exclusión mutua de bajo nivel ya implementada por el hardware.

El notablemente elegante e intuitivo «Algoritmo de la Panadería» de Lamport no hace eso. Su solución organiza los procesos que compiten en una cola implícita según su orden de llegada, como una cola de espera en una panadería. Sin embargo, no importa si un procesador que lee datos que están siendo actualizados por otro procesador recibe basura. El algoritmo sigue funcionando.

Lamport recuerda su descubrimiento del algoritmo de la panadería.

El algoritmo de la panadería se ha convertido en material de libro de texto, y la mayoría de los estudiantes de informática lo encuentran en el curso de sus estudios.

2. Fundamentos de la programación concurrente

Del trabajo del algoritmo Bakery surgieron varios conceptos nuevos importantes, una tendencia que se repitió varias veces en la carrera de Lamport. La experiencia de idear algoritmos concurrentes y verificar su corrección hizo que se centrara en los fundamentos básicos que harían que los multiprocesadores se comportaran de manera que los programadores pudieran razonar matemáticamente. Mientras trabajaba en una solución para un problema concreto, Lamport inventó abstracciones y reglas generales necesarias para razonar sobre su corrección, y estas aportaciones conceptuales se convirtieron luego en pilares teóricos de la programación concurrente.

Libertad de bucle: El trabajo del Algoritmo de la Panadería introdujo un concepto importante llamado «libertad de bucle». Algunas soluciones obvias que vienen a la mente para el problema de la exclusión mutua preasignan «turnos» de rotación entre los procesos. Pero esto obliga a los procesos a esperar a otros que son lentos y aún no han llegado al punto de contención. Utilizando la analogía de la panadería, sería parecido a llegar a una panadería vacía y que te pidan que esperes a un cliente que aún no ha llegado a la panadería. En cambio, la libertad de bucle expresa la capacidad de los procesos de progresar independientemente de la velocidad de otros procesos. Como el algoritmo de la panadería asigna los turnos a los procesos por orden de llegada, tiene libertad de bucle. Este es un concepto crucial que se ha utilizado en el diseño de muchos algoritmos posteriores y en el diseño de arquitecturas de memoria. La libertad de espera, una condición que requiere un progreso independiente a pesar de los fallos, tiene sus claras raíces en la noción de libertad de bucle y en el concepto de puerta de la panadería. Posteriormente fue ampliamente explorado por otros, incluyendo a Maurice Herlihy.

Consistencia secuencial: Trabajar con una arquitectura multinúcleo que tenía memoria caché distribuida llevó a Lamport a crear especificaciones formales para el comportamiento coherente de la caché en sistemas multiprocesadores. Ese trabajo puso algo de orden en el caos de este campo al inventar la consistencia secuencial , que se ha convertido en el estándar de oro para los modelos de consistencia de la memoria. Esta noción sencilla e intuitiva proporciona el nivel justo de «atomicidad» para que el software funcione. Hoy en día, diseñamos sistemas de hardware con un ordenamiento de marca de tiempo o de tienda parcial, con instrucciones de valla de memoria añadidas, lo que permite a los programadores hacer que el hardware parezca secuencialmente consistente. Los programadores pueden entonces implementar algoritmos que proporcionan fuertes propiedades de consistencia. Esta es la clave de los modelos de consistencia de memoria de Java y C++. Nuestros procesadores multinúcleo funcionan hoy en día basándose en los principios descritos por Leslie Lamport en 1979.

Registros atómicos y regulares: El Algoritmo Bakery también llevó a Lamport a preguntarse por la semántica precisa de la memoria cuando varios procesos interactúan para compartir datos. Tardó casi una década en formalizarlo, y el resultado es la abstracción de los registros regulares y atómicos.

Su teoría da a cada operación en un registro compartido una duración explícita, que comienza con una invocación y termina con un resultado. Los registros pueden implementarse mediante diversas técnicas, como la replicación. No obstante, se supone que las interacciones de los procesos con un registro atómico «parecen» accesos en serie a la memoria compartida real. La teoría también incluye una semántica de interacción más débil, como la de un registro regular. Un registro regular captura situaciones en las que los procesos leen diferentes réplicas del registro mientras se actualiza. En cualquier momento, algunas réplicas pueden estar actualizadas y otras no, y finalmente todas las réplicas tendrán el valor actualizado. Es importante destacar que esta semántica más débil es suficiente para soportar la exclusión mutua: el algoritmo Bakery funciona correctamente si un lector que se superpone a un escritor obtiene de nuevo cualquier valor arbitrario.

Lamport describe su trabajo para definir con precisión las abstracciones para los registros atómicos, regulares y seguros.

Este trabajo inició un subcampo distinto de investigación en la computación distribuida que todavía está floreciendo. Los objetos atómicos de Lamport sólo admitían operaciones de lectura y escritura, es decir, eran registros atómicos. Maurice Herlihy y Jeannette Wing generalizaron la noción a otros tipos de datos, y su término «linealidad» se convirtió en sinónimo de atomicidad. Hoy en día, esencialmente todos los sistemas de almacenamiento no relacionales desarrollados por empresas como Amazon, Google y Facebook adoptan la linealidad y la consistencia secuencial para sus garantías de coherencia de datos.

3. Fundamentos de los sistemas distribuidos

Un tipo especial de sistema concurrente es un sistema distribuido, caracterizado por tener procesos que utilizan mensajes para interactuar entre sí. Leslie Lamport ha tenido un gran impacto en la forma de pensar sobre los sistemas distribuidos, así como en las prácticas de ingeniería del campo.

Relojes lógicos: Mucha gente se dio cuenta de que una noción global del tiempo no es natural para un sistema distribuido. Lamport fue el primero en precisar una noción alternativa de «relojes lógicos», que imponen un orden parcial a los eventos basado en la relación causal inducida por el envío de mensajes de una parte del sistema a otra . Su artículo sobre «Time, Clocks, and the Ordering of Events in a Distributed System» se ha convertido en el más citado de los trabajos de Lamport, y en el lenguaje informático los relojes lógicos reciben a menudo el apodo de Lamport timestamps. Su trabajo ganó el Premio a la Ponencia Influyente de la Conferencia sobre Principios de Computación Distribuida del año 2000 (que más tarde pasó a llamarse Premio Edsger W. Dijkstra en Computación Distribuida), y ganó un Premio del Salón de la Fama de ACM SIGOPS en 2007.

Lamport describe su trabajo «Time, Clocks…» y su relación con la relatividad especial.

Para entender por qué ese trabajo ha llegado a ser tan influyente, hay que reconocer que en el momento de la invención no había una buena manera de capturar el retardo de la comunicación en los sistemas distribuidos, excepto utilizando el tiempo real. Lamport se dio cuenta de que el retraso de la comunicación hacía que esos sistemas fueran muy diferentes de un sistema multiprocesador de memoria compartida. La idea surgió al leer un artículo sobre bases de datos replicadas y darse cuenta de que su ordenamiento lógico de comandos podría violar la causalidad.

Usar el ordenamiento de los eventos como una forma de probar la corrección del sistema es lo que la gente hace hoy en día para las pruebas intuitivas de los algoritmos de sincronización concurrentes. Otra poderosa contribución de este trabajo fue demostrar cómo replicar una máquina de estado utilizando relojes lógicos, lo que se explica a continuación.

Instancias distribuidas: Una vez que se define el orden causal, la noción de estados globales consistentes sigue naturalmente. Esto condujo a otro trabajo perspicaz. Lamport y Mani Chandy inventaron el primer algoritmo para leer el estado (tomar una «instantánea») de un sistema distribuido arbitrario. Se trata de una noción tan poderosa que otros la utilizaron posteriormente en diferentes ámbitos, como las redes, la autoestabilización, la depuración y los sistemas distribuidos. Este artículo recibió el premio ACM SIGOPS Hall of Fame 2013.

4. Tolerancia a fallos y replicación de máquinas de estado

`Un sistema distribuido es aquel en el que el fallo de un ordenador que ni siquiera sabías que existía puede dejar inutilizado tu propio ordenador» es una famosa ocurrencia de Lamport. Gran parte de su trabajo tiene que ver con la tolerancia a los fallos.

State Machine Replication (SMR): Quizás la más significativa de las muchas contribuciones de Lamport es el paradigma de Replicación de Máquinas de Estado, que fue introducido en el famoso documento sobre «Time, Clocks, and the Ordering of Events in a Distributed System» (Tiempo, relojes y el orden de los eventos en un sistema distribuido), y desarrollado poco después. La abstracción captura cualquier servicio como una máquina de estado centralizada, una especie de motor de computación universal similar a una máquina de Turing. Tiene un estado interno y procesa órdenes en secuencia, cada una de las cuales da lugar a un nuevo estado interno y produce una respuesta. Lamport se dio cuenta de que la desalentadora tarea de replicar un servicio en múltiples ordenadores puede simplificarse notablemente si se presenta la misma secuencia de comandos de entrada a todas las réplicas y éstas proceden a través de una sucesión idéntica de estados.

Este perspicaz paradigma de SMR subyace en muchos sistemas fiables, y se considera un enfoque estándar para construir sistemas distribuidos replicados debido a su elegancia. Pero antes de que Lamport desarrollara una solución completa utilizando para SMR, necesitaba abordar un ingrediente central, el acuerdo, que fue abordado en su siguiente trabajo.

Acuerdo bizantino: Mientras que los enfoques de las máquinas de estado que son resistentes a los fallos de colisión son suficientes para muchas aplicaciones, los sistemas más críticos, como para la aviónica, necesitan un modelo aún más extremo de tolerancia a los fallos que es impermeable a los nodos que podrían interrumpir el sistema desde dentro.

En el Instituto de Investigación de Stanford (más tarde llamado SRI International) en los años 70, Lamport formó parte de un equipo que ayudó a la NASA a diseñar un sistema de control de aviónica robusto. Las garantías formales eran una necesidad absoluta debido a la naturaleza crítica de la misión. Había que garantizar la seguridad frente a los fallos más extremos del sistema que se pudieran imaginar. Uno de los primeros retos que se pidió al equipo de SRI fue demostrar la corrección de un esquema de control de la cabina, que la NASA había diseñado, con tres sistemas informáticos que utilizan la votación por mayoría para enmascarar cualquier componente defectuoso.

El resultado del trabajo del equipo fue varios conceptos y conocimientos fundamentales sobre estos estrictos tipos de sistemas robustos. Incluía una definición fundamental de robustez en este entorno, una abstracción del problema de coordinación que subyace en cualquier sistema replicado hasta la fecha, y una sorprendente revelación de que los sistemas con tres ordenadores nunca pueden dirigir con seguridad una cabina de mando de misión crítica!

En efecto, en dos trabajos seminales («LPS») publicados con Pease y Shostak , el equipo identificó por primera vez una vulnerabilidad un tanto peculiar. LPS postuló que «un componente que falla puede exhibir un tipo de comportamiento que a menudo se pasa por alto, es decir, enviar información conflictiva a diferentes partes del sistema». En términos más generales, un componente que falla podría funcionar de una manera completamente inconsistente con su comportamiento prescrito, y podría parecer casi malicioso.

El nuevo modelo de fallos necesitaba un nombre. Por aquel entonces existía un reto clásico relacionado con la coordinación de dos ordenadores comunicados, introducido en un artículo de 1975 y al que Jim Gray se refirió como la «Paradoja de los dos generales». Esto llevó a Lamport a pensar en los ordenadores de control de una cabina como un ejército de generales bizantinos, con el ejército tratando de formar un ataque coordinado mientras los traidores internos enviaban señales conflictivas. Se adoptó el nombre de «fallos bizantinos» para este modelo de fallos, y le siguió una avalancha de trabajos académicos. El modelo de fallos bizantinos sigue utilizándose para captar el peor tipo de percances y fallos de seguridad en los sistemas.

Lamport explica su uso de una historia sobre «generales bizantinos» para enmarcar un problema en los sistemas distribuidos tolerantes a fallos.

Los fallos bizantinos analizan las cosas malas que pueden ocurrir. Pero, ¿qué pasa con las cosas buenas que tienen que pasar? LPS también dio una formulación abstracta del problema de alcanzar la coordinación a pesar de los fallos bizantinos; esto se conoce como el problema del «Acuerdo Bizantino». Esta formulación sucinta expresa la tarea de coordinación del control como el problema de formar una decisión de acuerdo para un bit individual, comenzando con bits potencialmente diferentes de entrada a cada componente. Una vez que se ha llegado a un acuerdo sobre un solo bit, es posible utilizarlo repetidamente para mantener coordinado todo un sistema complejo. El documento muestra que se necesitan cuatro ordenadores para llegar a un acuerdo sobre un solo bit ante una sola avería. Tres no son suficientes, porque con tres unidades, una unidad defectuosa puede enviar valores conflictivos a las otras dos unidades, y formar una mayoría diferente con cada una. En términos más generales, demostraron que se necesitan 3F+1 unidades para superar F componentes defectuosos simultáneamente. Para demostrarlo, utilizaron un bello argumento de simetría que ha pasado a conocerse como el «argumento del hexágono». Este argumento arquetipo ha encontrado otros usos cuando se argumenta que una unidad que funciona mal y que envía información conflictiva a diferentes partes del sistema parece indistinguible de una situación simétrica en la que se invierten los papeles correcto y defectuoso.

LPS también demostró que 3F+1 unidades son suficientes, y presentaron una solución para alcanzar un Acuerdo Bizantino entre las 3F+1 unidades en F+1 rondas de comunicación sincrónica. También demostraron que si se utilizan firmas digitales, sólo 2F+1 unidades son suficientes y necesarias.

El problema del Acuerdo Bizantino y sus soluciones se han convertido en el sello de los sistemas tolerantes a fallos. La mayoría de los sistemas construidos con redundancia hacen uso de ella internamente para la replicación y para la coordinación. El propio Lamport lo utilizó más tarde para crear el paradigma de Replicación de Máquinas de Estado que se discute a continuación, y que proporciona la base algorítmica de la replicación.

El artículo de 1980 fue galardonado con el Premio Edsger W. Dijkstra 2005 en Computación Distribuida, y el artículo de 1982 recibió el Premio Jean-Claude Laprie en Computación Confiable.

Paxos: Con una creciente comprensión del problema del acuerdo para la computación distribuida, era el momento de que Lamport volviera a la Replicación de Máquinas de Estado y abordara los fallos allí. La primera solución de SMR que presentó en su artículo de 1978 suponía que no había fallos, y hacía uso del tiempo lógico para hacer pasar a las réplicas por la misma secuencia de comandos. En 1989, Lamport diseñó un algoritmo tolerante a fallos llamado Paxos . Continuando con su tendencia a contar parábolas humorísticas, el documento presenta la historia imaginaria de un parlamento gubernamental en una antigua isla griega llamada Paxos, donde la ausencia de cualquier número de sus miembros, o posiblemente de todos ellos, puede ser tolerada sin perder consistencia.

Lamport describe los orígenes de su algoritmo Paxos para la computación distribuida tolerante a fallos.

Desgraciadamente, la ambientación como parábola griega hizo que el artículo fuera difícil de comprender para la mayoría de los lectores, y tardó nueve años desde su presentación hasta su publicación en 1998. Sin embargo, el informe técnico del DEC de 1989 sí que llamó la atención. El colega de Lamport, Butler Lampson, evangelizó la idea a la comunidad de la informática distribuida. Poco después de la publicación de Paxos, el sistema Chubby de Google y el ZooKeeper de código abierto de Apache ofrecieron la Replicación de Máquinas de Estado como un servicio externo y ampliamente desplegado.

Paxos cose una sucesión de decisiones de acuerdo en una secuencia de comandos de máquinas de estado de manera optimizada. Es importante destacar que la primera fase del componente de acuerdo que se da en el documento de Paxos (llamada Sínodo) puede evitarse cuando el mismo líder preside múltiples decisiones; esa fase sólo debe realizarse cuando un líder necesita ser reemplazado. Este avance tan perspicaz explica gran parte de la popularidad de Paxos, y posteriormente el equipo de Google lo denominó Multi-Paxos. El artículo de Lamport sobre Paxos ganó el premio ACM SIGOPS (Special Interest Group on Operating Systems) Hall of Fame Award en 2012.

SMR y Paxos se han convertido en el marco estándar de facto para diseñar y razonar sobre métodos de consenso y replicación. Muchas empresas que construyen sistemas de información críticos, como Google, Yahoo, Microsoft y Amazon, han adoptado los fundamentos de Paxos.

5. Especificación formal y verificación de programas

En los primeros días de la teoría de la concurrencia surgió la necesidad de contar con buenas herramientas para describir soluciones y demostrar su corrección. Lamport ha hecho contribuciones centrales a la teoría de la especificación y verificación de programas concurrentes. Por ejemplo, fue el primero en articular las nociones de propiedades de seguridad y propiedades de liveness para algoritmos distribuidos asíncronos. Éstas fueron la generalización de las propiedades de «corrección parcial» y «corrección total» definidas anteriormente para los programas secuenciales. Hoy en día, las propiedades de seguridad y de liveness forman la clasificación estándar para las propiedades de corrección de los algoritmos distribuidos asíncronos.

Otro trabajo, con Martin Abadi , introdujo una abstracción especial llamada variables de profecía a un modelo de algoritmo, para manejar una situación en la que un algoritmo resuelve una elección no determinista antes de que lo haga la especificación. Abadi y Lamport señalaron las situaciones en las que surgen estos problemas, y desarrollaron la teoría necesaria para apoyar esta extensión de la teoría. Además, demostraron que siempre que un algoritmo distribuido se encuentra con una especificación, donde ambos se expresan como máquinas de estado, la correspondencia entre ellos puede demostrarse utilizando una combinación de variables de profecía y nociones anteriores como las variables de historia. Este trabajo ganó el premio LICS Test-Of-Time 2008.

Lenguajes de modelado formal y herramientas de verificación: Además de desarrollar las nociones básicas anteriores, Lamport ha desarrollado el lenguaje TLA (Lógica Temporal de Acciones) y el conjunto de herramientas TLA+, para el modelado y la verificación de algoritmos y sistemas distribuidos.

Lamport describe TLA y su conexión con el mapeo de refinamiento.

TLA y TLA+ soportan la especificación y la prueba de propiedades tanto de seguridad como de capacidad de respuesta, utilizando una notación basada en la lógica temporal. Lamport ha supervisado el desarrollo de herramientas de verificación basadas en TLA+, especialmente el verificador de modelos TLC construido por Yuan Yu. TLA+ y TLC se han utilizado para describir y analizar sistemas reales. Por ejemplo, estas herramientas se utilizaron para encontrar un importante error en el protocolo de coherencia utilizado en el hardware de la Xbox 360 de Microsoft antes de su lanzamiento en 2005. En Intel, se utilizó para el análisis del protocolo de coherencia de la caché del Intel Quick Path Interconnect tal y como se implementó en el procesador de núcleo Nehalem. Para enseñar a los ingenieros a utilizar sus herramientas de especificación formal, Lamport ha escrito un libro. Más recientemente, Lamport ha desarrollado el lenguaje formal PlusCAL y herramientas para su uso en la verificación de algoritmos distribuidos; este trabajo se basa en TLA+.

6. LaTeX

Cuando se crea una colección tan vasta de documentos impactantes, es natural desear una herramienta de composición tipográfica conveniente. Lamport no sólo deseó una, sino que la creó para toda la comunidad. Fuera del ámbito de la concurrencia está el sistema Latex de Lamport , un conjunto de macros para utilizar con el sistema de composición tipográfica TeX de Donald Knuth. LaTeX añadió tres cosas importantes a TeX:

1. El concepto de ‘entorno de composición tipográfica’, que se había originado en el sistema Scribe de Brian Reid.
2. Un fuerte énfasis en el marcado estructural más que en el tipográfico.
3. Un diseño de documento genérico, lo suficientemente flexible como para ser adecuado para una amplia variedad de documentos.

Lamport no originó estas ideas, pero al llevarlas lo más lejos posible creó un sistema que proporciona la calidad de TeX y gran parte de su flexibilidad, pero es mucho más fácil de usar. Latex se convirtió en el estándar de facto para la publicación técnica en ciencias de la computación y en muchos otros campos.

Hay muchos otros trabajos importantes de Leslie Lamport, demasiados para describirlos aquí. Se enumeran en orden cronológico en la página web de Lamport, acompañados de notas históricas que describen la motivación y el contexto de cada resultado.

Cada vez que acceda a un ordenador moderno, es probable que reciba el impacto de los algoritmos de Leslie Lamport. Y todo este trabajo comenzó con la búsqueda de entender cómo organizar una cola en una panadería local.

Autor: Dahlia Malkhi
Contribuidores adicionales: Martin Abadi, Hagit Attiya, Idit Keidar,
Nancy Lynch, Nir Shavit,
George Varghese y Len Shustek