skip to main content
10.1145/1480945.1480960acmconferencesArticle/Chapter ViewAbstractPublication PagespepmConference Proceedingsconference-collections
research-article

Program transformation for numerical precision

Published: 19 January 2009 Publication History

Abstract

This article introduces a new program transformation in order to enhance the numerical accuracy of floating-point computations. We consider that a program would return an exact result if the computations were carried out using real numbers. In practice, roundoff errors due to the finite representation of values arise during the execution. These errors are closely related to the way formulas are evaluated. Indeed, mathematically equivalent formulas, obtained using laws like associativity, distributivity, etc., may lead to very different numerical results in the computer arithmetic. We propose a semantics-based transformation in order to optimize the numerical accuracy of programs. This transformation is expressed in the abstract interpretation framework and it aims at rewriting pieces of numerical codes in order to obtain results closer to what the computer would output if it used the exact arithmetic.

References

[1]
ANSI/IEEE. IEEE Standard for Binary Floating-point Arithmetic, std 754-1985 edition, 1985.
[2]
David F. Bacon, Graham Susan L., and Oliver J. Sharp. Compiler transformations for high-performance computing. ACM Comput. Surv., 26(4):345--420, 1994.
[3]
Christian Bischof, Paul D. Hovland, and Boyana Norris. Implementation of automatic differentiation tools. In Partial Evaluation and Semantics-Based Program Transformations, PEPM'02. ACM Press, 2002.
[4]
M. Ceberio and V. Kreinovich. Greedy algorithms for optimizing multivariate horner schemes. ACM-SIGSAM Bulletin, 38(1):8--15, 2004.
[5]
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. In Principles of Programming Languages 4, pages 238--252. ACM Press, 1977.
[6]
P. Cousot and R. Cousot. Systematic design of program transformation frameworks by abstract interpretation. In Conference Record of the Twentyninth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 178--190, Portland, Oregon, 2002. ACM Press, New York, NY.
[7]
M. Dalla Preda and R. Giacobazzi. Control code obfuscation by abstract interpretation. In International Conference on Software Engineering and Formal Methods, SEFM'05, pages 301--310. IEEE Computer Society Press, 2005.
[8]
D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Computing Surveys, 23(1):5--48, 1991.
[9]
E. Goubault. Static analyses of the precision of floating-point operations. In Static Analysis Symposium, SAS'01, number 2126 in Lecture Notes in Computer Science, pages 234--259. Springer-Verlag, 2001.
[10]
E. Goubault, M. Martel, and S. Putot. Asserting the precision of floating-point computations: a simple abstract interpreter. In $11^th$ European Symposium on Programming, ESOP'02, number 2305 in Lecture Notes in Computer Science, pages 209--212, 2002.
[11]
E. Goubault, M. Martel, and S. Putot. Some future challenges in the validation of control systems. In Proceedings of the European Congress on Embedded Real Time Software (ERTS'06), 2006.
[12]
N. Jones, C. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice Hall International, Int. Series in Computer Science, 1993.
[13]
P. Langlois and N. Louvet. How to ensure a faithful polynomial evaluation with the compensated Horner algorithm? In P. Kornerup and J.-M. Muller, editors, 18th IEEE International Symposium on Computer Arithmetic, pages 141--149. IEEE Computer Society, June 2007.
[14]
Information Management and Technology Division. Patriot missile defense : Software problem led to system failure in Dhahran, saudi arabia. Technical Report B-247-094, United State General Accounting Office, 1992.
[15]
M. Martel. Propagation of roundoff errors in finite precision computations: a semantics approach. In $11^th$ European Symposium on Programming, ESOP'02, number 2305 in Lecture Notes in Computer Science, pages 194--208. Springer-Verlag, 2002.
[16]
M. Martel. An overview of semantics for the validation of numerical programs. In Verification, Model Checking and Abstract Interpretation, VMCAI'05, number 3385 in Lecture Notes in Computer Science, pages 59--77. Springer-Verlag, 2005.
[17]
M. Martel. Semantics of roundoff error propagation in finite precision calculations. Journal of Higher Order and Symbolic Computation, 19:7--30, 2006.
[18]
M. Martel. Semantics-based transformation of arithmetic expressions. In Static Analysis Symposium, SAS'07, number 4634 in Lecture Notes in Computer Science. Springer-Verlag, 2007.
[19]
M. Martel. Enhancing the implementation of mathematical formulas for fixed-point and floating-point arithmetics. In First International Workshop on Numerical Abstractions for Software Verification, NSV'08, 2008.
[20]
D. Monniaux. The pitfalls of verifying floating-point computations. TOPLAS, 30(3), May 2008.
[21]
R. Rocher, D. Menard, N. Herve, and Sentieys. Fixed-point configurable hardware components. EURASIP Journal on Embedded Systems (JES), 2006, 2006.
[22]
R. Rocher, D. Menard, O. Sentieys, and P. Scalart. Analytical accuracy evaluation of fixed-point systems. In EUSIPCO'07Poznan, Pologne, 2007.
[23]
P. H. Sterbenz. Floating-point Computation. Prentice Hall International, 1974.

Cited By

View all
  • (2022)Detecting High Floating-Point Errors via Ranking Analysis2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00052(397-406)Online publication date: Dec-2022
  • (2020)Debugging and detecting numerical errors in computation with positsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386004(731-746)Online publication date: 11-Jun-2020
  • (2020)Towards Numerical AssistantsSoftware Verification10.1007/978-3-030-63618-0_13(213-220)Online publication date: 6-Dec-2020
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
PEPM '09: Proceedings of the 2009 ACM SIGPLAN workshop on Partial evaluation and program manipulation
January 2009
208 pages
ISBN:9781605583273
DOI:10.1145/1480945
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 19 January 2009

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. abstract interpretation
  2. compiler optimizations
  3. floating-point numbers
  4. numerical precision
  5. program transformation

Qualifiers

  • Research-article

Conference

PEPM '09
Sponsor:
PEPM '09: Partial Evaluation and Program Manipulation
January 19 - 20, 2009
GA, Savannah, USA

Acceptance Rates

Overall Acceptance Rate 66 of 120 submissions, 55%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)6
  • Downloads (Last 6 weeks)0
Reflects downloads up to 18 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Detecting High Floating-Point Errors via Ranking Analysis2022 29th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC57359.2022.00052(397-406)Online publication date: Dec-2022
  • (2020)Debugging and detecting numerical errors in computation with positsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3386004(731-746)Online publication date: 11-Jun-2020
  • (2020)Towards Numerical AssistantsSoftware Verification10.1007/978-3-030-63618-0_13(213-220)Online publication date: 6-Dec-2020
  • (2019)Global optimization of numerical programs via prioritized stochastic algebraic transformationsProceedings of the 41st International Conference on Software Engineering10.1109/ICSE.2019.00116(1131-1141)Online publication date: 25-May-2019
  • (2018)Fine-grained floating-point precision analysisInternational Journal of High Performance Computing Applications10.1177/109434201665246232:2(231-245)Online publication date: 1-Mar-2018
  • (2018)Finding root causes of floating point errorACM SIGPLAN Notices10.1145/3296979.319241153:4(256-269)Online publication date: 11-Jun-2018
  • (2018)Rigorous Estimation of Floating-Point Round-Off Errors with Symbolic Taylor ExpansionsACM Transactions on Programming Languages and Systems10.1145/323073341:1(1-39)Online publication date: 11-Dec-2018
  • (2018)Finding root causes of floating point errorProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192411(256-269)Online publication date: 11-Jun-2018
  • (2017)Rigorous floating-point mixed-precision tuningACM SIGPLAN Notices10.1145/3093333.300984652:1(300-315)Online publication date: 1-Jan-2017
  • (2017)Rigorous floating-point mixed-precision tuningProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009846(300-315)Online publication date: 1-Jan-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media