- UCAR Home
- About Us
- For Staff
Tuesday, April 15, 2014
10:00 AM – 11:00 AM
NCAR Mesa Lab Main Seminar Room
Program Synthesis for Network Updates
We first give a brief overview of the new field of program synthesis. We describe the role that declarative, logical specifications can play in making programmers more efficient. Second, we describe an application of this approach: synthesis of programs that update network configurations.
Configuration updates are a leading cause of instability in networks. A key factor that makes updates difficult to implement is that networks are distributed systems with hundreds or thousands of nodes all interacting with each other. Even if the initial and final configurations are correct, naively updating individual nodes can easily cause the network to exhibit incorrect behaviors such as forwarding loops, black holes, and security vulnerabilities. This paper presents a new approach to the network update problem: we automatically generate updates that are guaranteed to preserve important correctness properties, given in a temporal logic. Our system is based on counterexample-guided search and incorporates heuristics that quickly identify correct updates in many situations. We exploit the fact that the search algorithm asks a series of related model checking questions, and develop an efficient incremental LTL model checking algorithm. We present experimental results showing that it efficiently generates updates for real-world topologies with thousands of nodes.