Configuration Migration Planning through Decoupled Modeling and Searching

• Operators need safe update orders that prevent traffic disruption and transient or persistent routing violations, while also accommodating varied operational intents.Source: §1 · p. 1
• Existing migration planners focus on safe sequential plans but have limitations in efficiency, scalability, completeness, and support for optimal or parallel plans.Source: §1 · p. 2
• Smoothie encodes migration safety in PDDL and separates problem modeling from plan search, allowing different backend planners to address different planning tasks.Source: §1 · p. 2
• Symbolic simulation represents updates with Boolean variables and simulates routing and forwarding behavior, assuming deterministic convergence.Source: §1 · p. 2
• Up to thousands of configuration updates are compressed into no more than 3 parallel steps; most planning tasks finish in less than 1 hour.Source: §1 · p. 2

2.1 Manual Migration Planning is Hard

• A real CSP's seemingly simple iBGP-to-eBGP migration took experienced operators one month to plan, and the initial update order caused multi-path inconsistency and indirect routing.The route choice sent traffic along a longer path instead of the direct path, while packets sent to different routers became inconsistent.Source: §2.1 · pp. 2–3

2.2 Diverse Migration Planning Tasks

• Safe migration orders must preserve route availability and avoid forwarding loops, yet the example has 7! safe plans from which operators may choose.Operators may prefer sequential execution, satisfy soft ordering constraints, or minimize steps with a parallel plan.Source: §2.2 · p. 3
• Operators may seek a safe sequential plan quickly, optimize operational preferences, or minimize steps through parallel planning.Parallel plans also avoid imposing a total order on independent updates.Source: §2.2 · p. 3

2.3 Limitations of Existing Work

• Existing migration planners are tied to particular search algorithms, while different planning tasks call for different strategies, motivating a customizable framework.The passage contrasts DFS-based preference search with A* or weighted A* for sequential plans and SAT/SMT methods for parallel plans.Source: §2.3 · p. 4

2.4 SMOOTHIE Preview

• Smoothie symbolically simulates the control plane to encode a migration problem in PDDL, which can then be solved by off-the-shelf planners.The preview applies this framework to the iBGP-to-eBGP migration and produces a sequential plan.Source: §2.4 · p. 4
• Both previewed plans are safe, and the parallel plan removes the session identified as causing longer forwarding paths at the outset.Operators valued avoiding multi-path inconsistency over preserving equivalent paths; an added preference to avoid path reduction conflicted with that safety property and left the plans unchanged.Source: §2.4 · p. 4

3.1 Preliminaries to Automated Planning

• Classical automated planning models finite discrete states, deterministic actions, and transitions from an initial state to goal states; PDDL separates domain and problem descriptions.The domain defines shared predicates and actions; the problem specifies objects, initial state, and goals.Source: §3.1 · p. 4

3.2 Automated CMP

• A migration maps each update to a Boolean state variable, starts with all updates unapplied, and reaches a goal where all are applied.Applying an update requires that it has not already been applied and that the current state is safe.Source: §3.2 · p. 5
• Decoupling safety modeling from plan search lets Smoothie use existing planners optimized for sequential, optimal, and parallel objectives.PDDL also supports additional soft constraints, such as update-duration preferences, with dedicated planners.Source: §3.2 · p. 5

3.3 Challenges and Our Approach

• Concrete simulation can require 2^n rounds for n updates, so Smoothie uses symbolic simulation to identify safe states across the large state space.Symbolic states can exploit equivalences among intermediate configurations.Source: §3.3 · p. 5
• For parallel plans, Smoothie encodes ∀-step semantics with SMT: every intermediate state between grouped updates must be safe.This semantic check avoids relying on syntactic overlap to determine whether updates are independent.Source: §3.3 · pp. 5–6

4 Symbolic Simulation

• Smoothie extends SRE symbolic simulation by generalizing how symbolic routes are initialized and transferred for configuration migrations.Figure 4 presents the symbolic simulation process.Source: §4 · p. 6, Figure 4 · p. 7

4.1 Configuration Symbolization

• Each configuration difference becomes an insertion, removal, or modification update, represented by a Boolean indicating whether it has been applied.The variable determines whether the corresponding configuration component exists in a given state.Source: §4.1 · p. 6

4.2 Symbolic Route Computation

• Symbolic route computation initializes, transfers, and merges routes until switch RIBs reach a fixpoint.A symbolic route pairs a concrete route with the condition under which it becomes the best route.Source: §4.2 · p. 6
• Conditional route modifications encode symbolic transfer functions across configuration states, generalizing SRE’s link-failure model.The model covers states where different concrete transfer functions apply.Source: §4.2 · p. 6

4.3 Symbolic Packet Forwarding

• Symbolic packet forwarding propagates packet equivalence classes and records forwarding paths and statuses across configuration states.Statuses include arrival, looping, and dropping.Source: §4.3 · p. 7

5 PDDL Generation

• A common PDDL template is specialized by filling in scenario-specific safety and preference constraints, and users may further edit the generated file.The template represents migration updates and safe intermediate states.Source: §5 · p. 7

5.1 Encoding Safety Constraints

• Safety conditions become preconditions on update actions, preventing plan expansion through unsafe states.The encoded properties include routing and forwarding requirements; constant-true or constant-false safety formulas can identify immediately whether any plan is safe.Source: §5.1 · pp. 7–8

5.2 Encoding Preferences

• Soft preference violations add plan cost rather than blocking a plan, allowing planners to favor plans satisfying more preferences.Supported precedence preferences favor applying one update before another.Source: §5.2 · p. 8

5.3 Optimizations

• Global reachability can produce formulas that make search intractable; safety constraint simplification replaces it with equivalent control-plane reachability and data-plane loop-freedom conditions.The equivalence holds when no data-plane packet filtering or rewriting configuration exists, and the simpler formula avoids planner-side minimization.Source: §5.3 · pp. 8–9

6 Plan Searching

• The SMT-based planner tests increasing plan lengths k and returns the shortest plan found.For each k, it encodes the existence of a k-step plan as SMT constraints.Source: §6 · p. 9
• States are bit-vectors marking applied updates, and the constraints encode initial and goal states plus transitions between successive states.A successor state retains all updates already applied and adds at least one update.Source: §6 · p. 9
• Under ∀-step parallelism, every intermediate state between successive plan states must be safe, ensuring the grouped updates work in any order.The transition constraints encode this safety requirement.Source: §6 · p. 9

7.2 Plan Qualities

• FM2RR sequential plans use up to two orders of magnitude fewer steps than updates, while RRx2 plans usually have roughly as many steps as updates.Many FM2RR session removals do not affect safety; for the GtsPoland example, one removal order creates a forwarding loop, while SMOOTHIE exposes the consequential ordering constraints.Source: §7.2 · p. 10, Figure 7 · p. 10
• ≤3 steps suffice for the shortest parallel plans in every non-timeout instance, compressing hundreds or thousands of updates.Figure 6 compares update counts with parallel-plan steps for FM2RR and RRx2.Source: Figure 6 · p. 10, §7.2 · p. 10

7.4 Comparison with SOTA

• Snowcap takes less than 0.1s on all instances, versus SMOOTHIE's O(10)s on FM2RR and LPx2 and O(10^3)s on NetAcq.Snowcap's simpler simulator and mostly backtrack-free scenarios explain its speed; with Batfish as simulator, Snowcap is slower than SMOOTHIE for most cases.Source: Figure 9 · p. 11, §7.4 · p. 11

7.3 Performance on Different Tasks

• Different planners excel on different tasks: ENHSP finishes most optimal searches within 100 seconds, while the parallel planner finds shortest plans in under one minute except for 7 FM2RR timeouts.For around 45% of instances, parallel planning is more efficient than sequential planning; sequential search unrolls the transition relation once per update.Source: Figure 8 · p. 10, §7.3 · p. 11

7.5 Scalability of Symbolic Simulation

• Incremental simulation's compression ratio is generally under 10, while SMOOTHIE's rises on larger state spaces; grouping causes sharp drops.SMOOTHIE's compression is higher on FM2RR than on NetAcq and LPx2 because FM2RR has a larger state space with greater equivalence.Source: Figure 10 · p. 11, §7.5 · p. 12

Configuration Migration in the traditional networks

• Some traditional-network approaches run initial and final configurations in parallel, gradually switching traffic to the final data plane while avoiding forwarding loops.The required control- and data-plane duplication creates overhead and needs router support, impeding deployment.Source: §8 · p. 12
• Progressive configuration-update planners preserve correct routing or forwarding behavior after each step without requiring special router support.The paper contrasts these tools with SMOOTHIE on support for diverse operational intents.Source: §8 · p. 12

Physical Infrastructure Migration

• Physical infrastructure migration adds, removes, or swaps switches and links; existing tools automate transitions using traffic models.Whether SMOOTHIE can capture this setting's safety constraints and diverse intents is future work.Source: §8 · p. 12

9 Discussion

• Temporary updates can enable safe plans unavailable when updates are restricted to differences between initial and final configurations.The discussion gives temporary removal of equal-cost static routes as an example and notes that broader temporary-update support and automatic selection are needed.Source: §9 · p. 12
• SMOOTHIE models converged states rather than transient behavior during convergence, so complementary techniques can manage each update's safe execution after update ordering.The discussion names Chameleon for BGP and for IGP.Source: §9 · p. 12
• When network convergence is nondeterministic, SMOOTHIE considers safety for only one possible converged outcome.Source: §9 · p. 12
• Preliminary experiments suggest LLMs can plan sequential migrations from PDDL inputs, but optimal and parallel planning may require more attempts and lack optimality or shortest-plan guarantees.The experiments used synthetic cases; natural-language tests found precomputed safety information improved accuracy and reduced time and token usage.Source: §9 · p. 12

10 Conclusion

• SMOOTHIE supports diverse network designs and operational preferences, including safe parallel plans, by decoupling safety and preference encoding from plan search.Source: §10 · p. 12
• Most sequential-planning cases finish within 1 hour.Source: §10 · p. 12
• Large migrations can be compressed into no more than 3 parallel steps.Source: §10 · p. 12

A Additional Evaluation Results

• The appendix adds results for evaluations introduced in §7.4 and §7.5.Source: A Additional Evaluation Results · p. 16
• Figure 11 compares end-to-end time to find a safe sequential plan for RRx2 and IGPx2 instances using Snowcap, Batfish, and SMOOTHIE.Instances where SMOOTHIE does not finish within 100 seconds are also shown with updates divided randomly into three groups and simulated separately.Source: Figure 11 · p. 16
• Figure 12 compares incremental simulation by Snowcap and Batfish and symbolic simulation by SMOOTHIE against full simulation of intermediate states, using compression ratio.Source: Figure 12 · p. 16