Mi búsqueda de una solución basada en principios para los fallos metaestables me ha llevado de vuelta a la autoestabilización. Un artículo reciente relacionó el problema con la composición de sistemas autoestabilizantes, pero la búsqueda bibliográfica no arrojó nada útil. La estabilización por capas ya estaba en su lugar a principios de la década de 2000, y no parece haberse añadido nada fundamental desde entonces.

Atacé el problema utilizando un ejemplo concreto: un modelo TLA+ de rely-guarantee de una tormenta de reintentos como dos componentes con contratos. Ese modelo reproduce el fallo metaestable porque la composición funcionaba desde estados buenos pero fallaba cuando un gran shock eliminaba el caso base. Buscando la composición rely-guarantee desde cada estado, encontré un artículo de teoría de control de 2017 de Kim, Arcak y Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts". Este artículo hace aproximadamente lo que quiero: descargar el razonamiento circular entre dos componentes sin capas ni bloqueo. Pero tiene serias limitaciones. Un componente es una relación de entrada-salida sobre señales, y los contratos relacionan un límite de entrada con un límite de salida. Esta visión sin memoria no puede expresar la acumulación de trabajo pendiente de rondas anteriores, lo que descarta las colas. Tampoco tiene conexión con la estabilización.

Aun así, hay piezas que vale la pena robar hacia una teoría composicional de la autoestabilización y la metaestabilidad. A continuación intento elaborar esto... con cierto fracaso.

En nuestro modelo original, la garantía del reintentador era condicional: "si la cola está por debajo de 6, no envío reintentos". La gran idea del artículo paramétrico de asunción-garantía es escribir una familia de contratos que cubran todas partes. Constantes: S=3 capacidad del servidor, A_max=2 llegadas nuevas, T=2 tiempo de espera, umbral de latencia S·T=6. Esto da λ(L) = ⌊(L-6)/2⌋. El contrato antiguo es la fila superior: λ(6)=0. Cada fila obtiene una promesa, así que obtenemos un paquete de contratos ordinarios, uno por nivel de maldad p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). El lado de la asunción es una disyunción porque los niveles son alternativas. El lado de la garantía es una conjunción; las obligaciones son acumulativas. Las filas cuya condición es falsa no cuestan nada; los niveles anidados significan que gana el más estricto.

Entidades clave: Personas: Kim, Arcak, Seshia