Abstract
Numerical programs performing floating-point computations are very sensitive to the way formulas are written. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their accuracy and, in this article, we go one step further by automatically transforming larger pieces of code containing assignments and control structures. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve the numerical accuracy of the target variable. We use abstract interpretation-based static analysis techniques to over-approximate the roundoff errors in programs and during the transformation of expressions. A prototype has been implemented and experimental results are presented concerning classical numerical algorithm analysis and algorithm for embedded systems.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
ANSI/IEEE. IEEE Standard for Binary Floating-Point Arithmetic. SIAM (2008)
Appel, A.-W.: Modern Compiler Implementation in ML. Cambridge University Press (1998)
Barr, E.-T., Vo, T., Le, V., Su, Z.: Automatic detection of floating-point exceptions. In: Symposium on Principles of Programming Languages, POPL 2013, pp. 549–560. ACM (2013)
Benz, F., Hildebrandt, A., Hack, S.: A dynamic program analysis to find floating-point accuracy problems. In: Programming Language Design and Implementation, PLDI 2012, pp. 453–462. ACM (2012)
Bertrane, J., Cousot, P., Cousot, R., Feret, F., Mauborgne, L., Miné, A., Rival, X.: Static analysis by abstract interpretation of embedded critical software. ACM SIGSOFT Software Engineering Notes 36(1), 1–8 (2011)
Chapoutot, A., Damouche, N., Martel, M.: Automatic transformation of a PID controller. In: International Workshop on Numerical Software Verification (2014)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977)
Cousout, P., Cousot, R.: Systematic design of program transformation frameworks by abstract interpretation. In: Principles of Programming Languages, pp. 178–190. ACM (2002)
Cytron, R., Gershbein, R.: Efficient accomodation of may-alias information in SSA form. In: Programming Language Design and Implementation (PLDI), pp. 36–45. ACM (1993)
Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of FLUCTUAT on safety-critical avionics software. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009)
Feron, E.: From control systems to control software. IEEE Control Systems Magazine 30(6), 50–71 (2010)
Gao, X., Bayliss, S., Constantinides, G.-A.: SOAP: structural optimization of arithmetic expressions for high-level synthesis. In: Field-Programmable Technology, FPT, pp. 112–119. IEEE (2013)
Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 1–3. Springer, Heidelberg (2013)
Goubault, E., Putot, S.: Static analysis of finite precision computations. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 232–247. Springer, Heidelberg (2011)
Hankin, E.: Lambda Calculi A Guide For Computer Scientists. Clarendon Press, Oxford (1994)
Ioualalen, A., Martel, M.: A new abstract domain for the representation of mathematically equivalent expressions. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 75–93. Springer, Heidelberg (2012)
Ioualalen, A., Martel, M.: Synthesizing accurate floating-point formulas. In: Application-Specific Systems, Architectures and Processors, ASAP, pp. 113–116 (2013)
Jones, N.-D.: An introduction to partial evaluation. ACM Computing Surveys 28(3), 480–503 (1996)
Kendall, A.: An Introduction to Numerical Analysis. John Wiley & Sons (1989)
Logozzo, F., Ball, T.: Modular and verified automatic program repair. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA, pp. 133–146. ACM (2012)
Martel, M.: Accurate evaluation of arithmetic expressions (invited talk). Electr. Notes Theor. Comput. Sci. 287, 3–16 (2012)
Martel, M.: Semantics of roundoff error propagation in finite precision calculations. Higher-Order and Symbolic Computation 19(1), 7–30 (2006)
Muller, J.-M., Brisebarre, N., De Dinechin, F., Jeannerod, C.-P., Lefèvre, V., Melquiond, G., Revol, N., Stehlé, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkhäuser (2010)
Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: A new approach to optimization. Logical Methods in Computer Science 7(1) (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Damouche, N., Martel, M., Chapoutot, A. (2015). Intra-procedural Optimization of the Numerical Accuracy of Programs. In: Núñez, M., Güdemann, M. (eds) Formal Methods for Industrial Critical Systems. FMICS 2015. Lecture Notes in Computer Science(), vol 9128. Springer, Cham. https://doi.org/10.1007/978-3-319-19458-5_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-19458-5_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19457-8
Online ISBN: 978-3-319-19458-5
eBook Packages: Computer ScienceComputer Science (R0)