Switch Code Generation Using Program Synthesis
Switch Code Generation Using Program Synthesis
复制标题
DOI：
10.1145/3387514.3405852
复制
发表时间：
2020-07
期刊：
影响因子：
--
通讯作者：
Xiangyu Gao;Taegyun Kim;Michael D. Wong;Divya Raghunathan;A. Varma;Pravein G. Kannan;Anirudh Sivaraman;S. Narayana;Aarti Gupta
中科院分区：
文献类型：
--
作者：
Xiangyu Gao;Taegyun Kim;Michael D. Wong;Divya Raghunathan;A. Varma;Pravein G. Kannan;Anirudh Sivaraman;S. Narayana;Aarti Gupta
为可编程交换机流水线编写数据包处理程序极具挑战性，因为它们具有全有或全无的性质：程序要么在流水线资源允许的范围内以线速运行，要么根本无法运行。编译器有责任将程序纳入流水线资源。然而，使用重写规则生成交换机代码的交换机编译器经常会拒绝程序，因为这些规则无法将程序转换成可以映射到流水线有限资源的形式--即使实际上存在映射。本文介绍了一种编译器 Chipmunk，它将代码生成表述为程序合成问题。Chipmunk 使用程序合成引擎 SKETCH 将高级程序转换为交换机代码。然而，将代码生成天真地表述为程序合成会导致编译时间过长。因此，我们开发了一种新的特定领域综合技术--切片技术，它能将编译时间缩短 1-387 倍，平均缩短 51 倍。通过使用交换机硬件模拟器，我们发现 Chipmunk 能编译许多被以前基于规则的编译器 Domino 拒绝的程序。与 Domino 相比，Chipmunk 生成的机器代码的流水线级数也更少。用于 Tofino 可编程开关的 Chipmunk 后端表明，程序合成可以生成高速开关的机器代码。
Writing packet-processing programs for programmable switch pipelines is challenging because of their all-or-nothing nature: a program either runs at line rate if it can fit within pipeline resources, or does not run at all. It is the compiler's responsibility to fit programs into pipeline resources. However, switch compilers, which use rewrite rules to generate switch machine code, often reject programs because the rules fail to transform programs into a form that can be mapped to a pipeline's limited resources---even if a mapping actually exists. This paper presents a compiler, Chipmunk, which formulates code generation as a program synthesis problem. Chipmunk uses a program synthesis engine, SKETCH, to transform high-level programs down to switch machine code. However, naively formulating code generation as program synthesis can lead to long compile times. Hence, we develop a new domain-specific synthesis technique, slicing, which reduces compile times by 1-387x and 51x on average. Using a switch hardware simulator, we show that Chipmunk compiles many programs that a previous rule-based compiler, Domino, rejects. Chipmunk also produces machine code with fewer pipeline stages than Domino. A Chipmunk backend for the Tofino programmable switch shows that program synthesis can produce machine code for high-speed switches.