CRII: SHF: Foundations for Stateful Network Programming

CRII：SHF：状态网络编程的基础

• 批准号: 1849622
• 负责人: Jedidiah McClurg
• 金额: $ 17.5万
• 依托单位: University of New Mexico
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-03-01 至 2019-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1849622&HistoricalAwards=false
• 关键词: CRII; SHF; Foundations; Stateful; Network

Billions of people use web-based services on a daily basis for a variety of tasks, such as communication, social networking, and navigation. These services rely on correct and efficient functioning of complex networked systems, which are prone to failures that are often caused by human error. Existing technologies such as software-defined networking (SDN) seek to reduce human error by providing centralized network management and programmability via a standard API, and by separating network management (the SDN "control-plane") from packet forwarding (the SDN "data-plane"). While centralization permits a single network controller to have a global view of the network--which simplifies the control logic--it suffers from severe scalability limitations when the size of a network increases. Moreover, modern SDN data-planes feature powerful, decentralized devices that are able to perform computations and update their local state based on packet contents, thereby allowing them to implement functionality traditionally restricted to the SDN control-plane. Such decentralization requires viewing a network program as a distributed system running on network hardware, rather than as a process running on a controller and interacting with switches. This project establishes a new approach for constructing modern network programs, viewed as distributed systems. The project's novelties are (i) a new abstraction for writing network programs that takes distribution into account and ensures that a network program correctly maintains distributed views of global state; and (ii) techniques for ensuring efficiency of network programs: the techniques ensure that network performance is not penalized by maintenance of global state. The project's impacts are (i) contributions to the general understanding of how to properly build distributed systems, and (ii) development of a language and associated tools which eliminate some of the difficulties domain experts face in building these systems.The key contribution is a thorough investigation of the network data-plane as a platform for executing dynamic, stateful code, resulting in a programming system which allows network functions to be realized in the data-plane, and ensures that network programs are verifiably correct and efficiently implementable. The project has two research thrusts. The first thrust focuses on generalizing and implementing event nets. While previous work introduced the concept of event nets (a Petri-nets-based abstraction) for event-driven programming in the context of SDN, this project enriches the event nets language with functionality needed to make it easily usable in other domains such as wireless sensor networking (WSN), internet of things (IoT), and data-centric programming. The resulting language allows programmers to write, for each of these domains, event-driven network programs that use global data structures to describe network-wide behavior, without having to handle unexpected data races during program execution on the (distributed) switches. Additionally, the project implements a compiler that produces executable code from an extended event net: specifically, the compiler automatically constructs a network program's distributed version that targets modern hardware such as Barefoot Network's Tofino chip. The second research thurst focuses on formalizing event nets. The project investigates an algebraic formalization of the extended event nets language, allowing (mechanized) formal reasoning about dynamic, stateful network programs. Finally, the project explores ways in which event nets can be used as a pedagogical tool in teaching undergraduate classes on Computer Networks.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.

每天有数十亿人使用基于Web的服务来完成各种任务，例如通信、社交网络和导航。这些服务依赖于复杂的网络系统的正确和有效的功能，而这些系统很容易因人为错误而发生故障。诸如软件定义网络（SDN）的现有技术试图通过经由标准API提供集中式网络管理和可编程性，以及通过将网络管理（SDN“控制平面”）与分组转发（SDN“数据平面”）分离来减少人为错误。虽然集中化允许单个网络控制器拥有网络的全局视图-这简化了控制逻辑-但当网络规模增加时，它会受到严重的可扩展性限制。此外，现代SDN数据平面具有强大的分散式设备，这些设备能够执行计算并基于数据包内容更新其本地状态，从而允许它们实现传统上限于SDN控制平面的功能。这种去中心化要求将网络程序视为在网络硬件上运行的分布式系统，而不是在控制器上运行并与交换机交互的进程。该项目建立了一种新的方法来构建现代网络程序，被视为分布式系统。该项目的新颖之处是（i）一个新的抽象编写网络程序，考虑到分布，并确保网络程序正确地维护全局状态的分布式视图;和（ii）技术，确保网络程序的效率：该技术确保网络性能不受惩罚的维护全局状态。该项目的影响是（i）对如何正确构建分布式系统的一般理解的贡献，以及（ii）消除领域专家在构建这些系统时面临的一些困难的语言和相关工具的开发。关键贡献是对网络数据平面作为执行动态，有状态代码的平台进行了彻底的调查，从而产生一种编程系统，该编程系统允许在数据平面中实现网络功能，并确保网络程序是可验证正确的和可有效实现的。该项目有两个研究重点。第一个重点是推广和实现事件网。虽然以前的工作在SDN的上下文中引入了事件网络（基于Petri网的抽象）的概念，但该项目丰富了事件网络语言，使其易于在其他领域使用，如无线传感器网络（WSN），物联网（IoT）和以数据为中心的编程。由此产生的语言允许程序员为这些域中的每一个域编写事件驱动的网络程序，这些程序使用全局数据结构来描述网络范围的行为，而不必在（分布式）交换机上执行程序期间处理意外的数据竞争。此外，该项目实现了一个编译器，从扩展的事件网络中产生可执行代码：具体来说，编译器自动构建一个网络程序的分布式版本，目标是现代硬件，如Barefoot Network的Tofino芯片。第二个研究集中在事件网的形式化。该项目研究了扩展事件网语言的代数形式化，允许（机械化）对动态，有状态的网络程序进行形式化推理。最后，该项目探讨了如何将事件网作为计算机网络本科教学的教学工具。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Dryadic: Flexible and Fast Graph Pattern Matching at Scale

Dryadic：灵活快速的大规模图形模式匹配

• DOI: 10.1109/pact52795.2021.00028
• 发表时间: 2021
• 期刊: 30th International Conference on Parallel Architectures and Compilation Techniques
• 作者: Mawhirter, Daniel;Reinehr, Samuel;Han, Wei;Fields, Noah;Claver, Miles;Holmes, Connor;McClurg, Jedidiah;Liu, Tongping;Wu, Bo
• 通讯作者: Wu, Bo

Correct-by-Construction Network Programming for Stateful Data-Planes

• DOI: 10.1145/3482898.3483362
• 发表时间: 2021-10
• 期刊: Proceedings of the ACM SIGCOMM Symposium on SDN Research (SOSR)
• 作者: Jedidiah McClurg