GoKawiilMy 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 Contracts
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.
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.
... continue reading