Title: Verifying Non-Deterministic Convergence on a Global Production WAN
Authors: Xing Fang (Xiamen University); Fangdan Ye, Yifei Yuan (Alibaba Group); Zhongyu Guan (Alibaba Cloud); Duncheng She (Alibaba Group); Xiaobo Zhu (Alibaba Cloud); Qiao Xiang (Xiamen University)
Reviewer: Xing Fang (SNG fifth-year PhD student)
Introduction
This paper presents TianYan, a production system that verifies whether routing protocols can converge to more than one stable state. It has operated in Alibaba Cloud’s global WAN for over a year and analyzes roughly two million prefixes every day. Unlike a traditional tool that simulates one routing convergence, TianYan asks whether the same configuration and route inputs admit other stable data planes and locates the policy-dependency cycles that cause the difference. In production, it found approximately 40,000 non-deterministic prefixes, about 30,000 of which could cause the existing simulator to produce a result inconsistent with the live network.
Large networks commonly use simulation to validate configuration changes. A tool reads the topology, routing configuration, and input routes, executes a protocol model to obtain one converged data plane, and checks properties such as reachability and link load. This approach is scalable, interpretable, and widely used in production, but it relies on a critical assumption: for a given input, the control plane converges to a single stable outcome.
Policy-rich routing does not always satisfy that assumption. Routers may prefer paths through one another and form a preference-dependency cycle. The network can still settle, but the message arrival order may lead it to different stable data planes. A simulator usually produces only one of them. If the production network converges to another, property checks performed on the simulated state may produce an incorrect conclusion.
The paper illustrates the problem through a simplified real incident. Four router groups connect three autonomous systems, and one prefix has two stable data planes. The simulator reached DP1, which met both reachability and capacity requirements, so the configuration was approved. After several routers restarted, the production network instead converged to DP2. All affected traffic detoured through links attached to group C, overloading them and reducing throughput while increasing latency. Postmortem analysis identified the topology as a DISAGREE instance of the Stable Paths Problem (SPP).
Figure 1: The same configuration and route inputs can produce stable data planes DP1 and DP2; DP2 detours traffic and overloads selected links.
Alibaba Cloud had previously used SPP and SMT in its simulation-based verifier, Hoyan, to detect this problem, but the method handled only around one hundred routers and ten thousand prefixes. As the WAN grew to roughly one thousand routers, one hundred thousand links, and millions of prefixes, path enumeration and solving became prohibitively expensive, and the feature was disabled. Existing pure-SMT, graph-abstraction, and model-checking approaches also struggle to combine WAN-scale performance, routing-policy expressiveness, and complete analysis.
Core Ideas and Contributions
The fundamental obstacle is the path space. For every prefix, a standard SPP model must enumerate all permitted paths and their preference relationships. In a network with m × n routers, the upper bound on simple paths reaches O((mn)!). Even when the instance can be constructed, asking an SMT solver to find multiple stable solutions adds unacceptable computational cost.
The authors observe that production WANs organize routers into groups by role and location for reliability and automated management. Devices in the same group typically use common configuration templates and similar policies and are expected to choose next hops from the same group. TianYan abstracts this operational practice as routing similarity: in every stable state, routers in the same group choose next hops that belong to the same group.
Under this assumption, TianYan applies two sufficient pruning conditions. First, among multiple concrete paths sharing the same group path, at most one can appear in a stable state. Second, a path that traverses the same router group more than once cannot be stable. These conditions reduce the upper bound on candidate paths to a fixed destination from O((mn)!) to O(n!), where each group commonly contains around ten routers. If routing similarity holds, the pruned SPP and the original instance have the same stable solutions, but the pruned model is far smaller.
Configuration similarity does not theoretically guarantee routing similarity. Alibaba Cloud validates the assumption empirically through template-based configurations, daily simulation, and observed next-hop behavior, trading absolute correctness for production-scale performance. TianYan is therefore not an unconditional general-purpose solver; it actively exploits regularity in the network’s design to shrink the verification space.
TianYan consists of a path generator, convergence analyzer, and root-cause localizer connected to the existing simulation-based verifier. It reads the same topology, configurations, and route inputs and outputs non-deterministic prefixes, related routers, and policy-dependency cycles. Operators then use these results either to repair routing policy or to align the simulated state with the observed production data plane.
Figure 2: TianYan’s three-stage architecture and its relationship with the existing simulation-based verifier and production data plane.
Path generation. A conventional protocol simulation advertises only the current best route to a neighbor and therefore cannot construct a complete SPP instance. TianYan modifies the simulation so that routers continue advertising received candidate paths while immediately applying the two group-path pruning rules. This design reuses the production verifier’s BGP policy parsing and execution without first enumerating every path. It also preserves the required candidate relationships for configurations such as ADD-PATH that advertise multiple routes.
Convergence analysis. TianYan first applies Greedy+, a polynomial-time check that quickly proves unique convergence for many prefixes. Because it is a sufficient rather than complete condition, its unresolved set contains a small number of false positives. TianYan sends those suspicious prefixes to 2-SMT: the solver finds one stable solution, blocks it, and solves again. A second satisfiable result proves that at least two stable data planes exist, while an unsatisfiable result confirms unique convergence. Combining a fast filter with complete solving confines the expensive SMT step to a small fraction of prefixes.
Root-cause localization. For an instance with multiple confirmed solutions, TianYan builds a preference-dependency graph among unstable nodes and their stable alternative paths, then uses DFS to find dispute wheels. An even-length dependency wheel can produce multiple stable convergence outcomes. The system then compares local preference, weight, AS-PATH, MED, Origin, and other attributes along the wheel and reports the devices, paths, and policy differences to operators.
Figure 3: The complete workflow, from pruned SPP construction to Greedy+ and 2-SMT analysis, root-cause localization, and either policy repair or simulator alignment.
Production optimization and verifier integration. Tens of thousands of suspicious prefixes are often caused by a small number of common dispute wheels. TianYan groups prefixes by root-cause set, reducing roughly ten thousand SMT analyses to about one hundred representative groups. Operators remove straightforward cycles with route filters or policy changes. When immediate repair is impractical, TianYan controls route-announcement order in the simulation to reproduce the observed data plane, so subsequent property checks apply to the current production state. This alignment cannot predict a not-yet-deployed configuration, so for a proposed update TianYan instead reports the affected prefixes and dispute wheels for operator risk assessment.
The system has explicit boundaries. It may miss stable states that violate the routing-similarity assumption. It currently excludes several thousand management prefixes whose group paths still explode, and it does not fully model time-dependent policies, inter-protocol redistribution, route aggregation, or arbitrary multi-link failures. These limitations need to be interpreted together with the system’s verification results.
Experimental Evaluation
TianYan’s offline evaluation runs on one server with 96 logical cores and 754 GB of memory. A daily analysis of approximately two million prefixes takes about 14 hours, with path generation and Greedy+ filtering accounting for most of the runtime. After pruning, SPP path generation completes within one second for most prefixes. Greedy+ and root-cause localization require less than 100 milliseconds for the majority, while the relatively few 2-SMT cases take seconds to minutes. A baseline that advertises as many paths as possible not only creates larger instances but also misses about half of the non-deterministic prefixes because of path explosion.
After more than a year in Alibaba Cloud’s global WAN, TianYan has found about 40,000 non-deterministic prefixes—roughly 2% of two million—and most of them carry production traffic. Without TianYan’s simulation alignment, around 30,000 prefixes could be simulated to an outcome different from the live network. The system groups these cases into about 100 distinct dispute-wheel root causes. Every reported wheel was validated against production data, while the complete SMT phase eliminated three false positives left by Greedy+.
Figure 4: Three representative scenarios found by TianYan in the production WAN, involving RR–BR, RR–CR, and ER–CR interactions.
The production cases show that the problem usually comes not from a complex protocol defect, but from a cycle created by several local configuration decisions. Common patterns include unconditionally de-preferencing routes when weight is omitted for selected neighbors, unconditionally preferring another router group for capacity or egress-location reasons, and two groups becoming mutually preferred through configuration evolution. Among two-node dispute wheels, local preference/weight paired with the same attribute family affects 61.6% of prefixes, while pairing it with AS-PATH length affects another 35.0%. Anycast prefixes are also disproportionately represented because announcements from multiple locations make preference cycles more likely.
Deployment also exposes a practical tradeoff between repair and risk. Removing some cycles would require network-wide changes to many route reflectors, and the change risk can exceed the impact of occasional detours for non-critical traffic. Operators therefore enforce deterministic behavior first for business-critical prefixes and temporarily use simulation alignment for some low-impact legacy policies. The paper recommends recording fine-grained preference intent and avoiding unconditional and mutual-preference patterns early in network design and configuration evolution.
Q&A
Q1: If a link failure partitions the network, routers in the same group may choose next hops from different groups. Would the groups need to be recomputed, and how does TianYan handle this form of link resilience?
A1: We have not yet considered this issue systematically. A network partition can indeed violate intra-group routing similarity, invalidating the assumption used by TianYan’s pruning. This is a current limitation. The paper also identifies link-failure analysis and validation of routing similarity under failures as future work.
Personal thoughts
What surprised us most after deploying TianYan was that non-deterministic convergence is not a corner case caused by a few unusual policies. It affects about 2% of prefixes in the production WAN, making the risk of relying on a single simulated outcome far more widespread than we had expected.
We also learned that identifying a configuration problem does not mean operators will fix it immediately. Some issues are rooted in network-wide policies accumulated over years, so repairing them requires broad, risky changes. For low-impact, non-critical traffic, temporarily aligning the simulator or continuing to monitor the issue can be more prudent than an immediate fix.
More concerningly, many prefixes had already converged to unintended states without triggering an alarm from the existing verifier. The main reasons were not insufficient expressiveness, but incomplete fine-grained intent and coarse consistency checks between simulated and live states. This made us realize that verifying the state produced by a simulator is not enough; we must also remain aware of what the verification process itself cannot see.