In Search of a Compositional Theory of Self-Stabilization

This explores building a compositional theory of self-stabilization by attacking a concrete retry-storm example rather than relying on layered stabilization. A parametric assume-guarantee idea from control theory (Kim, Arcak, Seshia, 2017) is repurposed: instead of a conditional promise ("if queue ≤6 then zero retries") the component promises a family of bounds λ(L) on retries for every queue level L, turning assumptions into a disjunction over levels and guarantees into a conjunction that enforces monotone obligations. That approach recovers some circular-discharge reasoning without layering but fails to capture stateful components: it treats components as memoryless input-output relations, so queues, backlog accumulation, and convergence proofs via potential functions remain out of scope.

Applying linear analysis to a concrete system with S=3, Amax=2, T=2 (latency threshold 6) uncovers a nontrivial fixed point at (f,d)=(8,4). Linearization yields per-unit effects: f→f=11/12, f→d=7/12, d→f=1/6, d→d=5/6. A small-gain check on the coupling terms (7/12·1/6≈0.10) would predict stability, but including the diagonal “memory” terms produces eigenvalues whose larger root is ≈1.19, so disturbances grow. Practical mitigations - retry budgets, fresh-first service, or tight caps - suppress coupling and restore decay; loose caps only bound divergence and cause metastable high-backlog equilibria. The lesson: compositional self-stabilization must handle memory and multi-dimensional badness, not just scalar, memoryless gains.