基于K Framework的向量化机器学习指令语义形式化
作者:
作者单位:

作者简介:

黄厚华(1995-),男,硕士生,CCF学生会员,主要研究邻域为形式化方法程序验证;刘嘉祥(1987-),男,博士,助理教授,CCF专业会员,主要研究领域为形式化方法,程序验证,神经网络验证;施晓牧(1987-),女,博士,CCF专业会员,主要研究领域为形式化方法,定理证明技术及其在安全关键系统的应用

通讯作者:

施晓牧,E-mail:xshi0811@gmail.com

中图分类号:

TP18

基金项目:

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


Semantics Formalization of Vectorized Machine Learning Instructions in K Framework
Author:
Affiliation:

Fund Project:

  • 摘要
  • |
  • 图/表
  • |
  • 访问统计
  • |
  • 参考文献
  • |
  • 相似文献
  • |
  • 引证文献
  • |
  • 资源附件
  • |
  • 文章评论
    摘要:

    ARM针对ARMv8.1-M微处理器架构推出基于M-Profile向量化扩展方案的技术, 并命名为ARM Helium, 声明能为ARM Cortex-M处理器提升达15倍的机器学习性能. 随着物联网的高速发展, 微处理器指令执行正确性尤为重要. 指令集的官方手册作为芯片模拟程序, 片上应用程序开发的依据, 是程序正确性基本保障. 主要介绍利用可执行语义框架K Framework对ARMv8.1-M官方参考手册中向量化机器学习指令的语义正确性研究. 基于ARMv8.1-M的官方参考手册自动提取指令集中描述向量化机器学习指令执行过程的伪代码, 并将其转换为形式化语义转换规则. 通过K Framework提供的可执行框架利用测试用例, 验证机器学习指令算数运算执行的正确性.

    Abstract:

    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.

    参考文献
    相似文献
    引证文献
引用本文

黄厚华,刘嘉祥,施晓牧.基于K Framework的向量化机器学习指令语义形式化.软件学报,2023,34(8):3853-3869

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-05
  • 最后修改日期:2021-10-14
  • 录用日期:
  • 在线发布日期: 2022-01-28
  • 出版日期:
您是第位访问者
版权所有:中国科学院软件研究所 京ICP备05046678号-3
地址:北京市海淀区中关村南四街4号,邮政编码:100190
电话:010-62562563 传真:010-62562533 Email:jos@iscas.ac.cn
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号