My quest for a principled solution for metastable failures has taken me back to self-stabilization. A recent paper related the problem to composition of self-stabilizing systems, but literature search yielded nothing useful. Layered stabilization was already in place by the early 2000s, and nothing fundamental seems added since.

I attacked the problem using a concrete example: a rely-guarantee TLA+ model of a retry storm as two components with contracts. That model reproduces metastable failure because the composition worked from good states but failed when a large shock removed the base case. Searching for rely-guarantee composition from every state turned up a 2017 control theory paper by Kim, Arcak and Seshia, "A Small Gain Theorem for Parametric Assume-Guarantee Contracts". This paper does roughly what I want: discharging circular reasoning between two components without layering or blocking. But it has serious limitations. A component is an input-output relation on signals, and contracts relate an input bound to an output bound. This memoryless view cannot express backlog accumulating from previous rounds, ruling out queues. It also has no connection to stabilization.

Still, pieces are worth stealing toward a compositional theory of self-stabilization and metastability. Below I try to work this out... somewhat unsuccessfully.

In our original model, the retrier's guarantee was conditional: "if the queue is under 6, I send no retries". The parametric assume-guarantee paper's big idea is to write a family of contracts covering everywhere. Constants: S=3 server capacity, A_max=2 fresh arrivals, T=2 timeout, latency threshold S·T=6. This gives λ(L) = ⌊(L-6)/2⌋. The old contract is the top row: λ(6)=0. Every row gets a promise, so we get a bundle of ordinary contracts, one per badness level p: φ_a = ∨_p ψ_a(p); φ_g = ∧_p (ψ_a(p) ⇒ ψ_g(λ(p))). The assumption side is a disjunction because levels are alternatives. The guarantee side is a conjunction; obligations are cumulative. Rows whose condition is false cost nothing; nested levels mean the tightest wins.