Abstract
In this article, we describe a static program analysis to determine the lowest floating-point precisions on inputs and intermediate results that guarantees a desired accuracy of the output values. A common practice used by developers without advanced training in computer arithmetic consists in using the highest precision available in hardware (double precision on most CPU’s) which can be exorbitant in terms of energy consumption, memory traffic, and bandwidth capacity. To overcome this difficulty, we propose a new precision tuning tool for the floating-point programs integrating a static forward and backward analysis, done by abstract interpretation. Next, our analysis will be expressed as a set of linear constraints easily checked by an SMT solver.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Patriot missile defense: Software problem led to system failure at Dhahran, Saudi Arabia. Technical report GAO/IMTEC-92-26, General Accounting Office (1992)
Chiang, W.F., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamarić, Z.: Rigorous floating-point mixed-precision tuning. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). ACM (2017)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252 (1977)
Damouche, N., Martel, M.: Salsa: an automatic tool to improve the numerical accuracy of programs. In: Shankar, N., Dutertre, B. (eds.) Automated Formal Methods. Kalpa Publications in Computing, EasyChair (2018)
Darulova, E., Kuncak, V.: Sound compilation of reals. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014. ACM (2014)
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)
Gaubert, S., Goubault, E., Taly, A., Zennou, S.: Static analysis by policy iteration on relational domains. In: De Nicola, R. (ed.) Programming Languages and Systems. Springer, Heidelberg (2007)
Halfhill, T.R.: The truth behind the Pentium bug: how often do the five empty cells in the Pentium’s FPU lookup table spell miscalculation? (1995)
Lam, M.O., Hollingsworth, J.K., de Supinski, B.R., Legendre, M.P.: Automatically adapting programs for mixed-precision floating-point computation. In: Proceedings of the 27th International ACM Conference on International Conference on Supercomputing, ICS 2013. ACM (2013)
Martel, M.: Floating-point format inference in mixed-precision. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 230–246. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_16
Muller, J.M.: On the definition of ULP(x). Research Report RR-5504, LIP RR-2005-09, INRIA, LIP, February 2005. https://hal.inria.fr/inria-00070503
Muller, J.M., et al.: Handbook of Floating-Point Arithmetic, 1st edn. Birkhäuser, Boston (2009)
Parr, T.: The Definitive ANTLR 4 Reference, 2nd edn. Pragmatic Bookshelf, Raleigh (2013)
Rubio-González, C., et al.: Precimonious: tuning assistant for floating-point precision. In: International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2013, Denver, CO, USA, 17–21 November 2013 (2013)
Rubio-González, C., et al.: Floating-point precision tuning using blame analysis. In: 2016 IEEE/ACM 38th International Conference on Software Engineering (ICSE) (2016)
Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic Taylor expansions. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 532–550. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_33
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Ben Khalifa, D., Martel, M., Adjé, A. (2020). POP: A Tuning Assistant for Mixed-Precision Floating-Point Computations. In: Hasan, O., Mallet, F. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2019. Communications in Computer and Information Science, vol 1165. Springer, Cham. https://doi.org/10.1007/978-3-030-46902-3_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-46902-3_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-46901-6
Online ISBN: 978-3-030-46902-3
eBook Packages: Computer ScienceComputer Science (R0)