对抗性共识模拟中的时间语义与活性伪影

中文摘要 AI 辅助

对抗性共识模拟器不仅需要消息传递模型，还需要时间模型。对于超时敏感的协议，将协议时间推进与调度器活动耦合，可能使通信调度影响故障检测器的超时触发。我们使用受控的Multi-Paxos和Raft实验在VeriProtocol中研究这一交互。在主要的Multi-Paxos研究中，我们比较了EventCoupled计时（每次调度器机会都推进协议时间）与RoundTick计时（将单个调度器事件与超时推进解耦）。在N=5时，将有界消息延迟预算从K=6增加到K=14，使得观测到的EventCoupled领导权不稳定率在测试网格上从5%增加到100%，而在对应的140次RoundTick执行中，没有发生任何额外的有效领导者选举。在K=0时，两种模型均未产生额外选举。匹配轨迹分析揭示了机制：在EventCoupled计时下，用于扰动通信的调度器活动也直接推进故障检测器状态。在RoundTick下，相当的调度器活动并不意味着等效的协议时间推进。一项针对性的心跳延迟控制证实，RoundTick不会抑制超时驱动的选举；当领导者联系在足够的逻辑时间内不可用时，额外的选举仍然可达。

英文摘要

Adversarial consensus simulators require not only a model of message delivery but also a model of time. For timeout-sensitive protocols, coupling protocol-time progression to scheduler activity can allow communication scheduling to influence when failure detectors expire. We study this interaction in VeriProtocol using controlled Multi-Paxos and Raft experiments. In the primary Multi-Paxos study, we compare EventCoupled timing, where every scheduler opportunity advances protocol time, with RoundTick timing, which decouples individual scheduler events from timeout progression. At N=5, increasing the bounded message-delay budget from K=6 to K=14 increased the observed EventCoupled leadership-instability rate from 5\% to 100\% across the tested grid, while no additional valid leader elections occurred in any of the corresponding 140 RoundTick executions. At K=0, neither model produced additional elections. Matched-trace analysis identifies the mechanism: under EventCoupled timing, scheduler activity used to perturb communication also directly advances failure-detector state. Under RoundTick, comparable scheduler activity does not imply equivalent protocol-time progression. A targeted heartbeat-delay control confirms that RoundTick does not suppress timeout-driven elections; an additional election remains reachable when leader contact is unavailable across sufficient logical time.

发表机构

• University of California, Merced（加州大学默塞德分校）

机构由 AI 辅助整理，请以论文原文为准。