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

Semantics Formalization of Vectorized Machine Learning Instructions in K Framework

作　　者：黄厚华 刘嘉祥 施晓牧 HUANG Hou-Hua;LIU Jia-Xiang;SHI Xiao-Mu(College of Computer Science and Software Engineering,Shenzhen University,Shenzhen 518060,China)

机构地区：[1]深圳大学计算机与软件学院,广东深圳518060

出　　处：《软件学报》2023年第8期3853-3869,共17页Journal of Software

基　　金：深圳市科创委基础研究面上项目(JCYJ20210324094202008);国家自然科学基金(62002228);深圳市高等院校稳定支持计划(20200810045225001)。

摘　　要：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.

关 键 词：ARMv8.1-M架构 向量化指令 机器学习 K Framework 形式化语义 

分 类 号：TP18[自动化与计算机技术—控制理论与控制工程]