PaperlayerView exact revision on arXiv

Source-linked AI summary

Efficient Synthesis of Network Updates

Jedidiah McClurg, Hossein Hojjat, Pavol Cerny, Nate Foster

arXiv:1403.5843v3cs.PL

TL;DR

Global SDN updates are difficult to implement safely because individually updating distributed switches can create incorrect transient behavior. The paper formalizes updates and synthesizes property-preserving programs through counterexample-guided search and incremental model checking. The resulting tool supports efficient updates, scales to large networks, and reduces overhead relative to more expensive update mechanisms.

  • Problem

    Manually transitioning distributed switches between global configurations can create transient violations, while existing general consistency mechanisms impose substantial memory and rule-churn costs.

  • Method

    The system synthesizes update programs from initial and final configurations and an LTL property using counterexample-guided search with incremental model checking.

  • Results

    The implementation demonstrates effective synthesis on real-world networks, scales to over one-thousand switches, and achieves strong performance improvements over monolithic model-checking tools.

  • Takeaways & Limitations

    Property-directed synthesis can automatically produce correct update sequences while avoiding the unnecessary overhead of universally enforcing two-phase consistency.

  • Takeaways & Limitations

    The model assumes failure-free switches and links with bounded packet-processing time, and careful command sequences separate switch updates with waits.

Abstract

from arXiv · show

Software-defined networking (SDN) is revolutionizing the networking industry, but current SDN programming platforms do not provide automated mechanisms for updating global configurations on the fly. Implementing updates by hand is challenging for SDN programmers because networks are distributed systems with hundreds or thousands of interacting nodes. Even if initial and final configurations are correct, naively updating individual nodes can lead to incorrect transient behaviors, including loops, black holes, and access control violations. This paper presents an approach for automatically synthesizing updates that are guaranteed to preserve specified properties. We formalize network updates as a distributed programming problem and develop a synthesis algorithm based on counterexample-guided search and incremental model checking. We describe a prototype implementation, and present results from experiments on real-world topologies and properties demonstrating that our tool scales to updates involving over one-thousand nodes.

1. Introduction

SDN enables centralized control of programmable switches, but safely changing global network state remains difficult because switches update individually and intermediate configurations can violate desired behavior. The paper proposes automatically synthesizing property-preserving updates using formal specifications, counterexample-guided search, and incremental model checking, with experiments showing scalability and performance improvements.

  • Motivation: SDN centralizes control over programmable switches, enabling applications such as routing, traffic engineering, virtualization, and fine-grained access control.The controller responds to topology, traffic, and connection events by pushing forwarding rules to switches.
  • Problem: Global network changes are difficult because controllers modify one switch at a time, forcing programmers to construct intermediate configurations manually.These transitions are tedious and error-prone in distributed networks.
  • Problem: Intermediate update configurations can produce transient forwarding loops, black holes, access-control violations, service outages, and broken connections.Existing invariant-preservation techniques address only particular protocols and properties.
  • Prior approaches: Two-phase updates preserve consistency by ensuring packets use either the initial or final configuration, but they increase rule memory and update-time overhead.They maintain rules for both configurations simultaneously, which can strain switches with limited memory and cause rule churn.
  • Approach: The proposed system synthesizes correct update programs from initial and final configurations plus an LTL property, or reports failure when no valid program exists.Property-specific synthesis can use less restrictive strategies than universal two-phase consistency.
  • Contributions: The paper formalizes network updates, develops a correct counterexample-guided search algorithm, and introduces incremental LTL model checking for loop-free models.The implementation includes model-checking backends and experiments on real-world networks and properties.

2. Overview

The paper contrasts expensive two-phase consistency with ordering updates that preserve selected properties through carefully sequenced switch changes and waits. Its implementation synthesizes such updates and removes most unnecessary waits in practice.

  • Consistency and Two-Phase Updates: Two-phase updates preserve packet consistency but require switches to maintain both configurations, increasing memory use and update latency.The paper notes that rule changes can take about 10ms per rule, making the added churn costly.
  • Ordering Updates: Ordering updates can achieve consistency by choosing a correct switch-update order, such as updating C2 before A1 when shifting traffic between paths.For some target paths, no ordering achieves full consistency, motivating property-specific guarantees instead.
  • In-Flight Packets and Waits: Additional waits can enforce properties involving in-flight packets, while reachability-based analysis removes many waits in practice.The paper compares second-scale switch updates with microsecond-scale packet transit times.
  • Implementation and Summary: The implementation synthesizes updates for OpenFlow switches through Frenetic, including sequences with switch changes separated by a wait.An example updates A2, A4, and T1, waits, then updates C1 while preserving stated connectivity and traversal requirements.

3. Preliminaries and Network Model

The paper models networks operationally as interacting switches, links, packets, and a controller, then represents packet behavior as traces checked against LTL properties. Updates use atomic switch changes and waits to reason about safe transitions.

  • Network Model: The operational model represents switches, links, packets, and controller behavior using small-step transitions over network states.Figure 3 defines interactions between subsets of network elements according to OpenFlow-style semantics.
  • Commands: A switch-granularity command atomically replaces one switch’s forwarding table, while rule-granularity updates provide a finer alternative.The tool supports both modes but frames most discussion around switch-granularity updates.
  • Synchronization: The wait command increments the packet epoch and blocks until packets from the previous epoch have exited the network.The model uses epochs for reasoning; implementations may use a conservative delay instead of explicit synchronization.
  • Packet Traces: Single-packet traces capture end-to-end observations, and the model restricts attention to loop-free traces because forwarding loops can waste bandwidth and degrade performance.Trace observations are linked by a successor relation across monotonically increasing epochs.
  • Properties: LTL specifies trace-based properties such as reachability, while Kripke-structure soundness permits equivalent LTL model checking.The paper states that each single-packet trace corresponds to a trace of the network Kripke structure and vice versa.
  • Update Problem: For careful command sequences, checking each induced static network against the LTL property is sufficient to establish update correctness.Careful sequences separate every pair of switch updates with a wait.

4. Update Synthesis Algorithm

The synthesis algorithm searches for simple update orders, checks candidate configurations incrementally against LTL properties, and uses counterexamples to prune failures. The paper proves soundness and completeness for the stated class of careful sequences.

  • Algorithm: ORDERUPDATE searches for simple update sequences in which each switch appears at most once, failing when no such sequence exists.Its depth-first search incrementally adds switches to a candidate sequence.
  • Algorithm: Incremental model checking reuses Kripke-structure labels after a switch update, checking only nodes whose outgoing transitions changed.The update procedure returns the new network, changed-node set, and updated Kripke structure.
  • Search and Pruning: A true model-checking result lets the search recurse, whereas a false result triggers backtracking and counterexample-based pruning.Counterexamples identify configurations that can be excluded from future checks without repeating certain failures.
  • Search and Pruning: Early termination derives ordering constraints from counterexamples to stop searching when no switch-granularity update sequence is possible.A counterexample involving updated and non-updated nodes can impose precedence requirements.
  • Wait Removal: Wait removal eliminates synchronization when reachability proves that a switch cannot receive a packet traversing an earlier-updated switch.This optimization maintains reachability-between-switches information during the update.
  • Formal Properties: The algorithm is sound for returned careful updates and complete for simple careful sequences when such a sequence exists.Soundness guarantees correctness of returned commands; completeness guarantees finding a simple careful sequence if one exists.

5. Incremental Model Checking

The incremental model checker reuses labels from a previously checked Kripke structure, relabeling only states affected by an update and their ancestors. For loop-free structures, this yields correct LTL checks with work proportional to the affected region.

  • 5.1 State Labeling: The checker labels states with the LTL formulas satisfied by traces starting at each state, using specialized handling for sink and non-sink states.Sink states use Holds0 over their unique self-loop trace; non-sink states derive labels from successor labels.
  • 5.2 Incremental algorithm: Incremental checking reuses a prior labeling and updates labels only for modified nodes and their ancestors.If an update changes only node J, relabeling can propagate through J’s ancestors and stop when labels remain unchanged.
  • 5.2 Incremental algorithm: The relabeling procedure is correct when the prior labeling is correct outside the updated nodes’ ancestor set.Theorem 3 establishes that relabeling produces a correct labeling for the entire structure.
  • 5.2 Incremental algorithm: The incremental model checker returns true exactly when the updated Kripke structure satisfies the LTL property.This correctness result applies both to full model checking and to checks that reuse a previous labeling.
  • 5.2 Incremental algorithm: The full checker runs in O(|K| × 2^|ϕ|), whereas incremental checking runs in O(|ancestors_K(U)| × 2^|ϕ|).The incremental bound depends on the ancestors of the updated nodes U rather than the entire structure.

6. Implementation and Experiments

The prototype combines several model-checking backends with synthesis experiments on real and synthetic network topologies. Incremental checking substantially outperforms batch and comparison tools, while the synthesizer scales to updates involving more than one thousand switches.

  • Implementation: The prototype contains 7K lines of OCaml and supports Incremental, Batch, NuSMV, and NetPlumber checker backends.Incremental reuses labels, Batch relabels the whole graph, and NuSMV invokes a symbolic checker in batch mode.
  • Performance comparisons: 447.23x was the geometric-mean speedup over NuSMV on 247 completed Topology Zoo reachability inputs.Mean speedups were 465.03x on FatTree and 4484.73x on Small-World examples.
  • Performance comparisons: Incremental was faster than Batch on almost all examples, with mean speedups of 4.26x, 5.27x, and 11.74x across the three datasets.The experiments compare the Incremental and Batch solvers on the same inputs.
  • Performance comparisons: Incremental was faster than NetPlumber on all experiments, with mean speedups of 6.41x, 4.90x, and 17.19x across the three datasets.The comparison uses rule-granularity mode because NetPlumber performs rule-granularity updates.
  • Scalability: The tool handled Small-World topologies with up to 1500 switches, including a largest update involving 1015 switches.Maximum synthesis times for the three properties were 129.04s, 30.11s, and 0.85s.
  • Scalability: Rule-granularity solved switch-impossible instances for up to 1000 switches, with maximum times of 776.13s, 512.84s, and 82.00s.At switch granularity, the corresponding inputs were reported unsolvable.
  • Scalability: The wait-removal heuristic eliminated about 99.9% of waits in the largest experiments.It removed 1397/1399 waits in one experiment and 55823/55826 in another.

7. Related Work

The paper extends prior work with a more realistic model, an integrated incremental checker, optimized search, and broader evaluation. It differs from traditional concurrent-program synthesis and existing network-verification approaches in its reachability formulation and LTL-focused incrementality.

  • Extensions: This paper extends preliminary workshop work with a more precise network model, an integrated incremental checker, optimized search, and comprehensive real-world benchmarks.The revised system replaces expensive external checker calls and adds synthesis heuristics.
  • Synthesis of concurrent programs: Unlike traditional concurrent-program synthesis, the network-update problem searches configuration reachability rather than playing a scheduling game against an environment.Checking each network configuration is itself a model-checking problem.
  • Network updates: Prior network-update techniques are often protocol- or property-specific, whereas this work targets a broader class of updates using formal specifications.Earlier SDN work includes consistent updates and two-phase mechanisms, while other approaches address particular routing scenarios.
  • Model checking: The checker uses LTL properties and tracks which portions of a property hold at each node to keep incremental rechecks low.This differs from NetPlumber’s regular-expression specification and incrementality strategy.
  • Model checking: The incremental algorithm specializes prior incremental model-checking ideas to LTL properties and loop-free network structures.The paper exploits the no-forwarding-loops assumption in its algorithm.

8. Conclusion

The paper presents a practical tool for synthesizing correct network update sequences from formal specifications and identifies extensions for failures and bandwidth constraints.

  • The tool automatically synthesizes correct network update sequences from formal specifications.Experiments on real-world topologies demonstrate the approach’s effectiveness for synthesis.
  • The incremental model checker performs orders of magnitude better than state-of-the-art monolithic tools.
  • Future work includes handling network failures and bandwidth constraints and developing deeper foundations for network updates.

A. Network Model Auxiliary Definitions

The network model defines active forwarding tables, packet observations, successor relations, traces, and a Kripke structure that captures possible packet behaviors. Several lemmas connect dynamic command executions with equivalent sequences of static networks and traces.

  • Active tables and observations: An active forwarding table is the table the controller will eventually produce for a switch in a given epoch.The initial table is active in epoch 0; later epochs use scheduled updates or retain the prior active table.
  • Active tables and observations: A successor observation represents one packet-processing step through an internal link or out an egress.The step uses a switch table active in the relevant epoch.
  • Trace definitions: Unconstrained single-packet traces allow observations that need not begin at a host, while constrained traces impose host-start and terminating-egress conditions.
  • Kripke structures: The network Kripke structure represents states as switch, port, and packet-header sets, with transitions for forwarding, delivery, dropping, or reaching an egress.Its labeling function records the possible header values at each switch state.
  • Trace correspondence: The trace relation connects finite network observations to infinite Kripke traces by matching observed packets with the state labels and repeating the final observation.
  • Trace correspondence: For command sequences without update commands, single-packet traces are preserved across static networks, and induced dynamic sequences are pointwise trace-equivalent to their update-generated static configurations.Stable-network unconstrained traces can also be extended to constrained traces by adding a suitable prefix.

B. Synthesis Algorithm Correctness Proofs

The correctness proofs show that careful update sequences can be analyzed through induced static networks, enabling soundness and completeness guarantees for ORDERUPDATE. The algorithm returns updates reaching the final configuration while preserving the specified LTL property.

  • Trace and carefulness lemmas: The network Kripke structure is sound: every network single-packet trace corresponds to a Kripke trace, and vice versa.
  • Trace and carefulness lemmas: For a careful command sequence, every network trace belongs to some stable static network induced by that sequence.This reduces reasoning about dynamic updates to reasoning about the induced static configurations.
  • Careful correctness: If every induced static network satisfies an LTL formula, a careful command sequence is correct with respect to that formula.
  • Soundness: ORDERUPDATE returns a command sequence that reaches a configuration equivalent to the final configuration and is correct with respect to the specified LTL property.The algorithm checks the induced static networks and can enforce carefulness through adequate delays between updates.
  • Completeness: ORDERUPDATE is complete for simple, careful command sequences: if one exists, the algorithm returns such a sequence.This follows because the search examines all simple and careful sequences.

C. Incremental Checking Correctness Proofs

The incremental model-checking proofs establish that relabeling only affected ancestors preserves correct LTL labeling. Consequently, incremental checking returns the same satisfaction result as ordinary model checking.

  • Labeling correctness: Lemma 3 characterizes Holds for sink and non-sink states in terms of traces satisfying maximally consistent formula sets.
  • Relabeling: Relabeling ancestors of a vertex set preserves a labeling correct with respect to the LTL formula and the entire Kripke structure.The proof proceeds by induction over levels measured by longest simple paths to the affected vertices.
  • Incremental checking: The incremental model checker is correct: it returns true exactly when the Kripke structure satisfies the LTL formula.This matches the correctness condition of the ordinary model checker.
  • Incremental checking: The proof derives correctness by showing that relabeling the relevant state ancestors yields a correct labeling before initial states are checked.
Loading 1403.5843v3…