// HACKER NEWS — CYBERSECURITY
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.
In 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.
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:
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_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.