FMitF: Transplanting Syntax-Guided Synthesis to Computer Networks

FMITF：将语法引导综合移植到计算机网络

• 批准号: 1837023
• 负责人: Xiaokang Qiu
• 金额: $ 74.2万
• 依托单位: Purdue University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1837023&HistoricalAwards=false
• 关键词: FMitF; Transplanting; Syntax; Guided; Synthesis

Computer networks are difficult to manage since there exists a wide gulf between the high-level goals that operators have for their networks (e.g., security, Quality of Service etc.), and the low-level configurations in heterogeneous devices in which such intent must be expressed. While the advent of Software-Defined Networking (an emerging technology that centralizes control decisions regarding how traffic must be handled, and separates them from the devices that actually forward each packet) helps, the process of designing networks is still ad-hoc, leading to high operational costs, design faults that account for a large fraction of network downtime, and costly security breaches. This project is motivated by the vision of design automation for networking, inspired by the success of the approach in other domains such as chip design. The project will develop methods for network architects to express their intent at higher levels of abstraction, and techniques to automatically synthesize low-level switch configurations that realize this intent correctly and efficiently.The project will tackle network automation through syntax-guided synthesis, which has been a popular paradigm embodied in many program synthesis systems. Rather than directly synthesize low-level switch flow-table rules and switch configurations like current network synthesis efforts, the project will explore how to synthesize code from user-provided sketches and specifications, corresponding to a network programming language, which may then be translated into low-level switch configurations. This approach will enable human experts to convey their insights and hints, which are critical for applying modern synthesis techniques. The project will develop a network programming language that is expressive yet has the necessary formal semantics to enable synthesis, explore the design space of sketches for network synthesis, and develop ways to improve the performance of synthesis for computer networks. The broader impact of this project is to raise the level of abstraction for managing large networks, leading to much lower management costs, better performance, security and reliability. The project will extensively involve graduate and undergraduate students, and incorporate new curriculum material in programming language and networking classes.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

计算机网络难以管理，因为在运营商对其网络的高级目标（例如，安全、服务质量等），以及必须在其中表达这种意图的异构设备中的低级配置。虽然软件定义网络（一种新兴技术，集中控制有关必须如何处理流量的决策，并将其与实际转发每个数据包的设备分离）的出现有所帮助，但设计网络的过程仍然是临时的，导致高运营成本，设计故障占网络停机时间的很大一部分，以及代价高昂的安全漏洞。该项目的动机是网络设计自动化的愿景，灵感来自于该方法在芯片设计等其他领域的成功。该项目将开发网络架构师在更高抽象层次上表达其意图的方法，以及自动合成正确有效实现此意图的低级交换机配置的技术。该项目将通过语法引导合成来解决网络自动化问题，这是许多程序合成系统中体现的流行范例。该项目将探索如何从用户提供的草图和规范中合成代码，而不是像当前的网络合成工作那样直接合成低级交换机流表规则和交换机配置，这些草图和规范对应于网络编程语言，然后可以转换为低级交换机配置。这种方法将使人类专家能够传达他们的见解和提示，这对于应用现代合成技术至关重要。该项目将开发一种网络编程语言，该语言具有表达能力，但具有必要的形式语义，以实现合成，探索网络合成草图的设计空间，并开发提高计算机网络合成性能的方法。该项目的更广泛影响是提高了管理大型网络的抽象水平，从而大大降低了管理成本，提高了性能、安全性和可靠性。该项目将广泛涉及研究生和本科生，并将新的课程材料纳入编程语言和网络课程。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估。

项目成果

Reconciling enumerative and deductive program synthesis

协调枚举和演绎程序综合

• DOI: 10.1145/3385412.3386027
• 发表时间: 2020
• 期刊: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation
• 作者: Huang, Kangjing;Qiu, Xiaokang;Shen, Peiyuan;Wang, Yanjun
• 通讯作者: Wang, Yanjun

Program synthesis with algebraic library specifications

使用代数库规范进行程序综合

• DOI: 10.1145/3360558
• 发表时间: 2019
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Mariano, Benjamin;Reese, Josh;Xu, Siyuan;Nguyen, ThanhVu;Qiu, Xiaokang;Foster, Jeffrey S.;Solar-Lezama, Armando
• 通讯作者: Solar-Lezama, Armando

Learning Network Design Objectives Using A Program Synthesis Approach

使用程序综合方法的学习网络设计目标

• DOI: 10.1145/3365609.3365861
• 发表时间: 2019
• 期刊: Proceedings of the 18th ACM Workshop on Hot Topics in Networks - HotNets '19
• 作者: Wang, Yanjun;Jiang, Chuan;Qiu, Xiaokang;Rao, Sanjay G.
• 通讯作者: Rao, Sanjay G.

Comparative Synthesis: Learning Near-Optimal Network Designs by Query

• DOI: 10.1145/3571197
• 发表时间: 2023-01-01
• 期刊: PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL
• 影响因子: 1.8
• 作者: Wang，Yanjun;Li，Zixuan;Rao，Sanjay
• 通讯作者: Rao，Sanjay

Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations

用于位向量操作的语法引导合成的增强枚举技术

• DOI: 10.1145/3632913
• 发表时间: 2024
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Ding, Yuantian;Qiu, Xiaokang
• 通讯作者: Qiu, Xiaokang