一种基于执行路径状态比对的科学计算程序等效性判定方法  

A Method for Equivalence Checking of Scientific Programs Based on State Comparison of Execution Paths

作　　者：曲海鹏[1] 张敏媛 韩庆迪 林喜军[1] Qu Haipeng;Zhang Minyuan;Han Qingdi;Lin Xijun(College of Information Science and Engineering, Ocean University of China, Qingdao 266100, China)

机构地区：[1]中国海洋大学信息科学与工程学院,山东青岛266100

出　　处：《中国海洋大学学报（自然科学版）》2021年第11期86-93,共8页Periodical of Ocean University of China

基　　金：国家自然科学基金项目(41976184)资助。

摘　　要：科学计算程序的计算等效性判定是科学计算领域的重要问题。科学计算程序在算法改进、程序优化和版本迭代过程中经常对函数进行等价转换,转换前后的同一函数需要确保其计算过程的等效性。针对该问题,提出基于程序路径的状态匹配验证方法——SCEP,通过对程序不同版本在相同的输入空间的路径状态进行约束求解和精确比对,判定其计算的等效性。将SCEP方法与已有的判定方法在多个库函数组成的spcLib测试程序集上进行了对比实验,结果表明SCEP能判定更多的函数转换类型,不仅可用于“Fortran-to-Fortran”源码等效性检查,还能对“Fortran-to-C/C++”源码转换进行等价性判定。该方法有助于为科学计算程序的优化改进过程和向C/C++迁移过程提供完备的计算等效性保证。The computing equivalence checking of scientific programs is an important issue in the field of scientific computing.Semantics-preserving transformation on scientific programs is quite common in the process of algorithm improvement,program optimization,and version evolution.The same function before and after transformation must ensure the equivalence of the calculation process.For this problem,A state comparison of execution paths method—SCEP is proposed,which determines the equivalence of calculations through constraint solving and precise comparison of the execution path states of different program versions in the same input space.SCEP method was compared with the existing methods on the spcLib test data set composed of multiple library functions.The result shows that SCEP can identify more equivalent function transformation types,not only for“Fortran-to-Fortran”transformation,but also for the“Fortran-to-C/C++”.SCEP approach helps to provide complete calculation equivalence guarantee for the optimization and improvement process of scientific codes and the migration process from Fortran to C/C++.

关 键 词：程序等效性验证 科学计算程序 状态匹配 回归验证 语义不变的转换 

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