汤恩义团队在软件数值误差自动检测与优化研究中取得突破性进展

发布日期:2020-04-26 浏览次数:



       由数值误差问题而引发的软件错误是高可信软件关注的重要缺陷之一。随着软件规模的增加,依靠人工来排查与修复软件的数值错误已经难以满足实际需求,在这一背景下,汤恩义老师及其团队研究了软件数值错误的自动检测、诊断以及优化技术,取得了突破性进展。



图1 数值稳定性错误的来源、检测与诊断



       数值误差问题近年来引起了软件工程领域的重视,相关工作中已经有一些数值稳定性错误的自动检测方法被陆续提出,然而,在汤老师及其团队的工作发表之前,业界对软件中数值稳定性错误的来源及自动诊断方法的认识仍然较为模糊。按照软件开发过程,汤老师将软件中数值稳定性错误的来源归为两类:1) 来源于软件需求,由问题背景引起的数值稳定性错误。该类错误在软件需求不变,数值类型字长不变的情况下不可修复。2) 来源于软件的设计与实现。该类错误由软件本身的实践而引发,由于理论上会存在更稳定的数值算法,该类错误可以通过改进软件的实现来直接修复。

       研究团队设计并实现了一组随机方法与高精度计算相结合的检测诊断工具来自动分析与诊断软件中的数值稳定性错误。它首先通过程序变换技术将待测软件中的数值模块自动转为高精度数值计算;并进一步同时在不同的进度级别上对程序进行扰动;最终通过自动获得数值计算的条件数来度量低精度扰动与高精度扰动的波动状况,并进一步由比对普通精度程序与高精度程序的执行路径来定位发生稳定性问题的实现模块,从而为软件的设计开发人员提供准确的检测诊断信息与有效的修复提示。此成果论文发表在TSE 2017上。



图2 数值软件全局优化示意图



       在此基础上,汤恩义老师及其团队进一步研究了数值软件的全局自动优化。即为用户编写的数值程序自动找到一种高效、高精度的表达方式,使其在计算机的运行过程中既能保障运行速度,又能够在精度上得到提升。如图2所示,该方法给出了一套考虑了优化程序全局信息的数值优化框架,这在国际上尚属首次。该框架提出了一套用于数值程序优化的中间语言表示,并结合了符号执行追踪、自动化的随机代数变换、静态程序分析、以及启发式的稳定性分析等一系列技术来设计与实施。此成果论文发表在ICSE 2019上。