基于K Framework的向量化机器学习指令语义形式化.pdf

基于 K Framework 的向量化机器学习指令语义形式化*黄厚华,刘嘉祥,施晓牧(深圳大学计算机与软件学院,广东深圳518060)通信作者:施晓牧,E-mail:摘要:ARM 针对 ARMv8.1-M 微处理器架构推出基于 M-Profile 向量化扩展方案的技术,并命名为 ARMHelium,声明能为 ARMCortex-M 处理器提升达 15 倍的机器学习性能.随着物联网的高速发展,微处理器指令执行正确性尤为重要.指令集的官方手册作为芯片模拟程序,片上应用程序开发的依据,是程序正确性基本保障.主要介绍利用可执行语义框架 KFramework 对 ARMv8.1-M 官方参考手册中向量化机器学习指令的语义正确性研究.基于ARMv8.1-M 的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码,并将其转换为形式化语义转换规则.通过 KFramework 提供的可执行框架利用测试用例,验证机器学习指令算数运算执行的正确性.关键词:ARMv8.1-M 架构;向量化指令;机器学习;KFramework;形式化语义中图法分类号:TP18中文引用格式:黄厚华,刘嘉祥,施晓牧.基于KFramework的向量化机器学习指令语义形式化.软件学报,2023,34(8):38533869.http:/ Formalization of Vectorized Machine Learning Instructions in K FrameworkHUANGHou-Hua,LIUJia-Xiang,SHIXiao-Mu(CollegeofComputerScienceandSoftwareEngineering,ShenzhenUniversity,Shenzhen518060,China)Abstract:ARMdevelopsanM-ProfilevectorextensionsolutionintermsofARMv8.1-MmicroprocessorarchitectureandnamesitARMHelium.It is declared that ARM Helium can increase the machine learning performance of the ARM Cortex-M processor by up to 15times.AstheInternetofThingsdevelopsrapidly,thecorrectexecutionofmicroprocessorsisimportant.Inaddition,theofficialmanualofinstruction sets provides a basis for developing chip simulators and on-chip applications,and thus it is the basic guarantee of programcorrectness.This study introduces these mantic correctness of vectorized machine learning instructions in the official manual of theARMv8.1-M architecture by using K Framework.Furthermore,the study automatically extracts pseudo codes describing the vectorizedmachinelearninginstructionoperationbasedonthemanualandthenformalizestheminsemanticsrules.WiththeexecutableframeworkprovidedbyKFramework,thecorrectnessofmachinelearninginstructionsinarithmeticoperationisverified.Key words:ARMv8.1-Marchitecture;vectorizedinstruction;machinelearning;KFramework;formalsemanticsARMHelium 是 2019 年 ARM 推出的新技术.其针对 ARMv8.1-M 版本的架构设计了 M-profilevectorextension(MVE)向量化扩展,加强了 ARMCortex-M 系列处理器在特定应用场景的计算性能.例如,Helium 可以为 ARMCortex-M 系列处理器提升 5 倍的信号处理性能以及 15 倍机器学习(machinelearning,ML)性能,其中能为终端设备深度学习的推理过程减少 50%90%的用时以及更少的能量消耗.Helium 指令集的特点是实现特定场景下频繁应用的运算向量化以加速复杂程序,例如深度学习推理过程,快速傅里叶变换,滤波算法,循环缓冲,多项式展开,密*基金项目:深圳市科创委基础研究面上项目(JCYJ20210324094202008);国家自然科学基金(62002228);深圳市高等院校稳定支持计划(20200810045225001)本文由“智能系统的分析和验证”专题特约编辑明仲教授、张立军教授和秦胜潮教授推荐.收稿时间:2021-09-05;修改时间:2021-10-14;采用时间:2022-01-10;jos 在线出版时间:2022-01-28CNKI 网络首发时间:2023-01-19软件学报ISSN1000-9825,CODENRUXUEWE-mail:Journal of Software,2023,34(8):38533869doi:10.13328/ki.jos.006595http:/中国科学院软件研究所版权所有.Tel:[phone]码学大整数域运算等.ARMCortex-M55 处理器是第 1 个采用 ARMv8.1-M 架构的处理器.STMicroelectronics等公司已将 ARMCortex-M55 集成到下一代人工智能终端及其生态环境.开发人员已经在使用开源库(如 CMSIS-DSP,CMSIS-NN)和 ML 框架(如用于微控制器的 TensorFlowLite)将机器学习应用程序移植到 Cortex-M 设备上,TensorFlowLite 设计使用在内存占用非常小的处理器上运行机器学习模型,CMSIS-DSP 和 CMSIS-NN 库中添加了对 Cortex-M55 的支持,这使得将 ML 应用程序移植到 Cortex-M55 变得更为容易,开发人员可以使用它们熟悉的库和神经网络框架,通过调用 Helium 技术的向量化指令集以及更强的数据处理能力,提升机器学习性能.ARM 公司估计到 2022 年,超过 20%的物联网终端设备将拥有 ML 支持,可以预计 Cortex-M55 在物联网中将会得到广泛应用.由于物联网对于微处理器的需求量很大,比如在无人机导航或控制,终端人工智能,机器人控制等,因此若底层架构指令或官方文档出现错误,将会造成巨大的隐患,有可能使得物联网出现大规模的损失.因此对于 ARMv8.1-M微处理器架构而言,其指令正确性尤为重要.本文目的是验证 ARMv8.1-M 架构官方手册1中,ARMHelium 技术中向量化 ML 指令的语义正确性.验证 Helium 技术的向量化 ML 指令,存在以下的一些难点:(1)与之前版本的ARMv8 的 M 架构不同,ARMv8.1-M 的 Helium 技术的指令引入了新的加速数据存取以及操作的向量化特性;(2)引入向量化寄存器及节拍(Beat)的概念;(3)同一个助记符,在操作寄存器类型不同时有不同的功能实现.KFramework2,3作为实现语义形式化4,5的工具,它具有以下优点:(1)具备模块化的特性,这有利于扩展现有架构的指令集,当架构有新指令扩展时,可以在已有的框架基础上实现新功能的语义扩展;(2)可以自动生成可执行的解释器,指令语义可以直接通过官方提供的测试集以及补充测试集进行测试,在语义正确的基础下,解释器等自动生成的工具具备 correct-by-construction 的特点,帮助使用架构的开发者更快地熟悉指令功能;(3)基于重写与matchinglogic 理论,提供程序中可达性等问题的验证能力;(4)KFramework 的标准模块支持整型,二进制位向量和浮点数数据类型及相应的运算操作,如数据类型转换,位向量转换为浮点数或整型,以及位向量的移位操作等,有利于实现位向量指令语义的形式化.所以本文应用 KFramework 作为向量化 ML 指令语义形式化的工具框架.相关工作,其中包括运用 KFramework 进行指令语义形式化的工作,如 Dasgupta 等人6运用 KFramework 对x86-64 架构的用户级指令集进行语义形式化并验证其语义正确性;如 Wang 等人7在 KFramework 中定义了RUST 语言的可执行语义 KRust 并成功测试了官方基准测试程序;以及 C,Java 等语言上的实现.另外相关工作还包括 ARMv8 架构指令集的验证工作,如针对 ARMv8-A 架构指令进行语义形式化的工作,Armstrong 等人8运用Sail 语言及其工具集对 ARMv8-A 架构的指令集体系结构(ISA)语义进行形式化并验证.Sail 是专用于描述 ISA9的语言.其作为中间语言负责将官方提供的 ISA 的架构规范语言(ASL)转换到用于仿真或验证的其他语言,包括用于仿真的 C 与 OCaml,用于验证的 Isabelle/HOL,HOL4,Coq.用 Sail 实现指令语义的描述主要目的在于 ISA 仿真程序的生成,或并发执行的研究.由于这些用途,Sail 语言被设计的尽可能贴近 ARM 官方文本中的伪码,且需要对 ISA 具体的特征建模.而 KFramework 相比 Sail 用途更加广泛,KFramework 作为更为通用的语义描述语言更适用于描述特定应用的形式化语义.在本工作中采用 KFramework 的优势有两点:(1)相比 Sail,KFramework 可以根据需求对语义涉及的指令集架构的模型进行抽象,如果我们关心的是指令伪码在运算操作上的正确性,则对于一些内存管理与 IO 异常处理暂不建模也可以定义完整的指令语义规则;(2)KFramework 提供及时验证测试的能力,可以根据现有语法语义及时生成解释器测试,以及通过 Kprove 功能调用 SMT 验证语义规则满足规约.而Sail 的核心在于根据官方提供的官方架构描述 ASL,直接生成可执行仿真程序,或者生成可以用于验证的Isabelle/HOL 等模型,但对于 Sail 除了静态类型检测外其缺乏在建模过程中能及时测试验证的能力,需要建立较完整的模型后才能通过转换成 C 来仿真测试,或者转换成如 Coq 模型进行验证.由于第一和第二条原因,Sail 的工作更加依赖于官方的 ASL,如果没有该 ASL 则建模需要手动进行,得到可以测试和验证工具的工作量很大,不适合对于一个指令扩展集进行验证.Armstrong 等人8在 ARMv8-A 的工作依赖于官方提供的 ASL,因此若想复用该自动化的工具链对其他架构进行指令语义的定义则需要官方提供该架构对应的 ASL,但 ARMv8.1-M 的 ASL 并未发布.另外,Reid 等人10对 ARMv8-A 和 ARMv8-M 架构官方手册进行规范并创建了 ASL,对于 ARMv8-A 架构其开源网站上有长期维持架构版本的追踪与更新,而 ARMv8-M 在其网站上没有开源,且论文中对 M 架构进行规范的版本是 2006 年的官方手册.ARMv8 的 A 架构与 M 架构中的指令即使助记符相同,但其功能却大不相同,两3854软件学报2023 年第 34 卷第 8 期个架构差异很大.因此,迄今为止,据我们所知还没有发现对 ARMv8.1-M 架构最新官方手册的指令语义进行形式化的工作.本文运用 KFramework 对 ARMv8.1-M 架构最新版本手册 ARMHelium 技术的向量化 ML 指令进行语义形式化.主要有以下 3 点贡献.(1)对 ARMv8.1-M 的最新版本架构扩展中 Helium 技术的向量化 ML 指令语义进行形式化验证.(2)在文档中自动提取向量化 ML 指令语义的伪代码,利用 KFramework 的模块化定义其形式化语义.(3)通过官方提供的测试用例与自动生成的测试用例进行实验,验证 ML 指令运算功能正确性.本文第 1 节介绍了 KFramework 以及手册中向量化 ML 指令的相关知识.第 2 节介绍了应用 KFramework实现可执行的向量化 ML 指令语义的框架.第 3 节讲述了 KFramework 定义向量化 ML 指令的语法与语义规则.第 4 节描述了单指令语义形式化的具体实现.第 5 节展示了关于可执行语义的实验.第 6 节是总结与展望.1 背景知识本节首先简单介绍 KFramework 的背景知识,然后介绍在 ARMv8.1-M 架构的官方手册中关于向量化 ML 指令语义的相关内容.1.1 K FrameworkKFramework(以下称 K 框架)是基于重写逻辑的可执行语义工具框架,它是一种用于设计和建模编程语言和软件/硬件系统的工具.K 框架的核心是一种称为 K 的编程,建模和规范语言,以及基于 matchinglogic 的验证能力.K 框架包括用于编译 K 描述的语义规则以构建解释器,模型检查器,验证器,相关文档等的工具.当给定语法与语义,K 框架可以自动生成该语言的解析器(parser),解释器(interpreter)以及演绎程序验证器(deductiveprogramverifiers)等形式化分析工具,不需要进行额外的开发.运用 K 框架的解释器可以立即测试语言的语义以显著提高语义形式化开发的效率.此外,形式化分析工具有助于给定语言语义的形式化推导.这在语义的适用性和语义本身的工程方面都有帮助.简单来说,在 K 框架中语言的语法(syntax)以传统的巴科斯范式(BNF)定义.语言的语义(semantics)被定义为规则(rule),另外由配置(configuration)来定义状态.配置是程序代码和状态规约的集合,直观说它是一个元组,这个元组的元素(称为 cells)代表着语义中的状态集合,例如内存或寄存器的状态.K 框架中,有一个命名为 k 的特殊 cell,其包含一个将要被 K 框架执行运算(computation)的列表.一个运算本质上是一个程序片段,而原始程序被扁平化为一个或多个运算的线性序列.规则描述的语义定义了配置之间的一步转换.模块化的规则定义使得 K框架定义的语义规则比其他框架下定义的形式化语义更简洁易读.K 框架已被应用于很多项目中以实现语义形式化,如 C11,12,WebAssembly13,LLVM14,Python15,Java16,17,JavaScript18,Boogie 等.C 语言的项目根据官方的 C11 标准定义了 K 框架下的语义规则,还包括 C 语言的翻译,链接和执行语义.该 C 语言形式化项目已被用于构建运行时验证工具 RV-Match19.其通过 C 语义运行测试套件来检测用户程序中未定义的行为.还有 WebAssembly,KWasm 是它的 K 框架语义,WebAssembly 是一种底层(但简单且流线型)的汇编语言,最初开发的目的是为基于浏览器的工具提供快速执行引擎.最近,它已在多个区块链智能合约平台中用作执行金融协议的基础语言.KWasm 已用于测量测试套件对WebAssembly 代码的覆盖率并验证编译为 WebAssembly 的程序.1.2 向量化机器学习指令本文验证的对象是 ARMv8.1-M 架构的官方参考手册(以下称 ARM 手册)中关于 ARMHelium 技术的向量化机器学习(machinelearning,ML)指令.其中 ARMHelium 技术是 ARMv8.1-M 架构的新型 M-ProfileVectorExtension(MVE)向量扩展,为架构带来计算能力的增强,大幅提升机器学习以及信号处理等性能.本文主要验证 ARMHelium 中关于 ML 的指令集扩展,该扩展主要包含在机器学习中常用的向量大小比较和向量内积这两方面的向量化指令.向量比较大小的指令可以用于如 ReLU 激活函数的实现,神经网络分类结果判断等.向量内积的指令则可以用于矩阵乘加,卷积运算等.向量化的指令使得同一时钟周期内可以执行更多的运算黄厚华等:基于 KFramework 的向量化机器学习指令语义形式化3855操作.本文涉及的向量化 ML 指令范围:所要验证的 ML 指令包含 21 条(区分整型和浮点数),助记符 17 个,且假设在应用模式下而非系统内核模式下进行语义形式化.21 条指令中有 4 条调用浮点寄存器,比较两个源寄存器值的大小,并保存最大或最小值到目标寄存器;4 条关于判断一个向量寄存器与通用寄存器的值的最大或最小值,并保存在此通用寄存器中;12 条是关于判断向量寄存器间的值的最大或最小值,并将结果保存到目标向量寄存器中,其中 4 条关于整型,8 条关于浮点数;还有 1 条指令是向量内积运算,即机器学习中常用到的,求两向量内对应元素的乘积的和的运算.以上除了 4 条助记符相同的指令未涉及向量寄存器其他都是向量化指令,所有统称为向量化 ML 指令(以下简称 ML 指令).这些 ML 指令用于计算神经网络分类结果,如比较大小的操作.由于我们重点关注的是 ML 指令的比较运算(包括整数,浮点数)和向量内积运算(整数)执行的语义正确性,所以文中重点描述算术运算的处理细节,如 NaN(notanumber)处理.由于涉及的指令与其他算术运算无关,因此建模中不涉及进位等标志符(向量内积运算不影响标志符).本文验证的 ML 指令中,要处理的数据类型分为整型和浮点数.这 21 条 ML 指令的寻址方式都是寄存器寻址,因此需要官方文档中寄存器寻址方式的定义.因为 ML 指令大部分是向量化寄存器处理,因此还需要与向量寄存器存取相关的定义.如图 1 所示,向量寄存器 Q 长度为 128 位,由 2 个 64 位双精度浮点寄存器组成,每个双精度浮点数寄存器由 2 个 32 位的单精度浮点数寄存器 S 组成.官方文档中描述关于向量寄存器指令时用到节拍(beat)的概念.一个指令执行分为 4 个节拍,每个节拍按 32 位(即一个 S 寄存器值)执行一次运算.因此每执行一次关于向量寄存器的 ML 指令都会运行 4 次操作.S0S31D0D15Q0Q7S1S0S2S3S4S5S6S7S28S29S30S31D15D14Q7Q1Q0D3D2D1D0图1向量寄存器 Q 与浮点寄存器 S,D在向量寄存器内,每个元素的二进制位数大小必须相等.对于整型值,按照向量内每个元素的二进制位大小,分为 8,16 和 32 位.因此向量寄存器内整型元素大小最长为 32 位,最小为 8 位.而对于浮点数,元素大小分为16 位,32 位与 64 位.当为 16 位时,首位为符号位,次 5 位为指数位,最后 10 位为尾数位;当为 32 位时,首位为符号位,次 8 位为指数位,最后 23 位为尾数位.64 位的首位是符号位,次 11 位为指数位,最后 52 位为尾数位.浮点数的处理为 IEEE754 标准.关于指令语义的具体处理及其形式化在第 3 节中详细说明.官网手册中 ML 指令描述结构由功能简述,二进制编码,语法,译码伪代码,汇编符号解析以及操作伪代码组成.其中操作伪码即为诠释 ML 指令的执行语义,因此着重于操作伪代码的分析.如图 2 所示为指令 VMAXNM的操作伪代码.通常伪代码中应用的数据类型包含二进制位向量,整型,布尔值,真实值(数学意义上的值),枚举,元组,结构和数组.如 bits(N)是长度为 N 的位向量,整型就是以十进制数表示.本文验证的 ML 指令大部分涉及向量寄存器的存取操作,经常用到位操作.在伪代码中,取 S 寄存器的位向量中第 8 到 24 位,则以“S24:8”的形式表示,即当“:”前后是整数值时表示取位向量的相应连接位数.另外当“:”前后为变量或者位向量时,作为位向量连接符,如将两个变量 D,T 的位向量连接,表示为“D:T”.这是在伪码提取时按项表达式区分的.本文目标是验证应用模式下 ML 指令执行语义正确性,在操作伪码提取时提取完整的伪代码作为形式化语义规则的基础,以确保语义的完整.如图 2 中 1,2 行所示,操作伪码先判断 ML 指令当前是否可以进入应用模式的状态,根据判断结果决定是否会继续执行剩余的运算部分.是否能够进入应用模式并正常执行指令是由一些内存映3856软件学报2023 年第 34 卷第 8 期射寄存器和特殊目的寄存器(以下统称状态寄存器)决定.例如 CPACR(协同处理访问控制寄存器)的 CP10 标志为“11”,NSACR(非安全访问控制寄存器)的 CP10 标志为“1”,且 CPPWR(协同处理功耗控制寄存器)的 SU10 标志为“0”时,代表拥有浮点数形式的访问权限.如图 2 所示,伪代码中关于函数的定义,形式为字符串加上“()”或“”,如图 2 第 2 行“ExecuteFPCheck()”和第7 行的“Qn,curBeat”.大部分函数的详细语义在手册中有对应的伪代码描述,而小部分函数则由自然语言描述其语义.图 2 第 1 行的 EncodingSpecificOperations()为当前指令的编码部分操作,编码部分影响操作部分的信息,包括图 2 中的 n,m,esize 和 absolute 都是从编码部分中获取的.其中 n 代表源向量寄存器是第 n 个向量寄存器,m 代表源向量寄存器是第 m 个向量寄存器,esize 是向量寄存器中每个元素的位宽,absolute 用来判断指令是否进行绝对值操作.第 2 行的 ExecuteFPCheck()为检测指令当前是否处于浮点数操作状态.第 4 行的 GetCurInstrBeat()确定 ML 向量化指令当前处于哪个节拍,以及获取元素掩码,元素掩码决定最终结果是否写入到目标寄存器中(应用模式下正常运行的元素掩码为“1111”).第 6 行的 Zeros(32)函数返回一个长度为 32 的由 0 组成的位向量,用来初始化名为 result 的临时变量,并最终写入目标寄存器.第 7 行的 Qn,curBeat 根据当前节拍,获取向量寄存器 Q 在当前节拍所对应的单精度浮点寄存器 S(1 个 Q 由 4 个 S 组成,如 Q0=S3:S2:S1:S0),如 Q0 的第 0 个节拍为 S0,Q0 的第 3 个节拍对应 S3.第 9 行的 for 循环根据每个 S 寄存器中元素的个数,进行两个源寄存器的元素大小比较.第 12 行的“Elemop1,e,esize”函数,获取 S 寄存器(op1)中第 e 个位宽为 esize 的元素.接着用第 17 行的FPMaxNum 函数比较浮点数大小,最后将最大值返回到 result 中.紧接着第 19 行的 for 循环,将 result 中的位向量,以字节为单位循环 4 次,写入当前节拍向量寄存器 Q 所对应的 S 寄存器中.图2VMAXNM 指令的操作伪代码 2 ML 指令语义形式化框架本文运用 K 框架实现 ML 指令语义的形式化,ML 指令语义形式化以及测试的框架如图 3 所示.语法定义语法解析语义执行结果测试流程K 框架官方测试用例和生成测试用例语义形式化图3基于 K 框架的语义形式化与测试黄厚华等:基于 KFramework 的向量化机器学习指令语义形式化3857第 1 部分(图 3 上方两个方框),定义 ML 指令的语法,然后根据官方手册 ML 指令操作语义用 K 框架定义指令的执行规则.ML 指令语义执行基本流程如图 4 所示,每一部分对应一组接口函数模块.指令执行语义的定义是通过这些模块建立的,将每个模块内接口函数功能用语义规则实现,按照指令语义执行逻辑流程构建每条 ML 指令的语义.图 4 中每一模块的形式化语义在第 3.2 节中详细说明.状态检测类型分析寄存器按位取值整型类型转换否比较大小或算术运算写入寄存器类型转换NaN 处理是否NaN?是浮点数图4ML 指令语义执行流程第 2 部分(图 3 中间区域),在 KFramework 下描述的 ML 指令语法语义可以自动生成解释器.得到可执行语义还需要配置(configuration)描述系统的执行状态.配置主要用于描述系统状态以及初始化.其中系统状态包括寄存器与内存两部分,寄存器为从寄存器名称到值的映射,内存为从地址到值的映射.值以 WV 表示,其中 W 为位宽,V 为数值.初始化过程包括系统状态的初始化与程序初始化两部分.系统状态初始化是将寄存器与内存映射表赋初值.程序初始化内容包括指定程序与指定内存加载程序起始位置.根据配置中程序初始化的内容,语法解析模块逐行扫描指定程序并将符合语法的指令加载到指定的起始位置以及后续的内存地址中.如果出现不符合语法的指令,解析程序中断并返回当前系统状态,可由加载程序的内存状态判断出哪条指令违反了语法.当程序正确加载完成后将进入语义执行模块,先将程序初始位置赋予程序计数器 PC 寄存器,根据语义的转换规则逐条执行并更新配置中的系统状态(寄存器与内存),向量化寄存器的使用涉及节拍,所以指令执行过程中会根据节拍更新状态.每执行完一条指令后,更新程序计数器 PC 指向下一个地址值.第 3 步(图 3 下方区域),测试用例包括官方提供的测试用例与自动生成的数百条测试用例.通过 K 框架自动生成的解释器运行并记录结果.本部分内容在第 5 节详细介绍.3 形式化语法与语义本节首先介绍 ML 指令语法的定义,接着介绍用 K 框架规则对 ML 指令执行语义的形式化.3.1 ML 指令语法图 5 给出了 ML 指令的语法的 BNF 形式定义.本文验证的 ML 指令是关于元素比较和乘法累积的操作.元素有不同的数据类型(DataType),如 U8 中的 U 代表着无符号数整数,8 代表着位宽度为 8 位,S8 代表 8 位有符号数整数,F16 代表 16 位的浮点数.ML 指令的操作数(Operand)皆为寄存器(Reg),分为向量寄存器(Q128),双精度浮点寄存器(D64),单精度浮点寄存器(S32)和通用寄存器(R32).在向量寄存器中,元素类型包含除 F64 外的所有数据类型,而双精度浮点数 F64 只存在 D64 中.ARM-8.1MVE 中向量寄存器有 8 个,浮点寄存器 D64 有 16 个,浮点寄存器 S32 有 32 个,通用寄存器有 16 个.其中向量寄存器 Q 由 4 个 S32 寄存器组成,如 Q0=S3:S2:S1:S0;且D64 寄存器由 2 个 S32 组成,如 D0=S1:S0.SPReg 指代特殊寄存器,用于记录处理器当前的状态.包括,FPSCR(浮点数状态与控制寄存器),CONTROL(控制寄存器,控制处于何种状态模式)等.如 ML 指令中包含浮点数据类型,在对浮点数进行处理的时候,可能会出现 NaN 异常,该状态下会修改 FPSCR 中的 IOC(invalidoperationcumulativeexception,无效操作累积异常)标志位,即最低位,并将其置 1.3858软件学报2023 年第 34 卷第 8 期图5ML 指令语法ML 指令的语法定义如图 5 中的 Inst 所示.ML 指令都是寄存器寻址方式,且指令及有三地址码与二地址码两种格式.当指令是三地址码时,目标操作数为左边第 1 个操作数,源操作数为余下两个操作数.当指令为二地址码时,目标操作数为左边第 1 个操作数,两个均为源操作数.VMAX 指令是按照数据类型,比较两个源向量寄存器中位向量的对应元素的值,即 Q0 第 1 个元素与 Q1 第 1 个元素比较返回最大值,直到所有元素对比较完毕,将最终结果写入目标向量寄存器中,如 VMAX.U8Q2,Q0,Q1,数据类型为 U8,比较 Q0 和 Q1 中元素,每 8 位为一个元素,即分别比较 Q0 和 Q1 的第 1 到第 16 个元素,将这 16 次比较中的较大值写入目标向量寄存器的相应位.VMAXA 指令是将 VMAX 指令的元素取绝对值后再进行比较.VMAXNM 指令是进行浮点数比较,它的操作数分别包含着 S32,D64,Q128 这 3 种类型的寄存器.对于同一指令(如 VMAXNM),不同操作数类型的操作有不一样的执行操作.其中操作数类型标志为 S32 时,数据类型为单精度浮点数 F32,且 S32 中仅包含一个元素,比较返回最大值;当操作数类型标志为 D64 时,数据类型为双精度浮点数 F64,D64 寄存器内仅包含一个元素;Q128 为操作数类型时,数据类型可为 F16 和 F32,向量寄存器 Q128 内包含多个元素,比较也按对应元素位的值进行.VMAXNMA 指令是二地址格式,比较源向量寄存器与目标向量寄存器的元素的绝对值,返回最大值到目标向量寄存器中.VMAXNMV 指令是二地址格式,将源向量寄存器的元素与目标通用寄存器的元素以浮点数型式比较,将向量寄存器与通用寄存器中所有元素的最大值,返回到目标通用寄存器中.VMAXNMAV 指令是 VMAXNMV的绝对值形式.VMAXV 指令与 VMAXNMV 的差别,在于比较的是整型数.VMAXAV 指令是 VMAXV 指令的绝对值形式.VMIN 指令与 VMAX 指令相似,差异是返回的是最小值.剩余的以 VMIN 为前缀的指令,皆与对应的以 VMAX 为前缀指令相似,差异是返回的是最小值.VMLAV 指令是将两个向量寄存器中各对应元素相乘,并且将各乘积相加求和,并将最终结果的低 32 位写入目标寄存器(32 位通用寄存器)中的运算.关于程序的定义 Prog,以单个指令或多个指令序列性构成.ML 指令的数据类型总共 9 种,不同指令能使用的数据类型种类有区别.且对于不同指令,操作数类型是有限制的,比如 VMAXNM 指令对不同类型操作数实现功能各不相同.3.2 ML 指令语义3.2.1状态检测与类型分析本文对处理器状态的假设是其运行在应用模式下对 ML 指令的执行语义进行验证.指令执行语义的第 1 部分是状态监测与类型分析.因此,需要将处理器中的特殊寄存器预设为满足应用模式下运行状态的值.通过判断寄存器标志,让 ML 指令正常进入应用模式并开始运行算数运算的操作部分.状态寄存器的预设,通过将状态寄存器的黄厚华等:基于 KFramework 的向量化机器学习指令语义形式化3859特殊位赋予相应的值.如控制寄存器 CONTROL,它的第 2 位(最低位开始)影响当前运行状态是否允许浮点数扩展,当为 0 时浮点数扩展不激活,为 1 时激活.当指令需要在浮点数状态下运行时,可以通过判断 CONTROL 的第2 位是否等于 1 来表示是否执行浮点数的相关操作.而当其等于 0 时,不可以执行浮点数的相关操作,但可以执行整型的相关操作.其他影响 ML 指令运行状态的状态寄存器以相同的方式检测.类型分析是分析当前执行的 ML 指令涉及的数据类型.本文所验证的 ML 指令因为大部分都涉及元素的大小比较,且分为整数和浮点数.数据类型分为 9 种类型,即语法中的 DataType.因此,当从指令表中获取当前执行的ML 指令语法后,由于指令助记符中包含了 DataType 的标志,所以可以通过判断输入的 DataType 是否等于语法中所定义的类型,且 DataType 是否为当前指令所能接受的数据类型.若都判断为真,则进入此 DataType 标志对应的操作,以此实现检测数据类型.如当前执行的 ML 指令为:VMAX.U16Q0,Q1,Q2 时,因为 U16 为正确的数据类型,且 VMAX 指令可以接受包含 U16 数据类型,那么它会进入对应 U16 的操作语义中实现 VMAX 指令的操作部分.3.2.2寄存器取值Beat in(0,1,2,3)(0,1,2,3)向量寄存器是由 4 个 32 位浮点寄存器 S32 构成(如 Q0=S3:S2:S1:S0),并且根据节拍,提取当前节拍中,向量寄存器对应的 S32 寄存器.图 6 所示的 convSubVecRegsToRegs 规则,构成根据节拍获取向量寄存器对应元素的S32 寄存器的语义,subR 代表构成向量寄存器的子寄存器.convSubVecRegsToRegs 规则根据向量寄存器以及当前的节拍值(从 0 开始),返回向量寄存器当前节拍的子寄存器(即 S32 寄存器),如 convSubVecRegsToRegs(Q0,0)S0,convSubVecRegsToRegs(Q1,2)S6.其中,以图 6 的 convSubVecRegs-ToRegs 规则为例,解释语义规则图中的规则形式所代表的含义.比如,在横线右侧的字符串代表着当前规则的名称.在横线上方的各项,代表着执行此规则所需要满足的条件,如 R:Reg 则代表需要满足 R 是 Reg 寄存器类型(图 6),代表着要满足 Beat是这个集合的其中一项.而横线下方则代表着当前语义规则的操作,当满足横线上方的条件后,调用convVecRegsToSubRegs 规则就会根据给定的向量寄存器以及第几个 Beat 得到目标子寄存器 subR.其他规则在文中表示形式与 convSubVecRegsToRegs 规则形式相似.图6寄存器取值语义规则图 6 中的第 2 和第 3 条语义规则为构成 ML 指令中寄存器取值和按位取值规则.ML 指令中常用到寄存器按位取值操作,比如 ML 指令,必须先从向量中取出元素再作比较或相乘,因此需要实现寄存器取值和按位取值操作.其中 getRegisterValue 规则表示从寄存器中取对应的位向量,只要满足寄存器 R 是通用寄存器 Reg 类型,且寄存器映射表 RSMap 中包含 R 的映射关系,当在 RSMap 中,R 指向(|)位向量 WV,那么规则最终会返回 WV.按位取值操作则由图 6 中的 extractMInt 规则实现,当要在位向量 WV 中取某一段位向量时,可通过extractMInt(WV,start,end)实现,需要满足 start(开始位)大于等于 0 并且小于 W,end(终止位)大于 0 并且小于等于 W.此处需要注意的是,WV 的最低位是在右边第 1 位,而 extractMInt 规则提取位向量时,以位向量的左边第 1位作为最低位,此处的 start 和 end 都是以 extractMInt 规则的标准来对齐位向量中的位,且 end 所对应的位不被提取,所以转换为 WV(Wstart1):(Wend).例如,对于位向量“1100”,即 46,extractMInt(46,0,2)=463:2,即提取位向量“1100”的第 2 和第 3 位,“11”,而 start(0)对应位向量左边数起第 1 位:“1”,end(2)对应位向量左边数起第 3位:“0”.3.2.3类型转换ML 指令大部分是关于获取一组数据中最大或最小值的操作,与之伴随的是比较大小.比较就涉及类型转换,而且 K 框架中的比较规则涉及整型,浮点数以及位向量,比较时需将比较的元素转换为相同的对应类型后才能比3860软件学报2023 年第 34 卷第 8 期较.按照原语义,需将位向量转换为对应的整型或浮点数后,运用比较规则进行比较.接下来说明位向量转换为浮点数和整型类型的语义实现.图 7 中,列出了位向量转换为浮点数表示的实数的语义规则.MInt2Float 规则通过调用多条规则,实现将位向量转换为浮点数的语义.先