Verifying Non-Deterministic Convergence on a Global Production WAN

Abstract

This paper presents our experience deploying TianYan on Alibaba Cloud's global production WAN, which is, to the best of our knowledge, the first system for verifying non-deterministic convergence on a global production WAN. In daily operation, we rely on simulation-based configuration verifiers that assume a single converged data plane to ensure reliability and performance. However, non-deterministic convergence—where a configuration yields different converged data planes—undermines verification accuracy and has caused a production incident, motivating the need to analyze non-deterministic convergence itself. At scale, this is challenging because the analysis space grows exponentially with the number of routers. TianYan addresses this challenge with a key insight: by leveraging routing similarity among routers within the same group—a common fault-tolerance practice—it reduces exponential complexity from the number of routers to the number of groups, enabling efficient convergence analysis. Over a year of deployment, TianYan identified non-deterministic convergence in ~2% of all prefixes, exposed unnoticed design flaws, and improved simulation-based verification accuracy through integration. We share representative cases and evaluation results from our production WAN, distilling key operational lessons and practical guidelines for managing nondeterminism at scale.