URL: https://doi.org/10.1145/3563766.3564085
Bibtex Entry:
@inproceedings{2023-Agarwal-hotnets, author = “Agarwal, Anup and Arun, Venkat and Ray, Devdeep and Martins, Ruben and Seshan, Srinivasan”, title = “Automating Network Heuristic Design and Analysis”, year = “2022”, isbn = “9781450398992”, publisher = “Association for Computing Machinery”, address = “New York, NY, USA”, url = “https://doi.org/10.1145/3563766.3564085”, doi = “10.1145/3563766.3564085”, abstract = “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.”, booktitle = “Workshop on Hot Topics in Networking (HotNets)”, pages = “8–16”, numpages = “9”, keywords = “congestion control, automated reasoning”, location = “Austin, Texas”, series = “HotNets ‘22”, month = “November” }