Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Formal Methods

FM 2018: Formal Methods pp 355–363Cite as

Combining Tools for Optimization and Analysis of Floating-Point Computations

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10951))

Abstract

Recent renewed interest in optimizing and analyzing floating-point programs has lead to a diverse array of new tools for numerical programs. These tools are often complementary, each focusing on a distinct aspect of numerical programming. Building reliable floating point applications typically requires addressing several of these aspects, which makes easy composition essential. This paper describes the composition of two recent floating-point tools: Herbie, which performs accuracy optimization, and Daisy, which performs accuracy verification. We find that the combination provides numerous benefits to users, such as being able to use Daisy to check whether Herbie’s unsound optimizations improved the worst-case roundoff error, as well as benefits to tool authors, including uncovering a number of bugs in both tools. The combination also allowed us to compare the different program rewriting techniques implemented by these tools for the first time. The paper lays out a road map for combining other floating-point tools and for surmounting common challenges.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    We found that neither interval analysis without subdivision nor alternate SMT solvers provided tighter bounds.

  2. 2.

    Indicating that it could not prove the absence of invalid operations, such as divisions by zero.

References

  1. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)

    Google Scholar 

  2. Becker, H., Panchekha, P., Darulova, E., Tatlock, Z.: Combining tools for optimization and analysis of floating-point computations. arXiv preprint arXiv:1805.02436 (2018)

  3. Chiang, W.F., Baranowski, M., Briggs, I., Solovyev, A., Gopalakrishnan, G., Rakamarić, Z.: Rigorous floating-point mixed-precision tuning. In: Symposium on Principles of Programming Languages (POPL), pp. 300–315. ACM (2017)

    Google Scholar 

  4. Chiang, W.F., Gopalakrishnan, G., Rakamaric, Z., Solovyev, A.: Efficient search for inputs causing high floating-point errors. In: Symposium on Principles and Practice of Parallel Programming (PPoPP), vol. 49, pp. 43–52. ACM (2014)

    Google Scholar 

  5. Damouche, N., Martel, M., Chapoutot, A.: Intra-procedural optimization of the numerical accuracy of programs. In: Núñez, M., Güdemann, M. (eds.) FMICS 2015. LNCS, vol. 9128, pp. 31–46. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19458-5_3

    Chapter  MATH  Google Scholar 

  6. Damouche, N., et al.: Toward a standard benchmark format and suite for floating-point analysis. In: Bogomolov, S., Martel, M., Prabhakar, P. (eds.) NSV 2016. LNCS, vol. 10152, pp. 63–77. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-54292-8_6

    Chapter  Google Scholar 

  7. Darulova, E., Horn, E., Sharma, S.: Sound mixed-precision optimization with rewriting. In: International Conference on Cyber-Physical Systems (ICCPS) (2018)

    Google Scholar 

  8. Darulova, E., et al.: Daisy - framework for analysis and optimization of numerical programs (tool paper). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 270–287. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_15

    Chapter  Google Scholar 

  9. Darulova, E., Kuncak, V.: Towards a compiler for reals. ACM Trans. Program. Lang. Syst. (TOPLAS) 39(2), 8 (2017)

    Article  Google Scholar 

  10. De Dinechin, F., Lauter, C.Q., Melquiond, G.: Assisted verification of elementary functions using Gappa. In: ACM Symposium on Applied Computing, pp. 1318–1322. ACM (2006)

    Google Scholar 

  11. 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. http://dl.acm.org/citation.cfm?id=1792734.1792766

    Chapter  Google Scholar 

  12. Goubault, E., Putot, S.: Robustness analysis of finite precision implementations. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 50–57. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-03542-0_4

    Chapter  Google Scholar 

  13. IEEE Computer Society: IEEE standard for floating-point arithmetic. IEEE Std 754–2008 (2008)

    Google Scholar 

  14. Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  15. Magron, V., Constantinides, G., Donaldson, A.: Certified roundoff error bounds using semidefinite programming. ACM Trans. Math. Softw. 43(4), 1–34 (2017)

    Article  MathSciNet  Google Scholar 

  16. Moscato, M., Titolo, L., Dutle, A., Muñoz, C.A.: Automatic estimation of verified floating-point round-off errors via static analysis. In: Tonetta, S., Schoitsch, E., Bitsch, F. (eds.) SAFECOMP 2017. LNCS, vol. 10488, pp. 213–229. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66266-4_14

    Chapter  Google Scholar 

  17. Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: Conference on Programming Language Design and Implementation (PLDI) (2015)

    Google Scholar 

  18. Ramananandro, T., Mountcastle, P., Meister, B., Lethin, R.: A unified Coq framework for verifying C programs with floating-point computations. In: Certified Programs and Proofs (CPP), pp. 15–26. ACM (2016)

    Google Scholar 

  19. Rubio-González, C., Nguyen, C., Nguyen, H.D., Demmel, J., Kahan, W., Sen, K., Bailey, D.H., Iancu, C., Hough, D.: Precimonious: tuning assistant for floating-point precision. In: Proceedings of the International Conference on High Performance Computing, Networking, Storage and Analysis, SC 2013, pp. 27:1–27:12. ACM (2013)

    Google Scholar 

  20. Sanchez-Stern, A., Panchekha, P., Lerner, S., Tatlock, Z.: Finding root causes of floating point error with herbgrind. arXiv preprint arXiv:1705.10416 (2017)

  21. Schkufza, E., Sharma, R., Aiken, A.: Stochastic optimization of floating-point programs with tunable precision. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 53–64. ACM (2014)

    Google Scholar 

  22. 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

    Chapter  Google Scholar 

  23. Zou, D., Wang, R., Xiong, Y., Zhang, L., Su, Z., Mei, H.: A genetic algorithm for detecting significant floating-point inaccuracies. In: IEEE International Conference on Software Engineering (ICSE), vol. 1, pp. 529–539. IEEE (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MPI-SWS, Saarbrücken, Germany

    Heiko Becker & Eva Darulova

  2. University of Washington, Seattle, USA

    Pavel Panchekha & Zachary Tatlock

Authors
  1. Heiko Becker
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pavel Panchekha
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eva Darulova
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zachary Tatlock
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Eva Darulova .

Editor information

Editors and Affiliations

  1. NASA Jet Propulsion Laboratory, Pasadena, California, USA

    Klaus Havelund

  2. University of Bremen, Bremen, Germany

    Jan Peleska

  3. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

  4. Eindhoven University of Technology, Eindhoven, The Netherlands

    Erik de Vink

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Becker, H., Panchekha, P., Darulova, E., Tatlock, Z. (2018). Combining Tools for Optimization and Analysis of Floating-Point Computations. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds) Formal Methods. FM 2018. Lecture Notes in Computer Science(), vol 10951. Springer, Cham. https://doi.org/10.1007/978-3-319-95582-7_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-95582-7_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-95581-0

  • Online ISBN: 978-3-319-95582-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation