¿Cómo pudo haber pensado Leslie Lamport para inventar Paxos?

“Why should you pay attention to me?”

Estudiando el curso “Lamport TLA+ Course”, me resultó muy curiosa la forma de manejar la enseñanza e investigación de Leslie Lamport (sin mencionar los curiosos sombreros que utiliza en sus lecciones). En la lección 1: “Introduction to TLA+”, el presenta su biografía con una pregunta gratamente sarcástica: “what kind of clown am i claiming that i know what can make you think better… why should you pay attention to me?”. Esto me hizo pensar en la creatividad de Lamport, quien, mediante una analogía tan peculiar como la de una isla ficticia de la antigua Grecia, bautizó a su algoritmo más famoso de consenso distribuido: Paxos.

Volando un poco sobre el tema, comencé a pensar, ¿cómo?, ¿cómo logró Lamport inventar tan complejo y consistente algoritmo? ¿Lo hizo iterando sobre reglas hasta concebirlas en un mismo algoritmo?, ¿requirió pruebas masivas?, ¿fue producto de iluminación divina con suerte de Terry Davis?…

Motivación

En este post no pretendo explicar Paxos, si lo hiciera, perdería cabello en el proceso (suponiendo que logro concretar una explicación total de Paxos, misma para la que aún no me considero adeucado).

Pretendo hacer una reflexión personal e inferir cómo pudo haber sido el proceso intelectual de Lamport detrás de la creación de Paxos, basándome en sus publicaciones, conferencias y en la forma en que suele abordar el diseño de algoritmos.

Ordenamiento Parcial y Relojes Lógicos

Para entender cómo Lamport conceptualizó Paxos, primero debemos mirar retrospectivamente su obra fundamental de 1978 sobre el ordenamiento de eventos. En un sistema asíncrono distribuido, el tiempo físico es como una ilusión porque no existe un reloj global. Lamport se dio cuenta de que establecer un consenso requería un ordenamiento parcial estricto de los eventos, lo cual logró a través de relojes lógicos.

Paxos depende de este concepto, cada propuesta es etiquetada con un número de secuencia unico y creciente (tenemos aquí la base teórica del algoritmo). Al forzar a que los nodos solo puedan aceptar propuestas con un número de secuencia mayor al que han visto previamente, Lamport creó una flecha direccional del tiempo que evita que propuestas mas antiguas y retrasadas sobrescriban decisiones más nuevas y ya establecidas.

Intersección de Quórums y el Principio del Palomar

El gran avance teórico de Paxos no se trata de la comunicación en red; se trata fundamentalmente de la teoría de conjuntos y el Principio del Palomar (Pigeonhole Principle). Lamport estructuró el algoritmo en torno al concepto de quórums (mayorías). En un sistema compuesto por $N = 2F + 1$ nodos (donde $F$ es el número máximo de fallos tolerables), cualesquiera dos quórums siempre se intersecarán en al menos un nodo.

Este es el motor matemático de Paxos. Si un valor es aceptado por una mayoría de nodos en la fase de Accept, y un líder posterior intenta aprender el estado actual consultando a una mayoría en la fase de Prepare, la intersección garantiza que el nuevo líder recibirá respuesta de al menos un nodo que contenga el valor previamente aceptado. Este invariante es lo que garantiza una consistencia absoluta en toda la máquina de estados distribuida.

Diseño Basado en Invariantes (precursor de TLA+)

Lamport no aborda los sistemas distribuidos como secuencias de ejecución de código (de aquí que repito que nuestra noción como desarrolladores iterativos cae), sino como sistemas formales de transición de estados. Mucho antes de estandarizar TLA+ (Lógica Temporal de Acciones), su metodología ya estaba cimentada en la definición de matemáticas discretas. Para Lamport, un sistema es simplemente un estado inicial y un conjunto de pasos atómicos permitidos (acciones) que transicionan el sistema de un estado a otro.

Para garantizar Safety (la propiedad de que nada malo ocurra jamás), definió condiciones que deben cumplirse en todo espacio de estados posible. En los métodos formales, si $I$ es el predicado del estado inicial y $N$ es la acción del estado siguiente, una propiedad de seguridad $P$ se demuestra como un invariante si satisface dos condiciones:

$I \Rightarrow P$ $P \land N \Rightarrow P'$

Al definir las restricciones de las fases de Prepare y Accept estrictamente a traves de estos invariantes, Lamport aseguró que la regla central —solo se puede elegir un único valor— fuera matemáticamente inquebrantable, independientemente de particiones de red, duplicación de mensajes o retrasos asíncronos.

Teorema de Imposibilidad FLP

Cualquier discusión teórica sobre el consenso debe abordar el Teorema de Imposibilidad FLP (Fischer, Lynch y Paterson, 1985). Este teorema demuestra que el consenso determinista en un sistema asíncrono es imposible si incluso un solo nodo puede fallar, porque es imposible distinguir un nodo colapsado de un mensaje de red con mucho retraso.

La genialidad de Lamport fue desacoplar completamente Safety (Seguridad) de Liveness (Vivacidad). Paxos garantiza la seguridad incondicionalmente a través de sus intersecciones de quórums. Sin embargo, para la vivacidad (la propiedad de que algo bueno eventualmente suceda), “relaja” el requisito determinista. Paxos depende de un mecanismo débil de elección de líder (que se mapea conceptualmente a un detector de fallos $\Omega$ ). Si surgen múltiples líderes debido a la inestabilidad de la red, podrían entrar en un “livelock” al anular continuamente los números de propuesta de los demás. En este escenario, Paxos simplemente se detiene. Sacrifica la vivacidad para preservar una seguridad estricta, eludiendo brillantemente los límites imposibles del teorema FLP.

Concluyendo

Es aquí cuando intento trazar el proceso intelectual de Lamport para concebir Paxos, pero no intuyo nada de refactorización de código o arquitecturas de red. Infiero un cumulo de conceptos matemáticos y lógica formal pura. Su camino lógico probablemente se desarrolló bajo esta línea de tiempo conceptual:

Ausencia de Tiempo Global (Relojes Lógicos) $\rightarrow$ Replicación de Máquinas de Estado $\rightarrow$ Desacoplamiento de Safety y Liveness (Aceptando los límites del FLP) $\rightarrow$ Intersección de Quórums (El Principio del Palomar) $\rightarrow$ Definición de Invariantes (Lógica Formal en Fases) $\rightarrow$ Analogía Griega (El Parlamento de Paxos)

Para desglosarlo:

Ausencia de Tiempo Global: Comprendió que en sistemas distribuidos el tiempo físico no existe, creando los Relojes Lógicos para ordenar eventos (números de propuesta).
Replicación de Máquinas de Estado: Conceptualizó el problema no como nodos comunicándose, sino como una única máquina de estado determinista que necesitaba replicarse.
Desacoplamiento de Safety y Liveness: Aceptó que garantizar consistencia (Safety) y disponibilidad (Liveness) al mismo tiempo en redes asíncronas era imposible. Eligió garantizar la consistencia de forma absoluta, permitiendo que el sistema se detuviera si era necesario.
Intersección de Quórums: Usó la matemática de conjuntos básicos para asegurar que las mayorías superpuestas siempre compartieran al menos un nodo, garantizando la retención del estado.
Definición de Invariantes: Formuló las reglas estrictas de preparación (Prepare) y aceptación (Accept) para asegurar matemáticamente que la regla dorada —nunca elegir dos valores distintos— fuera inviolable.
Analogía Griega: Finalmente, tomó ésta compleja estructura matemática y, en un intento por hacerla “más amigable”, la envolvió en la historia de los legisladores de la isla de Paxos (soy auténtico seguidor de que las analogías son herramientas muy poderosas para el aprendizaje).

Lamport no inventó Paxos probando qué funcionaba en un clúster de servidores, sino que lo inventó definiendo primero las leyes lógicas y dejando que el algoritmo fuera la única conclusión matemática posible. Y esa, sin duda, es la verdadera genialidad detrás de los sistemas distribuidos.