CRII: SHF: Foundations for Stateful Network Programming

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

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.