Automating network heuristic design and analysis
Automating network heuristic design and analysis
复制标题
DOI：
10.1145/3563766.3564085
复制
发表时间：
2022-11
期刊：
影响因子：
--
通讯作者：
Anup Agarwal;V. Arun;Devdeep Ray;R. Martins;S. Seshan
中科院分区：
文献类型：
--
作者：
Anup Agarwal;V. Arun;Devdeep Ray;R. Martins;S. Seshan
启发式算法在计算机系统中无处不在。示例包括拥塞控制、自适应比特率流、调度、负载平衡和缓存。在某些领域，理论证明已经提供了保证启发式有效的条件。这在所有领域都是不可能的，因为证明这种保证可能涉及组合推理，使其变得困难，繁琐和容易出错。在本文中，我们认为，计算机应该帮助人类的组合推理的一部分。我们将推理问题建模为推理公式[1]，并使用反例引导归纳合成（CEGIS）框架解决它们。作为初步证据，我们原型CCmatic，一个工具，半自动合成拥塞控制算法，可证明是强大的。它重新发现了一个最近的拥塞控制算法，可证明实现高利用率和有限的延迟下具有挑战性的网络模型。它还发现了以前未知的算法变体，实现了不同的吞吐量-延迟权衡。
Heuristics are ubiquitous in computer systems. Examples include congestion control, adaptive bit rate streaming, scheduling, load balancing, and caching. In some domains, theoretical proofs have provided clarity on the conditions where a heuristic is guaranteed to work well. This has not been possible in all domains because proving such guarantees can involve combinatorial reasoning making it hard, cumbersome and error-prone. In this paper we argue that computers should help humans with the combinatorial part of reasoning. We model reasoning questions as ∃∀ formulas [1] and solve them using the counterexample guided inductive synthesis (CEGIS) framework. As preliminary evidence, we prototype CCmatic, a tool that semi-automatically synthesizes congestion control algorithms that are provably robust. It rediscovered a recent congestion control algorithm that provably achieves high utilization and bounded delay under a challenging network model. It also found previously unknown variants of the algorithm that achieve different throughput-delay trade-offs.