Minha busca por uma solução baseada em princípios para falhas metaestáveis me levou de volta à autoestabilização. Um artigo recente relacionou o problema à composição de sistemas autoestabilizantes, mas a busca na literatura não rendeu nada útil. A estabilização em camadas já estava em vigor no início dos anos 2000, e nada fundamental parece ter sido adicionado desde então.

Atacei o problema usando um exemplo concreto: um modelo TLA+ de rely-guarantee de uma tempestade de retentativas como dois componentes com contratos. Esse modelo reproduz a falha metaestável porque a composição funcionava a partir de bons estados, mas falhava quando um grande choque removia o caso base. Procurando a composição rely-guarantee a partir de cada estado, encontrei um artigo de teoria de controle de 2017 de Kim, Arcak e Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts". Este artigo faz aproximadamente o que quero: descarregar o raciocínio circular entre dois componentes sem camadas ou bloqueio. Mas tem sérias limitações. Um componente é uma relação de entrada-saída sobre sinais, e os contratos relacionam um limite de entrada a um limite de saída. Essa visão sem memória não pode expressar o backlog acumulado de rodadas anteriores, excluindo filas. Também não tem conexão com a estabilização.

Ainda assim, há peças que valem a pena roubar para uma teoria composicional da autoestabilização e metaestabilidade. Abaixo tento elaborar isso... com algum insucesso.

Em nosso modelo original, a garantia do retentador era condicional: "se a fila estiver abaixo de 6, não envio retentativas". A grande ideia do artigo paramétrico de suposição-garantia é escrever uma família de contratos cobrindo todos os lugares. Constantes: S=3 capacidade do servidor, A_max=2 novas chegadas, T=2 tempo limite, limite de latência S·T=6. Isso dá λ(L) = ⌊(L-6)/2⌋. O contrato antigo é a linha superior: λ(6)=0. Cada linha recebe uma promessa, então obtemos um pacote de contratos comuns, um por nível de maldade p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). O lado da suposição é uma disjunção porque os níveis são alternativas. O lado da garantia é uma conjunção; as obrigações são cumulativas. Linhas cuja condição é falsa não custam nada; níveis aninhados significam que o mais restrito vence.

Entidades-chave: Pessoas: Kim, Arcak, Seshia