Verified compilation of floating-point computations. (English) Zbl 1331.68047
Summary: 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.
MSC:
| 68N20 | Theory of compilers and interpreters |
| 65G50 | Roundoff error |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
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) · Zbl 1291.68321 |
| [2] | Boldo, S.: Preuves formelles en arithmétiques à virgule flottante. Ph.D. thesis, École Normale Supérieure de Lyon (2004) · Zbl 1388.65200 |
| [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) · Zbl 1388.65200 · doi:10.1109/TC.2007.70819 |
| [5] | Boldo, S.; Melquiond, G.; Antelo, E. (ed.); Hough, D. (ed.); Ienne, P. (ed.), Flocq: A unified library for proving floating-point algorithms in Coq, 243-252 (2011), Tübingen |
| [6] | Boldo, S., Nguyen, T.M.T.: Proofs of numerical programs when the compiler optimizes. Innov. Syst. Softw. Eng. 7, 151-160 (2011) · doi:10.1007/s11334-011-0151-6 |
| [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) · doi:10.1109/TC.2004.37 |
| [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) · Zbl 1108.68422 |
| [9] | Clinger, W.D.: How to read floating-point numbers accurately In: Programming language design and implementation (PLDI’90), pp. 92-101. ACM (1990) · Zbl 1187.68141 |
| [10] | Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Monniaux, D.; Rival, X., The ASTRÉE analyzer, 21-30 (2005), Berlin Heidelberg New York · Zbl 1108.68422 |
| [11] | Dekker, T.J.: A floating point technique for extending the available precision. Numerische Mathematik 18(3), 224-242 (1971) · Zbl 0226.65034 · doi:10.1007/BF01397083 |
| [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, 53-69 (2009), Berlin Heidelberg New York |
| [13] | Figueroa, S.A.: When is double rounding innocuous?. SIGNUM Newsl. 30(3), 21-26 (1995) · doi:10.1145/221332.221334 |
| [14] | Goldberg, D.: What every computer scientist should know about floating point arithmetic. ACM Comput. Surv. 23(1), 5-47 (1991) · doi:10.1145/103162.103163 |
| [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.; Bertot, Y. (ed.); Dowek, G. (ed.); Hirschowitz, A. (ed.); Paulin, C. (ed.); Théry, L. (ed.), A machine-checked theory of floating point arithmetic, 113-130 (1999), Nice |
| [17] | Harrison, J., Formal verification of floating point trigonometric functions, 217-233 (2000), Austin |
| [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, 75-93 (2012), Berlin Heidelberg New York |
| [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) · doi:10.5381/jot.2006.5.2.c8 |
| [22] | Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107-115 (2009) · doi:10.1145/1538788.1538814 |
| [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.; Nicola, RD (ed.), Structure of a proof-producing compiler for a subset of higher order logic, 205-219 (2007), Braga · Zbl 1187.68141 |
| [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) · Zbl 0259.68008 |
| [27] | Monniaux, D.: The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst. 30(3), 1-41 (2008) · doi:10.1145/1353445.1353446 |
| [28] | Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461-492 (1989) |
| [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) · Zbl 1197.65001 |
| [30] | Myreen, Magnus O.: Formal verification of machine-code programs. Ph.D. Thesis, University of Cambridge (2008) |
| [31] | Nguyen, TMT; Marché, C.; Jouannaud, JP (ed.); Shao, Z. (ed.), Hardware-dependent proofs of numerical programs, 314-329 (2011), Berlin Heidelberg New York · Zbl 1350.68241 |
| [32] | Nickolls, J., Dally, W.: The GPU computing era. IEEE Micro 30(2), 56-69 (2010) · doi:10.1109/MM.2010.41 |
| [33] | Rump, S., Ogita, T., Oishi, S.: Accurate floating-point summation Part I: Faithful rounding. SIAM J. Sci. Comput. 31(1), 189-224 (2008) · Zbl 1185.65082 · doi:10.1137/050645671 |
| [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) · Zbl 0910.68008 · doi:10.1112/S1461157000000176 |
| [35] | Sterbenz, P.H.: Floating point computation. Prentice Hall, Englewood Cliffs (1974) |
| [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) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
