Optimizing horn solvers for network repair
Optimizing horn solvers for network repair
复制标题
优化喇叭求解器以进行网络修复
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
Nate Foster
中科院分区：
文献类型：
--
作者：
Hossein Hojjat;P. Rümmer;Jedidiah McClurg;Pavol Cerný;Nate Foster
自动修理会修改一个有缺陷的程序，以使其相对于规格正确基于修复不可分析的Horn条款集的更通用技术。引入挑战，例如浏览可能的维修空间，我们提出了一种保守的语义修复技术，该技术只能消除不正确的行为，并且不引入新的行为。可能的维修空间，并使用一种新颖的本地搜索技术，该技术利用启发式方法避免通过搜索搜索可行的维修。为了说明我们的方法的适用性，我们将其应用于软件定义的网络（SDN）中，并说明了它如何通过正确过滤UneSiled流量来帮助网络运营商修复错误的配置。晶格是该域中优化晶格的有效选择，我们启用了优化对象，例如修改最小数量的开关。工具，并在数据中心和拥挤网络中使用实际拓扑和现实维修方案对几个基准进行初步实验结果。
Automatic program repair modifies a faulty program to make it correct with respect to a specification. Previous approaches have typically been restricted to specific programming languages and a fixed set of syntactical mutation techniques — e.g., changing the conditions of if statements. We present a more general technique based on repairing sets of unsolvable Horn clauses. Working with Horn clauses enables repairing programs from many different source languages, but also introduces challenges, such as navigating the large space of possible repairs. We propose a conservative semantic repair technique that only removes incorrect behaviors and does not introduce new behaviors. Our proposed framework allows the user to request the best repairs — it constructs an optimization lattice representing the space of possible repairs, and uses a novel local search technique that exploits heuristics to avoid searching through sub-lattices with no feasible repairs. To illustrate the applicability of our approach, we apply it to problems in software-defined networking (SDN), and illustrate how it is able to help network operators fix buggy configurations by properly filtering undesired traffic. We show that interval and Boolean lattices are effective choices of optimization lattices in this domain, and we enable optimization objectives such as modifying the minimal number of switches. We have implemented a prototype repair tool, and present preliminary experimental results on several benchmarks using real topologies and realistic repair scenarios in data centers and congested networks.