基于Coq的矩阵代码生成技术  

Coq-based Matrix Code Generation Technology

作　　者：麻莹莹 陈钢 MA Ying-Ying;CHEN Gang(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106

出　　处：《软件学报》2022年第6期2224-2245,共22页Journal of Software

摘　　要：矩阵程序在智能系统中扮演着越来越重要的角色.随着矩阵应用的复杂性日益增加,生成正确矩阵代码的难度也在不断变大.并行硬件能够极大地提高矩阵运算的速度,然而,使用并行硬件进行编程以实现并行运算,需要编程人员在程序中描述功能以及如何利用硬件资源来交付结果.这些程序通常是命令式语言,难以推理并且重构,以尝试不同的并行化策略.在Coq中实现了由高级矩阵算子到C代码的矩阵表达式代码生成技术,其能够将带有执行策略的函数式矩阵代码转换为高效低级命令式代码.未来,将把矩阵的形式化同矩阵代码自动生成融合在一起,对矩阵代码转换的过程进行形式化验证,以保障生成的矩阵代码的可靠性,为实现基于矩阵形式化方法的高可靠性深度学习编译器的研制打下基础.Matrix programs are taking increasing important role in the intelligent systems. As the complexity of matrix applications grows,the difficulty of producing correct matrix code does the same. Parallel hardware can greatly increase the speed of matrix operations;nevertheless, using parallel hardware for programming to achieve parallel operations requires programmers to describe functions in the program and to manage how to use hardware resources to deliver results. These programs are usually written in imperative languages that are difficult to reason about and refactor for different parallelization strategies. A matrix expression code generation technology has been implemented from high-level matrix operators to C code in Coq, which can convert functional matrix code with execution strategies into efficient low-level imperative code. In the future, the formal verification of the matrix will be integrated with the automatic generation of matrix code, and formal verification of the matrix code conversion process will be performed to ensure the reliability of the generated matrix code, laying the foundationfor the development of a high-reliability deep learning compiler based on the matrix formal method.

关 键 词：定理证明 矩阵代码生成 形式化工程数学 高阶定理证明 COQ 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]