In Search of a Compositional Theory of Self-Stabilization
2 hours ago
- The author found no useful recent work on composing self-stabilizing systems beyond the early 2000s layered approach.
- They used a rely-guarantee TLA+ model of a retry storm with two components and contracts, which reproduced metastable failure from good states after a large shock.
- A 2017 paper by Kim, Arcak, and Seshia introduced parametric assume-guarantee contracts for circular reasoning without layering, but it is memoryless and cannot model queues or stabilization.
- The parametric approach replaces a single conditional promise with a family of contracts indexed by environment badness, as illustrated by the retrier's lambda(L) function.
- The small gain theorem requires linear components and a single scalar for stability analysis, which fails for systems with multiple queues and nonlinear response.
- Analysis of two queues (fresh and duplicates) yields four slopes: diagonal (memory) and off-diagonal (coupling); the coupling product alone suggests stability, but including memory gives an eigenvalue >1, indicating instability.
- Fixes like retry budgets or fresh-first service zero the coupling and restore stability, while queue caps can bound divergence but lead to metastability at high caps.
- The parametric contracts improved promise specification but did not provide a practical compositional recipe; however, each term in the table originates from a single component, hinting at future composability.