Program Synthesis for Network Updates
Joint Talk with Department of Mathematics - Talk is at 4:00 PM in BESC 185. Refreshments will be at 3:30 PM in MATH 350.
;Ìý
Date and time:Â
Friday, February 28, 2014 - 4:00pm
³¢´Ç³¦²¹³Ù¾±´Ç²Ô:Ìý
BESC 185
´¡²ú²õ³Ù°ù²¹³¦³Ù:Ìý
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 talk 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 modelchecking algorithm. We present experimental results showing that it efficiently generates updates for real-world topologies with thousands of nodes.