一句话:提出基于微结构的动态无 Oracle 方法,自动合成修复以显著降低浮点程序数值误差。
浮点表示广泛用于数值软件,但其近似性带来固有数值误差,修复通常需要数值专业知识或高精度 Oracle。本文提出一种全自动、无需 Oracle 的动态修复合成方法。核心是微结构(micro-structure)概念,用于刻画浮点误差的结构模式,并利用其统计数据指导修复合成的搜索与验证。在 36 个常用数值程序上的评估表明,该方法能即时合成修复;与原程序相比,修复后程序浮点误差降低多个数量级,且运行性能更快。
The floating-point representation provides widely-used data types (such as “float” and “double”) for modern numerical software. Numerical errors are inherent due to floating-point’s approximate nature, and pose an important, well-known challenge. It is nontrivial to fix/repair numerical code to reduce numerical errors — it requires eithernumerical expertise(for manual fixing) or high-precisionoracles(for automatic repair); both are difficult requirements. To tackle this challenge, this paper introduces aprincipled dynamic approachthat isfully automatedandoracle-freefor effectively repairing floating-point errors. The key of our approach is the novel notion ofmicro-structurethat characterizes structural patterns of floating-point errors. We leverage micro-structures’ statistical information on floating-point errors to effectively guide repair synthesis and validation. Compared with existing state-of-the-art repair approaches, our work is fully automatic and has the distinctive benefit of not relying on the difficult to obtain high-precision oracles. Evaluation results on 36 commonly-used numerical programs show that our approach is highly efficient and effective: (1) it is able to synthesize repairs instantaneously, and (2) versus the original programs, the repaired programs have orders of magnitude smaller floating-point errors, while having faster runtime performance.
@article{paperbot1426,
title = {Oracle-free repair synthesis for floating-point programs},
author = {Daming Zou and Yuchen Gu and Yuanfeng Shi and MingZhe Wang and Yingfei Xiong and Zhendong Su},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563322}
}