FPCC: Detecting Floating-Point Errors via Chain Conditions
Article No.: 324, Pages 1504 - 1531
Abstract
Floating-point arithmetic is notorious for its rounding errors, which can propagate and accumulate, leading to unacceptable results. Detecting inputs that can trigger significant floating-point errors is crucial for enhancing the reliability of numerical programs. Existing methods for generating error-triggering inputs often rely on costly shadow executions that involve high-precision computations or suffer from false positives. This paper introduces chain conditions to capture the propagation and accumulation of floating-point errors, using them to guide the search for error-triggering inputs. We have implemented a tool named FPCC and evaluated it on 88 functions from the GNU Scientific Library, as well as 21 functions with multiple inputs from previous research. The experimental results demonstrate the effectiveness and efficiency of our approach: (1) FPCC achieves 100% accuracy in detecting significant errors for the reported rank-1 inputs, while 72.69% rank-1 inputs from the state-of-the-art tool ATOMU can trigger significant errors. Overall, 99.64% (1049/1053) of the inputs reported by FPCC can trigger significant errors, whereas only 19.45% (141/723) of the inputs reported by ATOMU can trigger significant errors; (2) FPCC exhibits a 2.17x speedup over ATOMU in detecting significant errors; (3) FPCC also excels in supporting functions with multiple inputs, outperforming the state-of-the-art technique. To facilitate further research in the community, we have made FPCC available on GitHub at https://github.com/DataReportRe/FPCC.
References
[1]
Tao Bao and Xiangyu Zhang. 2013. On-the-fly detection of instability problems in floating-point program execution. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA ’13). Association for Computing Machinery, New York, NY, USA. 817–832. isbn:9781450323741 https://doi.org/10.1145/2509136.2509526
[2]
Florian Benz, Andreas Hildebrandt, and Sebastian Hack. 2012. A dynamic program analysis to find floating-point accuracy problems. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’12). Association for Computing Machinery, New York, NY, USA. 453–462. isbn:9781450312059 https://doi.org/10.1145/2254064.2254118
[3]
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2003. A static analyzer for large safety-critical software. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI ’03). Association for Computing Machinery, New York, NY, USA. 196–207. isbn:1581136625 https://doi.org/10.1145/781131.781153
[4]
Jing Chen, Jianbin Fang, Weifeng Liu, and Canqun Yang. 2021. BALS: Blocked Alternating Least Squares for Parallel Sparse Matrix Factorization on GPUs. IEEE Trans. Parallel Distributed Syst., 32, 9 (2021), 2291–2302. https://doi.org/10.1109/TPDS.2021.3064942
[5]
Zhaoyun Chen, Wei Quan, Mei Wen, Jianbin Fang, Jie Yu, Chunyuan Zhang, and Lei Luo. 2020. Deep Learning Research and Development Platform: Characterizing and Scheduling with QoS Guarantees on GPU Clusters. IEEE Trans. Parallel Distributed Syst., 31, 1 (2020), 34–50. https://doi.org/10.1109/TPDS.2019.2931558
[6]
Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, and Alexey Solovyev. 2014. Efficient search for inputs causing high floating-point errors. In Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP ’14). Association for Computing Machinery, New York, NY, USA. 43–52. isbn:9781450326568 https://doi.org/10.1145/2555243.2555265
[7]
Sangeeta Chowdhary, Jay P. Lim, and Santosh Nagarakatte. 2020. Debugging and detecting numerical errors in computation with posits. In Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, Alastair F. Donaldson and Emina Torlak (Eds.). ACM, 731–746. https://doi.org/10.1145/3385412.3386004
[8]
Sangeeta Chowdhary and Santosh Nagarakatte. 2021. Parallel shadow execution to accelerate the debugging of numerical errors. In ESEC/FSE ’21: 29th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Athens, Greece, August 23-28, 2021, Diomidis Spinellis, Georgios Gousios, Marsha Chechik, and Massimiliano Di Penta (Eds.). ACM, 615–626. https://doi.org/10.1145/3468264.3468585
[9]
Sangeeta Chowdhary and Santosh Nagarakatte. 2022. Fast shadow execution for debugging numerical errors using error free transformations. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), 1845–1872. https://doi.org/10.1145/3563353
[10]
George A. Constantinides, Fredrik Dahlqvist, Zvonimir Rakamaric, and Rocco Salvia. 2021. Rigorous Roundoff Error Analysis of Probabilistic Floating-Point Computations. In Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, Alexandra Silva and K. Rustan M. Leino (Eds.) (Lecture Notes in Computer Science, Vol. 12760). Springer, 626–650. https://doi.org/10.1007/978-3-030-81688-9_29
[11]
Eva Darulova and Viktor Kuncak. 2014. Sound compilation of reals. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 235–248. isbn:9781450325448 https://doi.org/10.1145/2535838.2535874
[12]
Arnab Das, Ian Briggs, Ganesh Gopalakrishnan, Sriram Krishnamoorthy, and Pavel Panchekha. 2020. Scalable yet rigorous floating-point error analysis. In Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2020, Virtual Event / Atlanta, Georgia, USA, November 9-19, 2020, Christine Cuicchi, Irene Qualters, and William T. Kramer (Eds.). IEEE/ACM, 51. https://doi.org/10.1109/SC41405.2020.00055
[13]
Marc Daumas and Guillaume Melquiond. 2010. Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw., 37, 1 (2010), Article 2, jan, 20 pages. issn:0098-3500 https://doi.org/10.1145/1644001.1644003
[14]
Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. 2011. Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. IEEE Trans. Comput., 60, 2 (2011), 242–253. https://doi.org/10.1109/TC.2010.128
[15]
Laurent Fousse, Guillaume Hanrot, Vincent Lefèvre, Patrick Pélissier, and Paul Zimmermann. 2007. MPFR: A Multiple-precision Binary Floating-point Library with Correct Rounding. ACM Trans. Math. Softw., 33, 2 (2007), Article 13, June, issn:0098-3500 https://doi.org/10.1145/1236463.1236468
[16]
François Févotte and Bruno Lathuilière. 2016. VERROU: a CESTAC evaluation without recompilation. In International Symposium on Scientific Computing, Computer Arithmetics and Verified Numerics (SCAN). Uppsala, Sweden.
[17]
J. M. Gablonsky and C. T. Kelley. 2001. A Locally-Biased Form of the DIRECT Algorithm. J. of Global Optimization, 21, 1 (2001), sep, 27–37. issn:0925-5001 https://doi.org/10.1023/A:1017930332101
[18]
Hui Guo, Ignacio Laguna, and Cindy Rubio-González. 2020. PLINER: Isolating Lines of Floating-Point Code for Compiler-Induced Variability. In SC20: International Conference for High Performance Computing, Networking, Storage and Analysis. 1–14. https://doi.org/10.1109/SC41405.2020.00053
[19]
Hui Guo and Cindy Rubio-González. 2018. Exploiting community structure for floating-point precision tuning. In Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2018). Association for Computing Machinery, New York, NY, USA. 333–343. isbn:9781450356992 https://doi.org/10.1145/3213846.3213862
[20]
Hui Guo and Cindy Rubio-González. 2020. Efficient generation of error-inducing floating-point inputs via symbolic execution. In ICSE ’20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June - 19 July, 2020. ACM, 1261–1272.
[21]
Hui Guo and Cindy Rubio-González. 2020. Efficient generation of error-inducing floating-point inputs via symbolic execution. In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering (ICSE ’20). Association for Computing Machinery, New York, NY, USA. 1261–1272. isbn:9781450371216 https://doi.org/10.1145/3377811.3380359
[22]
Leopold Haller, Alberto Griggio, Martin Brain, and Daniel Kroening. 2012. Deciding floating-point logic with systematic abstraction. In Formal Methods in Computer-Aided Design, FMCAD 2012, Cambridge, UK, October 22-25, 2012. IEEE, 131–140.
[23]
Nicholas J. Higham. 2002. Accuracy and Stability of Numerical Algorithms (second ed.). Society for Industrial and Applied Mathematics. https://doi.org/10.1137/1.9780898718027
[24]
IEEE-754. 2008. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2008, 1–70. https://doi.org/10.1109/IEEESTD.2008.4610935
[25]
D. R. Jones, C. D. Perttunen, and B. E. Stuckman. 1993. Lipschitzian Optimization without the Lipschitz Constant. J. Optim. Theory Appl., 79, 1 (1993), oct, 157–181. issn:0022-3239
[26]
Wonyeol Lee, Rahul Sharma, and Alex Aiken. 2016. Verifying bit-manipulations of floating-point. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’16). Association for Computing Machinery, New York, NY, USA. 70–84. isbn:9781450342612 https://doi.org/10.1145/2908080.2908107
[27]
Wonyeol Lee, Rahul Sharma, and Alex Aiken. 2017. On automatically proving the correctness of math.h implementations. Proc. ACM Program. Lang., 2, POPL (2017), Article 47, dec, 32 pages. https://doi.org/10.1145/3158135
[28]
Harshitha Menon, Michael O. Lam, Daniel Osei-Kuffuor, Markus Schordan, Scott Lloyd, Kathryn Mohror, and Jeffrey Hittinger. 2018. ADAPT: algorithmic differentiation applied to floating-point precision tuning. In Proceedings of the International Conference for High Performance Computing, Networking, Storage, and Analysis, SC 2018, Dallas, TX, USA, November 11-16, 2018. IEEE / ACM, 48:1–48:13.
[29]
Jorge J. Moré and David J. Thuente. 1994. Line Search Algorithms with Guaranteed Sufficient Decrease. ACM Trans. Math. Softw., 20, 3 (1994), sep, 286–307. issn:0098-3500 https://doi.org/10.1145/192115.192132
[30]
Jean-Michel Muller, Nicolas Brisebarre, Florent de Dinechin, Claude-Pierre Jeannerod, Vincent Lefèvre, Guillaume Melquiond, Nathalie Revol, Damien Stehlé, and Serge Torres. 2009. Handbook of Floating-Point Arithmetic (1st ed.). Birkhäuser Basel. isbn:081764704X
[31]
Pavel Panchekha, Alex Sanchez-Stern, James R. Wilcox, and Zachary Tatlock. 2015. Automatically improving accuracy for floating point expressions. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 1–11. isbn:9781450334686 https://doi.org/10.1145/2737924.2737959
[32]
Kevin Quinn. 1983. Ever had problems rounding off figures. This stock exchange has. The Wall Street Journal.
[33]
Alex Sanchez-Stern, Pavel Panchekha, Sorin Lerner, and Zachary Tatlock. 2018. Finding root causes of floating point error. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018. ACM, 256–269.
[34]
Geoffrey Sawaya, Michael Bentley, Ian Briggs, Ganesh Gopalakrishnan, and Dong H. Ahn. 2017. FLiT: Cross-platform floating-point result-consistency tester and workload. In 2017 IEEE International Symposium on Workload Characterization, IISWC 2017, Seattle, WA, USA, October 1-3, 2017. IEEE Computer Society, 229–238.
[35]
Robert Skeel. 1992. Roundoff error and the Patriot missile. In SIAM News (1992).
[36]
Alexey Solovyev, Marek S. Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamarić, and Ganesh Gopalakrishnan. 2018. Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor Expansions. ACM Trans. Program. Lang. Syst., 41, 1 (2018), Article 2, dec, 39 pages. issn:0164-0925 https://doi.org/10.1145/3230733
[37]
David E. Stewart and Zbigniew Leyk. 1994. Meschach Library. https://www.netlib.org/c/meschach/
[38]
Laura Titolo, Marco A. Feliú, Mariano M. Moscato, and César A. Muñoz. 2018. An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings, Isil Dillig and Jens Palsberg (Eds.) (Lecture Notes in Computer Science, Vol. 10747). Springer, 516–537. https://doi.org/10.1007/978-3-319-73721-8_24
[39]
Ran Wang, Daming Zou, Xinrui He, Yingfei Xiong, Lu Zhang, and Gang Huang. 2016. Detecting and fixing precision-specific operations for measuring floating-point errors. In Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE 2016). Association for Computing Machinery, New York, NY, USA. 619–630. isbn:9781450342186 https://doi.org/10.1145/2950290.2950355
[40]
Wikipedia. 2024. Ariane 5 flight 501. http://en.wikipedia.org/wiki/Ariane_5_Flight_501
[41]
Frank Wilcoxon. 1992. Individual Comparisons by Ranking Methods. Springer New York, New York, NY. 196–202. isbn:978-1-4612-4380-9 https://doi.org/10.1007/978-1-4612-4380-9_16
[42]
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji. 2017. Efficient Global Search for Inputs Triggering High Floating-Point Inaccuracies. In 2017 24th Asia-Pacific Software Engineering Conference (APSEC). 11–20. https://doi.org/10.1109/APSEC.2017.7
[43]
Xin Yi, Liqian Chen, Xiaoguang Mao, and Tao Ji. 2019. Efficient automated repair of high floating-point errors in numerical libraries. Proc. ACM Program. Lang., 3, POPL (2019), Article 56, jan, 29 pages. https://doi.org/10.1145/3290369
[44]
Xin Yi, Hengbiao Yu, Liqian Chen, Xiaoguang Mao, and Ji Wang. 2024. FPCC: Detecting Floating-Point Errors via Chain Conditions (Paper Artifact). https://doi.org/10.5281/zenodo.13618683
[45]
Daming Zou, Yuchen Gu, Yuanfeng Shi, MingZhe Wang, Yingfei Xiong, and Zhendong Su. 2022. Oracle-free repair synthesis for floating-point programs. Proc. ACM Program. Lang., 6, OOPSLA2 (2022), Article 159, oct, 29 pages. https://doi.org/10.1145/3563322
[46]
Daming Zou, Ran Wang, Yingfei Xiong, Lu Zhang, Zhendong Su, and Hong Mei. 2015. A genetic algorithm for detecting significant floating-point inaccuracies. In Proceedings of the 37th International Conference on Software Engineering - Volume 1 (ICSE ’15). IEEE Press, 529–539. isbn:9781479919345
[47]
Daming Zou, Muhan Zeng, Yingfei Xiong, Zhoulai Fu, Lu Zhang, and Zhendong Su. 2019. Detecting floating-point errors via atomic conditions. Proc. ACM Program. Lang., 4, POPL (2019), Article 60, dec, 27 pages. https://doi.org/10.1145/3371128
Index Terms
- FPCC: Detecting Floating-Point Errors via Chain Conditions
Recommendations
Detecting floating-point errors via atomic conditions
This paper tackles the important, difficult problem of detecting program inputs that trigger large floating-point errors in numerical code. It introduces a novel, principled dynamic analysis that leverages the mathematically rigorously analyzed condition ...
Roundoff errors in block-floating-point systems
Block-floating-point representation is a special case of floating-point representation, where several numbers have a joint exponent term. In this paper, roundoff errors in signal processing systems utilizing block-floating-point representation are ...
Necessary and Sufficient Conditions on Block Codes Correcting/Detecting Errors of Various Types
Necessary and sufficient conditions are given for block codes to be capable of correcting up to t/sub 1/ symmetric errors, up to t/sub 2/ unidirectional errors, and up to t/sub 3/ asymmetric errors, as well as detecting from t/sub 1/+1 up to d/sub 1/ ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2024
2691 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution International 4.0 License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 08 October 2024
Published in PACMPL Volume 8, Issue OOPSLA2
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Funding Sources
- National Key R&D Program of China
- National Natural Science Foundation of China
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 204Total Downloads
- Downloads (Last 12 months)204
- Downloads (Last 6 weeks)84
Reflects downloads up to 28 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in