Adversarial consensus timing models affect leader election stability
Time Semantics and Liveness Artifacts in Adversarial Consensus Simulation
Distributed, Parallel, and Cluster Computing
Summary
In systems where multiple computers try to agree on something, timing matters a lot. The authors studied how different ways of measuring time inside a simulation can make leader changes happen more or less often. They found that one timing method causes more instability because it ties protocol time closely to how the system schedules messages. Another method separates these, leading to fewer unnecessary leader changes. This helps to better understand how simulated timing can affect testing of consensus protocols.
What this means in practice
- •For distributed systems engineers: Improve reliability testing of leader election by choosing timing models that avoid false positives in failure detection during simulations.
- •For network reliability teams: Use insights on message timing and failure detection coupling to better design timeout settings for stable leader election under variable network delays.
Authors
Nasit S Sony, Xianzhong Ding
Abstract
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.