CRII: SHF: Foundations for Stateful Network Programming

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

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.