Correct-by-Construction Network Programming for Stateful Data-Planes
Correct-by-Construction Network Programming for Stateful Data-Planes
复制标题
DOI：
10.1145/3482898.3483362
复制
发表时间：
2021-10
期刊：
影响因子：
--
通讯作者：
Jedidiah McClurg
中科院分区：
文献类型：
--
作者：
Jedidiah McClurg
随着开关硬件变得更快，更状态和更可编程的功能，曾经仅限于结束主机或将控制平面推入数据平面。例如，最近关于自适应拥塞控制和重击球手检测的工作使用状态开关来实施复杂的功能，仅少量控制器参与。在正确性取决于单个开关做出连贯决策的应用程序中，重要的是，开关必须对全球状态保持一致的视图。但是，这种一致性要求使得由于CAP定理，因此很难保持效率（高吞吐量）。此外，以前关于数据平面编程的工作几乎没有内置的支持来解决这一困难。我们提出了回调状态机（CSM），这是一种新的高级声明网络编程抽象，允许操作员可以针对全球状态编写正确的数据平面程序。 CSM为程序员提供有用的一致性保证，而无需管理如何在单个开关级别复制/更新全局状态。为了帮助实施此高级编程框架，我们提出了一个灵活的新中间表示（IR），称为Tapir，本身支持状态数据平面功能，以及一个编译器来生成特定于设备的代码，例如Tapir代码的P4 。此外，我们通过使用它来构建康加拥塞控制系统的工作实施来证明TAPIR本身的力量。
As switch hardware becomes faster, more stateful, and more programmable, functionality that was once confined to end hosts or the control plane is being pushed into the data plane. For example, recent work on adaptive congestion control and heavy hitter detection uses stateful switches to implement sophisticated functionality with only minor controller involvement. In applications where correctness depends on individual switches making coherent decisions, it is important that the switches have a consistent view of global state. However, such a consistency requirement makes it difficult to maintain efficiency (high throughput), due to the CAP theorem. Moreover, previous work on data-plane programming provides little to no built-in support for addressing this difficulty. We propose Callback State Machines(CSMs), a new high-level declarative network programming abstraction which allows operators to write correct data-plane programs against global state. CSMs offer programmers useful consistency guarantees without the need to manage how global state is replicated/updated at the individual switch level. To aid in the implementation of this high-level programming framework, we present a flexible new intermediate representation (IR) called TAPIR that natively supports stateful data plane functionality, as well as a compiler to generate device-specific code such as P4 from TAPIR code. Additionally, we demonstrate the power of TAPIR itself by using it to build a working implementation of the CONGA congestion control system.