[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Verified Compilation of Floating-Point Computations

  • Published:
Journal of Automated Reasoning Aims and scope Submit manuscript

Abstract

Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, this is not sufficient to guarantee the final result of a program, as several other actors are involved: programming language, compiler, and architecture. The CompCert formally-verified compiler provides a solution to this problem: this compiler comes with a mathematical specification of the semantics of its source language (a large subset of ISO C99) and target platforms (ARM, PowerPC, x86-SSE2), and with a proof that compilation preserves semantics. In this paper, we report on our recent success in formally specifying and proving correct CompCert’s compilation of floating-point arithmetic. Since CompCert is verified using the Coq proof assistant, this effort required a suitable Coq formalization of the IEEE-754 standard; we extended the Flocq library for this purpose. As a result, we obtain the first formally verified compiler that provably preserves the semantics of floating-point programs.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  1. Ayad, A., Marché, C.: Multi-prover verification of floating-point programs. In: Giesl, J., Hähnle, R. (eds.) 5th international joint conference on automated reasoning (IJCAR), Lecture Notes in Computer Science, vol. 6173. Springer, Edinburgh (2010)

  2. Boldo, S.: Preuves formelles en arithmétiques à virgule flottante. Ph.D. thesis, École Normale Supérieure de Lyon (2004)

  3. Boldo, S., Filliâtre, J.C.: Formal verification of floating-point programs. In: Kornerup, P., Muller, J.M. (eds.) 18th IEEE International symposium on computer arithmetic (ARITH). IEEE, pp. 187–194, Montpellier (2007)

  4. Boldo, S., Melquiond, G.: Emulation of FMA and correctly-rounded sums: Proved algorithms using rounding to odd. IEEE Trans. Comput. 57(4), 462–471 (2008)

    Article  MathSciNet  Google Scholar 

  5. Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) 20th IEEE symposium on computer arithmetic, pp. 243–252. IEEE, Tübingen (2011)

    Google Scholar 

  6. Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. 7, 151–160 (2011)

    Article  Google Scholar 

  7. Brisebarre, N., Muller, J.M., Raina, S.K.: Accelerating correctly rounded floating-point division when the divisor is known in advance. IEEE Trans. Comput. 53(8), 1069–1072 (2004)

    Article  Google Scholar 

  8. Carreño, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS In: 8th international workshop on higher-order logic theorem proving and its applications (HOL95), Aspen Grove, UT (1995)

  9. Clinger, W.D.: How to read floating-point numbers accurately In: Programming language design and implementation (PLDI’90), pp. 92–101. ACM (1990)

  10. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer In: 14th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 3444, pp. 21–30. Springer, Berlin Heidelberg New York (2005)

    Google Scholar 

  11. Dekker, T.J.: A floating point technique for extending the available precision. Numerische Mathematik 18(3), 224–242 (1971)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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: Formal methods for industrial critical systems (FMICS), Lecture Notes in Computer Science, vol. 5825, pp. 53–69. Springer, Berlin Heidelberg New York (2009)

    Google Scholar 

  13. Figueroa, S.A.: When is double rounding innocuous?. SIGNUM Newsl. 30(3), 21–26 (1995)

    Article  Google Scholar 

  14. Goldberg, D.: What every computer scientist should know about floating point arithmetic. ACM Comput. Surv. 23(1), 5–47 (1991)

    Article  Google Scholar 

  15. Granlund, T., Montgomery, P.L.: Division by invariant integers using multiplication In: Programming language design and implementation (PLDI’94), pp. 61–72. ACM (1994)

  16. Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) In: 12th International conference on theorem proving in higher order logics (TPHOLs’99), Lecture Notes in Computer Science, vol. 1690, pp. 113–130. Springer, Nice (1999)

    Google Scholar 

  17. Harrison, J.: Formal verification of floating point trigonometric functions In: 3rd International conference on formal methods in computer-aided design (FMCAD), Lecture Notes in Computer Science, vol. 1954, pp. 217–233. Springer, Austin (2000)

    Google Scholar 

  18. IBM: The PowerPC compiler writer’s guide. Warthman Associates (1996)

  19. Ioualalen, A., Martel, M.: A new abstract domain for the representation of mathematically equivalent expressions In: 19th international symposium on static analysis, Lecture Notes in Computer Science, vol. 7460, pp. 75–93. Springer, Berlin Heidelberg New York (2012)

    Google Scholar 

  20. ISO: International standard ISO/IEC 9899:2011, Programming languages – C (2011)

  21. Leavens, G.T.: Not a number of floating point problems. J. Object Technol. 5(2), 75–83 (2006)

    Article  Google Scholar 

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

    Article  Google Scholar 

  23. Leroy, X.: The CompCert verified compiler, software and commented proof. Available at http://compcert.inria.fr/ (2014)

  24. Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: Nicola, R.D. (ed.) In: 16th european symposium on programming (ESOP), Lecture Notes in Computer Science, vol. 4421, pp. 205–219. Springer, Braga (2007)

    Google Scholar 

  25. Microprocessor Standards Subcommittee: IEEE Standard for Floating-Point Arithmetic. IEEE Std. 754-2008 pp. 1–58 (2008)

  26. Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) 7th annual machine intelligence workshop, Machine Intelligence, vol. 7, pp. 51–72. Edinburgh University Press (1972)

  27. Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30(3), 1–41 (2008)

    Article  Google Scholar 

  28. Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461–492 (1989)

    Google Scholar 

  29. 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)

  30. Myreen, Magnus O.: Formal verification of machine-code programs. Ph.D. Thesis, University of Cambridge (2008)

  31. Nguyen, T.M.T., Marché, C.: Hardware-dependent proofs of numerical programs. In: Jouannaud, J.P., Shao, Z. (eds.) International conference on certified programs and proofs (CPP), Lecture Notes in Computer Science, vol. 7086, pp. 314–329. Springer, Berlin Heidelberg New York (2011)

    Google Scholar 

  32. Nickolls, J., Dally, W.: The GPU computing era. IEEE Micro 30(2), 56–69 (2010)

    Article  Google Scholar 

  33. Rump, S., Ogita, T., Oishi, S.: Accurate floating-point summation Part I: Faithful rounding. SIAM J. Sci. Comput. 31(1), 189–224 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  34. Russinoff, D.M.: A mechanically checked proof of IEEE compliance of the floating point multiplication, division and square root algorithms of the AMD-K7 processor. LMS J. Comput. Math. 1, 148–200 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  35. Sterbenz, P.H.: Floating point computation. Prentice Hall, Englewood Cliffs (1974)

    Google Scholar 

  36. Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers In: 32nd ACM SIGPLAN conference on programming language design and implementation (PLDI), pp. 283–294. ACM Press (2011)

Download references

Author information

Authors and Affiliations

  1. Inria, LRI, CNRS UMR 8623, Université Paris-Sud, Bât 650 (PCRI), 91405, Orsay, France

    Sylvie Boldo & Guillaume Melquiond

  2. Inria Paris-Rocquencourt, Domaine de Voluceau, BP 105, 78153, Le Chesnay, France

    Jacques-Henri Jourdan & Xavier Leroy

Authors
  1. Sylvie Boldo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jacques-Henri Jourdan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xavier Leroy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Guillaume Melquiond
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Xavier Leroy.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Boldo, S., Jourdan, JH., Leroy, X. et al. Verified Compilation of Floating-Point Computations. J Autom Reasoning 54, 135–163 (2015). https://doi.org/10.1007/s10817-014-9317-x

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10817-014-9317-x

Keywords

Search

Navigation