黄厚华(1995-), 男, 硕士生, CCF学生会员, 主要研究邻域为形式化方法程序验证
刘嘉祥(1987-), 男, 博士, 助理教授, CCF专业会员, 主要研究领域为形式化方法, 程序验证, 神经网络验证
施晓牧(1987-), 女, 博士, CCF专业会员, 主要研究领域为形式化方法, 定理证明技术及其在安全关键系统的应用
ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术, 并命名为ARM Helium, 声明能为ARM Cortex-M处理器提升达15倍的机器学习性能. 随着物联网的高速发展, 微处理器指令执行正确性尤为重要. 指令集的官方手册作为芯片模拟程序, 片上应用程序开发的依据, 是程序正确性基本保障. 主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究. 基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码, 并将其转换为形式化语义转换规则. 通过K Framework提供的可执行框架利用测试用例, 验证机器学习指令算数运算执行的正确性.
ARM develops an M-Profile vector extension solution in terms of ARMv8.1-M micro processor architecture and names it ARM Helium. It is declared that ARM Helium can increase the machine learning performance of the ARM Cortex-M processor by up to 15 times. As the Internet of Things develops rapidly, the correct execution of microprocessors is important. In addition, the official manual of instruction sets provides a basis for developing chip simulators and on-chip applications, and thus it is the basic guarantee of program correctness. This study introduces these mantic correctness of vectorized machine learning instructions in the official manual of the ARMv8.1-M architecture by using K Framework. Furthermore, the study automatically extracts pseudo codes describing the vectorized machine learning instruction operation based on the manual and then formalizes them in semantics rules. With the executable framework provided by K Framework, the correctness of machine learning instructions in arithmetic operation is verified.
ARM Helium是2019年ARM推出的新技术. 其针对ARMv8.1-M版本的架构设计了M-profile vector extension (MVE)向量化扩展, 加强了ARM Cortex-M系列处理器在特定应用场景的计算性能. 例如, Helium可以为ARM Cortex-M系列处理器提升5倍的信号处理性能以及15倍机器学习(machine learning, ML)性能, 其中能为终端设备深度学习的推理过程减少50%–90%的用时以及更少的能量消耗. Helium指令集的特点是实现特定场景下频繁应用的运算向量化以加速复杂程序, 例如深度学习推理过程, 快速傅里叶变换, 滤波算法, 循环缓冲, 多项式展开, 密码学大整数域运算等. ARM Cortex-M55处理器是第1个采用ARMv8.1-M架构的处理器. STMicroelectronics等公司已将ARM Cortex-M55集成到下一代人工智能终端及其生态环境. 开发人员已经在使用开源库(如CMSIS-DSP, CMSIS-NN)和ML框架(如用于微控制器的TensorFlow Lite)将机器学习应用程序移植到Cortex-M设备上, TensorFlow Lite设计使用在内存占用非常小的处理器上运行机器学习模型, CMSIS-DSP和CMSIS-NN库中添加了对Cortex-M55的支持, 这使得将ML应用程序移植到Cortex-M55变得更为容易, 开发人员可以使用它们熟悉的库和神经网络框架, 通过调用Helium技术的向量化指令集以及更强的数据处理能力, 提升机器学习性能. ARM公司估计到2022年, 超过20%的物联网终端设备将拥有ML支持, 可以预计Cortex-M55在物联网中将会得到广泛应用. 由于物联网对于微处理器的需求量很大, 比如在无人机导航或控制, 终端人工智能, 机器人控制等, 因此若底层架构指令或官方文档出现错误, 将会造成巨大的隐患, 有可能使得物联网出现大规模的损失. 因此对于ARMv8.1-M微处理器架构而言, 其指令正确性尤为重要. 本文目的是验证ARMv8.1-M架构官方手册[
K Framework[
相关工作, 其中包括运用K Framework进行指令语义形式化的工作, 如Dasgupta等人[
(1) 对ARMv8.1-M的最新版本架构扩展中Helium技术的向量化ML指令语义进行形式化验证.
(2) 在文档中自动提取向量化ML指令语义的伪代码, 利用K Framework的模块化定义其形式化语义.
(3) 通过官方提供的测试用例与自动生成的测试用例进行实验, 验证ML指令运算功能正确性.
本文第1节介绍了K Framework以及手册中向量化ML指令的相关知识. 第2节介绍了应用K Framework实现可执行的向量化ML指令语义的框架. 第3节讲述了K Framework定义向量化ML指令的语法与语义规则. 第4节描述了单指令语义形式化的具体实现. 第5节展示了关于可执行语义的实验. 第6节是总结与展望.
本节首先简单介绍K Framework的背景知识, 然后介绍在ARMv8.1-M架构的官方手册中关于向量化ML指令语义的相关内容.
K Framework (以下称K框架)是基于重写逻辑的可执行语义工具框架, 它是一种用于设计和建模编程语言和软件/硬件系统的工具. K框架的核心是一种称为K的编程, 建模和规范语言, 以及基于matching logic的验证能力. K框架包括用于编译K描述的语义规则以构建解释器, 模型检查器, 验证器, 相关文档等的工具. 当给定语法与语义, K框架可以自动生成该语言的解析器(parser), 解释器(interpreter)以及演绎程序验证器(deductive program verifiers)等形式化分析工具, 不需要进行额外的开发. 运用K框架的解释器可以立即测试语言的语义以显著提高语义形式化开发的效率. 此外, 形式化分析工具有助于给定语言语义的形式化推导. 这在语义的适用性和语义本身的工程方面都有帮助.
简单来说, 在K框架中语言的语法(syntax)以传统的巴科斯范式(BNF)定义. 语言的语义(semantics)被定义为规则(rule), 另外由配置(configuration)来定义状态. 配置是程序代码和状态规约的集合, 直观说它是一个元组, 这个元组的元素(称为cells)代表着语义中的状态集合, 例如内存或寄存器的状态. K框架中, 有一个命名为
K框架已被应用于很多项目中以实现语义形式化, 如C[
本文验证的对象是ARMv8.1-M架构的官方参考手册(以下称ARM手册)中关于ARM Helium技术的向量化机器学习(machine learning, ML)指令. 其中ARM Helium技术是ARMv8.1-M架构的新型M-Profile Vector Extension (MVE)向量扩展, 为架构带来计算能力的增强, 大幅提升机器学习以及信号处理等性能.
本文主要验证ARM Helium中关于ML的指令集扩展, 该扩展主要包含在机器学习中常用的向量大小比较和向量内积这两方面的向量化指令. 向量比较大小的指令可以用于如ReLU激活函数的实现, 神经网络分类结果判断等. 向量内积的指令则可以用于矩阵乘加, 卷积运算等. 向量化的指令使得同一时钟周期内可以执行更多的运算操作. 本文涉及的向量化ML指令范围: 所要验证的ML指令包含21条(区分整型和浮点数), 助记符17个, 且假设在应用模式下而非系统内核模式下进行语义形式化. 21条指令中有4条调用浮点寄存器, 比较两个源寄存器值的大小, 并保存最大或最小值到目标寄存器; 4条关于判断一个向量寄存器与通用寄存器的值的最大或最小值, 并保存在此通用寄存器中; 12条是关于判断向量寄存器间的值的最大或最小值, 并将结果保存到目标向量寄存器中, 其中4条关于整型, 8条关于浮点数; 还有1条指令是向量内积运算, 即机器学习中常用到的, 求两向量内对应元素的乘积的和的运算. 以上除了4条助记符相同的指令未涉及向量寄存器其他都是向量化指令, 所有统称为向量化ML指令(以下简称ML指令). 这些ML指令用于计算神经网络分类结果, 如比较大小的操作. 由于我们重点关注的是ML指令的比较运算(包括整数, 浮点数)和向量内积运算(整数)执行的语义正确性, 所以文中重点描述算术运算的处理细节, 如NaN (not a number)处理. 由于涉及的指令与其他算术运算无关, 因此建模中不涉及进位等标志符(向量内积运算不影响标志符). 本文验证的ML指令中, 要处理的数据类型分为整型和浮点数.
这21条ML指令的寻址方式都是寄存器寻址, 因此需要官方文档中寄存器寻址方式的定义. 因为ML指令大部分是向量化寄存器处理, 因此还需要与向量寄存器存取相关的定义. 如
向量寄存器
在向量寄存器内, 每个元素的二进制位数大小必须相等. 对于整型值, 按照向量内每个元素的二进制位大小, 分为8, 16和32位. 因此向量寄存器内整型元素大小最长为32位, 最小为8位. 而对于浮点数, 元素大小分为16位, 32位与64位. 当为16位时, 首位为符号位, 次5位为指数位, 最后10位为尾数位; 当为32位时, 首位为符号位, 次8位为指数位, 最后23位为尾数位. 64位的首位是符号位, 次11位为指数位, 最后52位为尾数位. 浮点数的处理为IEEE 754标准. 关于指令语义的具体处理及其形式化在第3节中详细说明.
官网手册中ML指令描述结构由功能简述, 二进制编码, 语法, 译码伪代码, 汇编符号解析以及操作伪代码组成. 其中操作伪码即为诠释ML指令的执行语义, 因此着重于操作伪代码的分析. 如
VMAXNM指令的操作伪代码
本文目标是验证应用模式下ML指令执行语义正确性, 在操作伪码提取时提取完整的伪代码作为形式化语义规则的基础, 以确保语义的完整. 如
如
本文运用K框架实现ML指令语义的形式化, ML指令语义形式化以及测试的框架如
基于K框架的语义形式化与测试
第1部分(
ML指令语义执行流程
第2部分(
第3步(
本节首先介绍ML指令语法的定义, 接着介绍用K框架规则对ML指令执行语义的形式化.
ML指令语法
ML指令的语法定义如
ML指令的数据类型总共9种, 不同指令能使用的数据类型种类有区别. 且对于不同指令, 操作数类型是有限制的, 比如VMAXNM指令对不同类型操作数实现功能各不相同.
本文对处理器状态的假设是其运行在应用模式下对ML指令的执行语义进行验证. 指令执行语义的第1部分是状态监测与类型分析. 因此, 需要将处理器中的特殊寄存器预设为满足应用模式下运行状态的值. 通过判断寄存器标志, 让ML指令正常进入应用模式并开始运行算数运算的操作部分. 状态寄存器的预设, 通过将状态寄存器的特殊位赋予相应的值. 如控制寄存器CONTROL, 它的第2位(最低位开始)影响当前运行状态是否允许浮点数扩展, 当为0时浮点数扩展不激活, 为1时激活. 当指令需要在浮点数状态下运行时, 可以通过判断CONTROL的第2位是否等于1来表示是否执行浮点数的相关操作. 而当其等于0时, 不可以执行浮点数的相关操作, 但可以执行整型的相关操作. 其他影响ML指令运行状态的状态寄存器以相同的方式检测.
类型分析是分析当前执行的ML指令涉及的数据类型. 本文所验证的ML指令因为大部分都涉及元素的大小比较, 且分为整数和浮点数. 数据类型分为9种类型, 即语法中的
向量寄存器是由4个32位浮点寄存器
寄存器取值语义规则
按位取值操作则由
ML指令大部分是关于获取一组数据中最大或最小值的操作, 与之伴随的是比较大小. 比较就涉及类型转换, 而且K框架中的比较规则涉及整型, 浮点数以及位向量, 比较时需将比较的元素转换为相同的对应类型后才能比较. 按照原语义, 需将位向量转换为对应的整型或浮点数后, 运用比较规则进行比较. 接下来说明位向量转换为浮点数和整型类型的语义实现.
位向量转为浮点数语义规则
第4行的
第5行的
第6行的
第7行的
第8行的
第9到第12行的
最后一行的位向量到浮点数转换规则
位向量转换为整型数的类型转换规则, 可以用K框架的标准模块MINT中内置的位向量转换为整数的规则实现. 比如, 将位向量转换为有符号数整数, 就可以调用
从第3.2.3节可知, 当指数位向量所代表的整数值与指数位为E所能表示的最大整数值相等, 并且尾数位向量所代表的整数值大于0时, 位向量所代表的浮点数就是NaN. 因此, 需要对位向量进行NaN处理. 官方手册中, ML指令处理NaN的语义将NaN分为QNaN和SNaN两种类型. QNaN与SNaN的不同之处在于, QNaN的尾数部分最高位(即
对于NaN处理, 我们按照指令原语义实现. NaN处理有3种情况, 如
NaN处理语义规则
该NaN检测位于比较操作之前, 即未经类型转换, 数据类型仍为位向量. 因此保证了不会有NaN参与类型转换和比较操作, 与官方手册的语义一致.
经过NaN处理与类型转换后, 指令执行可以进入元素间的大小比较阶段. 在K框架的标准模块中, 包含着各种数据类型的比较规则, 如整型, 浮点值和位向量. 本文应用了位向量和浮点值的比较规则, 以实现整型ML指令和浮点数ML指令的比较操作. K框架中的MInt模块中,
本节介绍为指令语义形式化而定义的算术运算规则. ML指令中的VMLAV指令实现向量内积的功能, 是将两个源操作数, 即两个向量寄存器中的对应元素, 做乘法运算, 再将得到的乘积做累加求和, 最终取结果的低32位写入目标寄存器(32位通用寄存器)中. VMLAV指令的数据类型是整型, 区分无符号和有符号整型. 并且该指令不会改变任何标识符, 如进位等, 因为过程中的乘法与加法运算是以整数的形式(先将位向量转换为对应的整型)进行, 再将运算得到的整型结果转换为位向量形式的最终结果, 并且只保留结果的低32位, 因此不涉及进位和溢出等标志符, 亦不会影响其他任何标志符.
如
算术运算的语义规则
操作数为向量寄存器的ML指令一般包含4个节拍, 每个节拍的操作相同. 以
按位写入与单节拍指令执行的语义规则
由此, 可以运用
本节以三地址指令VMAXNM.
指令VMAXNM.
K框架实现ML指令语义的形式化, 可以自动生成可执行的correct-by-construction的指令解释器. 本文利用该解释器, 对官方的ML指令测试集以及我们自动生成的多个测试用例进行实验, 检测ML指令语义的正确性. 此处的官方测试集是指ARM Cortex-M55官方手册[
官方测试用例实验结果
Benchmarks | 指令 | 测试
|
含NaN
|
正确 | NaN
|
整型 | VMAX | 1 | - | √ | - |
VMAXA | 1 | - | √ | - | |
VMAXV | 1 | - | √ | - | |
VMAXAV | 1 | - | √ | - | |
VMIN | 1 | - | √ | - | |
VMINA | 1 | - | √ | - | |
VMINV | 1 | - | √ | - | |
VMINAV | 1 | - | √ | - | |
VMLAV | 1 | - | √ | - | |
浮点数 | VMAXNM-S | 1 | 0 | √ | 0 |
VMAXNM-D | - | - | - | - | |
VMAXNM-Q | 1 | 0 | √ | 0 | |
VMAXNMA | 1 | 0 | √ | 0 | |
VMAXNMV | 1 | 0 | √ | 0 | |
VMAXNMAV | 1 | 0 | √ | 0 | |
VMINNM-S | 1 | 0 | √ | 0 | |
VMINNM-D | - | - | - | - | |
VMINNM-Q | 1 | 0 | √ | 0 | |
VMINNMA | 1 | 0 | √ | 0 | |
VMINNMV | 1 | 0 | √ | 0 | |
VMINNMAV | 1 | 0 | √ | 0 |
生成测试用例实验结果
生成测试用例 | 指令 | 测试
|
含NaN
|
正确 | NaN
|
整型 | VMAX | 30 | - | √ | - |
VMAXA | 30 | - | √ | - | |
VMAXV | 30 | - | √ | - | |
VMAXAV | 30 | - | √ | - | |
VMIN | 30 | - | √ | - | |
VMINA | 30 | - | √ | - | |
VMINV | 30 | - | √ | - | |
VMINAV | 30 | - | √ | - | |
VMLAV | 30 | - | √ | - | |
浮点数 | VMAXNM-S | 30 | 0 | √ | 0 |
VMAXNM-D | 30 | 0 | √ | 0 | |
VMAXNM-Q | 30 | 2 | √ | 2 | |
VMAXNMA | 30 | 0 | √ | 0 | |
VMAXNMV | 30 | 3 | √ | 3 | |
VMAXNMAV | 30 | 4 | √ | 4 | |
VMINNM-S | 30 | 2 | √ | 2 | |
VMINNM-D | 30 | 0 | √ | 0 | |
VMINNM-Q | 30 | 4 | √ | 4 | |
VMINNMA | 30 | 6 | √ | 6 | |
VMINNMV | 30 | 2 | √ | 2 | |
VMINNMAV | 30 | 1 | √ | 1 |
如
由于官方的测试用例没有涵盖操作数类型为双精度浮点寄存器的指令, 以及没有涵盖NaN检测的用例, 本文从而生成了满足上述两种情况的测试用例, 并覆盖到所有上文定义的语法语义. 从
上述的实验是对单个指令进行的测试, 此处举出一个运用不同指令组成的程序的测试用例. 此用例实现了神经网络中常用到的最大池化操作和全连接层操作的功能.
最大池化层与全连接层
通过分析ARMv8.1-M架构官方手册中关于ML的指令的语法与语义, 运用K Framework 定义了关于ARM Helium MVE技术的向量化ML指令的形式化执行语义. 详细介绍了如何运用K框架模块化的实现向量化ML指令语义规则以及如何利用K框架配置得到可执行的语义. 最终通过多个测试用例和官方基准用例, 对形式化的可执行语义进行测试, 验证了所有K框架中定义的ML指令语法语义及其运算逻辑.
本文所实现的ML指令只是ARMv8.1-M架构官方手册中ARM Helium MVE技术指令集的一部分, 且重点关注的是指令的算术运算执行逻辑, 因此未来工作包括: (1)不仅关注向量化ML指令的功能语义的形式化, 还会关注其他向量化指令; (2)运用K框架内置的验证功能, 如其内置的可达性验证功能和SMT工具调用功能, 验证程序正确性; (3)处理器状态, 内存状态检验的操作语义, 以及异常处理等方面的形式化实现; (4)并利用指令形式化语义对等价指令转换, 代码优化等方面进行验证.
https://developer.arm.com/documentation/ddi0553/bo]]>
Roșu G, Șerbănută TF. An overview of the K semantic framework. The Journal of Logic and Algebraic Programming, 2010, 79(6): 397–434. [doi: 10.1016/j.jlap.2010.03.012]
Şerbănuţă TF, Arusoaie A, Lazar D, Ellison C, Lucanu D, Roşu G. The
http://www.jos.org.cn/1000-9825/4851.htm]]>
http://www.jos.org.cn/1000-9825/4851.htm]]>
Armstrong A, Bauereiss T, Campbell B, Reid A, Gray KE, Norton RM, Mundkur M, Wassell M, French J, Pulte C, Flur S, Stark I, Krishnaswami N, Sewell P. ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPS. Proceedings of the ACM on Programming Languages, 2019, 3: 71. [doi: 10.1145/3290384]
® v8-A and v8-M system level architecture. In: Proc. of the 2016 Formal Methods in Computer-aided Design. Mountain View: IEEE, 2016. 161–168.]]>
Ellison C, Rosu G. An executable formal semantics of C with applications. ACM Sigplan Notices, 2012, 47(1): 533–544. [doi: 10.1145/2103621.2103719]
Stefanescu A. MatchC: A matching logic reachability verifier using the
https://developer.arm.com/documentation/101273/r0p2]]>