软件学报  2020, Vol. 31 Issue (8): 2285-2308   PDF    
一种包解析器硬件配置描述语言及其编译结构
李璜华1 , 李凌1 , 赵宇2 , 王生原1 , 李翔宇3     
1. 清华大学 计算机科学与技术系, 北京 100084;
2. 北京信息科技大学 理学院, 北京 100192;
3. 清华大学 微电子学研究所, 北京 100084
摘要: 设计了一种用于实现可重构网络数据包解析器的专用硬件配置描述语言P3.由于要有利于高安全等级网络的实现,侧重于从高可信性角度进行语言设计,包括形式化定义该语言的类型系统和操作语义,以及设计其可信编译结构.基于对可重构硬件基本需求的充分理解,从软硬件协同角度出发,最终明确了P3语言的核心特性及其编译器P3C的可信编译结构.由于可重构数据包解析器是软件定义网络(SDN)、可编程数据平面的重要一环,因此,实现P3C的可信编译结构将对SDN的安全性具有重大意义.期待P3C项目的开展能够促进网络与形式化领域相关工作的进一步研究.
关键词: 领域专用语言    可重构数据包解析器    形式语义    可信编译    软件定义网络    
Specification Language for Packet Parsers and Its Compiler Architecture
LI Huang-Hua1 , LI Ling1 , ZHAO Yu2 , WANG Sheng-Yuan1 , LI Xiang-Yu3     
1. Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China;
2. School of Applied Science, Beijing Information Science and Technology University, Beijing 100192, China;
3. Institute of Microelectronics, Tsinghua University, Beijing 100084, China
Abstract: This paper designs a domain-specific language P3 for reconfigurable protocol-independent packet parsers. Due to the requirement to facilitate the implementation of a high-security network, the language is designed from the perspective of high trustworthiness, including the formal definition of type system and operational semantics of the language and its trusted compiler architecture. Based on the full understanding of the basic requirements of the reconfigurable hardware, from the view of hardware-software codesign, the core characteristics of P3 language and its trusted compiler architecture named P3C are finally defined. As the reconfigurable packet parser is an important part of SDN and programmable data plane, implementing the trusted compiler architecture of P3C will be of great significance to the security of SDN. It is expected that the development of P3C project will promote the further research in the field of network and formal method.
Key words: domain-specific language    reconfigurable packet parser    formal semantics    trustworthy compiler    software-defined networking    

互联网的实现, 需要相应的网络设备对网络数据包进行处理和转发.考虑到处理速度, 目前大多数的交换机芯片都是采用固定功能的专用硬件实现, 如Broadcom公司的Trident[1]芯片.这样的交换机一经部署, 就只能支持固定的网络协议, 它具有很明显的缺陷.

●   首先, 近年来, 互联网产业发展迅猛, 各种新型网络技术层出不穷, 出现了大量的新型协议如MPLS[2], GRE[3]等.为了适应这些新的网络协议, 运营商只能反复更新网络的中转设备.然而开发新的硬件并推广一个新的硬件标准是十分花费时间和金钱的, 如VxLAN[4]协议在其被提出3年后才被新的硬件标准支持.

●   其次, 这种固定功能的硬件设备往往采用“自底向上”的设计模式, 在这种设计模式下, 设计者需要首先考虑芯片的数据清单, 确认硬件的资源能满足设计的要求后, 再规划好如何利用这些资源, 然后在这之上设计功能的实现.这对于设计者来说是十分不方便的, 因为设计者往往更自然地以“自顶向下”的方式来考虑问题, 即设计数据包的解析、处理和转发等过程的逻辑, 而不愿意考虑硬件的实现细节.

为了提高网络中转设备的通用性和灵活性、简化开发者的开发过程, 相关研究人员做出了大量的努力.

软件定义网络(software-defined networking, 简称SDN)[5]将控制平面和数据平面分离, 给予操作者对控制平面进行编程的能力, 由控制平面通过统一、标准的接口对不同的网络设备进行配置和管理.通过这种方式, SDN把网络设备逐渐变为可编程的软件平台, 操作者可以“自顶向下”地通过编程决定各网络设备的行为.

2013年, Bosshart等人提出了可编程交换机的抽象转发模型[6], 为实现可编程数据平面提供了可能.在这个模型中, 数据包在进行转发时会通过一连串的可重配置的匹配动作表(reconfigurable match-action tables, 简称RMT), 通过对这些灵活的匹配动作表的重新配置, 就可以使交换机支持不同的对数据包的处理、转发方式.2014年, Bosshart等人在抽象转发模型的基础上进一步提出了P4语言[7], 为可编程交换机提供了一种高级编程语言.P4语言专注于描述数据包在匹配动作表中被处理的逻辑过程, 并通过相应的编译器实现其到具体硬件的配置, 符合“自顶向下”的设计模式.P4具有对数据平面的重配置能力、协议无关性以及目标硬件无关性, 极大地提高了对交换机编程的通用性和灵活性, 也方便代码的跨平台迁移.自此, 可编程数据平面逐渐兴起, SDN的潜能得到了更大的开发.

软件的安全性始终是软件工作者感兴趣的话题, 随着P4的兴起, 软件工作者也开始尝试用形式化方法来验证P4程序的可靠性, 从而提高SDN的安全性.2018年, Liu等人[8]设计并开发了一个用于P4程序正确性验证的工具P4v, 该工具首先将P4程序转译为GCL(guarded command language), 然后通过添加特定注释并利用符号执行技术来验证P4程序的逻辑正确性.作者在他们的工作中指出, 相关的开源P4编译器是存在bug的, 因此他们构建了一个独立的编译器前端包括解析器、类型检查以及到GCL的翻译器.尽管这极大地提高了P4程序的可信度, 但P4程序和转换的GCL之间的一致性仍然是难以保证的, 所以Liu等人也把设计一个可验证的编译器甚至可验证的硬件作为感兴趣的未来研究工作.Lopes等人研究实现了一个基于Z3求解器的原型工具[9], 可用于验证P4编译过程(verifying P4 compilation).Kheradmand等人为P4语言定义了一种基于K-框架的形式语义[10], 并借助K-框架近期开发的原型工具KEQ[11], 给出一种实现P4编译过程的翻译确认[12]解决方案.

交换机在工作时, 第1步是实现数据包的解析.为了实现解析器的快速设计, Benacek等人[13]将P4语言编写的解析器程序映射到固定的硬件架构中, 可以快速生成解析器对数据包进行灵活的解析, 但没有实现资源的复用.李翔宇课题组为此提出了一种通过静态配置可以实现不同解析逻辑的数据包解析器基本处理单元(process element, 简称PE)[14], 经由编译器(本文工作)生成的配置文件配置后, 可用于任何一层协议(可自定义)的解析, 并通过流水线式级联的方式来搭建可以支持各种协议集合的可重构数据包解析器, 具有更少的资源占用率、更好的性能和更高的灵活性.本文工作的出发点之一就是围绕这一可重构数据包解析器进行软硬件协同设计, 提出并实现一种与硬件设计匹配的硬件配置描述语言.

本文工作的大背景是服务于一种高安全交换芯片的设计与实现, 需要从高安全可信的角度设计和实现这种硬件配置描述语言, 因此提出P3语言(specification language for reconfigurable protocol-independent packet parsers).P3语言比P4语言要简单很多, 仅面向上述可重构数据包解析器的设计.P4语言描述的是整个数据平面, 包括数据包的解析、处理和转发过程, 对于仅仅数据包解析器来说, 使用P4语言太过庞大冗余, 因此实现P4语言的安全可信编译器难度大、周期长, 不能满足本文工作的项目要求.为实现P3语言, 我们设计了具有高安全可信等级的P3C编译器结构, 可极大地提高网络数据包解析以至于SDN的安全性.

本文第1节对所针对的可重构数据包解析器硬件设计进行概述.第2节将介绍P3语言的核心特性.第3节介绍对P3类型系统进行严格规范以实现静态语义检查的设计工作.第4节为P3定义一种操作语义风格的形式化动态语义.第5节介绍P3语言编译器P3C的可信编译结构.

1 可重构数据包解析器硬件设计概述

本文工作的大背景是服务于一种高安全交换芯片的设计与实现, 该芯片的可重构Parser模块用于对输入数据包的头部信息(以太报文的L2~L4等头部)加以识别, 得到并修改后续业务处理所需要的相关字段.可重构Parser的总体结构如图 1所示, 整体是一个流水线结构, 由相同的基本处理单元(PE)级联而成, 这些PE被配置单元(PE_config)写入的配置文件配置成用于不同层的协议解析单元, 配置文件由编译器生成.从L2到L4, 包括各级子层(L2S, L3S), 每层的协议解析对应一级PE.PE间通过帧寄存器(frame, 也称为PKT寄存器)和中间值寄存器堆(intermediates register file, 简称IRF)进行数据交换.输入的数据包包头(PKT_header)会在frame数据通路中进行传输, 由一系列PE单元对包头封装中的协议进行逐层解析, 并将提取出的关键字段及处理结果存放到IRF中.

Fig. 1 Architecture of a packet parser 图 1 包解析器的整体架构

下面我们以一个简化的业务需求为例, 对该Parser进行直观说明.假设该解析器的输入为报文的头部, 我们需要从该报文头部中解析得到一些描述字段——包括报文类型(IPV4/IPv6/MPLS…)、L2/L3/L4封装头的偏移量、是否采用VLAN等.该报文头部首先进入frame数据通路, 并通过frame传入各个PE之中.接着, 各个PE会依次对该报文头部进行处理:首先, 在PE_L2层中可以提取出L2封装头的信息, 包括L2封装头的长度和是否采用了VLAN, 并将之存入IRF中; 然后, 根据L2封装头的长度给下一层传送偏移量(offset)信息, PE_L2S则根据该offset调整解析包头的区间(即对齐); 之后, 每层处理时也皆是如此.除了offset信息, 各PE还会给下一层传送一个bypass信号, 用于实现跨层处理, 比如Ethernet+IPv4+…的数据包, 在PE_L2层完成了Ethernet的解析, 而IPv4是在PE_L3层解析的, 因此需要跳过L2子层, 这时, PE_L2发出的bypass信号就会告诉PE_L2S不用处理, 直接跳过.按照这种方式, 各PE依序进行处理, L3层的报文类型(IPV4/IPv6/MPLS…)和L3封装头偏移量将在PE_L3处理完后存入IRF中, L4封装头偏移量则在PE_L4处理完后得到.

该数据包解析器的核心部分是一系列的可重构PE模块, 这些PE模块通过编译器生成的配置文件配置实现不同的硬件解析逻辑, 从而支持对不同协议包头的解析.

每一层的包头解析在PE中可以概括为提取、查找、动作这3个过程, 图 2为PE的硬件示意图, 包含了若干Cell单元、PE_bypass模块和Offset模块等.其中, 核心模块是Cell单元, 包头解析的3个过程都在Cell单元中完成, 它共包含PA, PB, PCAction几个部分.PA模块完成“提取”过程, 用来实现特定的数据域的提取, 它根据前一级PE输出的关键字段偏移量offsetIRF中的一些状态信息对本级frame寄存器中的数据包头部字段进行提取.PA层的输出送入PB层, PB层的核心是一个特征匹配查找表, 它将PA提取出来的关键字与一系列特征匹配模版进行对比, 找到匹配的模版, 模版的编号即对应协议的类型.根据协议类型和一些字段值, 可以判断下层需要解析的协议, 若需要跨层处理, PB就会往PE_bypass模块发送一个信号表示跳过下一层.PB中的特征模版完全根据PE_config写入的配置文件配置而成.PC的核心是一组查找表, 它的输入是PB输出的协议类型编号, 输出为根据类型编号索引得到的应该执行的操作指令, 和下一级解析时所需要设置的offset.同PB一样, PC的表项内容也是由PE_config配置而成.Action是一个指令执行模块, 根据PC索引的操作指令执行相应动作, 并把结果写入IRF中.为了提高硬件资源的复用率和通用扩展性, 硬件设计者设计了两种不同的Cell形式: Cell_ACell_B, 以1个Cell_A、0~2个Cell_B的形式组成PE实现并行解析, 其中, 计算offset和给PE_bypass传递信号只在Cell A中进行, Cell B仅包含其他解析过程.

Fig. 2 Architecture of a PE 图 2 PE结构

2 P3语言的设计

基于前面一节所述的可重构解析器架构, 本文设计了一种可重构数据包解析器的专用硬件配置描述语言P3, 作为较抽象的语言, 可用于“自顶向下”地描述一个自定义的数据包解析器.

2.1 P3基本概念

对应于数据包在该解析器中的解析过程, P3语言主要描述了以下两个抽象概念.

●   层(layer):描述了数据包在解析器中进行逐层解析时, 经过每一级PE时的解析操作.

●   协议(protocol):声明了在解析器中需要进行解析的网络协议模版, 描述了协议中应包含的各个协议域字段信息以及可选的在层中的固定解析操作.

下面, 本文通过一个例子用P3语言定义一个简单的IPv4数据包解析器, 它仅包含L2和L3层(对应图 1中的PE_L2和PE_L3), 以此来说明P3语言描述的两个抽象概念.

2.2 层(layer)

P3描述了数据包解析器对协议包头的逐层解析, 每一层对应一个可重构单元PE.在每一层中, P3声明了需要匹配的协议模版, 并且具体描述了在该PE中的每个Cell单元里需要执行的匹配查找条件以及相应动作.P3抽象了Cell中的硬件细节, 编程者无需关注PB, PCAction模块如何与配置文件相对应, 只需用人类容易理解的语法声明需要匹配的协议类型以及用条件语句描述匹配条件并给予执行动作, 编译器会生成相应的配置文件完成对这些硬件模块的配置.

图 3中的代码片段中, P3描述了数据帧在L2层中的解析过程.

Fig. 3 An example of L2 layer declaration 图 3 L2层声明示例

首先, XRegister代码块声明了在CellX中会涉及到的所有IRF寄存器访问标识符(X可为A, B0或B1, 对应1个CellA和0~2个CellB); 接着, 声明在L2层中需要进行匹配的协议包头模版(ethernet, ieee802-1qTag)实例, 所有出现的协议包头模版均由用户自定义, 定义规则会在第2.3节中介绍, 相关代码见后文图 5; 最后, CellX代码块描述了数据帧在相应CellX中的解析过程, 具体包括由if语句指定的匹配查找条件、设置重要参数和一些基本寄存器操作.设置重要参数指的是length, next_headerbypass这3个参数.

●   length表示该层协议的包头长度, 用于给Offset单元设置下一层协议包头匹配的偏移量;

●   next_header表示下一层需要解析的协议类型;

●   bypass用于设置PE_bypass单元, 从而实现协议的跨层处理(如在L2层中, bypass=1表示下次解析L3层协议).

基本寄存器操作指的是在action代码块(action{·}也可以省略不写)中的下列4类简单寄存器指令(对应下一节图 8中的抽象语法定义).

●   set Reg, e:将寄存器访问表达式Reg表示的寄存器区间置为表达式e的值(常量值);

●   mov RegM, e:将表达式e(可能含有对多个协议域的访问)的值传送到寄存器访问表达式RegM(可能对应多个寄存器访问表达式所描述字段的合并)所描述的寄存器区间;

●   lg Reg, a, b:若a大于b, 则将寄存器访问表达式Reg表示的寄存器区间置为1;否则置为0;

●   eq Reg, a, b:若a等于b, 则将寄存器访问表达式Reg表示的寄存器区间置为1;否则置为0.

在本例中, P3对L3层的描述与L2层相似, 主要是对IPv4协议包头的匹配解析, 相应实现可参考图 4左侧代码片段.特别地, 由于IPv4协议包头的解析规则相对固定, 所以可以直接把它的匹配查找条件、设置重要参数和一些寄存器操作写在协议声明部分(见第2.3节), 从而可以在不同的层中重用而使得层的描述部分更加简洁.

Fig. 4 Examples of L3 layer declaration and IPv4 protocol declaration 图 4 L3层声明和IPv4协议声明示例

由此可见, P3在对每层的描述中主要包含3个部分.

●   声明在CellX中可能涉及到的IRF寄存器访问标识符;

●   按顺序声明需要进行匹配的协议模版实例;

●   描述在CellX中进行协议匹配的条件以及相应解析操作.

2.3 协议(protocol)

借鉴了P4的部分语法[15], P3通过声明一个字段名以及其位宽的有序集合来定义一个协议包头模版, 并用一个length参数(不同于层中的length)来显式指定包头的长度(length参数的取值不小于所有字段总的字节数).同时, 协议声明中还允许加入层解析中的自定义解析条件, 用来描述该协议包头相对固定的解析规则, 从而可以简化对层部分的描述.

图 5是标准以太网和虚拟局域网的协议声明部分.

Fig. 5 Examples of the header's fields in two protocol declarations 图 5 两个协议声明中的包头数据域示例

IPv4的协议包头也按照这种方式进行声明, 不过由于其包头长度不固定, 因此加入条件语句进行描述, 部分声明如图 4右侧代码片段所示, 代码片段中的条件语句描述了IPv4协议包头的变长情况.根据IPv4协议的包头结构[16], 第4个~第7个比特(第0个开始)对应的协议域字段(样例中的ihl)指定了IPv4包头的长度, 因此, 这里的length参数是由ihl字段的值来决定的.另外要注意, 协议声明中出现的所有寄存器访问(IRF_l3_type)都应在层声明中的ARegisters部分预先定义.

结合层的描述与协议声明部分, 在这个简单的例子中, 数据帧在L2层完成了对以太网协议包头和虚拟局域网包头的解析, 执行逻辑如下:数据帧进入L2层后, 首先让包头匹配以太网包头(ethernet)模版, 进行偏移后, 再匹配IEEE802.1Q标准的VLAN协议模版.此时eth.etherType提取出当前包头的第13、第14字节, 而vlan.etherType提取出当前包头的第17、第18字节.根据以太网帧和IEEE802.1Q包头的协议域字段含义[16], 若eth.etherType为0x8100, 则表示这是一个加了802.1Q标签的帧, 以太网类型在vlan.etherType字段中; 若为0x0800, 则为网际协议(IP), 所以下一层需要解析IPv4协议.若eth.etherType为0x0800, 则说明它是没有加802.1Q标签的网际协议, 同样指定下一协议包头为IPv4.在每个条件分支中, 最后都会通过action代码块中的set操作将解析结果保存至IRF的对应位置中.

在完成了对L2层协议的解析后, 数据帧进入L3层.在L3层中完成对IPv4协议模版的匹配, 并保存解析结果至IRF中.

2.4 P3语言特性

在传统网络编程时, 对包头协议域字段进行读取或对寄存器进行读写是需要非常小心的事情, 因为编程者需要清楚地知道相应的字段应该处于一长串二进制位的哪一段, 并准确地用十六进制(或二进制)将其表示出来, 一个0/1位的偏移就会引发巨大的错误.并且, 对一大堆十六进制(或二进制)串进行查错也是十分麻烦的一件事.为了方便网络编程者使用, P3语言包含了一些特性.

2.4.1 字段合并

在寄存器的操作中, 有时编程者需要对位置相邻的寄存器区间或协议域字段进行合并, 然后一次性进行读写.为此, P3加入了一个二元运算符“++”来完成这种操作.

图 3的例子中, 出现了以下操作:

$ movIRF\_outer\_vlan\_high++IRF\_outer\_vlan\_low, vlan.pcp++vlan.cfi++vlan.vid; $

表示的就是将vlan.pcp, vlan.cfi, vlan.vid这3个连续的协议域字段先进行合并, 然后存储到IRF_outer_vlan_hignIRF_outer_vlan_low两个标识符表示的IRF寄存器区间合并起来的连续区间中.需要特别注意的是, 通过“++”连接起来的两个寄存器区间或协议域字段必须是连续的.

2.4.2 重新编址

在对每一层的协议包头进行解析时, 每解析完一层, 就要将提取出来的信息保存至公共的IRF中.为方便起见, 可将IRF看作一个公共的长存储区, 若采用图 6中的固定编址方案, 即根据IRF中的绝对位置进行索引, 随着提取到的信息量增加, 计算索引值会变得非常麻烦且容易出错.由于目标硬件解析器对每层协议的解析是由相同的PE模块完成的, 而每个PE模块的内部又是由相似的几个Cell单元构成, 所以我们对IRFCell单元为基本单位进行分段固定编址, 具体如图 7所示.

Fig. 6 Global fixed address of IRF 图 6 IRF全局固定编址

Fig. 7 Sectional fixed address of IRF 图 7 IRF分段固定编址

每一段对应一个Cell可以访问的IRF资源, 共24个字节(192个比特).由于一个PE中最多包含3个Cell单元(1个Cell_A、0~2个Cell_B), 所以固定给每一个PE分配3段, 共72个字节.对应图 1中的需要解析到L4层协议的交换机结构, 共包含5个PE模块, 因此IRF的总长度为72×5=360字节.编址时, 编程者只需根据当前位置在当前段中的相对位置进行索引, 在寄存器寻址时, 编译器会首先根据上下文确定当前应处于哪一段(即哪一个PE的哪一个Cell), 然后再加上相应的固定偏移在IRF中寻址.

另外, 在一些特殊情况中, 当前层可能会需要访问前一层提取到IRF中的协议包头信息, 所以P3也允许对前一层声明过的寄存器访问标识符进行跨层访问.

3 P3类型系统

为方便静态语义检查的实现, 本文对P3类型系统进行了严格规范.本节给出P3类型系统形式化定义的核心部分.在此之前, 需要先介绍P3抽象语法的相关内容, 见第3.1节.

3.1 抽象语法

图 8包括了我们所选取的部分P3抽象语法, 用于介绍本节的P3类型系统以及后一节的P3操作语义.在抽象语法的定义中, 非终结符采用了正体, 终结符和辅助关键字使用了斜体, 起始符号为parser_spec.Lreglen, Creglen, PsetLset等用于声明一个P3规范(为方便, 本文许多地方也称P3程序或代码)的几个参数:层寄存器长度、cell寄存器长度、协议名称集以及层名称集.语法的主体是decl分支, 由多个声明组成, 每个声明可以是常量声明(ConstDcl)、全局寄存器访问声明(RegAccSet)、协议声明(protocol_decl)或层声明(layer_action).每一层都有局部寄存器访问的声明, 包含3个部分(CellARegs, CellB0RegsCellB1Regs), 每个部分声明了各个cell的局部寄存器访问标识符.

Fig. 8 Abstract syntax of P3 (partial) 图 8 P3抽象语法(部分)

每一层需要声明一个或多个协议数据包头的实例(ProtocolDef), 在该层的各个cell规范中, 可通过域名表达式(Efield)访问某个实例的各个域.协议声明内部, 只要通过域名标识符即可以访问各个域.

语句(stmt)可以出现在各层的每个cell规范中, 也可以出现在协议声明中.后者主要是为了规范描述在多个层中复用, 各语句相当于出现在各相关层cell A中(由于域的访问需用相应实例的域名表达式替换, 所以要求这种情况下相关层中最多只能声明该协议包头的一个实例).每条语句可以是描述查表逻辑的分支语句(if_else_ stmt)、一系列的硬件指令(action_stmt)以及重要参数(NextHeader, Length, Bypass)设置(仅在cell A或在协议声明中设置).

图 8中, 后半部分内容(expr之后)主要描述与寄存器和协议域访问相关的部分, 是P3规范中最有代表性的内容, 本节和下一节的类型系统和操作语义将围绕这一主线进行介绍.

3.2 类型表达式

以下是用于定义P3类型系统的类型表达式:

type〉::=Int      有符号32位整数

   |Hexes(n)      n位十六进制数(串)

   |Bits(n)      n位二进制数(串)

   |RegAcc (k, i, j)    寄存器访问类型, 其中k表示当前上下文中的IRF寄存器大小, 满足0≤ji < k

   |FieldAcc(id, k, i, j)   位于Cell上下文中的协议域访问类型, id为协议实例标识符, k为该协议实例的长度, ij为访问区间, 满足0≤ij < k∨(i=kj is undefined), 析取运算的后半部分表示该协议存在optional域

   |FieldAcc(k, i, j)    位于协议上下文中的协议域选取类型, k为该协议实例的长度, ij为访问区间, 满足0≤ij < k∨(i=kj is undefined)

   |X         协议类型, 任意名字为X的协议的所有实例的类型为X

对于常数表达式, 在很多地方, 我们需要计算它的值以用于合法性检查, 因此, 我们给所有数值类型(Int, Hexes(n), Bits(n))增加了一个辅助值组成了一种特别地常数类型:

type〉::=(τ, i)         组合类型, τ表示某数值类型, i表示一个有符号32位整数值

3.3 类型环境

一个类型环境记录一类特定标识符在某个上下文或作用域中被赋予的类型表达式.我们分别用$\mathcal{C}$, $\mathcal{R}$, $\mathcal{L}$和P分别表示全局常量类型环境、特殊的全局寄存器访问类型环境(见下文解释)、层(layer)的局部类型环境和一个协议(protocol)的局部类型环境.层局部类型环境$\mathcal{L}$内部又嵌套有$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1这3个局部类型环境, 对应于CellA, CellB0和CellB1.某些时候, 会用$\mathcal{L}$id和Pid来表示在id这个标识符所表示的层或协议上下文中的局部类型环境.

我们引入特殊类型环境$\mathcal{R}$, 用来记录当前层前面一层的只读寄存器访问标识符的类型, 它会随着层间切换而动态更新.在一开始时, $\mathcal{R}$由全局寄存器访问的声明进行初始化, 这些全局寄存器访问标识符在第1个层中可见.当新的层声明出现时, $\mathcal{R}$更新为上一层的cell局部环境$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1的特殊并集(参见第3.4节).

最后, 为了保证一致性, 我们还定义了几个全局参数, 包括层寄存器大小、cell寄存器大小、协议集合以及层集合.为此, 我们引入了4个特殊的全局类型环境$\mathcal{L}$reglen, $\mathcal{C}$reglen, $\mathcal{P}$set$\mathcal{L}$set, 以及为了方便, 我们用符号$\mathcal{G}$来表示它们的组合, 即$\mathcal{G}$=($\mathcal{L}$reglen, $\mathcal{C}$reglen, $\mathcal{P}$set, $\mathcal{L}$set).

3.4 类型规则

P3包含了一系列类型规则以实现静态类型检查, 完整的类型规则可参见P3设计文档[17].本文会对其中一些有代表性的规则进行介绍, 这些规则主要是围绕着寄存器的读写以及协议域的访问来展开.

在这些类型规则中, 除了常规断言, 最主要的断言形式包括以下3种.

●   $\mathcal{E}$e:A;

●   $\mathcal{E}$D;

●   $\mathcal{E}$⊢◇.

其中, $\mathcal{E}$为一个或一系列类型环境, e为表达式(含各类标识符), A为类型表达式(见第3.2节), D对应于解析器规范各个部分的定义.$\mathcal{E}$e:A表示在环境(集)$\mathcal{E}$下, e类型良好且具有类型A.$\mathcal{E}$D表示在环境(集)$\mathcal{E}$下, D是类型良好的.E⊢◇表示某个环境$\mathcal{E}$是良好定义的(标识符的类型值唯一, 或者说域中无重名标识符).

3.4.1 寄存器和协议域访问类型环境的初始化

规则(1)用来初始化cellA中定义的寄存器访问.

$ \frac{\begin{align} & \mathcal{G}\vdash \mathcal{C}reglen(n)\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{{{\mathcal{L}}'}}_{\mathcal{A}}}\vdash {{e}_{1}}:(Int, {{n}_{1}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{{{\mathcal{L}}'}}_{A}}\vdash {{e}_{2}}:(Int, {{n}_{2}})\text{ }0\le {{n}_{2}}\le {{n}_{1}}<n\text{ }id\notin dom({{{{\mathcal{L}}'}}_{A}}) \\ & \forall i{d}'\in dom({{{{\mathcal{L}}'}}_{A}}).({{{{\mathcal{L}}'}}_{A}}\vdash i{d}':RegAcc(n, {{{{n}'}}_{1}}, {{{{n}'}}_{2}})\to {{{{n}'}}_{1}}<{{n}_{2}}\vee {{n}_{1}}<{{{{n}'}}_{2}})\text{ }{{\mathcal{L}}_{A}}={{{{\mathcal{L}}'}}_{A}}\cup \{id:RegAcc(n, {{n}_{1}}, {{n}_{2}})\} \\ \end{align}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{A}}\vdash IRF(id, {{e}_{1}}, {{e}_{2}})} $ (1)

这些定义形如id=IRF(e1, e2), 参见图 3中L2层的ARegisters声明部分; 在抽象语法中, 用一个IRF(id, e1, e2)节点来表示这样的定义.将这样的寄存器访问定义加入环境LA时需要检查3点.

●   一是检查访问的寄存器区间[n1, n2]不能超过当前cellIRF的范围(根据习惯, 区间上下界由大到小给出).全局环境$\mathcal{G}$中的抽象语法节点Creglen(n)指定了当前cell的寄存器长度为n, 表达式e1e2的值为n1n2, 指定了访问的区间上下界, 若0≤n2n1 < n, 则满足条件;

●   二是检查当前定义的标识符id没有被声明过, 即$id\notin dom({{{\mathcal{L}}'}_{A}})$;

●   最后要检查定义的各个寄存器区间是不重叠的, 以保证读写寄存器的安全性, 即对于所有已声明过的寄存器区间$[{{{n}'}_{1}}, {{{n}'}_{2}}]$应该与当前声明的区间[n1, n2]没有公共部分, 可表述为${{{n}'}_{1}}<{{n}_{2}}\vee {{n}_{1}}<{{{n}'}_{2}}$.

另外, 在cellB0或cellB1中的寄存器访问定义规则与cellA中一致, 只需将LA替换为LB0或LB1即可.后面规则中的类似情况, 将不再重复解释.

cellA中寄存器的某一位的访问定义规则为规则(2), 可简单将其看作规则(1)的特例, 即n2=n1的情况.

$ \frac{\begin{matrix} \mathcal{G}\vdash \mathcal{C}reglen(n)\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{{{\mathcal{L}}'}}_{A}}\vdash e:(Int, k)\text{ }0\le k<n\text{ }id\notin dom({{{{\mathcal{L}}'}}_{A}}) \\ \forall i{d}'\in dom({{{{\mathcal{L}}'}}_{A}}).({{{{\mathcal{L}}'}}_{A}}\vdash i{d}':RegAcc(n, {{{{n}'}}_{1}}, {{{{n}'}}_{2}})\to {{{{n}'}}_{1}}<k\vee k<{{{{n}'}}_{2}})\text{ }{{\mathcal{L}}_{A}}={{{{\mathcal{L}}'}}_{A}}\cup \{id:RegAcc(n, k, k)\} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{A}}\vdash IRF(id, e)} $ (2)

P3语言允许当前层中的cell单元访问前一层的寄存器空间, 可认为是一类全局寄存器访问空间.为此, 我们使用了特定的全局类型环境$\mathcal{R}$.规则(3)用来描述层切换时环境$\mathcal{R}$的初始化.

$ \frac{\begin{matrix} \mathcal{G}\vdash Lreglen(n)\text{ }\mathcal{G}\vdash Creglen(k)\text{ }n=3*k \\ \mathcal{R}=\{id:RegAcc(n, 2*k+{{n}_{1}}, 2*k+{{n}_{2}})|id:RegAcc(k, {{n}_{1}}, {{n}_{2}})\in {{\mathcal{L}}_{A}}\}\cup \\ \{id:RegAcc(n, k+{{n}_{1}}, k+{{n}_{2}})|id:RegAcc(k, {{n}_{1}}, {{n}_{2}})\in {{\mathcal{L}}_{B0}}\}\cup \\ \{id:RegAcc(n, {{n}_{1}}, {{n}_{2}})|id:RegAcc(k, {{n}_{1}}, {{n}_{2}})\in {{\mathcal{L}}_{B1}}\} \\ \end{matrix}}{\mathcal{R}\vdash \diamond } $ (3)

即在离开某一层的上下文环境时, 需要把当前层的$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1环境进行合并, 然后更新至环境$\mathcal{R}$.具体步骤如下:首先, 全局环境中的Lreglen(n)和Creglen(k)分别指定了当前层中的层寄存器长度nCell寄存器长度k, 每层的寄存器会平均分为3段给环境$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1, 因此n=3k; 然后, 需要将每段Cell寄存器中的地址转换为层寄存器中的地址, 在层寄存器的地址空间[n-1, 0]中, $\mathcal{L}$B1对应[k-1, 0]部分, $\mathcal{L}$B0对应[2k-1, k]部分, $\mathcal{L}$Asu对应[3k-1, 2k]部分, 因此, 在合并$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1时, 需要对其中声明的寄存器区间分别加上2k, k和0的偏移.另外值得注意的是, 在第1层开始处理的时刻, 环境$\mathcal{R}$由全局寄存器访问定义来初始化, 相应的规则类似于规则(1)和规则(2).

规则(4)用于初始化协议层类型环境P.

$ \frac{\begin{matrix} flds=((fi{{d}_{1}}:{{c}_{1}}), ..., (fi{{d}_{k}}:{{c}_{k}}))\text{ }ofld=(ofid:0)\text{ }\forall i:1\le i\le k.(\phi \vdash {{c}_{i}}:(Int, {{n}_{i}})) \\ n={{n}_{1}}+{{n}_{2}}+...+{{n}_{k}}\text{ }\forall i(1\le i\le k\to {{n}_{i}}>0) \\ \forall i, j(1\le i<j\le k\to fi{{d}_{i}}\ne fi{{d}_{j}})\text{ }\forall i(1\le i\le k\to fi{{d}_{i}}\ne ofid) \\ \mathcal{G}\vdash \diamond \text{ }\mathcal{C}\vdash \diamond \text{ }\mathcal{R}\vdash \diamond \text{ }\mathcal{L}\vdash \diamond \text{ }{{\mathcal{L}}_{A}}\vdash \diamond \text{ }{\mathcal{P}}'\vdash \diamond \text{ }\forall i(1\le i\le k\to fi{{d}_{i}}\notin dom({\mathcal{P}}'))\text{ }ofid\notin dom({\mathcal{P}}') \\ \mathcal{P}=\mathcal{P}'\cup \{fi{{d}_{i}}:FieldAcc(n, {{n}_{1}}+...+{{n}_{i-1}}, {{n}_{1}}+...+{{n}_{i}}-1)|1\le i\le k\}\cup \{ofid:FieldAcc(n, n, null)\} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{A}}, \mathcal{P}\vdash (Fields(flds), OptionField(ofld))} $ (4)

$\mathcal{P}$中域名标识符的类型为FieldAcc(k, i, j), 记录了协议包头固定长度数据域(除option域外)的长度(k)及各个域的起始和结束位置.本文对option域标识符的类型作了特殊技术处理, 假设其长度为0.在针对协议域定义时, 需要检查所有定长域的长度为正整数, 以及所有的协议域名没有重复.

3.4.2 表达式中寄存器和协议域的访问

表达式中寄存器访问标识符的类型已经由规则(1)和规则(2)进行过初始化, 可以直接从环境中得到, 如在cell局部类型环境中, 可由下式得到.

$ \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{\mathcal{C}}}⊢rid:RegAcc\left( n, {{n}_{1}}, {{n}_{2}} \right) $

在进行寄存器访问时, 我们可能需要选取已有寄存器访问的一段区间或某一位进行访问, 规则(5)和规则(6)分别描述了这两种情况.

$ \frac{\begin{matrix} \mathcal{G}\vdash \mathcal{C}reglen(n)\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}:RegAcc(n, {{n}_{1}}, {{n}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{2}}:(Int, {n}') \\ \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{3}}:(Int, {n}'')\text{ }0\le {{n}_{2}}\le {{n}_{1}}<n\text{ }0\le {n}''\le {n}'\le {{n}_{1}}-{{n}_{2}}\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash ERegSection({{e}_{1}}, {{e}_{2}}, {{e}_{3}}):RegAcc(n, {{n}_{2}}+{n}'', {{n}_{2}}+{n}')} $ (5)
$ \frac{\begin{matrix} \mathcal{G}\vdash \mathcal{C}reglen(n)\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}:RegAcc(n, {{n}_{1}}, {{n}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{2}}:(Int, {n}') \\ 0\le {{n}_{2}}\le {{n}_{1}}<n\text{ }0\le {n}'\le {{n}_{1}}-{{n}_{2}}\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash ERegBit({{e}_{1}}, {{e}_{2}}):RegAcc(n, {{n}_{2}}+{n}', {{n}_{2}}+{n}')} $ (6)

规则(5)中, ERegSection(e1, e2, e3)表示对寄存器访问e1的第e3到第e2位子区间进行访问.具体过程如下:设该Cell占用的IRF长度为n, 定义的寄存器访问e1表示当前IRF的[n1, n2]区间(满足0≤n2n1 < n), 现在需要访问e1的第n”位至第n’位这一子区间, 那么该规则需要检查要访问的子区间不能超过该字段的长度, 即0≤n”≤n’ < n1-n2.若检查通过, 最终访问的结果应为当前CellIRF的第n2+n”位至第n2+n’位, 因此赋予一个类型表达式RegAcc(n, n2+n”, n2+n’).类似的, 规则(6)为规则(5)的特例, 描述了对寄存器访问的某一位的访问.

在协议声明上下文里, 表达式中域标识符的类型已经由规则(4)进行过初始化, 可直接从环境中得到:

$ \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{\mathcal{C}}}, \mathcal{P}⊢ fid:FieldAcc\left( n, {{n}_{1}}, {{n}_{2}} \right). $

对指定协议的协议域访问只发生在Cell局部环境中, 如图 3中的域名表达式eth.etherTypevlan. etherType, 规则(7)对这样的访问进行检查.

$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}\vdash e:pid\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}\vdash (pid, (Fields(flds), OptionField(ofld)), ...)) \\ flds=((fi{{d}_{1}}:{{c}_{1}}), ..., (fi{{d}_{k}}:{{c}_{k}}))\text{ }ofld=(ofid:0)\text{ }\forall i:1\le i\le k.(\phi \vdash {{c}_{i}}:(Int, {{n}_{i}})) \\ n={{n}_{1}}+{{n}_{2}}+...+{{n}_{k}}\text{ }\exists i.fid=fi{{d}_{i}}\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash Efield(e, fid):FieldAcc(id, n, {{n}_{1}}+...+{{n}_{i-1}}, {{n}_{1}}+...+{{n}_{i}}-1)} $ (7)

抽象语法节点Efield(e, fid)表示访问协议实例efid定长协议域.假设epid这个协议类型的实例名, pid协议类型具有k个定长协议域fidi(1≤ik)和一个变长协议域ofid, 那么该规则需要检查访问的协议域名字fid应该为k个定长协议域名字fidi中的一个.

若要访问协议域的某一段区间或某一位, 可将协议域类比为寄存器访问区间, 然后仿照规则(5)或规则(6)便可以得到相应的检查规则, 这里就不再赘述.

3.4.3 指令中寄存器的访问

P3通过一系列基本指令来对寄存器进行操作, 在这些指令中对寄存器和协议域的访问也要满足相应的规则.在图 8instrucion非终结符中, 可以看到, 对于Set, EqLg指令的目标寄存器对应的非终结符为tgt_reg_ acc_name, 它表示单个寄存器访问标识符的寄存器空间访问(含区间嵌套).对应此类目标寄存器访问的规则包括规则(8)~规则(10).

$ \frac{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash id:RegAcc(n, {{n}_{1}}, {{n}_{2}})\text{ }{{\mathcal{L}}_{C}}\ is\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash TargetRegAccName(id):RegAcc(n, {{n}_{1}}, {{n}_{2}})} $ (8)
$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash tran:RegAcc(n, {{m}_{1}}, {{m}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}:(Int, {{k}_{1}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{2}}:(Int, {{k}_{2}}) \\ 0\le {{k}_{2}}\le {{k}_{1}}\le {{m}_{1}}-{{m}_{2}}\text{ }{{n}_{1}}={{m}_{2}}+{{k}_{1}}\text{ }{{n}_{2}}={{m}_{2}}+{{k}_{2}}\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash TargetRegAccName(tran, {{e}_{1}}, {{e}_{2}}):RegAcc(n, {{n}_{1}}, {{n}_{2}})} $ (9)
$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash tran:RegAcc(n, {{m}_{1}}, {{m}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash e:(Int, k) \\ 0\le k\le {{m}_{1}}-{{m}_{2}}\text{ }m={{m}_{2}}+k\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash TargetRegAccName(tran, e):RegAcc(n, m, m)} $ (10)

规则(8)指通过寄存器访问标识符id对定义的寄存器区间进行整体访问; 规则(9)指对tran表示的寄存器访问的第e2至第e1位子区间进行访问, 此时需要检查所访问的子区间是合法的; 规则(10)指对tran表示的寄存器访问的第e位进行访问, 可视为规则(9)的一个特例.这3条是在cell局部环境($\mathcal{L}$C)下的类型规则, 这里, $\mathcal{L}$C可以是$\mathcal{L}$A, $\mathcal{L}$B0$\mathcal{L}$B1.在$\mathcal{P}$环境下的访问规则也和这3条类似, 只需对类型环境作相应改变即可.

mov指令中对寄存器的访问有所不同, 它支持对多个定义的寄存器访问通过“++”运算符进行连接, 然后再统一赋值, 例如图 3例子中的mov IRF_outer_vlan_high++IRF_outer_vlan_low, vlan.pcp++vlan.cfi++vlan.vid.需要特别注意的是, 这里连接的寄存器访问指的是IRF_outer_vlan_highIRF_outer_vlan_low这两个标识符定义的寄存器区间, 而vlan.pcp++vlan.cfi++vlan.vid是作为表达式来进行处理的.从图 8中可以看到, mov指令访问寄存器对应的非终结符为mov_reg_acc_name, 本质为通过递归方式定义的一串tgt_reg_acc_name, 即一连串寄存器访问的连接, 对应的规则为规则(11)和规则(12).

$ \frac{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash tra:RegAcc(n, {{m}_{1}}, {{m}_{2}})\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash MovRegAccName(tra):RegAcc(n, {{m}_{1}}, {{m}_{2}})} $ (11)
$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash mra:RegAcc(n, {{m}_{1}}, {{m}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash tra:RegAcc(n, {{n}_{1}}, {{n}_{2}}) \\ {{m}_{2}}={{n}_{1}}+1\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash MovRegAccName(mra, tra):RegAcc(n, {{m}_{1}}, {{n}_{2}})} $ (12)

这里要注意, 当有多个寄存器访问通过“++”连接时, 需要按照规则(12)中的方式来检查两个寄存器区间是否相邻, 即m2=n1+1.

3.4.4 位串连接运算

除了传统的位串连接以外, P3还支持另外两种特殊的位串连接运算, 用来连接两个相邻的寄存器访问或协议域, 从而能够方便地对合并的位串进行整体的读取.

我们用“++”表示位串运算, 遇不同操作数时可重载.在LC环境下, 对寄存器访问和协议域的位串连接规则分别为规则(13)和规则(14).

$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}:RegAcc(k, {{n}_{1}}, {{n}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{2}}:RegAcc(k, {{m}_{1}}, {{m}_{2}}) \\ {{n}_{2}}={{m}_{1}}+1\text{ }0\le {{m}_{2}}\le {{m}_{1}}<{{n}_{2}}\le {{n}_{1}}<k\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}++{{e}_{2}}:RegAcc(k, {{n}_{1}}, {{m}_{2}})} $ (13)
$ \frac{\begin{matrix} \mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}:FieldAcc(id, k, {{n}_{1}}, {{n}_{2}})\text{ }\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{2}}:FieldAcc(id, k, {{m}_{1}}, {{m}_{2}}) \\ {{m}_{1}}={{n}_{2}}+1\text{ }0\le {{n}_{1}}\le {{n}_{2}}<{{m}_{1}}\le {{m}_{2}}<k\text{ }{{\mathcal{L}}_{C}}\ \text{is}\ {{\mathcal{L}}_{A}}, {{\mathcal{L}}_{B0}}\ \text{or}\ {{\mathcal{L}}_{B1}} \\ \end{matrix}}{\mathcal{G}, \mathcal{C}, \mathcal{R}, \mathcal{L}, {{\mathcal{L}}_{C}}\vdash {{e}_{1}}++{{e}_{2}}:FieldAcc(id, k, {{n}_{1}}, {{m}_{2}})} $ (14)

在对寄存器访问进行位串连接时, 一定要保证连接的两个寄存器访问必须是相邻的, 所以在规则(13)中, 假设需要连接的两个寄存器访问依次为当前IRF的[n1, n2]和[m1, m2]两个区间, 自然需要满足n2=m1+1.

在对协议域进行位串连接时, 同样要注意保证连接的两个协议域属于同一协议并且是相邻的.

4 P3操作语义

前面介绍的类型系统刻画了P3语言的静态语义, 可用于实现静态类型检查.能够通过静态类型检查的P3程序是类型良好的(well-typed).对于类型良好的P3程序, 可遵循其动态语义执行.本节基于图 8的P3抽象语法, 为P3定义一种操作语义风格的形式化动态语义.

4.1 语义环境

P3程序可以访问两个存储区:一个用来存放数据包包头信息, 称为PKT寄存器; 另一个是通用寄存器IRF.对于P3程序所描述的包解析器处理过程来说, 可以将PKT看作是只读寄存器, 而IRF是可以读和写的寄存器.在P3语义模型中, 对于IRF寄存器的访问, 我们采用的存储模型表示为regacc(n, i, j, bv), 其中,

●   n为当前语义环境下可访问的IRF寄存器大小(存储bit数);

●   ij(满足0≤jin)描述一个当前IRF寄存器的访问区间(i, j);

●   bv代表一个长度为ij+1的二进制位串值.

对于PKT寄存器的访问, 出于语义定义的需要, 不同于访问IRF, 我们采用的存储模型可表示为

$ fdacc(id, n, i, j, bv), $

其中, id标识某类协议数据包头的一个实例, n为该实例被分配的PKT寄存器大小(存储bit数), 而i, j, bv的含义与regacc(n, i, j, bv)中是类似的.

基于上述存储模型, 我们设计了定义P3语言语义所需要用到的语义环境, 如图 9所示.

Fig. 9 Semantic environment of the P3 language 图 9 P3语言语义环境

P3语言有多个层次的语义环境, 其中, 全局环境表示为ge, layer局部环境表示为le, cell局部环境用ce表示, 而protocol局部环境为ξρ.

环境ge, lece分别由各自的子环境构成, 即ge=(γ, σ, δ), le=(ξ, nh, len, bp)以及ce=(δA, δB0, δB1).

图 9给出了所涉及到的全部语义环境的定义及其基本含义.环境之间的嵌套层次关系从外到内依次为Global, Layer, CellProtocol, 即ge, le, ceξρ依次嵌套.

4.2 语义规则

下面给出所定义的P3语言操作语义的部分有代表性的语义规则.完整的语义规则定义可参考P3设计文档[17].除了常规断言, 语义规则中最主要的断言形式包括如下两种.

●   Γev;

●   Γ⊢(π, s)⇒π’.

其中, Γ为某些环境的集合, e为表达式(含各类标识符), s为各种定义或语句, ππ’为环境.Γev表示在环境(集)Γ下, e的计算结果为v.这里, v可以是整数和位串等常规类型取值, 也可以是第4.1节中所述的两类寄存器存储访问取值.Γ⊢(π, s)⇒π’表示在环境环境(集)Γ下, 由实施定义或执行语句s后, 环境(集)π将改变为π’.

4.2.1 寄存器访问环境的初始化

规则(15)用来初始化cell A中定义的寄存器访问.

$ \frac{\begin{matrix} ge=(\gamma , \sigma , \delta )\text{ }ge, le, {{\delta }_{A}}\vdash {{e}_{1}}\Rightarrow {{n}_{1}}\text{ }ge, le, {{\delta }_{A}}\vdash {{e}_{2}}\Rightarrow {{n}_{2}}\text{ }\gamma =(lr, creglen(n), ps, ls, \iota , \rho ) \\ 0\le {{n}_{2}}\le {{n}_{1}}<n\text{ }id\notin dom({{\delta }_{A}})\text{ }\forall i{d}'\in dom({{\delta }_{A}}).({{\delta }_{A}}\vdash i{d}'\Rightarrow regacc(n, i, j, bv)\to i<{{n}_{2}}\vee {{n}_{1}}<j) \\ {{{{\delta }'}}_{A}}={{\delta }_{A}}\cup \{id:regacc(n, {{n}_{1}}, {{n}_{2}}, null)\} \\ \end{matrix}}{ge, le\vdash ({{\delta }_{A}}, IRF(id, {{e}_{1}}, {{e}_{2}}))\Rightarrow {{{{\delta }'}}_{A}}} $ (15)

这些定义形如id=IRF(e1, e2), 参见图 3中L2层的ARegisters定义部分.当前环境下, 寄存器IRF的大小为n, 由全局环境γ中的creglen(n)保存.e1e2在当前环境下的取值n1n2决定了变量id的寄存器访问区间, 初始时, 将寄存器该区间的位串值置为null.如同前一节中类型规则(1)的限定, IRF(n1, n2)中的n1n2满足0≤n2n1 < n.

对于cell B0和cell B1中寄存器访问的初始化也类似于规则(15).硬件实现时可以保证:不同层的局部寄存器访问使用不同的IRF空间; 同一层中不同cell的局部寄存器访问也分别配备有互不冲突的私有IRF空间.后面规则中的类似情况, 将不再重复解释.

规则(16)也是用来初始化cell A中定义的寄存器访问.

$ \frac{\begin{matrix} ge=(\gamma , \sigma , \delta )\text{ }ge, le, {{\delta }_{A}}\vdash e\Rightarrow k\text{ }\gamma =(lr, creglen(n), ps, ls, \iota , \rho )\text{ }0\le k<n \\ id\notin dom({{\delta }_{A}})\text{ }\forall i{d}'\in dom({{\delta }_{A}}).({{\delta }_{A}}\vdash i{d}'\Rightarrow regacc(n, i, j, bv)\to i<k\vee k<j) \\ {{{{\delta }'}}_{A}}={{\delta }_{A}}\cup \{id:regacc(n, k, k, null)\} \\ \end{matrix}}{ge, le\vdash ({{\delta }_{A}}, IRF(id, e))\Rightarrow {{{{\delta }'}}_{A}}} $ (16)

这些定义形如id=IRF(e), 是访问寄存器IRF的某一bit的空间.

在P3语言中, 允许当前层中的cell单元访问前一层的寄存器空间, 为此, 我们使用了特定的全局环境δ.规则(17)用来描述在层切换的时刻环境δ的初始化.

$ \frac{\begin{matrix} ge=(\gamma , \sigma , \delta )\text{ }\gamma =(lreglen(n), creglen(k), ps, ls, \iota , \rho )\text{ }n=3*k \\ le=({{\xi }_{\iota }}, nextheader(pid), length(i), bypass(j))\text{ }ce=({{\delta }_{A}}, {{\delta }_{B0}}, {{\delta }_{B1}}) \\ {\delta }'=\{(id:regacc(n, 2*k+{{n}_{1}}, 2*k+{{n}_{2}}, bva))|(id:regacc(k, {{n}_{1}}, {{n}_{2}}, bva))\in {{\delta }_{A}}\}\cup \\ \{(id:regacc(n, k+{{n}_{1}}, k+{{n}_{2}}, bvb0))|(id:regacc(k, {{n}_{1}}, {{n}_{2}}, bvb0))\in {{\delta }_{B0}}\}\cup \\ \{(id:regacc(n, {{n}_{1}}, {{n}_{2}}, bvb1))|(id:regacc(k, {{n}_{1}}, {{n}_{2}}, bvb1))\in {{\delta }_{B1}}\} \\ g{e}'=(\gamma , \sigma , {\delta }')\text{ }l{e}'=(\phi , nextheader(null), length(null), bypass(null))\text{ }c{e}'=(\phi , \phi , \phi ) \\ \end{matrix}}{\vdash (ge, le, ce, ''layer-switch'')\Rightarrow (g{e}', l{e}', c{e}')} $ (17)

环境δ中, 可访问的寄存器IRF空间大小n记录在全局环境γlreglen(n)分量中.注意, 另一分量creglen(k)表示当前cell的局部IRF寄存器空间大小.由于每一层包含3个cell单元, 因此n=3k.另外值得注意的是, 在第1层开始处理的时刻, 环境δ由全局寄存器访问定义来初始化, 相应的规则类似于规则(15)和规则(16), 只是寄存器IRF空间的初始化由硬件来完成(不用置为null), 限于篇幅, 不在此列出.

由于在cell的局部寄存器访问环境(如δA)下也可以访问全局寄存器访问环境δ, 因此按照先本地后全局来处理可能的同名寄存器访问标识符的情形.

4.2.2 表达式中寄存器的访问

表达式中对寄存器的访问, 可以直接使用当前环境中已有定义的寄存器访问id, 比如环境δAid的寄存器访问的语义值为regacc(id, n, n1, n2, bv), 可由下式得到.

$ ge, le, {{\delta }_{A}}⊢id\Rightarrow regacc(n, {{n}_{1}}, {{n}_{2}}, bv). $

注意, 这里的id可能未在局部寄存器环境δA中有定义, 而是可能定义在ge包含的全局寄存器环境δ中.

规则(18)用于计算寄存器访问中某一位的语义值.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow regacc(n, {{n}_{1}}, {{n}_{2}}, bv)\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow {n}'\text{ }0\le {{n}_{2}}\le {{n}_{1}}<n \\ 0\le {n}'\le {{n}_{1}}-{{n}_{2}}\text{ }b=get\_binary\_bit(bv, {n}')\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash ERegBit({{e}_{1}}, {{e}_{2}})\Rightarrow regacc(n, {{n}_{2}}+{n}', {{n}_{2}}+{n}', b)} $ (18)

例如, 对于图 3中L2层cell A的寄存器访问定义IRF_tag_type_2b=IRF[23:16], 假设其当前语义值为regacc(n, 23, 16, bv), 则表达式IRF_tag_type_2b[2]在δA环境(及其外层环境)下的语义值为regacc(n, 18, 18, b).这里, bv为当前IRF[23,16]的位串值, bbv的第2位, 即IRF寄存器的第18位IRF[18]的bit值.该规则同样适用于cell B0和cell B1, 因此在规则中用δC代替.这里, δCδA, δB0δB1.这样, 规则(18)实际上相当于3条类似的规则.对此, 后面不再赘述.

规则(19)用于计算寄存器访问的子区间的语义值.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow regacc(n, {{n}_{1}}, {{n}_{2}}, bv)\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow {n}'\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{3}}\Rightarrow {n}'' \\ 0\le {{n}_{2}}\le {{n}_{1}}<n\text{ }0\le {n}''\le {n}'\le {{n}_{1}}-{{n}_{2}}\text{ }b{v}'=get\_binary\_bits(bv, {n}', {n}'')\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash ERegSection({{e}_{1}}, {{e}_{2}}, {{e}_{3}})\Rightarrow regacc(n, {{n}_{2}}+{n}', {{n}_{2}}+{n}'', b{v}')} $ (19)

例如, 对于图 3中L2层cell A的寄存器访问定义IRF_tag_type_2b=IRF[23:16], 假设其当前语义值为regacc(n, 23, 16, bv), 则表达式IRF_tag_type_2b[5, 2]δA环境(及其外层环境)下的语义值为regacc(n, 21, 18, bv’).这里, bv为当前IRF[23,16]的位串值, bv’为bv的第5位~第2位之间区间的bit串值, 即IRF寄存器的第21位~第18位区间IRF[21, 18]的bit串值.

寄存器访问支持任意(合法的)嵌套访问, 如IRF_tag_type_2b[5, 2][4, 2], IRF_tag_type_2b[5, 2][0], IRF_tag_type_2b[5, 2][4, 2][2], 等等.

4.2.3 表达式中协议域的访问

Protocol局部环境ξρ下, 表达式中可通过域名标识符对协议域进行直接访问.比如, 域名为fid的域的语义值为fdacc(id, n, n1, n2, bv), 可由下式得到.

$ ge, le, {{\delta }_{A}}, \xi \rho ⊢fid\Rightarrow fdacc(id, n, {{n}_{1}}, {{n}_{2}}, bv). $

这里, id为相应协议的一个实例标识符.注意:我们省略了环境ξρ的初始化规则, 在初始化ξρ时, 首先会置bvnull, 而在上式中的bv会在δA环境中由相应实例(id)的初始取值来获取.后者由硬件设置, 参考下面的规则(20)及其相应的解释.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash id\Rightarrow (pid, pins)\text{ }pins=((fi{{d}_{1}}, ({{n}_{1}}, b{{v}_{1}})), (fi{{d}_{2}}, ({{n}_{2}}, b{{v}_{2}})), ..., (fi{{d}_{k}}, ({{n}_{k}}, b{{v}_{k}}))) \\ n={{n}_{1}}+{{n}_{2}}+...+{{n}_{k}}\text{ }\exists i.fid=fi{{d}_{i}}\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash Efield(id, fid)\Rightarrow fdacc(id, n, {{n}_{1}}+{{n}_{2}}+...+{{n}_{i-1}}, {{n}_{1}}+{{n}_{2}}+...+{{n}_{i}}-1, b{{v}_{i}})} $ (20)

域名标识符只能在环境ξρ下直接访问, 若是在le环境的某个cell子环境δC下, 需要通过域名表达式来访问一个protocol实例的域, 见规则(20).域名表达式形如图 3中的eth.etherTypevlan.etherType.

在规则(20)中, 会根据域fid在包头中的位置和大小来计算语义值.如图 3eth.etherType的语义值形如fdacc(eth, 112, 96, 111, bv), 其中, bv为当前PKT寄存器中eth区域中对应于域fidbit空间取值, 由硬件进行初始化设置, 在cell单元的处理中仅能只读访问.

规则(21)用于计算协议域访问中某一位的语义值, 与规则(18)相似.

$ \frac{\begin{matrix} ge, le, {{\delta }_{A}}\vdash {{e}_{1}}\Rightarrow fdacc(id, n, {{n}_{1}}, {{n}_{2}}, bv)\text{ }ge, le, {{\delta }_{c}}\vdash {{e}_{2}}\Rightarrow {n}'\text{ }0\le {{n}_{1}}\le {{n}_{2}}<n \\ 0\le {n}'\le {{n}_{2}}-{{n}_{1}}\text{ }b=get\_binary\_bit(bv, {n}')\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash EFieldBit({{e}_{1}}, {{e}_{2}})\Rightarrow fdacc(id, n, {{n}_{1}}+{n}', {{n}_{1}}+{n}', b)} $ (21)

例如, 在图 3cell B0处理单元中, 计算表达式eth.dmac[40]得到的语义值为fdacc(eth, 112, 39, 39, b), 其中, b是硬件初始化的bit值.

规则(22)用于计算协议域访问的子区间的语义值, 与规则(19)相似.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow fdacc(id, n, {{n}_{1}}, {{n}_{2}}, bv)\text{ }ge, le, {{\delta }_{c}}\vdash {{e}_{2}}\Rightarrow {n}'\text{ }ge, le, {{\delta }_{c}}\vdash {{e}_{3}}\Rightarrow {n}'' \\ 0\le {{n}_{1}}\le {{n}_{2}}<n\text{ }0\le {n}''\le {n}'\le {{n}_{2}}-{{n}_{1}}\text{ }b{v}'=get\_binary\_bits(bv, {n}', {n}'')\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash EFieldSection({{e}_{1}}, {{e}_{2}}, {{e}_{3}})\Rightarrow fdacc(id, n, {{n}_{1}}+{n}', {{n}_{1}}+{n}'', b{v}')} $ (22)

例如, ethernet实例eth的访问表达式eth.smac[16, 23]进行计算得到语义值为fdacc(eth, 112, 63, 70, bv’), 其中, bv’是已被硬件初始化过的bitbv(对应于实例eth的数据包包头)的子串.

类似于寄存器的访问, 协议域的访问也支持任意(合法的)嵌套, 如eth.smac[16, 23][2,4], eth.smac[16, 23][0], eth.smac[16, 23][2,4][2], 等等.这里应注意:我们规定寄存器访问的上下界由大到小, 而协议域访问区间或子区间的上下界由小到大.

4.2.4 位串连接运算

位串连接(++)是二元运算.规则(23)描述两个常规bit串之间的连接语义, 类似于传统语言中的字符串连接(用函数cat计算).

$ \frac{ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow b{{s}_{1}}\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow b{{s}_{2}}\text{ }bs=cat(b{{s}_{1}}, b{{s}_{2}})\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}}}{ge, le, {{\delta }_{C}}\vdash ({{e}_{1}}++{{e}_{2}})\Rightarrow bs} $ (23)

位串连接运算在Protocol环境中也可以进行, 为节省篇幅, 我们省略相应的规则(其他地方也有类似的情况, 不再赘述).

规则(24)描述两个寄存器访问的位串连接语义.

$ \frac{\begin{align} & ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow regacc(k, {{n}_{1}}, {{n}_{2}}, b{{s}_{1}})\text{ }|b{{s}_{1}}|={{n}_{1}}-{{n}_{2}}+1\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow regacc(k, {{m}_{1}}, {{m}_{2}}, b{{s}_{2}}) \\ & |b{{s}_{2}}|={{m}_{1}}-{{m}_{2}}+1\text{ }{{n}_{2}}={{m}_{1}}+1\text{ }0\le {{m}_{2}}\le {{m}_{1}}<{{n}_{2}}\le {{n}_{1}}<k\text{ }bs=cat(b{{s}_{1}}, b{{s}_{2}})\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{align}}{ge, le, {{\delta }_{C}}\vdash ({{e}_{1}}++{{e}_{2}})\Rightarrow regacc(k, {{n}_{1}}, {{m}_{2}}, bs)} $ (24)

两个bit串(bs1bs2)之间的连接也是传统的字符串连接(用函数cat计算), 但要注意的是, 两个寄存器访问区间一定要连续(规则中的条件n1=m2+1).

规则(25)描述两个协议域访问的位串连接语义.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow fdacc(id, k, {{n}_{1}}, {{n}_{2}}, b{{s}_{1}})\text{ }|b{{s}_{1}}|={{n}_{2}}-{{n}_{1}}+1\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow fdacc(id, k, {{m}_{1}}, {{m}_{2}}, b{{s}_{2}}) \\ |b{{s}_{2}}|={{m}_{2}}-{{m}_{1}}+1\text{ }{{n}_{1}}={{m}_{2}}+1\text{ }0\le {{m}_{1}}\le {{m}_{2}}<{{n}_{1}}\le {{n}_{2}}<k\text{ }bs=cat(b{{s}_{1}}, b{{s}_{2}})\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le, {{\delta }_{C}}\vdash ({{e}_{1}}++{{e}_{2}})\Rightarrow fdacc(id, k, {{m}_{1}}, {{n}_{2}}, bs)} $ (25)

同样也要注意的是, 两个域访问是属于同一个实例, 并且域区间一定要连续.

4.2.5 指令中寄存器的访问

规则(26)描述set指令的语义:将表达式e的取值转化为bit串后, 替换当前环境下寄存器访问ra语义值中对应区间的bit串(${{{\delta }'}_{C}}={{\delta }_{C}}{{|}_{ra\Rightarrow regacc(k, i, j, b{v}')}}$).

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash e\Rightarrow v\text{ }ge, le, {{\delta }_{C}}\vdash ra\Rightarrow regacc(k, i, j, bv)\text{ }b{v}'=trans\_to\_bits(bv, n) \\ n=i-j+1\text{ }{{{{\delta }'}}_{C}}={{\delta }_{C}}{{|}_{ra\Rightarrow regacc(k, i, j, b{v}')}}\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le\vdash ({{\delta }_{C}}, Set(ra, e))\Rightarrow {{{{\delta }'}}_{C}}} $ (26)

Set指令中的表达式e比较简单, 其计算结果为普通类型的语义值, 相应的trans_to_bits函数较易实现.

规则(27)描述mov指令的语义:将表达式e的取值转化为bit串后, 替换当前环境下寄存器访问ra语义值中对应区间的bit串.

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash e\Rightarrow v\text{ }mra=(r{{a}_{1}}++r{{a}_{2}}++...++r{{a}_{m}})\text{ }ge, le, {{\delta }_{C}}\vdash r{{a}_{1}}\Rightarrow regacc(k, {{i}_{1}}, {{j}_{1}}, b{{v}_{1}}) \\ ge, le, {{\delta }_{C}}\vdash r{{a}_{2}}\Rightarrow regacc(k, {{i}_{2}}, {{j}_{2}}, b{{v}_{2}})...\ ge, le, {{\delta }_{C}}\vdash r{{a}_{m}}\Rightarrow regacc(k, {{i}_{m}}, {{j}_{m}}, b{{v}_{m}}) \\ {{j}_{1}}={{i}_{2}}+1\text{ }{{j}_{2}}={{i}_{3}}+1...\text{ }{{j}_{m-1}}={{i}_{m}}+1\text{ }b{v}'=trans\_to\_bits(bv, n)\text{ }n={{i}_{1}}-{{j}_{m}}+1 \\ b{{{{v}'}}_{1}}=b{v}'[{{i}_{1}}, {{j}_{1}}]\text{ }b{{{{v}'}}_{2}}=b{v}'[{{i}_{2}}, {{j}_{2}}]...\text{ }b{{{{v}'}}_{m}}=b{v}'[{{i}_{m}}, {{j}_{m}}] \\ {{{{\delta }'}}_{C}}={{\delta }_{C}}{{|}_{r{{a}_{1}}\Rightarrow regacc(k, {{i}_{1}}, {{j}_{1}}, b{{{{v}'}}_{1}}), r{{a}_{2}}\Rightarrow regacc(k, {{i}_{2}}, {{j}_{2}}, b{{{{v}'}}_{2}}), ..., r{{a}_{m}}\Rightarrow regacc(k, {{i}_{m}}, {{j}_{m}}, b{{{{v}'}}_{m}})}}\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le\vdash ({{\delta }_{C}}, Mov(mra, e))\Rightarrow {{{{\delta }'}}_{C}}} $ (27)

虽然非形式解释类似于set指令, 但mov指令的寄存器访问要复杂许多:首先, 寄存器访问mra可以是其他多个空间连续寄存器访问的连接, 因此在修改环境(规则中是δC)时, 要考虑对每一个寄存器访问变量的语义值进行替换; 另外, mov指令中的表达式e也比较复杂, 可以包含寄存器和协议域的访问以及它们的连接运算, 因此, 相应的trans_to_bits函数实现较复杂一些.

规则(28)描述eq指令的语义:对寄存器访问表达式e1e2的取值进行比较(等价于将它们分别转化为整数后在比较), 将比较结果(true/false)转换为bit串后, 替换当前环境下寄存器访问ra语义值中对应区间的bit串(${{{\delta }'}_{C}}={{\delta }_{C}}{{|}_{ra\Rightarrow regacc(k, i, j, b{v}')}}$).

$ \frac{\begin{matrix} ge, le, {{\delta }_{C}}\vdash {{e}_{1}}\Rightarrow {{v}_{1}}\text{ }ge, le, {{\delta }_{C}}\vdash {{e}_{2}}\Rightarrow {{v}_{2}}\text{ }ge, le, {{\delta }_{C}}\vdash ra\Rightarrow regacc(k, i, j, bv) \\ b=trans\_to\_int({{v}_{1}})==trans\_to\_int({{v}_{2}})\text{ }b{v}'=trans\_to\_bits(b, n)\text{ }n=i-j+1 \\ {{{{\delta }'}}_{C}}={{\delta }_{C}}{{|}_{ra\Rightarrow regacc(k, i, j, b{v}')}}\text{ }{{\delta }_{C}}\ \text{is}\ {{\delta }_{A}}, {{\delta }_{B0}}\ \text{or}\ {{\delta }_{B1}} \\ \end{matrix}}{ge, le\vdash ({{\delta }_{C}}, Eq(ra, {{e}_{1}}, {{e}_{2}}))\Rightarrow {{{{\delta }'}}_{C}}} $ (28)

对应于指令lg的语义规则与规则(28)相似.

5 P3语言编译器P3C的设计框架 5.1 编译结构

P3语言的编译器P3C正在实现中, 其编译结构如图 10所示.源是人工编写的P3语言源代码(P3 source), 目标是编译器生成的二进制硬件配置文件(configure file).整个编译过程分为4个步骤:源代码首先经过词法语法分析器生成一棵P3抽象语法树(P3 AST); 接着, 对该抽象语法树进行类型检查(type checking), 以保证该抽象语法树是类型良好的, 从而得到一棵类型良好的抽象语法树(Well-typed P3 AST); 下一步, 根据类型良好的抽象语法树生成一种称为P3汇编语言(P3 assembly, 简称P3 ASM)的中间语言代码, 作为P3源代码和目标配置文件之间的“桥梁”; 最后, 由P3汇编语言代码翻译到目标配置文件.

Fig. 10 Compiler architecture of P3C 图 10 P3C编译结构

在整个编译结构中, 我们十分注重保证编译过程的可信性.目前, 我们对语法分析、类型检查和翻译到P3汇编语言这3个过程做了可信性设计, 从而让P3C编译器更加安全可靠, 见第5.2节.

5.1.1 词法语法分析

词法语法分析是编译过程的第1步工作, 源代码首先要通过词法分析器的处理, 转换为单词序列, 然后输入到语法分析器中.语法分析器则根据预先定义好的语法, 接受单词序列输入生成抽象语法树为后续步骤提供输入和处理对象.这里主要的设计工作分为两个内容:定义P3语言的语法、定义抽象语法树节点.

词法和语法分析实现的基本原理与传统编译器相同, 只是在具体实现时采用了Jourdan等人提出的方法[18]对语法分析程序进行了形式化验证, 见第5.2.1节.

5.1.2 静态语义检查

通过以上的词法语法分析, 语法分析器构造出了P3抽象语法树.为了保证这样的一棵抽象语法树是类型安全的, 下一步要对它进行类型检查, 若它能够通过类型检查, 则为类型良好的P3抽象语法树.类型系统的设计工作已在第3节中给出.

5.1.3 生成汇编

由于P3源语言与需要生成的目标二进制配置文件跨度较大, 难以一次完成翻译; 同时, 软硬件开发人员也需要协同设计.为此, 我们定义了一种中间格式的P3汇编语言(P3 assembly, 简称P3 asm)作为“桥梁”, 用来实现从P3源语言到目标二进制配置文件的过渡.P3 asm更加关注硬件配置的细节, 很关键的一点就是, 它把P3源语言中对层解析过程中的匹配查找条件(if语句)和寄存器操作(action)的描述转换成了对PB, PC硬件模块的描述.图 11是针对图 3中描述L2层解析的P3规范片段翻译至汇编代码片段的示例.

Fig. 11 A segment of P3 assembly code 图 11 P3汇编代码片段

图 11中, L2层对应汇编代码的头两行中, Pins(eth, 112)表明协议数据包头eth(ethernet的实例)的总bit数为122, 可由ethernet各个fields的总字节数(14, 参见第2.3节)得到, 即8×14.类似地, vlan是ieee802-1qTag(参见第2.3节)的实例, 总bit数应为8×4, 因此汇编片段中包含Pins(vlan, 32).

接下来就是对应于解析器硬件动作的几张配置表.每一层共有7张配置表:cell A有3张, cell B0和cell B1各2张.图 11刻画了图 3所描述的L2层示例所对应的3张cell A和2张cell B0硬件配置表.cell B1的两张表和cell B0的配置表结构上是一致的.我们称cell A的3张表分别为cella_pb, cella_pc_curcella_pc_nxt; 称cell B0的2张表分别为cellb0_pbcellb0_pc_cur, 以及cell B1的2张表分别为cellb1_pbcellb1_pc_cur.

图 11中, AbeginAend之间的部分用来描述cella_pb表, ACbeginACend之间的部分用来描述cella_ pc_cur表, 以及ANbeginANend之间的部分用来描述cella_pc_nxt表; B0beginB0end之间的部分用来描述cellb0_pb表, 而B0CbeginB0Cend之间的部分用来描述cellb0_pc_cur表.

cella_pb表中每一项分5个部分(以图 11Abegin部分的第1项为例):第1部分0x1是layer编号, 代表l2是所声明的第1个layer; 第2部分({(eth, 96, 16)==0x8100, (vlan, 16, 16)==0x0800})代表一个逻辑公式(略复杂, 下一段单独解释), 刻画当前项对应的分支条件; 第3部分0x1指向cella_pc_cur中编号为0x1的动作集合; 第4部分对应当前分支对应的next_header属性, 如0x3代表ipv4(声明protocol时, ipv4处于第3位次); 第5部分对应本层的bypass, 可能的取值有0, 1, 2.

关于cella_pb表中每一项的第2部分, 对应一个分支的条件, 即用于查表的条件.比如, {(eth, 96, 16)==0x8100, (vlan, 16, 16)==0x0800}对应图 3cellA中所描述的分支条件(eth.etherType==0x8100) & & (vlan.etherType== 0x0800).观察一下etherTypeeth(ethernet的实例)中的偏移位置和位数, 可知其偏移量为96(0~95是dmacsmac占据), 位数为16.类似地, vlan(ieee802-1qTag的实例)中etherType的偏移量为16, 位数为16.类似地, cella_pb表第2行中的{(eth, 96, 16)==0x0800}对应图 3cellA中的分支条件(eth.etherType==0x0800).各行对应的分支条件之间是互斥的.每个cell中, 各if语句以及每条if语句内部的所有分支条件是互斥的(在P3的设计中, 可由静态类型检查来判定).多条平行的if语句可组合产生的分支条件全部是互斥的, 体现在汇编代码的cella_pb, cellb0_pbcellb1_pb表中也都是互斥的, 因此硬件实现查表动作不会发生条件冲突的情形.

cella_pc_cur中每一项分3个部分(以图 7ACbegin部分的第1项为例):第1部分对应一个索引号0x1, 编号规则不重要, 只要表中各项的索引号互不相同即可; 第3部分对应本层的length属性值(单位:字节), 比如, 这里的0x12(对应十进制数18)由图 3中的length语句length=eth.length+vlan.length得到(eth字节数14, 加上vlan字节数4);第2部分为所有指令的集合(这些指令在硬件中会并行执行), 比如, {(mov(IRF, 0, 16), (vlan, 0, 16)), (set(IRF, 16, 8), 1), (set(IRF, 24, 8), 0)}对应图 3中3条指令的集合.其中, (mov(IRF, 0, 16), (vlan, 0, 16))对应指令“mov IRF_outer_vlan_high++IRF_outer_vlan_low, vlan.pcp++vlan.cfi++vlan.vid”.试观察, 在ARegisters中有定义:IRF_ outer_vlan_high=IRF[7:0], IRF_outer_vlan_low=IRF[15:8].注意:它们是连续的两个字节, 对应IRF的0~15位, 共16位, 所以我们在asm中用(IRF, 0, 16)表示.而vlan.pcp++vlan.cfi++vlan.vid表示vlan(ieee802-1qTag的实例)中从开始连续的域pcp, cfivid的连接, 长度也是16位, 对应的偏移量为0, 因此我们在asm中用(vlan, 0, 16)表示.另两条(set(IRF, 16, 8), 1)和(set(IRF, 24, 8), 0)分别对应两条set指令:“set IRF_tag_type_2b, 1”, “set IRF_pkt_type_3b, 0”.从ARegistersIRF_tag_type_2bIRF_pkt_type_3b的定义容易看出, 二者分别对应(IRF, 16, 8)和(IRF, 24, 8).

cella_pc_nxt中每一项分2个部分(以图 7ANbegin部分的第1项也是唯一的一项为例):第1部分对应本层cella_pb中某些项的next_header所指向的协议编号, 0x3代表ipv4(声明protocol时ipv4处于第3位次); 第2部分略微麻烦, 包含3个子部分, 分别是对应于cellA, cellB0和cellB1这3个cell信息.每个子部分均含两个分量:第1个分量指明当前通用寄存器(这里指IRF)中哪些内容需要传到后面层中某个cell的查表分支中使用, 由于目前硬件设计方案尚未定型, 所以暂时将其置为空集(空表); 第2个分量对应于在后面层中某个cell的分支条件中需要用到该协议(ipv4)的所有字段所在的偏移位置(以字节为单位).图 11cella_pc_nxt中的{(·)+(0 9)}对应于cellA, {(·)+(0xc 0xd 0xe 0xf 0x10 0x11 0x12 0x13}对应于cellB0, {(·)+(6 7)}对应于cellB1.它们的第1个部分对应于IRF位的偏移, 均暂时置为空表(·).我们先来看cellB0和cellB1这两部分.从图 4左边可知, 后面的L3层中有对ipv4的处理, 见实例v4.在L3的cellB0中, v4的srcAddrdstAddr字段被用在分支条件中, 而在ipv4协议包头(如图 4右边所示)中, 这两个字段的偏移位置处于第13, 14, ..., 20字节, 若从0开始编号, 则对应的字节偏移位置分别为12, 13, 14, 15, 16, 17, 18和19, 换作hexadecimal数字可用表(0xc 0xd 0xe 0xf 0x10 0x11 0x12 0x13)来描述.同样, 在L3的cellB1中, v4的flagOffsetflags字段被用在分支条件中, 而在ipv4协议包头中, 这两个字段的偏移位置处于第7和8字节, 由于从0开始编号, 因此用表/集合(6 7)表示.理解了这两个之后, 再来看cellA对应的部分.虽然在L3的cellA描述中没有直接的分支条件, 但在ipv4协议中包含了分支, 本文的设计中默认在协议中的语句都将划归相应的cellA, 同时在这种情形(协议中包含了分支条件)下当前层中仅允许包含最多一个ipv4的实例, 这就不难理解(0 9)这个表/集合了.在ipv4协议中包含的分支条件中用到字段ihltheProtocol, 可对应到协议包头中的第1和第10个字节, 以0作为初始编号的话, 就对应了(0 9).

cellb0_pb的每一项包含3个部分, 其含义与表cella_pb的前3部分相同, 只是内容对应于cell B0而非cell A的定义.类似地, 表cellb0_pc_cur的每一项只有2个部分, 分别与表cella_pc_cur每一项的前两部分对应.

如果表cellb1_pb和表cellb1_pc_cur有定义的话, 其结构与cellb0_pbcellb0_pc_cur完全对应.

5.1.4 生成包解析器硬件配置文件

P3C编译器的最后一步, 是由P3汇编代码生成二进制硬件配置文件.具体来说, 就是对每一层生成与上一节中提到的7张表所对应的二进制配置表.如cell A的3张表(cella_pb, cella_pc_curcella_pc_nxt)中, 第1张表对应PB模块的配置, 第2和第3张对应PC模块的配置(如图 2所示).根据图 11中的asm片段, P3C会将L2层的cella_pb表最终生成为如图 12所示格式的二进制硬件配置表.

Fig. 12 Information for the binary hardware configuration 图 12 二进制硬件配置信息

从这张配置表的标注信息可知, 当前L2层cella_pb表的每一项包含407bit数据, 假设共32项.由于该硬件配置表的语义涉及到硬件的实现细节, 读者不必深入理解, 若感兴趣, 可参考P3C编译器的设计文档[17].

5.2 核心编译过程的可信设计

可编程的数据包解析器是可编程数据平面的第1环, 为之设计并实现一个高可信的编译器, 将对SDN的安全性有着十分重要的意义.同时, 本文研究的背景是面向高安全等级的网络方面的课题, 可信编译的需求更为突出.因此, P3C编译器在设计之初就明确了定位:其主体将在交互式证明辅助工具Coq中实现, 核心过程均实现基于定理证明的形式化验证.限于篇幅, 下面仅结合图 10简要介绍.

5.2.1 语法分析器的正确性

图 10所示, P3C的设计考虑了语法分析过程的可信验证.语法分析的理论和技术已经相当成熟, 并且现有各种语法分析器自动构造工具已被认为足够可信.然而, 作为编译器的重要组成部分, 语法分析器的形式化验证工作也是获得编译器正确性证据链的重要一环.已有成功的方法可以借鉴, 是本文对P3C语法分析过程进行形式化验证的一个重要原因.

本文采用Jourdan等人[18]提出的方法来构建经过形式化验证的语法分析器, 如图 13(源于文献[18])所示.这种方法即使用一个经过形式化验证的确认程序(validator)来对未经验证的语法分析器生成器(parser generator)所产生的LR(1)自动机进行确认.在“编译-编译期”时, 确认程序接受语法分析器生成器生成的LR(1)自动机、原文法(grammer)以及用作证书的辅助信息(certificate)作为输入, 然后验证LR(1)自动机和原文法的等价性.若通过验证, 就证明该语法分析器是正确的, 从而得到了一个经过形式化验证的语法分析器.该方法实现较为简单, 且适用于各类LR(1)自动机.Jourdan等人运用该方法成功构造出了CompCert编译器[19]的语法分析器.他们对语法分析器进行的形式化验证, 主要目的是证明语法分析器拥有某些特定的性质.这些性质分别是可靠性(soundness)、安全性(safety)、完备性(completeness)和无二义性(unambiguity).

Fig. 13 Process of the formal verification of the syntactic parser 图 13 语法分析器的形式化验证整体流程

限于篇幅, 详情请参阅文献[18].

语法分析过程是目前P3C中唯一完整实现并且经过形式化验证的部分, 实现情况及其各模块的功能如图 14所示.

Fig. 14 Parser component of P3C 图 14 P3C语法分析部分

P3C编译器的实现语言是Ocaml.如同Jourdan等人在CompCert编译器中的实现, P3C的语法分析程序是由Menhir[20](Ocaml的一种常用的语法分析器生成器)自动生成的, 词法分析程序是由面向Ocaml的词法分析器构造工具Ocamllex生成的.词法和语法分析相关代码中, 除去来自CompCert的validator(Coq代码3 138行)以及Coq的库代码, 包含Coq代码(Tree.v, Tokenizer.v, Extraction.v)522行、Ocaml代码(.ml)676行、lexer描述文件(.mll)183行以及parser描述文件(.vy)617行.

5.2.2 静态类型检查的正确性

静态类型检查过程对P3抽象语法树实施类型检查, 其正确性可从两个方面描述:(1)通过类型检查程序的AST一定是类型良好的; (2)类型良好的AST一定能通过类型检查(即类型检查过程能正常结束).假设类型检查过程实现为函数typecheck_prog; 基于类型规则(见第3节)可定义AST形式的P3规范, p是类型良好的, 用wt_spec(p)表示.这两个性质可以表示如下.

(1)    ∀p.typecheck_prog(p)=OK(p)→wt_spec(p);

(2)    ∀p.wt_spec(p)→typecheck_prog(p)=OK(p).

其中, typecheck_prog(p)=OK(p)表示函数typecheck_prog作用于P3规范p可正常终止, 且不对p进行任何修改(返回p本身).

5.2.3 产生汇编的正确性

生成P3汇编语言是P3C编译器的核心工作, 它将容易理解和使用的P3语言翻译成更加接近目标文件格式的一种中间语言.因此, 保证翻译前后两种语言语义的一致性, 将是保证编译过程正确性的关键.形式化验证是确保编译过程正确性的必要途径, 主要有两种方法:(1)构造并证明编译过程本身的正确性, 类似于CompCert编译器[19]的构造方法; (2)采用翻译确认[12]的思路, 构造一个validator检查翻译前后的程序/规范在语义上的一致性, 同时确保该确认程序的正确性(最好能够给出证明).P3C编译器选择的是后一种方法(参考图 10), 即构造从P3 AST到P3 ASM的一个确认程序, 并证明其正确性.这一选择的出发点主要有:

1)    因需要软硬件协同设计, 翻译程序需要尽早实现; 而同时, 其正确性证明的难度和工作量很大, 时间上不能承受.即使能够按期实现, 但协同设计的许多不确定性, 意味着翻译过程的修改比较频繁.然而证明过程无法重用, 导致整个工作成本大增.

2)    从我们的问题出发, 设计从P3 AST到P3 ASM的确认程序的方案是相对容易的, 而且其正确性证明比起直接验证翻译过程更加容易.

3)    P3 AST到P3 ASM的定义(语法、静态和动态语义)已经明确, 比如本文前面几节的P3类型系统和操作语义等内容.P3 ASM的语法和语义定义相对简单一些(限于篇幅本文不予介绍), 而这些内容不再变化, 因此构造一个确认程序并证明其正确性具有更好的可重用性.

确认程序也可以借助于被认为可信的工具(如模型检验器和自动求解器)实现.比如, Lopes等人基于Z3求解器的原型工具[9]完全可以作为确认程序, 用于确认翻译前后的某种语义一致性; Kheradmand等人基于KEQ[11]提出了一种P4编译器的翻译确认实现方案[10].然而, 一般不会尝试对此类工具进行正确性证明, 一方面难度很大, 另一方面, 人们对此类工具已足够信任.与此不同, P3C中确认程序将进行正确性证明.

确认程序的正确性可描述为[21]:∀S, C.Validate(S, C)=true⇒SC, 其中, SC分别为任一具体的P3 AST和P3 ASM, Validate(S, C)成真表示确认成功, SC表示SC语义上是一致的.

所有自定义寄存器的访问区间不重叠(参见第2.4.2节及第3.4.1节)的特性可简化确认程序正确性的证明.

确认程序是编译器的一部分, 将会附加于翻译过程之后.包含确认程序的翻译过程可描述如下[21].

Comp’(S)=match Comp(S) with

  |ErrorError

  |OK(C)→if Validate(S, C) then OK(C) else Error

6 总结及未来工作展望

本文的主要贡献是设计了一种面向安全网络的可重构数据包解析器的专用硬件配置描述语言P3, 并提出其可信实现方案.基于对可重构硬件基本需求的充分理解, 经过软硬件设计人员的反复沟通与协同设计, 最终明确了如文中展示的P3语言核心特性(第2节)及其编译结构(第5节).P3语言及其编译器P3C的设计侧重于可信需求, 因此本文重点描述了该语言的静态语义(第3节的类型系统)以及动态语义(第4节的操作语义)定义.

P3语言语法的完整定义参见设计文档[17], 该文档中也包含了P3编译器P3C设计中的中间语言(AST和汇编语言)和目标语言(硬件配置文件描述语言)的完整定义, 其他内容也会随着项目进展补充完善.限于篇幅, 关于中间语言和目标语言, 本文仅通过样例予以说明, 参见第5.1.3节和第5.1.4节.

本文的核心内容是P3语言的设计, 对于编译器P3C仅介绍其设计框架(参见第5节), 不包括其实现.基于图 10所示的编译器结构, P3C各个部分的实现工作正在进展中.当前已完整实现部分及其各模块功能如图 14所示, 代码可下载[22], 其中包括词法和语法分析(含语法分析的确认程序及其正确性验证)的完整实现(参见第5.1.1节和第5.2.1节), 下载后可安装运行.

现阶段P3C项目正在开展的工作包括静态类型检查和产生汇编的模块, 同时, 硬件方面也在设计更多的使用样例, 用于测试和协同设计.未来剩余的工作中, 最具挑战性的部分是产生汇编过程的正确性验证(参见第5.2.3节), 将采用翻译确认的方法实现一个validator, 并证明其正确性.确认程序本身的实现并不复杂, 仅与AST和汇编代码的结构相关, 与产生汇编代码的过程无关.确认程序的正确性证明涉及到AST和汇编语言的语义定义, 前者参见第4节, 后者已完成.剩余工作均在Coq中完成, 有一定的工作量.一些看似简单的工作, 在实现时也可能不简单(至少从代码量角度来看).比如, 根据本文第3节和第4节的定义, 针对P3操作语义, P3类型系统的可靠性是显然的, 在Coq实现中, 虽然证明思路也是显然的, 但给出相应的证明会有不小的工作量.

期待P3C项目的开展能促进相关工作的进一步研究, 比如实现P4语言编译器本身或者翻译确认程序的机器证明(对于P4语言编译器的正确性验证, 目前已有的工作主要集中在基于模型检验器或自动求解器进行翻译确认).

参考文献
[1]
Broadcom Corporation. Broadcom BCM56850 StrataXGSⓇTrident Ⅱ Switching Technology. Broadcom, 2013.
[2]
Davie BS, Rekhter Y. MPLS:Technology and Applications. Morgan Kaufmann Publishers Inc., 2000. http://cn.bing.com/academic/profile?id=82edd92afb40416c7bfe1429d9a92a71&encoded=0&v=paper_preview&mkt=zh-cn
[3]
Hanks S, Meyer D, Farinacci D, et al. Generic Routing Encapsulation (GRE). RFC 2784, 2000. http://cn.bing.com/academic/profile?id=4ff69df89b23ea0c9002baf1e95d8709&encoded=0&v=paper_preview&mkt=zh-cn
[4]
Mahalingam M, Dutt DG, Duda K, et al. Virtual eXtensible local area network (VXLAN):A framework for overlaying virtualized layer 2 networks over layer 3 networks. RFC 7348, 2014. http://cn.bing.com/academic/profile?id=8d441cb252b9ea6d97b3758a818e0969&encoded=0&v=paper_preview&mkt=zh-cn
[5]
McKeown N. Software-defined networking. INFOCOM Keynote Talk, 2009, 17(2): 30-32. http://cn.bing.com/academic/profile?id=a9de01b446e73b6638747c3c668e819b&encoded=0&v=paper_preview&mkt=zh-cn
[6]
Bosshart P, Gibb G, Kim HS, et al. Forwarding metamorphosis:Fast programmable match-action processing in hardware for SDN. ACM SIGCOMM Computer Communication Review, 2013, 43(4): 99-110. [doi:10.1145/2534169.2486011]
[7]
Bosshart P, Daly D, Gibb G, et al. P4:Programming protocol-independent packet processors. ACM SIGCOMM Computer Communication Review, 2014, 44(3): 87-95. [doi:10.1145/2656877.2656890]
[8]
Liu J, Hallahan W, Schlesinger C, et al. P4v: Practical verification for programmable data planes. In: Proc. of the 2018 Conf. of the ACM Special Interest Group on Data Communication. ACM, 2018. 490-503.
[9]
Lopes N, Bjørner N, McKeown N, et al. Automatically verifying reachability and well-formedness in P4 networks. Technical Report, 2016. http://cn.bing.com/academic/profile?id=490dc4c325a675fc3650b2cba162fae8&encoded=0&v=paper_preview&mkt=zh-cn
[10]
Kheradmand A, Rosu G. P4K: A formal semantics of P4 and applications. arXiv Preprint arXiv: 1804.01468, 2018.
[11]
The K Framework Development Team. KEQ. 2017. https://github.com/kframework/k/tree/keq
[12]
Pnueli A, Siegel M, Singerman E. Translation validation. In: Proc. of the Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems. Berlin, Heidelberg: Springer-Verlag, 1998. 151-166.
[13]
Benácek P, Pu V, Kubátová H. P4-to-Vhdl: Automatic generation of 100 Gbps packet parsers. In: Proc. of the 2016 IEEE 24th Annual Int'l Symp. on Field-programmable Custom Computing Machines (FCCM). IEEE, 2016. 148-155.
[14]
Zhao Y, Yin SJ, Li XY. Reconfigurable unit design in a reconfigurable Ethernet packet parser. Computer Engineering & Science, 2020, 42(2): 220-228(in Chinese with English abstract). [doi:10.3969/j.issn.1007-130X.2020.02.005]
[15]
P4 Language Consortium. P4 language specification, Version 1.0.4. 2017. https://p4.org/specs/
[16]
Peterson LL, Davie BS. Computer Networks:A Systems Approach. Elsevier, 2007. http://cn.bing.com/academic/profile?id=1b056e0016112d85526cb991a2382090&encoded=0&v=paper_preview&mkt=zh-cn
[17]
[18]
Jourdan JH, Pottier F, Leroy X. Validating LR (1) parsers. In: Proc. of the European Symp. on Programming. Berlin, Heidelberg: Springer-Verlag, 2012. 397-416.
[19]
CompCert Home. 2008. http://compcert.inria.fr/
[20]
Pottier F, Régis-Gianas Y. Menhir reference manual. 2018. http://gallium.inria.fr/~fpottier/menhir/manual.pdf
[21]
Leroy X. Formal verification of a realistic compiler. Communications of the ACM, 2009, 52(7): 107-115. [doi:10.1145/1538788.1538814]
[22]
[14]
赵宇, 殷树娟, 李翔宇. 一种可重构以太网数据包解析器中可重构单元的设计. 计算机工程与科学, 2020, 42(2): 220-228. [doi:10.3969/j.issn.1007-130X.2020.02.005]