In Search of a Compositional Theory of Self-Stabilization
2 hours ago
- 作者发现，除了2000年代初的分层方法之外，没有关于组合自稳定系统的有用近期工作。
- 他们使用了依赖-保证TLA+模型，带有两个组件和契约，用于重试风暴，该模型在大冲击后从良好状态重现了亚稳态故障。
- Kim、Arcak和Seshia在2017年发表的一篇论文引入了参数化假设-保证契约，用于无需分层的循环推理，但它是无记忆的，无法对队列或稳定化进行建模。
- 参数化方法用一个由环境恶劣程度索引的契约族替换单个条件承诺，如重试器的lambda(L)函数所示。
- 小增益定理要求线性组件和单个标量用于稳定性分析，这对于具有多个队列和非线性响应的系统会失效。
- 对两个队列（新消息和重复消息）的分析产生四个斜率：对角线（内存）和非对角线（耦合）；仅耦合乘积表明稳定性，但包括内存后特征值>1，表明不稳定。
- 诸如重试预算或优先处理新消息之类的修复措施将耦合置零并恢复稳定性，而队列上限可以限制发散，但在高上限时会导致亚稳态。
- 参数化契约改进了承诺规范，但没有提供实用的组合方法；然而，表中的每一项都源自单个组件，暗示了未来的可组合性。