In Search of a Compositional Theory of Self-Stabilization

My literature search for recent work on composing self-stabilizing systems didn't yield anything useful. The layered stabilization idea was already in place by the early 2000s, and nothing fundamental seems to have been added since. Frustrating.So I decided to attack the problem using the concrete example I have. I had composed a rely-guarantee TLA+ model of a retry storm as two components with contracts. That model reproduces metastable failure because the composition that worked from good states failed to work when a large shock removes the base case that let the two conditions hold each other up.Searching for  rely-guarantee based 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 comes with some serious limitations. In their formalism, a component is an input-output relation on signals, and contracts relate an input bound to an output bound. This is a memoryless view of a component, so it is not possible to express backlog accumulating from previous rounds. That rules out queues, among other useful distributed systems concepts. It also has no connection to stabilization. The paper does not talk about a variant/potential function and convergence reasoning. But there are still pieces there worth stealing toward a compositional theory of self-stabilization and metastability. Below I try to work this out... somewhat unsuccessfully.Understanding Parametric Assume-Guarantee ContractsIn our original model, the retrier's guarantee was conditional and partial: "if the queue is under 6, I send no retries". This contract does not say anything about when the queue is at 18. Since the "if" condition fails, the promise is vacuously satisfied and the component owes us nothing.The parametric assume-guarantee paper's big idea is to write a whole family of contracts that cover everywhere, rather than writing one promise with a precondition.Tired: If the queue is under 6, no retries.Wired: Whatever the queue length $L$ turns out to be, I send at most $\lambda(L)$ retries.Recall that my constants from the model are $S=3$ units of server capacity per round, $A_{max}=2$ maximum fresh arrivals per round, and a retry timeout of $T=2$ rounds, which makes the latency threshold $S \cdot T = 6$. This makes $\lambda(L) = \lfloor (L-6)/2 \rfloor$, which gives us: if the queue is at most... ...I send at most this many retries 6 0 8 1 10 2 12 3 14 4 16 5 18 6 The old contract is still in there, as the top row: $\lambda(6)=0$ says "queue under 6 means at most zero retries". Although the old contract is invalid at queue length of 18, under the parametrized assume-guarantee approach every row of the table gets a promise. So we get a bundle of ordinary contracts, one per badness level $p$:$$\varphi_a = \bigvee_p \psi_a(p)$$$$\varphi_g = \bigwedge_p \left( \psi_a(p) \Rightarrow \psi_g(\lambda(p)) \right)$$The assumption side, $\varphi_a$, is a disjunction because the levels are alternatives. The environment will be at one of them, whichever one it happens to be. "Queue at most 6, or at most 8, or at most 10, or..." is satisfied by essentially any environment, so there is no envelope left to fall outside of.The guarantee side, $\varphi_g$, is a conjunction over the same levels. Since the obligations are cumulative, we owe all of them at once. Rows whose condition is false cost us nothing, and since the levels are nested, several apply at once and the tightest wins. When queue is at 7, "at most 8" applies, and the component owes us at most 1 retry; "at most 10" also applies and it also owes us at most 2, but the first case already implies that. Monotonicity becomes key here.Deriving the Small Gain RuleWhat is the rule that says when such a loop settles? The paper calls this the small gain theorem. Let me start by explaining the intuition.You have seen this happen, right? When a microphone gets in front of a speaker, the mic picks up sound, and the amp boosts it. The speaker plays this back, which the mic picks it up again. Each lap around that loop multiplies the sound, and you hear a high pitched squeal. To quantify this process we need one number per component: how much badness out per unit of badness in. That is the slope of the component's response function, and control theory calls it the component's gain.When we chain the two components, and feed a nudge $x$ into the first, slope $g_1$, and $g_1 x$ comes out. When we feed that into the second, slope $g_2$, and $g_2 g_1 x$ comes out. One lap has multiplied the nudge by $g_1 g_2$. After $k$ laps the nudge is $(g_1 g_2)^k$ times its original size.