CRII: SHF: Foundations for Stateful Network Programming

点击翻译按钮获取中文摘要

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.