Definir antes de resolver: la propiedad que nadie había enunciado

Durante tres décadas, la investigación en edición colaborativa persiguió dos objetivos que sabía enunciar con precisión: que todas las réplicas acaben en el mismo estado y que ese estado respete un orden total sobre los elementos. Los algoritmos que cumplían ambos se declaraban correctos, y lo eran en el sentido estricto de que satisfacían la especificación disponible. El problema es que esa especificación permitía que dos usuarios escribieran huevos y pan en el mismo punto de una lista de la compra y que la fusión produjera hpuaenvos: un resultado en el que todas las réplicas coinciden, que respeta el orden total y que ningún ser humano aceptaría. La anomalía no era un fallo de implementación, era un hueco en el vocabulario formal. Lo que hace importante al trabajo de Weidner y Kleppmann no es haber construido otro algoritmo de listas replicadas, de los que ya existía una docena, sino haber cerrado ese hueco: enunciar una propiedad de corrección nueva, demostrar que es satisfacible —cosa que el intento anterior no era— y demostrar que un algoritmo concreto la cumple. Este nivel trata de esa secuencia, y la primera lección trata de por qué el orden de los factores importa: definir antes de resolver.

Una anomalía que ninguna especificación prohibía

El marco formal que la comunidad daba por bueno es la especificación fuerte de listas de Attiya y colegas, publicada en 2016. Exige dos cosas. La primera es convergencia: dos réplicas que han procesado el mismo conjunto de operaciones están en el mismo estado, con independencia del orden en que las recibieron. La segunda es que exista un orden total global sobre los elementos tal que el estado de cualquier réplica sea siempre la restricción de ese orden a los elementos que conoce. Es una especificación exigente y nada trivial de satisfacer: varios algoritmos de transformación operacional publicados en los años noventa resultaron no cumplirla, y la aparición de los CRDT se justificó en buena medida como respuesta a esos fallos de convergencia.

Conviene tener presente la genealogía completa, porque explica por qué el hueco se mantuvo tanto tiempo. La edición colaborativa nace en 1989 con Ellis y Gibbs, que introducen la transformación operacional; el enfoque se formaliza en los años noventa y uno de sus algoritmos, Jupiter, acaba siendo la base de la colaboración en tiempo real de Google Docs. Cuando se descubre que varios algoritmos de transformación no convergen en determinadas situaciones, aparecen los CRDT como alternativa con garantías demostrables, y con ellos la serie de algoritmos de texto que va de WOOT a Treedoc, Logoot y RGA. Toda esa cadena de más de tres décadas se organiza alrededor de una única pregunta —cómo garantizar que las réplicas coincidan— y la resuelve cada vez mejor. La pregunta de si el documento resultante tiene sentido para quien lo lee nunca entró en el marco.

Lo que conviene interiorizar es que la intercalación no viola ninguna de las dos condiciones. Un algoritmo puede producir hpuaenvos y seguir siendo perfectamente convergente: todas las réplicas llegan a esa misma cadena y todas la derivan del mismo orden total. La especificación no dice nada sobre la procedencia de los elementos vecinos, porque el orden total que postula es un objeto abstracto sin memoria de quién insertó qué ni de en qué ráfaga lo hizo. La anomalía cae fuera del alcance del enunciado, y por eso ninguna herramienta de verificación construida sobre él podía detectarla.

Documento inicial:   leche

Usuario A sin red:   leche          Usuario B sin red:   leche
                     huevos                              pan

Fusion con un algoritmo que permite intercalar:

                     leche
                     hpuaenvos      <- nadie escribio esto

El caso original del articulo usa eggs y bread y produce ebrgegasd.
Las dos replicas coinciden. El orden total existe. La especificacion
se cumple. Y el resultado es basura.

El artículo documenta con una tabla comparativa hasta qué punto el fenómeno estaba extendido, y el resultado es incómodo para todo el campo: aparecen anomalías de intercalación en los algoritmos de transformación operacional —adOPTed, Jupiter, GOT, SOCT2, TTF— y también en la mayoría de los CRDT de texto —WOOT, Logoot, LSEQ, Treedoc, RGA, Yjs—. No es un defecto de una familia frente a la otra, ni un descuido de un autor concreto. Es lo que ocurre cuando una propiedad deseable no forma parte de los criterios de aceptación: nadie la comprueba, nadie la pierde deliberadamente y todo el mundo la incumple.

La definición de 2019 y su imposibilidad

En 2019, Kleppmann, Gomes, Mulligan y Beresford presentaron en el taller PaPoC el primer trabajo que nombraba el problema en la literatura revisada y proponía una definición formal de no intercalación junto con un algoritmo pensado para satisfacerla. El artículo de Fugue es explícito al evaluar aquel intento: tiene dos defectos graves. El algoritmo propuesto no converge, y existe un contraejemplo concreto de no convergencia que Chandrassery encontró en 2021. Y, mucho más importante desde el punto de vista conceptual, la definición no puede satisfacerla ningún algoritmo.

La definición de 2019 decía, en paráfrasis: si dos conjuntos de elementos X e Y cumplen que todo elemento de X es concurrente con todo elemento de Y, y que la unión de ambos queda contigua en la lista una vez aplicadas sus inserciones y todas sus predecesoras causales, entonces o bien X entero precede a Y entero, o bien al revés. Suena razonable. Es la formalización directa de la intuición de que las ráfagas de cada usuario no deben mezclarse. Y no la cumple nadie, por una razón que cabe en cinco líneas.

Lista vacia. Cuatro replicas insertan un elemento cada una,
todas concurrentes entre si.

El estado final tiene que ser alguna ordenacion de los cuatro.
Digamos que es   a b c d

Tomamos ahora
  X = a y c
  Y = b y d

  todo elemento de X es concurrente con todo elemento de Y   se cumple
  la union de X e Y es contigua en la lista                  se cumple
  luego X va entero antes que Y o al reves                   FALLA

Y falla para cualquier algoritmo, porque cualquier algoritmo
tenia que producir alguna ordenacion de los cuatro elementos.

Conviene detenerse un segundo en dónde exactamente falla el enunciado, porque el error es sutil y de una clase que se repite mucho. La definición cuantifica sobre conjuntos arbitrarios de elementos, y esos conjuntos se pueden elegir después de conocer el resultado. Nada obliga a que X e Y correspondan a ráfagas reales escritas por personas distintas: basta con que sus elementos sean mutuamente concurrentes y queden contiguos, condición que cuatro inserciones simultáneas cumplen trivialmente y en todas sus particiones a la vez. La intuición de partida hablaba de dos usuarios escribiendo dos textos, y la formalización perdió por el camino la única información que hacía la intuición razonable: que cada ráfaga tiene una estructura interna, que cada carácter se insertó junto al anterior. Recuperar esa información es justamente lo que hará la definición de 2023 al hablar de orígenes.

El contraejemplo no ataca a un algoritmo, ataca a la definición: el cuantificador universal sobre conjuntos arbitrarios de elementos concurrentes es demasiado ambicioso, porque permite construir a posteriori dos conjuntos alternados a partir de cualquier orden que el algoritmo hubiera elegido. Una propiedad de corrección que ningún objeto puede satisfacer no es una propiedad exigente, es una propiedad vacía: no separa los algoritmos buenos de los malos, los rechaza a todos por igual y por tanto no aporta ninguna información.

flowchart TD
A[1989 a 2011 se construyen OT y CRDT para texto] --> B[especificacion fuerte de listas, convergencia mas orden total]
B --> C[la intercalacion no viola nada y por tanto es legal]
C --> D[2019 se nombra la anomalia y se propone una definicion]
D --> E[ningun algoritmo puede satisfacer esa definicion]
D --> F[el algoritmo propuesto ademas no converge]
E --> G[2023 no intercalacion maximal, satisfacible y demostrada]
F --> G
style C fill:#f38ba8,color:#11111b
style E fill:#fab387,color:#11111b
style F fill:#fab387,color:#11111b
style G fill:#a6e3a1,color:#11111b

Qué hace utilizable a una propiedad de corrección

Puestas en fila las dos tentativas, se deja leer el criterio que separa una intuición de una propiedad de corrección con la que se pueda trabajar. No es un criterio del artículo, es lo que se deduce de comparar el intento fallido con el que funcionó, y merece la pena tenerlo delante porque se aplica muchísimo más allá de la edición de texto.

El tercer punto es el que explica el fracaso de 2019 y el que más cuesta acertar en la práctica. Una propiedad enunciada sobre conjuntos elegidos a posteriori es siempre sospechosa, porque quien la evalúa puede buscar el conjunto que peor le venga al algoritmo, y en un sistema con concurrencia arbitraria ese conjunto casi siempre existe. Una propiedad enunciada sobre relaciones que quedaron fijadas en el momento de cada operación —quién estaba delante, quién estaba detrás— no admite esa clase de manipulación, porque los objetos sobre los que habla no se eligen: vienen dados por la historia. El cambio de un cuantificador sobre subconjuntos a un cuantificador sobre pares de elementos con una relación registrada es, técnicamente, la diferencia entre las dos definiciones.

El cuarto punto es el que da nombre a todo el nivel y el que la lección siguiente desarrolla en detalle. La palabra maximal no es un adorno retórico ni una promesa comercial: es el reconocimiento explícito de que existen ejecuciones en las que evitar toda intercalación es imposible, y de que la propiedad correcta no es nunca intercalar sino no intercalar más allá de lo que la propia consistencia obliga. Enunciar ese límite dentro de la definición, en vez de dejarlo como una advertencia en el texto, es lo que permite después demostrar teoremas en lugar de acumular casos de prueba.

La forma de la aportación

Con el criterio anterior en la mano, la estructura del artículo de 2023 se lee como lo que es: una aportación en tres piezas encadenadas, donde la primera es la que sostiene a las otras dos. Primero, una definición nueva —la no intercalación maximal— construida para ser satisfacible y compatible con la especificación fuerte de listas. Segundo, dos algoritmos hermanos, Fugue y FugueMax, con la demostración de que FugueMax satisface la definición y la observación de que Fugue, más simple, se queda a muy poca distancia. Tercero, una implementación medida sobre una traza real que muestra que el coste de todo esto es comparable al de la biblioteca más rápida del ecosistema.

Importa también el modelo de sistema en el que todo esto se plantea, porque es exactamente el del track. Cada sesión de usuario mantiene su propia réplica completa de la lista. Las operaciones locales se aplican de inmediato, sin esperar a ninguna comunicación, de modo que la interfaz responde con independencia de la latencia. Si alguien edita sin conexión, su cliente acumula las operaciones y las envía cuando vuelve. La única infraestructura que los CRDT presuponen es un protocolo de difusión causal, que puede construirse entre pares sin servidor central ni consenso, y que se encarga de retransmitir lo que se perdió. La transformación operacional, en cambio, suele apoyarse en un servidor que secuencia y transforma, como hace Jupiter. Esa diferencia de modelo es la razón por la que la última pregunta abierta del artículo —si existe una transformación operacional maximalmente no intercalante— no es una curiosidad académica sino una cuestión con consecuencias arquitectónicas directas.

Merece la pena señalar que el orden de exposición del artículo invierte el orden de importancia, como es habitual: el algoritmo se presenta antes que la definición porque así se lee mejor, pero la contribución que sobrevivirá es la definición. Los algoritmos envejecen y se reemplazan por otros más rápidos. Una propiedad de corrección bien enunciada se convierte en el criterio con el que se juzgan todos los algoritmos posteriores, incluidos los que aún no existen, y en este caso además viene acompañada de un resultado de unicidad que la lección siguiente examina y que la vuelve difícil de superar.