noxaur/verify-design-leases

Verificar concesiones de diseño

crates/server/tla/DesignLeases.tla es un modelo TLA+ de dos servidores Finite que comparten un almacén, y un diseño que se mueve entre ellos. TLC, el verificador de modelos TLA+, prueba cada orden de sus pasos dentro de límites pequeños y verifica dos reglas:

• StoredEditsStay (vallado): una vez que el almacén acepta una edición, ninguna copia obsoleta en otro servidor la sobrescribe nunca. Si esto se rompe, un servidor que se quedó bloqueado se despierta y borra las ediciones que guardó el nuevo propietario.
• AckedEditsStay: una edición que una herramienta MCP informó como realizada está en el almacén, o en una copia que aún puede guardarla, a menos que su servidor se haya estrellado o su concesión haya expirado antes de que la edición se guardara. Si esto se rompe, se le dice a un agente que su edición funcionó, y luego la edición desaparece. Los visores la ven desaparecer, y nada se lo notifica al agente.

El código hoy cumple la primera regla e incumple la segunda de cuatro formas conocidas. Están listadas en "Hallazgos conocidos" más abajo.

¿Tu cambio afecta esto?

Sí, si cambia cualquier función de esta tabla. Cada paso del modelo nombra el código que representa, y un revisor puede abrir ambos lado a lado.

Paso del modelo	Código
CallStarts, CallFindsHandle, CallLoads, CallEdits, CallReads	mcp/mod.rs design, edit_checked; api.rs open; hub/mod.rs Hub::open, handle_for; hub/design.rs DesignHandle::load, edit
SaveTakes, SaveWrites, SaveFenced, SaveFails, SaveReleases, SaveDrops	hub/mod.rs persist; hub/design.rs take_save, save_failed
Unload	hub/mod.rs Hub::sweep; hub/design.rs unload_if_idle, is_idle
TickRenews … TickDiscovers	hub/mod.rs Hub::tick, let_go, remove, drop_copy, discover, summaries; hub/design.rs retire, end, lease
Owns, LeaseLapses, HeartbeatExpires	cluster.rs Members::now, lapsed, renewed, Cluster::owns, owner
CanClaim, Claimed, escrituras del almacén	postgres/mod.rs claim, save, append, release, held; store.rs trait Store (el almacén compartido en memoria debe coincidir)
Start, Crash	hub/mod.rs Hub::shared

Las rutas están bajo crates/server/src/.

Commit de sincronización: 6606714. Ese es el último commit en el que se verificó el modelo contra este código. Para ver qué cambió en el código cubierto desde entonces, ejecuta:

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

Si el diff toca una función de la tabla, vuelve a leer el paso del modelo que está a su lado antes de confiar en una aprobación. Adelanta el commit de sincronización, en este archivo, solo después de haber confirmado que cada paso modificado sigue coincidiendo con el código en el nuevo commit.

Ejecutarlo

crates/server/tla/check.sh          # la verificación diaria, unos 2 minutos
crates/server/tla/check.sh --full   # añade Finding4.cfg y AllFixes.cfg, unos 3 minutos más

El script descarga TLC (tla2tools.jar v1.7.4, con verificación SHA-256) en ~/.cache/finite la primera vez que se ejecuta. Necesitas Java 11 o superior. Cada configuración imprime ok cuando da el resultado registrado para el código actual, y FAIL en caso contrario. Cuando una regla se rompe, la salida de TLC, con la ruta más corta hasta la rotura, se guarda como crates/server/tla/<config>.out. Git ignora esos archivos.

Configuración	Correcciones activas	Límites	Resultado actual
Fencing.cfg	ninguna	1 edición, 1 lectura, 2 manejadores, todo comportamiento hasta 18 pasos	pasa, aprox. 2.8M estados, 2 minutos
DesignLeases.cfg	ninguna	1 edición, 2 manejadores	hallazgo 1, segundos
Finding2.cfg	FixRetire	1 edición, 2 manejadores	hallazgo 2
Finding3.cfg	FixRetire, FixOrphan	2 ediciones, 2 manejadores	hallazgo 3
Finding4.cfg	+ FixStaleDrop	2 ediciones, 2 manejadores	hallazgo 4, aprox. 1 minuto
AllFixes.cfg	las cuatro	2 ediciones, 2 manejadores	pasa, aprox. 16M estados, 2 minutos

Cada configuración limita la época del almacén a 3, y ninguna incluye un bloqueo o una escritura fallida. Una lectura es una llamada que carga el diseño sin editarlo, como una herramienta de lectura MCP o el socket de un visor. El vallado necesita una, porque una copia obsoleta solo puede existir cuando dos llamadas han cargado el diseño. Su espacio de estados completo con esa lectura no terminó en 30 minutos, por lo que check.sh lo ejecuta con profundización iterativa de TLC (-dfid 18): todo comportamiento de hasta 18 pasos. La sobrescritura obsoleta más corta toma 17. Las configuraciones de hallazgo exploran todo dentro de sus límites. TLC se detiene en la primera regla rota, por lo que cada configuración de hallazgo activa las correcciones propuestas para los hallazgos anteriores. Las constantes Fix* son conmutadores hipotéticos. Con todas ellas en FALSE, el modelo es el código tal como es hoy.

Leer el resultado

Lee cada resultado con el skill /statechart. Convierte la ruta más corta de TLC hacia una regla rota en una lista numerada de pasos en lenguaje sencillo, y cuando una configuración pasa, dibuja un gráfico de cómo se mueve el diseño entre servidores.

Cuando una configuración imprime FAIL, decide si el error está en el código o en el modelo:

• Un error real da una ruta que puedes reproducir en el código. Recorre cada paso, abre la función de la tabla y comprueba que el código permite ese paso en ese orden. Luego informa la ruta en las palabras del código, como hacen los hallazgos más abajo. No debilites una regla o un límite hasta que la verificación pase, y no cambies el código del producto a menos que se te haya pedido.
• Un error de modelado da un paso que el código no puede dar. Ejemplos: dos pasos que el código ejecuta bajo un mismo bloqueo (el mutex de estado, el mutex de persistencia), separados en el modelo; un paso del modelo sin una guarda que el código tiene; o un latido que expira justo después de una renovación. Corrige el modelo para que coincida con el código y di qué arreglaste.
• Una rotura de Fencing.cfg proviene de la ejecución con límite de profundidad, cuya ruta no nombra sus pasos. Para obtener una ruta más corta nombrada, ejecuta la misma configuración en anchura: cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla. Se detiene en la primera rotura, lo que llevó unos 6 segundos para la rotura bajo "Cuando cambias el código cubierto a propósito".
• error significa que TLC no terminó: un error de análisis sintáctico, o una variable que una acción deja sin asignar. Lee el archivo .out.

Un FAIL donde el código solía romper la regla y ahora pasa es una buena noticia. La tabla de hallazgos bajo "Hallazgos conocidos" muestra cómo registrarlo.

Cuando cambias el código cubierto a propósito

1. Cambia el paso del modelo en el mismo commit que el código y mantén el comentario que nombra la función.
2. Si tu cambio corrige un hallazgo, pon la corrección en el modelo como código, no como un conmutador: elimina la constante Fix*, haz que el paso se comporte como el nuevo código, y elimina el conmutador de cada configuración. La configuración del siguiente hallazgo se convierte en la configuración por defecto, y check.sh obtiene los nuevos resultados esperados.
3. Antes de confiar en una aprobación, rompe el código a propósito en una copia de prueba, refleja la rotura en el modelo y verifica que la configuración la detecta. Por ejemplo, si eliminas AND epoch = $3 de PgStore::save y eliminas x.ptok = store.epoch de SaveWrites, Fencing.cfg rompe StoredEditsStay. Una verificación que nunca has visto fallar no prueba nada.
4. Ejecuta check.sh --full, luego adelanta el commit de sincronización.

Hallazgos conocidos

Cada uno es una condición de carrera en el código en 6606714. En cada una, la llamada a la herramienta del agente devuelve éxito y la edición desaparece.

1. Una edición cae en una copia que ya está guardando su última instantánea. El servidor A tiene el diseño cargado, y una llamada MCP ha pasado Hub::open. El servidor B se une y gana el diseño (una concesión caducada en A también lo hace). El tick de A llama a let_go, por lo que retire marca la copia como Retiring. La tarea de guardado take_save toma la última instantánea. Luego la llamada DesignHandle::edit toma el bloqueo y confirma en la copia retirada, porque edit nunca mira life. La tarea de guardado guarda la instantánea sin la edición, libera la concesión, y drop_copy limpia pending. B carga el diseño sin la edición. Para provocarlo en la aplicación real, las ediciones ya deben estar esperando el bloqueo del diseño cuando se ejecute el tick, por ejemplo, varios agentes ejecutando grandes llamadas write_html. Deshacer, rehacer, importar y actualizar comentarios toman el mismo camino.
2. Una edición cae en un manejador que el hub ya eliminó de su lista. La handle_for de una llamada devuelve un manejador que no está cargado. B se une, y el let_go de A no ve nada cargado, por lo que llama a remove. La llamada load reclama la concesión y carga una copia en ese manejador. La lista loaded del siguiente tick proviene de la lista del hub, que ya no tiene este manejador. Por lo tanto, el tick libera la concesión, y el siguiente guardado de la copia falla con Fenced. Esto no necesita un bloqueo, solo que un servidor se una.
3. El tick descarta una copia que fue cargada de nuevo después de que el tick la leyera. Un servidor, sin cambios de membresía. El tick lee lease() (token 1). Luego el diseño se descarga, y una llamada lo carga de nuevo (token 2) y confirma una edición. El tick lee held() (token 2), ve que 2 ≠ 1, y llama a drop_copy. drop_copy finaliza la nueva copia, edición pendiente incluida. La ventana está entre dos lecturas, por lo que es estrecha, pero se ejecuta en cada tick.
4. Un servidor que acaba de renovar su concesión sirve su copia obsoleta. B se bloquea más allá de su concesión, A toma el control del diseño y guarda una edición. B se despierta. Su tick renueva el latido, y desde ese momento Members::now cuenta a B como vivo y nuevamente el propietario. Pero el bucle let_go aún no se ha ejecutado. Una llamada en B carga la copia obsoleta aún Live y confirma una edición, que luego falla con Fenced. Primero necesita un bloqueo.

AllFixes.cfg verifica una corrección propuesta para cada hallazgo: edit rechaza una copia que no esté Live (1) o un manejador que no esté listado (2). El tick descarta una copia solo si su token es el que leyó (3). Un servidor que renovó después de un lapso se cuenta a sí mismo fuera hasta que haya soltado (4). Con las cuatro, AckedEditsStay se cumple en estos límites.

Lo que esto no cubre

• Un diseño, dos servidores, ediciones MCP. Deshacer, rehacer, importar, comentarios y renombrar toman el mismo camino de bloqueo y confirmación pero no se modelan por separado. Tampoco Hub::delete.
• El almacén de archivos y las transferencias de FINITE_NODES (hand_off_one, adopt), y el enrutador.
• Hub::flush al apagar, los umbrales de compactación del diario (COMPACT_AFTER, COMPACT_BYTES), y Recent, el búfer detrás de la reanudación del visor.
• Tiempo. TLC prueba cada orden de pasos, por lo que el modelo muestra que existe una carrera, no con qué frecuencia ocurre. Asume que el temporizador de concesión propio de un servidor (Members::lapsed) se agota a más tardar cuando la base de datos considera su latido como expirado. Eso se cumple cuando los dos relojes funcionan a la misma velocidad.
• Límites mayores. Más ediciones, lecturas, manejadores o épocas, bloqueos y escrituras fallidas no están en las configuraciones diarias. AllFixes.cfg también pasó con 1 edición, 1 bloqueo y 1 escritura fallida (3.4M estados). El vallado más allá de 18 pasos no ha terminado: con 1 edición y 1 lectura pasó 50M estados distintos y aún continuaba. No confíes en una aprobación de vallado anterior sin lectura: una sola edición carga solo una copia, por lo que nada puede quedar obsoleto.