Detecting Inaccuracies in Floating- Point Programs Yingfei Xiong, Peking University Collaboration with Daming Zou, Ran Wang, Zhendong Su, Xinrui He, Lu Zhang, Gang Huang, Hong Mei
Floating-Point Inaccuracy 0.1 + 0.1 + 0.1 + + 0.1 10000 times Code: float x = 0, a = 0.1; for(int i = 0; i < 10000; i++) { x = x + a; } printf("%.6f", x); Output: 999.902893
Floating-Point Inaccuracy 0.1 + 0.1 + 0.1 + + 0.1 10000 times Code: double x = 0, a = 0.1; for(int i = 0; i < 10000; i++) { x = x + a; } printf("%.6lf", x); Output: 1000.000000
问题背景 浮点误差会导致严重的后果 在海湾战争中, 爱国者导弹由于累积的浮点误差拦截失败, 造成了 28 人丧生
Measure Errors Absolute error: Error abs = x ideal x fp Relative error: Error rel = x ideal x fp x ideal x ideal
Precision Tuning Code: float x = 0, a = 0.1; for(int i = 0; i < 10000; i++) { x = x + a; } printf("%.6f", x); x orignal = 999.902893 Raise precision Code: double x = 0, a = 0.1; for(int i = 0; i < 10000; i++) { x = x + a; } printf("%.6lf", x); x high = 1000.000000
Measure Errors with Precision Tuning Absolute error: Error abs = x ideal x fp Relative error: Error rel = x ideal x fp x ideal x high x original x high x original x high
Precision-Unspecific Semantics Floating-point variables Real numbers Floating-point operations Real number operations Technique: precision tuning On-the-fly detection of instability problems in floating-point program execution A dynamic program analysis to find floating-point accuracy problems Efficient search for inputs causing high floating-point errors Trustworthy numerical computation in scala Automatically improving accuracy for floating point expressions A genetic algorithm for detecting significant floating-point inaccuracies
Assumption: High precision usually produce more accurate output Is it true?
Example A code piece simplified from exp function in the GNU C library: 1: double x = 3.7; 2: double n = 6755399441055744.0; 3: double y = (x + n) n; Answer from computer: y = 4 Raise precision to long double: Answer from computer: y = 3.7002
Example A code piece simplified from exp function in the GNU C library: 1: double x = 3.7; 2: double n = 6755399441055744.0; 3: double y = (x + n) n; The goal of this code is to round x to the nearest integer. n is a magic number specially designed for double precision. (n = 1.5 2 52 )
Example A code piece simplified from exp function in the GNU C library: 1: double x = 3.7; 2: double n = 6755399441055744.0; 3: double y = (x + n) n; A precision-specific operation
Precision-Specific Semantics double x = 3.7; double n = 6755399441055744.0; double y = (x + n) n; Interpret as rounding x to the nearest integer Problems Any other form of precision-specific operations? How to understand its intention? How to compose n for different precisions?
Precision-Specific Semantics double x = 3.7; double n = 6755399441055744.0; double y = (x + n) n; Interpret as rounding x to the nearest integer Problems Any other form of precision-specific operations? How to understand its intention? How to compose n for different precisions? Solution A heuristic to detect precision-specific operations. A fixing approach to enable precision tuning under the presence of precision-specific operations.
Heuristic An instruction is possibly precision-specific if it results in large error inflation in most executions. Intuition Two sources of errors in computations Accumulated Errors: usually small Cancellation: normally occurs in a few executions
Fixing High precision normal operation normal operation normal operation normal operation normal operation Precision-specific operation normal operation normal operation normal operation normal operation High precision Original precision High precision
Fixing Example... x = 3.7; n = 6755399441055744.0; temp = x + n; y = temp n;... Long Double Double Long Double
Automatic Detection Overview Sampling Fixing Execution Detection
Evaluation
Subjects 48 double version math functions of the GNU C library (GLIBC).
Research Questions Distribution Precision and recall Fixing Existing studies
RQ1: Distribution of Precision- Specific Operations FUNCTIONS Others 23 Precisionspecific functions 25
RQ1: Distribution of Precision- Specific Operations FILES Precisionspecific files 10 Others 33
RQ1: Distribution of Precision- Specific Operations In total, 48 precision-specific operations are detected. PRECISION SPECIFIC OPERATIONS Rounding 44 Multiplication 2 Bit operation 2
RQ2: Precision and Recall Precision: 77.5% Recall: 97.92% Detected operations False positives Multiplication Rounding Bit operation
RQ3: Fixing How effective is our fixing approach? We evaluate the average relative error to standard value. Original precision Average Relative error Program High precision Average Relative error Standard value High precision with fixing Average Relative error
RQ3: Automatic Fixing Automatic fixing: fix detected instruction. The results from automatic fix are more accurate than the original precision and the high precision in the vast majority of cases. Precision Recall, error, error Automatic Fixing (E = 10 7 ) > O < O > H < H 20 1 12 2 O: original precision. H: high precision. >: better than. <: worse than
RQ4: Review Existing Study subjects subjects subjects return call Precision-specific Fixed precisionspecific functions functions in GLIBCin GLIBC Function Reported error Actual error exprel_2 2.85e+00 5.25e-12 synchrotron_1 5.35e-03 2.24e-13 synchrotron_2 3.67e-03 5.97e-15 equake (sin, cos) Around 5.00e-01 --
小结与问题 修复精度特定运算之后, 我们可以得到一次计算的误差 如何知道整个程序上是否存在较大误差? 通常我们无法遍历整个程序的输入空间
基于搜索的误差查找 从输入空间选择一个输入 采用动态分析获得对应误差 分析获得下一个输入 关键问题
实证研究 从 GSL 中选取 4 个函数, 仅变化浮点数的尾数位或指数位, 观察它们和内部误差之间的关系 IEEE 754 Floating-Point Representation Single Precision Double Precision Sign Exponent Significand 1 8 23 1 11 52
Log(Relative Error) Log(Relative Error) Log(relative Error) Log(Relative Error) 指数位与误差的关系 -14-15 -16-17 -18 Relative Error by Exponent - legendre_q1 0 206 412 618 824 10301236144216481854 Exponent of Input -9-11 -14-16 -18 Relative Error by Exponent - erf 0 206 412 618 824 10301236144216481854 Exponent of Input Relative Error by Exponent - Ci Relative Error by Exponent - bessel_k0 0-5 -9-14 -18 0 206 412 618 824 10301236144216481854 Exponent of Input -4-8 -11-15 -18 1 104 207 310 413 516 619 722 825 928 Exponent of Input
指数部分对误差的大小有重大影响
能触发大误差的指数往往只存在于一个很小的范围
在大误差的附近常常有高于平均误差的小波动
大误差常常出现在浮点数中段位置
尾数位和浮点数之间的关系
尾数位对浮点误差有显著影响
大量尾数都能触发大误差, 并且在数轴上呈均匀分布
局部敏感型遗传算法 根据以上特征, 本研究设计了局部敏感型遗传算法 对于指数位 初始化时更多生成中位数附近 数值变异 对于尾数位 随机生成 随机变异
实验评估 有效性检验 : 在 6 个经典浮点数程序上测试 结果证明 LSGA 可以区分 stable 和 unstable 程序, 初步证明了算法的可行性与有效性 检验结果 Newton Inv Root Poly Exp Cos Stable? stable stable unstable unstable unstable unstable Max. Error Detected 2.8E-16 3.2E-16 8.1E+76 7.1E-11 1.0E+00 9.2E-01
实验评估 从 GSL 中选取 154 个函数 与随机算法, 标准遗传算法对比
实验评估 检测到最大误差 Total RAND STD LSGA Tied 154 11 (7%) 24 (16%) 105 (68%) 14 (9%) Sign Test 结果 n+ n- N p LSGA vs. RAND 127 12 139 < 4.14e-22 LSGA vs. STD 110 30 140 < 2.46e-11 STD vs. RAND 93 40 133 < 6.52e-06
实验评估 找到潜在内部精度问题的能力 如何定义潜在问题? 相对误差大于 0.1% 绝对误差大于预估绝对误差 10 倍以上
实验评估
小结 浮点数误差是软件开发的经典问题 本研究成果可以自动查找软件代码中的浮点误差问题 本研究成果避免了已有方法可能产生的错误结论 实验结果显示, 我们设计的算法可以在实践中被广泛使用的库函数中找到潜在的精度问题 相关论文 Daming Zou, Ran Wang, Yingfei Xiong, Lu Zhang, Zhendong Su, Hong Mei. A Genetic Algorithm for Detecting Significant Floating-Point Inaccuracies. ICSE'15: 37th International Conference on Software Engineering, pages 529-539, May 2015 Ran Wang, Daming Zou, Xinrui He, Yingfei Xiong, Lu Zhang, Gang Huang. Detecting and Fixing Precision-Specific Operations for Measuring Floating-Point Errors. FSE'16: 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering, November 2016.