Configuration Migration Planning through Decoupled Modeling and Searching

Configuration Migration Planning through Decoupled Modeling and Searching Dan Wang1,2 , Peng Zhang1 , and Ratul Mahajan2 1 Xi’an Jiaotong University

arXiv:2610.13161v1 [cs.NI] 9 Oct 2026

2 University of Washington

Abstract

Operational Preferences Planner Framework

Executing large network configuration changes, called migrations, is slow and error-prone today; operators must manually devise a safe order for updating devices that does not disrupt traffic and meets operational intents (e.g., low total time). We develop S MOOTHIE, a versatile migration planning framework that, unlike existing tools, can support diverse operational intents. Inspired by automated planning, it achieves versatility by decoupling the encoding of network safety and intents from the search for a viable plan. S MOOTHIE uses symbolic simulation for general and scalable safety encoding, after which it can use a range of planners, including existing off-the-shelf planners and a new one we developed for optimized parallel plans. We demonstrate S MOOTHIE’s versatility and benchmark its performance using diverse migration scenarios on many topologies. It finds both sequential plans and parallel plans, and the parallel ones compress up to thousands of configuration updates into no more than 3 steps. Its versatility does not come at the expense of performance: finishing most planning tasks in less than 1 hour.

1

-

+ +

Initial Config & Updates Safety Properties

Symbolic Simulator shortcut

Modeling

x.pddl

Problem Description

Planner A

Sequential Plan

Planner B

Optimal Plan

Planner C

Parallel Plan

…… …… Others

Other Plan

Searching

Any/No Plan

Figure 1: A decoupled framework for automated configuration migration planning. Beyond safety, operators may have diverse intent when planning a migration. For most of cases, they may just want to find a safe sequence as soon as possible, and therefore a sequential plan is enough. Besides this, operators may require or prefer one update should take place before or after another. In such cases, a sequential plan should not only be safe, but also satisfy some hard constraints and as many soft constraints as possible; we term such a plan as an optimal plan. Finally, operators of large-scale networks may desire a faster migration process, and therefore a parallel plan, where a set of updates can be executed in parallel [36], is more preferred. Despite the dual requirements on safety and diversity, today’s configuration migration planning (CMP) is still mostly a manual effort. This is not only time-consuming but also error-prone. For one example, a content service provider (§2) reported that manual planning typically took a month or even longer. Even after careful planning, a plan may still contain errors, which after deployment, take down a production network. For another, 56% of the disruptive customer-impacting incidents in Alibaba during 2016-2017 are due to configuration migration [31]. Recently, several tools have been proposed to automate the planning of configuration migration [9, 10, 43]. At a high level, these tools use specific search strategies and customized network simulators to find a feasible sequence of updates. For example, Snowcap [43] chooses one update each round, in-

Introduction

Modern networks are constantly evolving with large-scale configuration change [30, 46, 56, 58], e.g., moving from iBGP full mesh to route reflection, merging two networks, and changing the routing protocol from OSPF to BGP. Planning such large-scale changes, termed migrations, is highly demanding [30]. First, safety is the top concern: since a migrations can be highly risky, e.g., affecting hundreds and even thousands of devices, the order of updates must ensure that the network is always in a safe state. For example, before turning down a link, operators need to ensure the traffic has been shifted to another path, in order to not disrupt the live traffic. For another example, changing BGP configurations requires extreme carefulness to not introduce transient or persistent property violations, e.g., forwarding loops, blackholes (see §2). 1

crementally simulates the update, and validate the safety of the resultant state, until all updates have been applied. Different from Snowcap which validates the safety on the fly, SafeMigration [10] and Cursor [9] use symbolic simulation to pre-identify all safe or unsafe intermediate states, and then either invoke SMT solvers or analyze the partial orders of updates to search for a plan. These planners target at finding sequential plans, but fall short for finding optimal plans and parallel plans. Also, they are faced with efficiency issues [10], do not scale to large number of states [43], or are incomplete [9]. In this paper, we seek a principled treatment of migration planning. Specifically, we draw inspiration from the mature research direction of automated planning (AI planning), a subfield of artificial intelligence on automated synthesis of action sequences (i.e., plans). In automated planning, a planning task [32, 45, 51]) is executed in two phases: (1) a domainspecific problem modeling phase which models the problem in a standardized language, e.g., Planning Domain Description Language (PDDL) [20], and (2) a domain-independent plan searching, which finds a plan satisfying the model. Such a decoupled workflow offers great flexibility, e.g, they can mix-n-match options that work best for their situation, add new preferences without needing to change the search strategy, or pick a different search strategy without needing to change the problem model. Inspired by automated planning, we propose a framework for automated migration planning. As shown in Figure 1, the framework features the decoupling of problem modeling and plan searching. In the problem modeling phase, we identify the condition for an update to be safe, and encode the problem in the PDDL language [2]. This allows us to call different backend planners for different planning tasks. Realizing this framework is challenging. Particularly, supporting diverse planning tasks means that we need to identify all safe intermediate states, to ensure the searching phase can find update plans that visit only safe states; find the one with the minimum cost (for optimal plan); or identify a set of updates whose order does not matter (for parallel plan). Clearly, using a concrete simulator such as Batfish [14], is not realistic: given n updates, we will have to simulate up to 2n states 1 . Making the simulation incremental, as in Snowcap [43], offer limited help, as will be shown in §7.5. To overcome the scalability issue, we adapt the symbolic simulation approach [29,54,57,59], which leverages the equivalence among packet headers, link/node failures, or external routes to scale to a large search space. Specifically, we assign each update a Boolean variable indicating whether it is applied, and symbolically simulate the routing and forwarding behaviors of the network. The key difference is that updates

Figure 2: A simplified version of a real migration from iBGP to eBGP, in a content service provider’s WAN. can affect the existence or value of configuration components, such as BGP sessions and IGP link costs. We generalize SRE’s way of how to initialize and transfer symbolic routes to handle symbolic configurations. We implement a prototype of S MOOTHIE, and demonstrate its versatility with two planners, FastDownward [21] and ENHSP [41], to find sequential plans. Because a suitable parallel planner does not exist, we also develop a new SMTbased planner to find parallel plans. The prototype will be available to the community upon publication. We evaluate S MOOTHIE in both real and synthetic migration scenarios. Results show that S MOOTHIE generates useful plans appreciated by operators (§2.4), finds parallel plans that compress up to thousands of configurations updates into no more than 3 steps, while being efficient to finish most planning task in less than 1 hour (§7).

2

Motivation

We use two concrete scenarios to motivate the need of an automatic planner for network configuration migration, and why the the planner should be versatile.

2.1

Manual Migration Planning is Hard

Figure 2 shows a real but simplified migration scenario in a large content service provider (CSP). The CSP has multiple datacenters across the world, interconnected with a backbone WAN. As shown in the figure, A, B,C, D are backbone routers connecting datacenters DC1 and DC2 . Initially, the two backbone routers of DC1 (i.e., A, B) and the two backbone routers of DC2 (i.e., C, D) form pairwise iBGP sessions, as shown in Figure 2(a). One day, to improve control plane scalability, the operators decide to migrate to a new design with eBGP instead of iBGP, as shown in Figure 2(b). For this migration, the operators need to remove all iBGP sessions, and add two eBGP sessions.

1 This paper assumes deterministic convergence. That is, given two updates ui , uk , the network will converge to the same state, either applying ui first or applying uk first. Therefore, the number of intermediates states equals the number of subsets of all updates.

2

2.2

Diverse Migration Planning Tasks

Figure 3 shows another configuration migration scenario, where the operators want to add a new route reflector. For simplicity, we only consider switches that change their route reflector. Specifically, this migration involves three types of updates: (1) removing the client sessions from C, D, E to the old route reflector A; (2) adding the client sessions from C, D, E to the new route reflector B; and (3) change the session between B and A from Client-to-RR to Peer-to-Peer. To ensure safety, the plan should follow the “insert-before− remove” principle [24] (i.e., u+ XB before uXA ) for each switch to learn at least one route to the external destination. In ad− dition, it should enforce uCA after u− DA to avoid forwarding loops; after adding the new iBGP sessions to B and receiving routes from it, C and D still choose the route from A as the best route to reach the external destination due to time-based − tie-breaking for equal cost routes. If we apply uCA before u− DA , C will learn routes only from B and send the packets to B through D, while D still prefers A and sends packets to it via C. This will result in a forwarding loop between C and D. There can be multiple plans satisfying safety properties. In this example, there are a total of (8!/4/2) = 7! safe plans. Instead of picking a random one from all safe plans, operators often have operational preferences over them. For one case, they may want to apply updates switch by switch, and therefore prefer a sequential plan such − − + as u+DB , u−DA , uCB , uCA , u+ EB , uEA . Moreover, operators may have some soft constraints that one update should better take place before another, and want to find a plan that is optimal (satisfying as many constraints as possible), or good enough (satisfying ≥ 3 soft constraints). In another case, operators may want the migration process to be finished in shorter time, and therefore prefer a parallel − − − + + plan, e.g., [uCB , u+ DB , uEB ], [uDA , uEA ], [uCA ] . Besides being faster, a parallel plan is more flexible: they do not force a total order on independent updates, so that operations can flexibly pick the order of them.

Figure 3: Example configuration migration of adding a new route reflector. Unchanged switches (i.e., persistent clients of A) are omitted.

Although it looks simple, implementing this migration without interrupting live traffic requires careful planning—it took one month for experienced operators at the CSP to make a − m plan! To illustrate this, we will use u+ xy , uxy , and uxy to denote the addition, removal, and modification of the BGP session between two switches x and y, respectively. The Initial Plan (Incorrect). Since A (resp. C) and B (resp. D) are backing up each other, operators began with a straightforward plan u−AC , u−AD , u+AC , u−BC , u−BD , u+BD . That is, first remove the two iBGP sessions and add the one eBGP session for device A (i.e., u−AC , u−AD , u+AC ), and then perform similar steps for device B (i.e., u−BC , u−BD , u+BD ). However, they found that even after step u+ AC is executed, rather than choosing the eBGP route from A as expected, C kept choosing the iBGP route from B (due to shorter AS path). This way, C will forward traffic from DC2 to DC1 through the long, indirect path through D and B (i.e., the solid red arrows in Figure 2(c)), rather than the short, direct path through A (the dashed red arrows in Figure 2(c)). Since DC2 is load-balancing its traffic towards DC1 to C and D, there is inconsistency among packets sent to C and D (i.e., multi-path inconsistency [14]). To avoid the temporary multi-path inconsistency, the operators revise the plan as follows.

Summary. On top of safety, operators can have various operational intents, and an automated planer should be versatile enough to support those diverse needs. We summarize three different planning intents:

The Revised Plan (Still Incorrect). Operators revised the − above plan to perform another step ut after u− AC and uAD (i.e., − − − − + + uAC , uAD , ut , uAC , uBC , uBD , uBD ). That is, let B increase the AS path length of routes advertised to C by configuring an export policy PrependAsPath. This way, after step u+ AC is executed, C will prefer eBGP routes from A over the iBGP routes from B. However, this revision was ad hoc and it only solves the inconsistency after step u+ AC ; the long forwarding path still exists after step u− and before step u+ AC AC . Plans that fundamentally avoid multi-path inconsistency are shown in §2.4.

• Sequential Planning: find a safe sequential migration plan as soon as possible2 ; • Optimal Planning: find a safe sequential migration plan that satisfies as much operational preference as possible; • Parallel Planning: find a parallel plan that minimize the number of plan steps, thus enabling fast migration, which is a must for large-scale network.

Summary. This real scenario shows that manual planning configuration migrations is difficult and error-prone; even experienced operators struggle to plan quickly and correctly.

2 This is called “agile planning” in AI planning.

3

2.3

Limitations of Existing Work

consistency property. In fact, even after adding a preference to avoid path reduction, S MOOTHIE still returned the same plans , since the added preference is conflicting with the multi-path consistency property.

Existing network migration planners excel at finding any safe sequential plans, but fall short for diverse planning tasks, due to their close bounding of specific search algorithms. Snowcap [43] offers a flexible preference definition language to enable the finding of optimal plans. However, Snowcap adopts a counter-example guided DFS search strategy, which works well for sequential plans but does not scale well when finding optimal plans. The reason is finding optimal plans (as well as parallel plans) require exploring a huge number of states, but the DFS search strategy has a complexity proportional to the number of visited states (see §7.5). As reported in its paper, the number of states explored to find a local-optimal plan is quadric to the number of updates. Cursor [9] and SafeMigration [10] use dedicated search algorithms to find sequential plans, therefore are not amenable to efficiently support optimal and (or) parallel planning. The research area of automated planning acknowledges the above issues. Different planning tasks require different search strategies. For sequential plans, the A* algorithm can find optimal plans [19, 23], while weighted A* can offer better scalability if non-optimal but “good enough” plans are acceptable [18, 37]. Further, for parallel planning, satisfiability (SAT) or satisfiability modulo theory (SMT) based methods are a prominent approach, as they compactly encode concurrent action choices and avoid explicit enumeration of parallel action subsets [26, 27, 38]. Therefore, we should instead develop a framework that can be easily customized for different situations with different requirements.

2.4

3

Automated Planning for Configuration Migration

3.1

Preliminaries to Automated Planning

Automated planning aims to find a valid sequence of actions, called a plan, that transitions a system from an initial state to a set of goal states. In this paper, we restrict ourselves to the classical planning problems where the state space are discrete and finite, actions are deterministic, and the system changes only through the execution of actions. Problem definition (Adapted from [38]). An automated planning problem is defined as a 4-tuple (V, sI , SG , A), where V is a set of Boolean state variables and each state s is a valuation of V , i.e., an assignment s : V → {0, 1}; sI and SG are the initial state and the set of goal states, respectively; and A is the set of actions which define how a system transitions. Each action a ∈ A is a pair ⟨p, e⟩, where p and e are predicates over V , called precondition and effect of the action, respectively. That is, an action a = ⟨p, e⟩ is executable at a state s if s satisfies p, i.e., s |= p, and there is a unique successor state s′ = exec⟨p,e⟩ (s), where s′ |= e and s′ (v) = s(v) for all v not occurring in e. This means that the effects are true in the successor state, and all state variables not affected by the action retain their values.

S MOOTHIE Preview

The Language. Planning Domain Definition Language (PDDL [2]) is a widely adopted language for describing automated planning problems. PDDL divides the model of the planning problem into two major parts: a domain description that defines common elements shared by all problems in a domain, and a problem description that defines the specific planning problem. Listing 1 shows an example PDDL snippet, where the domain block (Lines 1–8) defines predicates (symbolic, boolean-valued functions that describe properties of objects), actions, etc., and the problem block (Lines 10–14) defines objects, the initial state, and the goal states.

As shown in Figure 1, S MOOTHIE is a configuration migration planning framework which decouples the plan searching and the problem modeling. Specifically, S MOOTHIE firstly symbolically simulates the control plane to obtain a migration problem, specified with a standard language (i.e., PDDL), such that the problem be solved by any off-the-shelf planners supporting that description language. We tested S MOOTHIE on the iBGP to eBGP migration shown in §2.1. We got a sequential plan u−BC , u−AC , u−AD , u+AC , u−BD , u+BD ; and a parallel plan [u−AD , u−BC ], u−AC , u+AC , u−BD , u+BD Both plans are safe. S MOOTHIE avoids the multi-path in− + consistency by removing u− AD (resp. uBC ) before adding uAC + (resp. uBD ). Such a principle is more obvious in the parallel − plan, as it removes u− AD and uBC , which are the root cause for longer forwarding paths, at the very beginning. When we showed S MOOTHIE’s plans to the operators, they were surprised how we found them automatically. They also pointed out that our plan would reduce the number of equivalent paths, making DC2 aware of the route changes during the reconfiguration. However, they still valued our plan much since the number of paths is not as important as the multi-path

Planners. Over decades, many automated planners have emerged. Most planners [13, 16, 22, 47, 48] are designed to find a sequential plan. Some of them [22] excel in finding any valid plan as quickly as possible. Others [16, 47] are good at finding a cost-optimal plan, i.e., a plan with the minimal cost, or a non-optimal but “good enough” plan (e.g., cost ≤ 10). A few planners are designed to find parallel plans, but most of them conclude a set of actions can be parallelized as long as at least one total order of them is valid (known as ∃-step parallelism), instead of requiring any order of them to be valid (known as ∀-step parallelism). 4

1 2 3 4 5 6 7 8

support more kinds of soft constraints. Such as using “temporal constraints” to specify application durations of updates, and call dedicated planners [5, 12, 16, 50] to make plans.

(define (domain config-migration ) (:requirements :strips :typing) (:types bit ) (:predicates ( applied ?u - bit )) (:action apply-update :parameters (? u - bit ) :precondition (and (not ( applied ?u)) safe) :effect ( applied ?u)))

3.3

Challenge 1: How to identify all safe states in a large space. The specification of safe field in Listing 1 (Line 7) is critical. To meet the need of diverse planning tasks, the safe field should cover all safe states. Specifically, covering all safe states guarantees the completeness of finding a safe plan if one indeed exists, and sufficient information to find optimal plans and shortest parallel plans. Using concrete simulation (e.g., Batfish [14]) is clearly unscalable, when the migration consists of n updates, we have to run 2n rounds of simulation. Making the simulation incremental (as used by Snowcap [43]) may speed up a single round of simulation, but does not fundamentally solve the problem, since the total time is proportional to the number of simulations (see §7.5). Our Approach: Symbolic Simulation. Fortunately, there exists equivalences among all possible intermediate states. For example, when a network migrates from iBGP full mesh to route reflection [8], most iBGP peer sessions in the full mesh carry no route exchange, and the states before and after their removals are equivalent. We can exploit such equivalence for scalable identification of safe states using symbolic simulation [29, 54, 59]. Specifically, we can symbolize the updates as symbolic configuration components, and walk through all states within a single symbolic simulation. Symbolic simulation also enable a shortcut: if it verifies that all or no states satisfy the safety requirements, we can quickly identify that all or no plans are safe (see §5.1). Challenge 2: How to find ∀-step parallel plans. We find none of existing planners [7, 25, 27, 38–40] are suitable for finding parallel configuration migration plans, where a subset of updates can be executed in arbitrary order. Some planners support ∃-step semantics for parallel plans, i.e., they conclude a set of actions can be parallelized when there exists one safe order for these actions. Taking the migration in Figure 3 for − − example, they will parallelize uCA , u− DA , uEA since there exists − − − a safe order (e.g., [uDA , uCA , uEA ]), even though other order− − ings (e.g., [uCA , u− DA , uEA ]) are unsafe. Such ∃-step parallel planners do not meet our needs since we require all orders of updates in the subset should be safe, i.e., ∀-step parallel plans. Other planners can find ∀-step parallel plans; but prior to plan searching, they identify mutually exclusive actions if their preconditions and effects contain overlapping objects [6]. Such a pure syntactical analysis will falsely conclude that all updates cannot be parallelized, while actually they are semantically independent and can be parallelized [1]. Our Approach: ∀-step Parallel Planner Identifying Semantical Independency. Instead of using pure syntactic preprocessing, we semantically encode the ∀-step parallelism with SMT constraints. In particular, we use the bit-vector

9 10 11 12 13 14

(define (problem instance ) (:domain config-migration ) (:objects u1 .. un ) (:init (not ( applied u1 )) .. (not ( applied un ))) (:goal (and ( applied u1 ) .. ( applied un ))))

Listing 1: An example PDDL file for configuration migration. Each ui in Line 12 represents a configuration update; the only action is to apply a given update (i.e., apply-update in Line 5); and safe in Line 7 is a placeholder of the formula representing all safe intermediate states where some updates are applied (i.e., (applied ui)) while others are not (i.e., (not (applied ui))).

3.2

Challenges and Our Approach

Automated CMP

We find that the configuration migration planning can be formulated as an automated planning problem, and such a formulation bring a lot of benefits. Problem Definition. A configuration migration problem with n updates {u1 , . . . , un } can be formulated as an automated planning problem (V, sI , SG , A). • V = {b1 , . . . , bn } is a set of Boolean variables, where bi indicates whether update ui has been applied or not, corresponding to Line 4 in Listing 1. • sI = 1≤i≤n ¬bi is the initial state where no updates are applied, corresponding to Line 13 in Listing 1. V

• SG = { 1≤i≤n bi } is the set of a single goal state where all updates have been applied, corresponding to Line 14 in Listing 1. V

• A is a set of actions, where an action ⟨pi , ei ⟩ ∈ A represents the application of update ui : pi = ¬bi ∧ safe (the current state is safe and ui has not been applied yet; ei = bi (ui is applied after the action. The corresponding semantics are encoded in Lines 5–8 in Listing 1. Benefits. By modeling the migration planning problem as an automated planning problem with PDDL, we decouple the process of finding a migration plan into two phases: (1) the domain-specific problem modeling phase, which identifies all safety constraints regarding network semantics with a verifier, and (2) the domain-independent plan searching phase, which enables easy plugin of existing AI planners that are optimized for diverse planning objectives (i.e., sequential, optimal, and parallel planning). Moreover, for optimal planning, since PDDL provides a rich set of features, it is also easy to 5

logic and represent states, e.g., 0000 for the initial state, and 0110 represents the 2nd and 3rd updates have been applied. If all intermediate states, e.g., 0100 and 0010, are safe, then we conclude the 2nd and 3rd updates can be parallel. The above semantics can be easily encoded with bit-vector operations (i.e., bvand). Details are provided in §6.

4

protocol (e.g., OSPF or BGP) specifying the prefix, next hop, and other protocol-specific attributes (e.g., AS Path); and cond encodes the condition of states where route becomes the best route. Each symbolic RIB consists of all possible routes that can materialize (i.e., become the best route) in certain states. Initializing Symbolic Routes is to import all routes declared in the symbolic configuration. Different from SRE, where symbolic routes are always initialized with cond = True, in S MOOTHIE, the condition of an initialized symbolic route depends on whether the declaration command is symbolic or not. If not, we set cond = True; otherwise, we set cond = bu or cond = ¬bu , depending on whether the update u inserts or removes the declaration command. Transferring Symbolic Routes refers to transform a symbolic route when it traverses from one switch p to another switch q, denoted as a function c f pq . Such transformation includes both route modification and condition refinement, with the route modification determined by protocol semantics and user-defined rules in configurations. Since configurations are symbolic, we encode the symbolic transformation c f pq as a collection of conditional route modifications, i.e.,

Symbolic Simulation

This section introduces the symbolic simulation of S MOOTHIE. The overall process is similar to SRE [59], while we generalize its way to initialize and transfer symbolic routes.

4.1

Configuration Symbolization

S MOOTHIE first computes the differences (diff) of the initial and final configurations, to get a set of updates V = {u1 , . . . , un }. Each update ui is either ⟨+, ci ⟩, ⟨−, ci ⟩, or ⟨ci , c′i ⟩, indicating configuration component ci is inserted (+), removed (-), or modified to c′i , from the initial configuration to the final configuration. For example, the following snippet shows the configuration diff of C in Figure 3, and the corresponding two updates: (1) uCA = ⟨−, iBGPCA ⟩ for removing the session between C and A; and (2) uCB = ⟨+, iBGPCB ⟩ for inserting the session between C and B. Then, S MOOTHIE makes the updates and the corresponding configuration components symbolic. For each update ui , we use a boolean variable bi to represent whether it is applied (bi = True) or not (bi = False). Therefore, the existence of configuration component ci is symbolic: it exists if the update is an insertion that has been applied, or the update is removal or modification, but the update has not been applied. Figure 4(a) shows the symbolic configuration components for the example in Figure 3. We can see that the iBGP session between C and A exists if bCA equals False (the update of removal has not been applied).

1 m c f pq := {( f pq , c1 ), . . . , ( f pq , cm )}

i }m is the set of all concrete transfer functions that where { f pq i=1 will appear during the migration, and each ci is the encoding i exists, satisfying W of all states where f pq i∈[1,m] ci = True. c Correspondingly, applying f pq on a symbolic route ⟨r, c⟩ is defined as: 1 m c f pq (⟨r, c⟩) := {⟨ f pq (r), c ∧ c1 ⟩, . . . , ⟨ f pq (r), c ∧ cm ⟩}

(2)

This encoding generalizes SRE’s link-failure model, in which each link either applies a fixed transfer function or drops all routes, depending on its up/down state. S MOOTHIE currently considers symbolic OSPF link cost, BGP session, and routing policy. Specifically, if there is an update u = ⟨w, w′ ⟩ that changes the OSPF link cost between p, q from w to w′ , we have

router bgp 64550 - neighbor 192.168.1.0 remote-as 64550 + neighbor 192.168.2.0 remote-as 64550

w w′ c f pq = {( f pq , ¬bu ), ( f pq , bu )},

4.2

(1)

Symbolic Route Computation

(3)

′

w (resp. f w ) increases the route cost by w (resp. w′ ); where f pq pq if there is an update u = ⟨+, session pq ⟩ that inserts a BGP session between p and q, we have

Symbolic route computation (SRC) propagates symbolic routes and generates symbolic RIBs. For each protocol, the simulation begins with switches initializing routes declared in the configurations (i.e., initialize). Then, switches iteratively exchange routes with their neighbors (i.e., transfer), and select the best routes from all received routes (i.e., merge). The simulation terminates until a fix-point is reached, i.e., the RIBs of switches do not change. We follow SRE to define a symbolic route as a 2-tuple R = ⟨route, cond⟩, where route is a concrete route for a specific

c f pq = {( f pq , bu ), ( f∞ , ¬bu )} ≡ {( f pq , bu )},

(4)

where f∞ denies all routes. It encodes the fact that the route propagation from p to q happens only after the session between them has established. For example, in Figure 4(b), C will receive a route for 128/1 from E after E and C both become clients of B (i.e., bEB bCB ). 6

Figure 4: Symbolic simulation of S MOOTHIE. We handle the removal of BGP sessions, and the modification and insertion/removal of a route policy similarly.

constraints below, users are free to manipulate the generated PDDL file.

Merging Symbolic Routes happens when a switch learns multiple routes for the same prefix. This step is the same as SRE: we rank these symbolic routes according to their priorities and update their conditions by negating the conditions of all higher-priority symbolic routes. For example, in Figure 4(b), C receives two routes from A and E, where the route from A has higher priority due to lower IGP cost. Then, the condition of the route from E is updated to bEB bCB ∧ ¬(¬bCA ) = bEB bCB bCA , meaning that only after − + u+ EB , uCB , uCA are applied, it will become the best route.

5.1

Encoding Safety Constraints

Safety constraints are a set of conditions on update states (whether each update is applied or not), under which a network satisfies a set of properties. We term such conditions as update conditions. For instance, to maintain the reachability property that all switches should reach the external prefix during the migration in §2, plans should let the network traverse only update state satisfying the condition: (¬bCA ∨ bCB ) ∧ (¬bDA ∨ bDB ) ∧ ¬(bEB bCB bCA ¬bDA ), (5)

4.3

Symbolic Packet Forwarding

where the first and second clauses represent states where C and D learn at least one route for the external prefix, respectively; and the third clause encodes the states without forwarding loop. Other switches, i.e., A, B, E will always learn the external prefix, thus relative variables (e.g., bAB ) do not show up in Equation (5). In the following, we show how to compute update conditions for different properties. We denote properties as Prop(sw, p, c), where sw is the source switch, p is the destination address, and c represents constraints on route attributes or packet forwarding paths. Routing (Control Plane) Property. A routing property Prop(sw, p, c) specifies that sw should learn a route for prefix p and the route attributes should satisfy a constraint c. Specifically, we denote Prop(sw, p, True) as CpReach(sw, p). The update condition for a routing property is computed as W R∈R R.cond, where

Symbolic Packet and PEC. Let 2IP and 2V be the universe set of all packet headers and configuration states, respectively. A symbolic packet is a 3-tuple Pkt = ⟨H, L, status⟩, where H ⊆ 2IP × 2V is a set of header-state pairs (called symbolic header), L is the forwarding path, and the forwarding status is either F LY, A RRIVE, L OOP, or D ROP. Essentially, a symbolic packet represents a set of concrete packets, which, under specific states, will traverse nodes in L, and have a certain status at the last hop in L. Each symbolic packet not F LYing is a packet equivalence class (PEC). Symbolic packet forwarding (SPF) propagates symbolic packets throughout the network to compute a set of PECs for each switch, in the same way as SRE [59]. Figure 4(b) shows the process for the example in Figure 3. When the symbolic packet reaches node C, a loop is detected, whose condition is bEB bCB bCA ¬bDA .

R = {R | R ∈ sw.RIB ∧ R.route.pre f ix = p

5

PDDL Generation

∧ R.route |= c}.

(6)

Forwarding (Data Plane) Property. A forwarding property Prop(sw, p, c) specifies that a packet sent from sw to destination p should traverse specific paths and/or have a specific final status encoded in c. Specifically, we refer to Prop(sw, p, status = A RRIVE) as DpReach(sw, p); and the

The snippet in Listing 1 is a template for all configuration migrations. To generate PDDL for a specific migration scenario, we only need to fill in the scenario-specific safety and preference constraints in the domain file. It’s worth mentioning that, while we focus on showing how to encode common 7

1 2

5.2

(define (domain config-migration ) (:predicates ( applied ?u - bit ) ( violated ))

Preference constraints are soft constraints. Their violation does not impact migration safety, but plans that satisfy more soft constraints are preferred. Therefore, when a soft constraint is violated, instead of blocking a plan to expand, we increase the “cost” of the plan. This way, the plan with the minimal cost is the plan that satisfies the most soft constraints. Currently, we support encoding precedence preferences, i.e., preferring plans where one update ui is applied before another update u j . Inspired by [35,55], we use conditional-effect to encode it in PDDL, as shown in Listing 2 (identical lines of Listing 1 omitted for brevity). In detail, we first define a predicate violated to flag preference violation (Line 2), and then define conditional effect (Lines 9 - 10), which encodes that the preference is violated if the current update is ui , and u j is already applied. If violated, the plan is blocked from expanding (Line 7) unless the penalty for preference violation is paid (Lines 12 - 16). Finally, we inform the planner to find the plan with the minimal cost (Line 19). If there are multiple such preferences, we encode their disjunction in Line 9.

3 4 5 6 7 8 9 10

(:action apply-update :parameters (? u - bit ) :precondition (and (not ( applied ?u)) safe (not ( violated ))) :effect (and ( applied ?u) (when (and (= ?u ui ) ( applied uj )) ( violated ))))

11 12 13 14 15 16

(:action pay-penalty :parameters () :precondition ( violated ) :effect (and (not ( violated )) (increase ( total-cost ) 100) )))

17 18 19

(define (problem instance ) (:metric minimize ( total-cost )))

Listing 2: Encode preference in PDDL. safe in Line 6 is a placeholder. negation of Prop(sw, p, status = L OOP) as LoopFree(sw, p). The update condition for a forwarding property is computed W as pec∈E Cond(pec.H ∧ p), where

5.3

E = {pec | pec ∈ sw.PECs ∧ pec.L |= c ∧ pec.status |= c}.

Encoding Preferences

Optimizations

For configuration migration, a common safety requirement is to maintain global (all switches’) reachability to specific destinations. However, we found that a direct computation of global reachability conditions using Equation (8) leads to a huge safe constraints, making plan searching untractable. To reduce the size of constraints, we introduce an optimization termed safety constraint simplification. This optimization converts the global reachability property for a prefix p into an equivalent one, i.e., control plane reachability plus data plane loop freedom. Formally, instead of computing:

(7)

and (pec.H ∧ p) is a Boolean formula that consists of both IP address variables and update variables, Cond() is to extract the condition from that formula. For example, Cond(p1 ) = True, Cond(p1 b1 ¬b2 ) = b1 ¬b2 . Multi-path Consistency specifies that all packets from sw to p, if forwarded through multiple paths, have the same final status. We first check DpReach(sw, p) and Prop(sw, p, status ∈ {L OOP, D ROP}), to get the condition when the destination is reached (cond1 ) or isolated (cond2 ), respectively. Then, we compute the update condition as cond1 ∧ ¬cond2 . More generally, we can also check the condition when all reachable paths have the same length, as required in the example in §2.1; or even the condition when all reachable paths should traverse the firewall. Since safety constraints should always be satisfied during updates, in PDDL we encode them into the precondition field of the apply-update action (e.g., Line 7 of Listing 1). This will block further expansion of a plan and force backtracing, when an unsafe state is visited. It is worth mentioning that if the Boolean constraint for safe states is True or False, we can directly identify that any or none plan is safe, respectively, without generating PDDL and calling the planners. Even if the Boolean constraint is not True or False, it will consists of much fewer update variables than the total number of updates when most updates have no impact on safety (see §7). Accordingly, we call planners to plan only the updates that impact safety.

^

DpReach(n1 )

(8)

n1 ∈N

where N is the set of all switches, we compute: (

^

CpReach(n1 )) ∧ (

^

LoopFree(n1 ))

(9)

n1 ∈loops

n1 ∈N

If no data plane packet filtering or rewriting configuration (e.g., ACL, NAT) exists, these two formulas are equivalent since the DP reachability of n1 , i.e., DpReach(n1 ), depends recursively on the DP reachability of its next-hops: DpReach(n1 ) ↔

_

(CpReach(n1 , n2 ) ∧ DpReach(n2 )

(n1 ,n2 )∈E

∧ ¬DpReach(n2 , n1 )),

(10)

where E is the link set of the network, CpReach(n1 , n2 ) represents n1 selects n2 as its next-hop, and DpReach(n1 , n2 ) represents n2 ’s data plane reachability via forwarding paths that traverses n1 . Specifically, the negation of DpReach(n1 , n2 ) 8

S MOOTHIE compares to state-of-the-art planners? (Q4) Can symbolic simulation scale?

prevents forwarding loops, which is a detailed counterpart of the loop freedom encoding in Equation (9). While equivalent, Equation (8) usually results in more complicated formulas than Equation (9), which will impede planners like FastDownward. Using Equation (9) directly frees S MOOTHIE from minimizing the formulas.

6

Implementation and Setup. We implemented a prototype of S MOOTHIE with around 25k lines of Java code. For the symbolic simulator of S MOOTHIE, we use BDD, specifically the JDD library [49], to encode Boolean formulas and operations. For the planning backend, we use FastDownward [21], ENHSP [41], and our parallel planner (§6) with Z3 [34] to find sequential and parallel plans, respectively. All evaluations are executed on a Linux server with two 16-core Intel Xeon CPUs @ 2.90GHz and 256G RAM.

Plan Searching

After obtaining the PDDL, we can invoke off-the-shelf planners based on operators’ intent. Specifically, we can use FastDownward [21] to find a sequential plan as soon as possible; if some soft constraints are appointed, we can use planners like ENHSP [41] to find the sequential plan that satisfies the most soft constraints. Since no existing planners can find ∀-step parallel plan for our problem, we customize our own planner based on SMT. Customized SMT-based Planner. Suppose there are n updates, our planner finds the shortest plan by checking whether there exists a k-step plan for an increasing k (1 ≤ k ≤ n). For each k, we convert the problem of searching a k-step plan into a set of SMT constraints:

7.1

We use 87 topologies from Topology Zoo [28]. The topologies have 5–82 switches (avg. 33), and 4–96 edges (avg. 39). For each topology, we configure (i) OSPF with uniform link cost; (ii) iBGP route reflection, where the switch with the maximum edge degree is the route reflector; and (iii) all external switches to announce the same prefix. We consider 5 synthetic migration scenarios. Except RRx2, all of them are from Snowcap [43]. The first three of the five scenarios are inspired by real-world migrations, while the last two are mainly for benchmarking. For all scenarios, we consider global reachability (§5) as the safety requirement, i.e., every internal switch can reach the external prefix.

I(s0 ) ∧ trans(s0 , s1 ) ∧ · · · ∧ trans(sk−1 , sk ) ∧ G(sk ), (11) where si represents the state after i steps, I(s0 ) and G(sk ) constraints s0 and sk to be the initial and goal state, respectively; trans(si , si+1 ) (i ∈ [0, k − 1]) constraints the transition between states. We represent states with bit-vectors of length n, with the ith position represents whether the ith update has been applied. s j is said to be a successor of si , denoted as si ≺ s j , if all updates that have been applied in state si , have also been applied in state s j , i.e., si ≺ s j := (bvand(si , s j ) = si ) ∧ (si ̸= s j ) .

(1) RRx2 adds a new route reflector. We randomly partition the network into two regions that are balanced in the number of switches using METIS [33]. For the region that does not contain the original reflector RR1 , we select a new reflector RR2 . For each switch other than RR2 in the second region, we delete its session to RR1 , and add a new session to RR2 . Thus, there are O(n) updates for a network with n switches. (2) FM2RR transforms from iBGP full mesh into route reflection. For a topology with n switches, there are O(n2 ) updates, with removing O(n2 ) iBGP sessions from the full mesh, and adding O(n) reflector-client sessions.

(12)

Then, a state s′ is said to be an intermediate state of si and s j if and only if si ≺ s′ ≺ s j . Under ∀-step parallelism semantics, the updates corresponding to bits that change from 0 in si to 1 in si+1 must be safely executable in any order. Equivalently, every intermediate state between si and s j must be safe: parallel(si , si+1 ) := ∀si ≺s≺si+1 safe(s),

(3) NetAcq merges two networks, a newly acquired network and an existing network, into a single one. During the migration, we adjust the OSPF cost of one network to the same value with the other, and configure the route reflectors of the two networks to set up an iBGP peer-to-peer session. The number of updates is also proportional to the number of edges in the topology. Only 62 topologies are eligible for this scenario since it requires one external switch for each network.

(13)

Finally, the trans constraints is encoded as: trans(si , s j ) := (si ≺ s j ) ∧ parallel(si , s j ).

7

Migration Scenarios

(4) IGPx2 doubles the OSPF cost for each link in the network. There are m updates for a topology with m edges.

(14)

(5) LPx2 doubles the local preference for each external neighbor of the network. If the network has p external neighbors, then there will be p updates. For all following figures using “Instance ID” as xtics, the topologies are sorted by increasing number of updates.

Evaluation

Our evaluation aims to answer the following questions: (Q1) Can S MOOTHIE find high quality plans? (Q2) How S MOOTHIE perform on different planning tasks? (Q3) How 9

#total #all-safe

RRx2

FM2RR

NetAcq

IGPx2

LPx2

82 2

87 42

62 62

87 87

87 87

External route for 128/1 1 6

#Steps

1032 101 10

7

#Updates

0

Plan Qualities

#Updates or #Steps

Timeout

loop

4 8

2 3

6

4

7 loop

5

(b) Unsafe States if # # Apply 𝑢!" before 𝑢$"

100 75 50 25 0 3 10

100

ENHSP (FM2RR) ENHSP (RRx2)

103

Time (s) (a) Sequential

We show qualities of the plans found by S MOOTHIE. Overall Statistics. As shown in Table 1, for 42 (2) FM2RR (RRx2) instances, and all instances of the other three scenarios, symbolic simulation concludes that all intermediate states satisfy the global reachability, i.e., all plans are safe, and there is no need to call a planner. In the following, we show details about the instances that really need to call a planner. Sequential Plans. Figure 5 shows the number of updates and sequential steps for each instance that needs planning. For FM2RR, the sequential plans have up to 2 magnitudes fewer steps than updates. This is because most updates are removing iBGP peer sessions that have no impact on safety: the end switches of such sessions only receive iBGP routes from the border switches that peer with external neighbors, or from the route reflector; therefore, they do not exchange routes with each other upon such sessions. On the contrary, for most RRx2 instances, the number of steps is roughly the same as the number of updates, since most updates will impact safety. Moreover, except for 5 timeouts, ENHSP successfully finds the optimal plan for all other instances. Parallel Plans. Figure 6 shows the number of updates and parallel plan steps for each instance. For all non-timeout instances, the shortest parallel plan contains only ≤ 3 steps! Compressing hundreds or thousands of updates into O(10)-

#Steps

3 7

FD (FM2RR) FD (RRx2)

20 40 60 RRx2 Instance ID

Figure 5: Number of updates and sequential plan steps for FM2RR and RRx2 instances.

7.2

4 5

1

2

6

Packet to 128/1

5

8

(c) Unsafe States if # # Apply 𝑢"% before 𝑢"&

Figure 7: The initial and unsafe states when applying FM2RR on GtsPoland, with Node 1 as the route reflector. Irrelevant nodes, iBGP sessions, and traffic are removed for simplicity.

101 0 10 20 30 40 FM2RR Instance ID

8

3

(a) Initial Forwarding State

Solved (%)

#Updates or #Steps

Table 1: Statistics for the five migration scenarios. #total means the total number of instances; #all-safe means the number of instances that symbolic simulation result indicates all intermediate states are safe.

1

2

Full Mesh

iBGP Session

100 75 50 25 0 3 10

100

103

Time (s) (b) Optimal

SMT (FM2RR) SMT (RRx2)

100 75 50 25 0 3 10

100

103

Time (s) (c) Parallel

Figure 8: The searching time when using different planners for three types of planning tasks. step parallel plans enables fast migration, which is a big win for highly automated production networks [36]. However, chances are certain migrations may be too complicated for the parallel planner to find the shortest parallel plan, as indicated by the timeouts. When that happens, we can trade off the plan length and try again, or fall back on using the more scalable sequential planners. Example. Figure 7 illustrates applying FM2RR on GtsPoland, whose shortest parallel plan has three steps. In the initial full mesh state, packets to the external prefix flows alone n2 → n3 → n4 → n5 . During the migration to the route reflection state, removing the iBGP session between n4 and n5 (i.e., − u− 45 ) before removing the one between n3 and n5 (i.e., u35 ) will cause forwarding loop between n3 and n4 , as shown in − Figure 7(b). Therefore, a safe plan should apply u− 35 before u45 . − − − Similarly, u25 (resp. u57 ) should be applied before u35 (resp. u− 58 ); For this instance, Snowcap outputs a sequential plan − − − − . . . , u− 25 , . . . , u35 , . . . , u57 , . . . , u45 , . . . , u58 , . . . . Even though safe, it is too concrete to reveal the fact that “updates other than − − − − u− 25 , u35 , u45 , u57 , u58 do no impact safety, and can be randomly ordered”. In contrast, S MOOTHIE outputs a sequential plan − − − − − − − − − u− 25 , u35 , u57 , u45 , u58 , or a parallel plan [u25 ], [u35 , u57 ], [u45 , u58 ] , indicating that the order of all other updates does not matter.

#Updates

102

101 100 0 10 20 30 40 100 0 20 40 60 FM2RR Instance ID RRx2 Instance ID

7.3

Performance on Different Tasks

This section evaluates how S MOOTHIE performs on different planning tasks, when equipped with different planners. Sequential Planning. Figure 8(a) shows the results for find-

Figure 6: Number of updates and parallel plan steps for FM2RR and RRx2 instances. 10

log (Compression ratio)

End-to-end Time (s)

Snowcap (Batfish) Smoothie Snowcap (native) Smoothie (grouped) 4 3 10 10 102 10 1 10 1 10 2 6 10 5 0 10 6 0 50 40 10 0 50 Instance ID Instance ID Instance ID (a) FM2RR (b) NetAcq (c) LPx2

Figure 9: End-to-end time to find any safe sequential plan using Snowcap (native), Snowcap (Batfish), S MOOTHIE, and S MOOTHIE (grouped). ing sequential plans using all three planners. In general, FastDownward is extremely scalable, finishes in less than one second for all instances; ENHSP is also scalable, completing within 100 seconds in most instances; while the SMT planner has the worst scalability, taking around 1000 seconds, or even runs out of time, on some complex instances. Optimal Planning. Figure 8(b) shows the results for appointing a random precedence preference and uses ENHSP to find the optimal plan, which is the only planner that supports such planning tasks. Compared to sequential planning, ENHSP is slightly slower for optimal planning; but it still completes the search on most instances within 100 seconds. Parallel Planning. Figure 8(c) shows the results for finding parallel plans using our SMT-based planner, the only planner that supports parallel planning. Our planner can find the shortest parallel plan in less than 1 minute, except for running out of time on 7 FM2RR instances. Interestingly, for around 45% of all instances, our planner is more efficient to find parallel plans than sequential plans. This is mainly because finding sequential plans requires unrolling trans in Equation (11) n times (where n is the number of updates), making the resulting SMT constraint too large to be solved efficiently. In sum, the results show that different planners excel on different planning tasks, no single planning strategy suites all operational requirements. This indicates a decoupled planning framework is necessary for support diverse planning tasks.

7.4

Snowcap (Batfish)

Snowcap (native)

4000

80

50

2000

40

25

0

0

50 Instance ID (a) FM2RR

0

0

40 Instance ID (b) NetAcq

0

Smoothie

0

50 Instance ID (c) LPx2

Figure 10: Compression ratio to full simulation of all explored states using incremental simulation (Snowcap (native) and (Batfish)) and symbolic simulation (S MOOTHIE). sub-milliseconds, order-or-magnitude faster than Batfish and S MOOTHIE (seconds). Second, the synthetic migration scenarios are so simple that for most cases Snowcap can find a safe plan without backtracking. On the contrary, S MOOTHIE targets at supporting diverse planning tasks, so it is necessary to explore all intermediate states with symbolic simulation. The cost pays off when finding optimal or parallel plans but can be an overkill for sequential plans. To validate the above hypotheses, we modified Batfish to support incremental simulation for a limited set of configuration changes (IGP link weight change, remove or addition of BGP sessions, routing policy modifications), and replay the search traces of Snowcap using the modified Batfish. As shown in Figure 9, using Batfish as the simulator, Snowcap’s planning time significantly increases, and slower than S MOOTHIE for most of the cases. Results for RRx2 and IGPx2 are similar and shown in Appendix A. This confirms our previous hypothesis why Snowcap is so fast. For S MOOTHIE, NetAcq is substantially harder than FM2RR and LPx2. In detail, its widespread OSPF weight modifications limit equivalence among intermediate states, and the number of route computed by S MOOTHIE grows exponentially with the number of updates. For instances exceeding 100 seconds, we randomly partition the updates into three groups and simulate each separately, and label them as S MOOTHIE (grouped). Grouping substantially reduces runtime: in some instances, even two-group partition reduces simulation time from O(103 ) to O(10) seconds.

Comparison with SOTA

This section compares S MOOTHIE with Snowcap [42], the state-of-the-art configuration migration planner. We compare their time to find any sequential plan. As shown in Figure 9, Snowcap is extremely fast. It takes less than 0.1s for all instances, while S MOOTHIE uses O(10)s for FM2RR and LPx2, and O(103 )s for NetAcq. These results are expected for two reasons. Firstly, the open-source implementation of Snowcap is overly simple, with no or limited support for many protocol features including longestprefix matching, ECMP, route aggregation, etc. Also, it restricts eBGP sessions to be established with external peers. As a result, Snowcap finishes a round of simulation in

7.5

Scalability of Symbolic Simulation

This section studies how well symbolic simulation scales to a large space of intermediate states, compared to incremental simulation as adopted in [43]. We use a metric called compression ratio, defined as (Tinit × Nstates )/Ttotal , where Tinit is the time to simulate the initial configuration, Nstates is the number of states explored, and Ttotal is the total simulation time. The compression ratio reflects how effectively a simulator can exploit equivalence in the state space. For incremental simulation, Nstates counts 11

the states visited during the DFS traversal and backtracking; while for symbolic simulation, Nstates = 2Nupdates , since all intermediate states are simulated symbolically in a single execution. When grouping is applied, Nstates is the sum of the states explored across all groups. Figure 10 shows the results. The compression ratio of incremental simulation, either Snowcap (native) or (Batfish), is generally under 10. This indicates that incremental simulation exploits only a limited number equivalent states, and the total simulation time is proportional to the number of states explored. In contrast, S MOOTHIE achieves higher compression ratio on larger state spaces, given that the instances are sorted by increasing number of updates. Moreover, S MOOTHIE achieves higher compression ratio on FM2RR than on NetAcq and LPx2, since the state space of FM2RR is larger while having greater equivalence. The dramatic drops of compression ratios in Figure 10(b) are caused by grouping. Similar results for RRx2 and IGPx2 are shown in Appendix A.

8

dates that results from the difference between the initial and final configurations. Consider a variant of the example in §2.1: suppose instead of receiving DC1’s BGP routes from routers C and D, DC2 is configured with two equal-cost default static routes (i.e., 0.0.0.0/0) towards C and D. Regardless of what migration plan we take, DC2 will always distribute its traffic towards DC1 to C and D evenly. In such cases, we have to temporarily remove the static routes to meet the forwarding requirements. Temporary removal of static routes is already supported by S MOOTHIE, but we need to add support for a broader range of temporary updates and automatically determine which ones are needed to devise a safe plan. Support for convergence behavior. Our symbolic simulation models the converged state of the network after applying updates, rather than transient behavior during convergence. Complementary techniques, such as Chameleon [44] for BGP and [15] for IGP, decompose individual updates into smaller steps to preserve specified safety properties during convergence. To make a plan that ensures safety both during and after re-convergence, we can first use S MOOTHIE to order all updates, then use [44] and [15] to manage the safe execution of each update. Like other control plane analysis tools [4, 14, 59], if the network converges nondeterministically [17], S MOOTHIE will consider safety for only one of them.

Related Work

Many prior works have studied network migrations in different contexts. We summarize them here and outline their relationship to our work. Configuration Migration in the traditional networks (nonSDN) coarsely has two main branches of research. Some works, e.g., [3,24], require routers to run both the initial and final configurations in parallel. Coexisting configurations result in coexisting data planes. This way, they gradually instruct switches to forward traffic according to the final data plane in an order that avoids forwarding loops [52, 53]. Despite being useful, the overhead and device support needed by control and data plane duplication on switches impede their deployment. Other research [9–11, 15, 43] directly finds a progressive deployment plan for configuration updates, ensuring that the network maintains correct routing and/or forwarding behaviors after each step. Compared to the above research, it does not require special support from routers. However, as mentioned earlier, unlike S MOOTHIE, these works are limited in their support for diverse operational intents. Physical Infrastructure Migration refers to adding, removing, or swapping switches and links. This requires maintaining bandwidth headroom to ensure the network can handle traffic demands. SOTA tools [60, 61] automate the physical transitions using different searching strategies on top of different traffic models. We’ll investigate whether S MOOTHIE can capture the safety constraints and diverse intents of physical infrastructure migration in the future.

9

Use LLM for configuration migration planning. While planning directly from raw configurations requires an agentic system, our decoupled framework readily accommodates an LLM as a backend planner. Preliminary experiments with ChatGPT-5.6 Sol using PDDL inputs show high first-attempt accuracy for sequential planning, but optimal and parallel planning often require more attempts and provide no guarantee of finding an optimal or shortest plan. Much of this success reflects the simplicity of the synthetic cases, where the model’s stated “insert-before-remove” strategy often suffices. Experiments with natural-language migration descriptions and planning objectives further show that precomputed safety information improves accuracy and reduces time and token usage. These preliminary results suggest that further research is needed to assess the practical value and reliability of LLMs for configuration migration planning.

10

Conclusion

S MOOTHIE is a versatile configuration migration planner that supports diverse network designs and operational preferences and can also find safe parallel plans. It achieves that by decoupling how safety constraints and preferences are encoded and how a viable plan is searched. Our experiments demonstrate that S MOOTHIE performs well, finding sequential plans for most cases within 1 hour while compressing large migrations into no more than 3 parallel steps.

Discussion

Use temporary updates to expand the envelope of safe plans. Sometimes, no safe plan exists if we are limited to up12

References

[11] Francois Clad, Stefano Vissicchio, Pascal Mérindol, Pierre Francois, and Jean-Jacques Pansiot. Computing minimal update sequences for graceful router-wide reconfigurations. IEEE/ACM Transactions on Networking, 23(5):1373–1386, 2014.

[1] Mohammad Abdulaziz and Friedrich Kurz. Formally verified sat-based ai planning. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 14665–14673, 2023.

[12] Amanda Coles, Andrew Coles, Maria Fox, and Derek Long. Forward-chaining partial-order planning. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 20, pages 42– 49, 2010.

[2] Constructions Aeronautiques, Adele Howe, Craig Knoblock, ISI Drew McDermott, Ashwin Ram, Manuela Veloso, Daniel Weld, David Wilkins Sri, Anthony Barrett, Dave Christianson, et al. Pddl—the planning domain definition language. Technical Report, Tech. Rep., 1998.

[13] Stefan Edelkamp and Malte Helmert. Mips: The modelchecking integrated planning system. AI magazine, 22(3):67–67, 2001.

[3] Richard Alimi, Ye Wang, and Y. Richard Yang. Shadow configuration as a network management primitive. In Proceedings of the ACM SIGCOMM 2008 Conference on Data Communication, SIGCOMM ’08, page 111–122, New York, NY, USA, 2008. Association for Computing Machinery.

[14] Ari Fogel, Stanley Fung, Luis Pedrosa, Meg WalraedSullivan, Ramesh Govindan, Ratul Mahajan, and Todd Millstein. A general approach to network configuration analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15), pages 469–483. USENIX Association, 2015.

[4] Ryan Beckett, Aarti Gupta, Ratul Mahajan, and David Walker. A general approach to network configuration verification. In Proceedings of the Conference of the ACM Special Interest Group on Data Communication, SIGCOMM ’17, page 155–168, New York, NY, USA, 2017. Association for Computing Machinery.

[15] Pierre Francois, Mike Shand, and Olivier Bonaventure. Disruption free topology reconfiguration in ospf networks. In IEEE INFOCOM 2007-26th IEEE International Conference on Computer Communications, pages 89–97. IEEE, 2007.

[5] Arthur Bit-Monnot. Experimenting with lifted planspace planning as scheduling: Aries in the 2023 ipc. In 2023 International Planning Competition at the 33rd International Conference on Automated Planning and Scheduling, 2023.

[16] Alfonso Gerevini, Ivan Serina, et al. Lpg: A planner based on local search for planning graphs with action costs. In Aips, volume 2, pages 281–290, 2002. [17] Tim A. Griffin and Geoff Huston. BGP Wedgies. RFC 4264, November 2005.

[6] Avrim L Blum and Merrick L Furst. Fast planning through planning graph analysis. Artificial intelligence, 90(1-2):281–300, 1997.

[18] Eric A Hansen and Rong Zhou. Anytime heuristic search. Journal of Artificial Intelligence Research, 28:267–297, 2007.

[7] Michael Cashmore, Daniele Magazzeni, and Parisa Zehtabi. Planning for hybrid systems via satisfiability modulo theories. Journal of Artificial Intelligence Research, 67:235–283, 2020.

[19] Peter E Hart, Nils J Nilsson, and Bertram Raphael. A formal basis for the heuristic determination of minimum cost paths. IEEE transactions on Systems Science and Cybernetics, 4(2):100–107, 1968.

[8] Enke Chen, Tony J. Bates, and Ravi Chandra. BGP Route Reflection: An Alternative to Full Mesh Internal BGP (IBGP). RFC 4456, April 2006.

[20] Patrik Haslum, Nir Lipovetzky, Daniele Magazzeni, Christian Muise, Ronald Brachman, Francesca Rossi, and Peter Stone. An introduction to the planning domain definition language, volume 13. Springer, 2019.

[9] Zibin Chen and Lixin Gao. Cursor: Configuration update synthesis using order rules. In IEEE INFOCOM 2023 - IEEE Conference on Computer Communications, pages 1–10, 2023.

[21] Malte Helmert. Fast Downward. fast-downward.org/latest/.

[10] Zibin Chen, Lixin Gao, and Ying Zhang. Safemigration: Safe large-scale migration planning via symbolic execution. In Proceedings of the 2nd Workshop on Formal Methods Aided Network Operation, pages 37–42, 2025.

https://www.

[22] Malte Helmert. The fast downward planning system. Journal of Artificial Intelligence Research, 26:191–246, 2006. 13

[23] Malte Helmert and Carmel Domshlak. Landmarks, critical paths and abstractions: what’s the difference anyway? In Proceedings of the international conference on automated planning and scheduling, volume 19, pages 162–169, 2009.

[33] Metis. http://glaros.dtc.umn.edu/gkhome/ views/metis.

[24] Gonzalo Gomez Herrero and Jan Antón Bernal Van der Ven. Network Mergers and Migrations: Junos Design and Implementation. John Wiley & Sons, 2011.

[35] Francesco Percassi and Alfonso E Gerevini. On compiling away pddl3 soft trajectory constraints without using automata. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 29, pages 320–328, 2019.

[34] Microsoft Research. Z3 Theorem Prover. https:// github.com/Z3Prover/z3.

[25] Daniel Höller and Gregor Behnke. Encoding lifted classical planning in propositional logic. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 32, pages 134–144, 2022.

[36] Sivaramakrishnan Ramanathan, Ying Zhang, Mohab Gawish, Yogesh Mundada, Zhaodong Wang, Sangki Yun, Eric Lippert, Walid Taha, Minlan Yu, and Jelena Mirkovic. Practical intent-driven routing configuration synthesis. In 20th USENIX Symposium on Networked Systems Design and Implementation (NSDI 23), pages 629–644, 2023.

[26] Henry Kautz and Bart Selman. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of the national conference on artificial intelligence, pages 1194–1201, 1996. [27] Henry A Kautz, Bart Selman, et al. Planning as satisfiability. In ECAI, volume 92, pages 359–363, 1992.

[37] Silvia Richter and Matthias Westphal. The lama planner: Guiding cost-based anytime planning with landmarks. Journal of Artificial Intelligence Research, 39:127–177, 2010.

[28] Simon Knight, Hung X Nguyen, Nickolas Falkner, Rhys Bowden, and Matthew Roughan. The internet topology zoo. IEEE Journal on Selected Areas in Communications, 29(9):1765–1775, 2011.

[38] Jussi Rintanen. Planning as satisfiability: Heuristics. Artificial intelligence, 193:45–86, 2012.

[29] Ruihan Li, Yifei Yuan, Fangdan Ye, Mengqi Liu, Ruizhen Yang, Yang Yu, Tianchen Guo, Qing Ma, Xianlong Zeng, Chenren Xu, Dennis Cai, and Ennan Zhai. A general and efficient approach to verifying traffic load properties under arbitrary k failures. In Proceedings of the ACM SIGCOMM 2024 Conference, ACM SIGCOMM ’24, page 228–243, New York, NY, USA, 2024. Association for Computing Machinery.

[39] Jussi Rintanen. Madagascar: Scalable planning with sat. Proceedings of the 8th International Planning Competition (IPC-2014), 21:1–5, 2014.

[30] Yikai Lin, Mohab Gawish, Shih-Hao Tseng, Lixin Gao, Cen Zhao, John Tracey, Sunyi Shao, Hyojeong Kim, and Ying Zhang. Centralium: A hybrid route-planning framework for large-scale data center network migrations. In Proceedings of the ACM SIGCOMM 2025 Conference, pages 395–408, 2025.

[41] Enrico Scala. ENHSP: Expressive Numeric Heuristic Search Planner. https://sites.google.com/view/ enhsp/.

[31] Hongqiang Harry Liu, Xin Wu, Wei Zhou, Weiguo Chen, Tao Wang, Hui Xu, Lei Zhou, Qing Ma, and Ming Zhang. Automatic life cycle management of network configurations. In Proceedings of the Afternoon Workshop on Self-Driving Networks, SelfDN 2018, page 29–35, New York, NY, USA, 2018. Association for Computing Machinery.

[43] Tibor Schneider, Rüdiger Birkner, and Laurent Vanbever. Snowcap: Synthesizing network-wide configuration updates. In Proceedings of the 2021 ACM SIGCOMM Conference, pages 33 – 49, New York, NY, 2021-08. Association for Computing Machinery. ACM SIGCOMM 2021 Conference; Conference Location: Online; Conference Date: August 23-27, 2021.

[32] Thomas McCluskey and Mauro Vallati. Embedding automated planning within urban traffic management operations. In Proceedings of the International Conference on Automated Planning and Scheduling, volume 27, pages 391–399, 2017.

[44] Tibor Schneider, Roland Schmid, Stefano Vissicchio, and Laurent Vanbever. Taming the transient while reconfiguring bgp. In ACM SIGCOMM ’23: Proceedings of the ACM SIGCOMM 2023 Conference, pages 77 – 93, New York, NY, 2023-09. Association for Computing

[40] Jussi Rintanen, Keijo Heljanko, and Ilkka Niemelä. Planning as satisfiability: parallel plans and algorithms for plan search. Artificial Intelligence, 170(12-13):1031– 1080, 2006.

[42] Tibor Schneider. Snowcap Prototype. github.com/nsg-ethz/snowcap.

14

https://

Machinery. 37th ACM SIGCOMM Conference (SIGCOMM 2023); Conference Location: New York, NY, USA; Conference Date: September 10-14, 2023.

ACM SIGCOMM 2024 Conference, ACM SIGCOMM ’24, page 197–212, New York, NY, USA, 2024. Association for Computing Machinery.

[45] Irfansha Shaik and Jaco Van De Pol. Optimal layout synthesis for quantum circuits as classical planning. In 2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD), pages 1–9. IEEE, 2023.

[55] Benedict Wright, Robert Mattmüller, and Bernhard Nebel. Compiling away soft trajectory constraints in planning. In KR, pages 474–483, 2018. [56] Xieyang Xu, Yifei Yuan, Zachary Kincaid, Arvind Krishnamurthy, Ratul Mahajan, David Walker, and Ennan Zhai. Relational network verification. In Proceedings of the ACM SIGCOMM 2024 Conference, ACM SIGCOMM ’24, page 213–227, New York, NY, USA, 2024. Association for Computing Machinery.

[46] Arjun Singh, Joon Ong, Amit Agarwal, Glen Anderson, Ashby Armistead, Roy Bannon, Seb Boving, Gaurav Desai, Bob Felderman, Paulie Germano, et al. Jupiter rising: A decade of clos topologies and centralized control in google’s datacenter network. ACM SIGCOMM computer communication review, 45(4):183–197, 2015.

[57] Fangdan Ye, Da Yu, Ennan Zhai, Hongqiang Harry Liu, Bingchuan Tian, Qiaobo Ye, Chunsheng Wang, Xin Wu, Tianchen Guo, Cheng Jin, Duncheng She, Qing Ma, Biao Cheng, Hui Xu, Ming Zhang, Zhiliang Wang, and Rodrigo Fonseca. Accuracy, scalability, coverage: A practical configuration verifier on a global wan. In Proceedings of the Annual Conference of the ACM Special Interest Group on Data Communication on the Applications, Technologies, Architectures, and Protocols for Computer Communication, SIGCOMM ’20, page 599–614, New York, NY, USA, 2020. Association for Computing Machinery.

[47] David Speck, Robert Mattmüller, and Bernhard Nebel. Symbolic top-k planning. In Vincent Conitzer and Fei Sha, editors, Proceedings of the Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI 2020), pages 9967–9974. AAAI Press, 2020. [48] Alvaro Torralba, Vidal Alcázar, Daniel Borrajo, Peter Kissmann, and Stefan Edelkamp. Symba*: A symbolic bidirectional a* planner. In International Planning Competition, pages 105–108, 2014. [49] Arash Vahidi. JDD, a pure Java BDD and Z-BDD library. https://bitbucket.org/vahidi/jdd/.

[58] Yifei Yuan, Fangdan Ye, Yifan Li, Jingkai Zhang, Mengqi Liu, Yuyang Sang, Ruizhen Yang, Duncheng She, Zhiqing Ye, Tianchen Guo, Xiaobo Zhu, Xinji Tang, Li Jia, Zhongyu Guan, Lingpeng Su, Ci Wang, Ruiyang Feng, Shuo Wu, Zhonghui Xie, Cheng Jin, Peng Zhang, Qing Ma, Xianlong Zeng, Dennis Cai, and Ennan Zhai. New evolution of hoyan: Enhancing scalability, usability, and accuracy for alibaba’s global wan verification. In Proceedings of the ACM SIGCOMM 2025 Conference, SIGCOMM ’25, page 809–825, New York, NY, USA, 2025. Association for Computing Machinery.

[50] Alessandro Valentini, Andrea Micheli, and Alessandro Cimatti. Temporal planning with intermediate conditions and effects. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 9975– 9982, 2020. [51] Mauro Vallati, Daniele Magazzeni, Bart De Schutter, Lukás Chrpa, and Thomas McCluskey. Efficient macroscopic urban traffic models for reducing congestion: A pddl+ planning approach. In Proceedings of the AAAI conference on artificial intelligence, volume 30, 2016.

[59] Peng Zhang, Dan Wang, and Aaron Gember-Jacobson. Symbolic router execution. In Proceedings of the ACM SIGCOMM 2022 Conference, SIGCOMM ’22, page 336–349, New York, NY, USA, 2022. Association for Computing Machinery.

[52] Laurent Vanbever, Stefano Vissicchio, Cristel Pelsser, Pierre Francois, and Olivier Bonaventure. Seamless network-wide igp migrations. In Proceedings of the ACM SIGCOMM 2011 Conference, pages 314–325, New York, NY, USA, 2011. Association for Computing Machinery.

[60] Yihao Zhao, Xiaoxiang Zhang, Hang Zhu, Ying Zhang, Zhaodong Wang, Yuandong Tian, Alex Nikulkov, Joao Ferreira, Xuanzhe Liu, and Xin Jin. Klotski: Efficient and safe network migration of large production datacenters. In Proceedings of the ACM SIGCOMM 2023 Conference, ACM SIGCOMM ’23, page 783–797, New York, NY, USA, 2023. Association for Computing Machinery.

[53] Stefano Vissicchio, Laurent Vanbever, Cristel Pelsser, Luca Cittadini, Pierre Francois, and Olivier Bonaventure. Improving network agility with seamless bgp reconfigurations. IEEE/ACM Transactions on Networking, 21(3):990–1002, 2012. [54] Dan Wang, Peng Zhang, and Aaron Gember-Jacobson. Expresso: Comprehensively reasoning about external routes using symbolic simulation. In Proceedings of the

[61] Hang Zhu, Varun Gupta, Satyajeet Singh Ahuja, Yuandong Tian, Ying Zhang, and Xin Jin. Network planning 15

with deep reinforcement learning. In Proceedings of the 2021 ACM SIGCOMM 2021 Conference, SIGCOMM ’21, page 258–271, New York, NY, USA, 2021. Association for Computing Machinery.

A

Additional Evaluation Results

End-to-end Time (s)

Figure 11 and Figure 12 show the additional results on RRx2 and IGPx2 for evaluations introduced in §7.4 and §7.5, respectively.

Snowcap (Batfish) Snowcap (native)

103 10 1 10 5 0

50 Instance ID (a) RRx2

Smoothie Smoothie (grouped)

104 10 1 10 6 0

50 Instance ID (b) IGPx2

log (Compression ratio)

Figure 11: End-to-end time to find any safe sequential plan for RRx2 and IGPx2 instances using Snowcap, Batfish, and S MOOTHIE. For instances where S MOOTHIE does not finish in 100 seconds, we randomly divide all updates into 3 groups and separately simulate each group. Such instances are tagged as S MOOTHIE (grouped).

Snowcap (Batfish)

Snowcap (native)

100

100

50

50

0

0

50 Instance ID (a) RRx2

0

0

Smoothie

50 Instance ID (b) IGPx2

Figure 12: Compression ratio (Tinit × Nstates /Ttotal ) of incremental simulation (Snowcap and Batfish) and symbolic simulation (S MOOTHIE) for RRx2 and IGPx2 instances, compared to full simulation of all considered intermediate states.

16

Related documents

• Configuration Migration Planning through Decoupled Modeling and Searching#1297513
• ReMP: Low-Downtime Runtime Model-Parallelism Reconfiguration for LLM Serving#618115
• ReMP: Low-Downtime Runtime Model-Parallelism Reconfiguration for LLM Serving#287100
• Benchmarking LLM-Driven Network Configuration Repair#134517
• ConfigSpec: Profiling-Based Configuration Selection for Distributed Edge--Cloud Speculative LLM Serving#10329