Document Open Access Logo

Verified Compilation and Optimization of Floating-Point Programs in CakeML

Authors Heiko Becker , Robert Rabe, Eva Darulova , Magnus O. Myreen , Zachary Tatlock , Ramana Kumar , Yong Kiam Tan , Anthony Fox

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2022.1.pdf
  • Filesize: 0.96 MB
  • 28 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Software and its engineering → Compilers
  • Software and its engineering → Software performance
Keywords
  • compiler verification
  • compiler optimization
  • floating-point arithmetic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Verified compilers such as CompCert and CakeML have become increasingly realistic over the last few years, but their support for floating-point arithmetic has thus far been limited. In particular, they lack the "fast-math-style" optimizations that unverified mainstream compilers perform. Supporting such optimizations in the setting of verified compilers is challenging because these optimizations, for the most part, do not preserve the IEEE-754 floating-point semantics. However, IEEE-754 floating-point numbers are finite approximations of the real numbers, and we argue that any compiler correctness result for fast-math optimizations should appeal to a real-valued semantics rather than the rigid IEEE-754 floating-point numbers.
This paper presents RealCake, an extension of CakeML that achieves end-to-end correctness results for fast-math-style optimized compilation of floating-point arithmetic. This result is achieved by giving CakeML a flexible floating-point semantics and integrating an external proof-producing accuracy analysis. RealCake’s end-to-end theorems relate the I/O behavior of the original source program under real-number semantics to the observable I/O behavior of the compiler generated and fast-math-optimized machine code.

Cite As Get BibTex

Heiko Becker, Robert Rabe, Eva Darulova, Magnus O. Myreen, Zachary Tatlock, Ramana Kumar, Yong Kiam Tan, and Anthony Fox. Verified Compilation and Optimization of Floating-Point Programs in CakeML. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 1:1-1:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.1

Author Details

Heiko Becker
  • MPI-SWS, Saarland Informatics Campus, (SIC), Saarbrücken, Germany
Robert Rabe
  • TU München, Germany
Eva Darulova
  • Uppsala University, Sweden
Magnus O. Myreen
  • Chalmers University of Technology, Gothenburg, Sweden
Zachary Tatlock
  • University of Washington, Seattle, WA, USA
Ramana Kumar
  • DeepMind, London, UK
Yong Kiam Tan
  • Carnegie Mellon University, Pittsburgh, PA, USA
Anthony Fox
  • Arm Limited, Cambridge, UK

Funding

  • Darulova, Eva: Part of this work was done while the author was at MPI-SWS, Germany.
  • Myreen, Magnus O.: Supported by the Swedish Foundation for Strategic Research.
  • Tatlock, Zachary: Supported in part by the U.S. Department of Energy under Award Number DE-SC0022081 (ComPort), and by the National Science Foundation under Grant No. 1749570. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the DOE or NSF.

Supplementary Materials

References

  1. Oskar Abrahamsson. A Verified Proof Checker for Higher-Order Logic. Journal of Logical and Algebraic Methods in Programming, 112, 2020. URL: https://doi.org/10.1016/j.jlamp.2020.100530.
  2. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Proof-Producing Synthesis of CakeML from Monadic HOL Functions. J. Autom. Reason., 64(7), 2020. URL: https://doi.org/10.1007/s10817-020-09559-8.
  3. A. Anta and P. Tabuada. To Sample or not to Sample: Self-Triggered Control for Nonlinear Systems. IEEE Transactions on Automatic Control, 55(9):2030-2042, 2010. URL: https://doi.org/10.1109/TAC.2010.2042980.
  4. Apache Software Foundation. The LLVM Compiler Infrastructure, 2020. URL: https://www.llvm.org/.
  5. Heiko Becker, Eva Darulova, Magnus O Myreen, and Zachary Tatlock. Icing: Supporting Fast-Math Style Optimizations in a Verified Compiler. In Computer Aided Verification (CAV), 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_10.
  6. Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O Myreen, and Anthony Fox. A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. In Formal Methods in Computer Aided Design (FMCAD), 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603019.
  7. Michael Berg. LLVM Numerics Blog, 2019. URL: http://blog.llvm.org/2019/03/llvm-numerics-blog.html.
  8. Hans-J. Boehm. Towards an API for the Real Numbers. In Programming Language Design and Implementation (PLDI), 2020. URL: https://doi.org/10.1145/3385412.3386037.
  9. Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, and Pierre Weis. Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, 50(4), 2013. URL: https://doi.org/10.1007/s10817-012-9255-4.
  10. Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond. Verified Compilation of Floating-Point Computations. Journal of Automated Reasoning, 54(2):135-163, 2015. URL: https://doi.org/10.1007/s10817-014-9317-x.
  11. Wei-Fan Chiang, Mark Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, and Zvonimir Rakamarić. Rigorous Floating-Point Mixed-Precision Tuning. In Principles of Programming Languages (POPL), 2017. URL: https://doi.org/10.1145/3009837.3009846.
  12. G. A. Constantinides, P. Y. K. Cheung, and W. Luk. Wordlength Optimization for Linear Digital Signal Processing. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 22(10), 2003. URL: https://doi.org/10.1109/TCAD.2003.818119.
  13. Nasrine Damouche, Matthieu Martel, and Alexandre Chapoutot. Improving the Numerical Accuracy of Programs by Automatic Transformation. International Journal on Software Tools for Technology Transfer, 19(4), 2017. URL: https://doi.org/10.1007/s10009-016-0435-0.
  14. Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, and Zachary Tatlock. Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. In Numerical Software Verification (NSV), 2016. URL: https://doi.org/10.1007/978-3-319-54292-8_6.
  15. Eva Darulova and Viktor Kuncak. Towards a Compiler for Reals. ACM Transactions on Programming Languages and Systems (TOPLAS), 39(2), 2017. URL: https://doi.org/10.1145/3014426.
  16. Eva Darulova, Saksham Sharma, and Einar Horn. Sound Mixed-Precision Optimization with Rewriting. In International Conference on Cyber-Physical Systems (ICCPS), 2018. URL: https://doi.org/10.1109/ICCPS.2018.00028.
  17. Florent De Dinechin, Christoph Quirin Lauter, and Guillaume Melquiond. Assisted Verification of Elementary Functions Using Gappa. In ACM Symposium on Applied Computing (SAC), 2006. URL: https://doi.org/10.1145/1141277.1141584.
  18. Anthony Fox. Improved Tool Support for Machine-Code Decompilation in HOL4. In International Conference on Interactive Theorem Proving. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-22102-1_12.
  19. Free Software Foundation. The GNU Compiler Collection, 2020. URL: https://gcc.gnu.org/.
  20. GCC Developers. GCC Wiki: Floating-point Math, 2020. URL: https://gcc.gnu.org/wiki/FloatingPointMath.
  21. Alejandro Gomez-Londono, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan. Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs. Proceedings of the ACM on Programming Languages (OOPSLA), 4, 2020. URL: https://doi.org/10.1145/3428272.
  22. Armaël Guéneau, Magnus O Myreen, Ramana Kumar, and Michael Norrish. Verified Characteristic Formulae for CakeML. In European Symposium on Programming (ESOP), 2017. URL: https://doi.org/10.1007/978-3-662-54434-1_22.
  23. Suyog Gupta, Ankur Agrawal, Kailash Gopalakrishnan, and Pritish Narayanan. Deep learning with limited numerical precision. In International Conference on Machine Learning (ICML), 2015. Google Scholar
  24. John Harrison. Floating Point Verification in HOL. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, 1995. URL: https://doi.org/10.1007/3-540-60275-5_65.
  25. Nicholas J. Higham. Accuracy and Stability of Numerical Algorithms. Society for Industrial and Applied Mathematics, 2nd edition, 2002. URL: https://doi.org/10.1137/1.9780898718027.
  26. IEEE. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008), 2019. URL: https://doi.org/10.1109/IEEESTD.2019.8766229.
  27. Bertrand Jeannet and Antoine Miné. Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verification (CAV), 2009. URL: https://doi.org/10.1007/978-3-642-02658-4_52.
  28. Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. A Formally-Verified C Static Analyzer. In Principles of Programming Languages (POPL), 2015. URL: https://doi.org/10.1145/2676726.2676966.
  29. Ramana Kumar. Self-Compilation and Self-Verification. PhD thesis, University of Cambridge, 2015. Google Scholar
  30. Juneyoung Lee, Chung-Kil Hur, and Nuno P Lopes. AliveInLean: a Verified LLVM Peephole Optimization Verifier. In International Conference on Computer Aided Verification. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_25.
  31. Xavier Leroy. Formal Certification of a Compiler Back-end, or: Programming a Compiler with a Proof Assistant. In Principles of Programming Languages (POPL), 2006. URL: https://doi.org/10.1145/1111037.1111042.
  32. Xavier Leroy. A Formally Verified Compiler Back-end. Journal of Automated Reasoning, 43(4), 2009. URL: https://doi.org/10.1007/s10817-009-9155-4.
  33. LLVM Developers. LLVM Language Reference: Fast-Math Flags, 2020. URL: https://llvm.org/docs/LangRef.html#fast-math-flags.
  34. Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Provably Correct Peephole Optimizations with Alive. In Programming Language Design and Implementation (PLDI), 2015. URL: https://doi.org/10.1145/2737924.2737965.
  35. Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus O. Myreen, Michael Norrish, Oskar Abrahamsson, and Anthony Fox. Verified Compilation on a Verified Processor. In Programming Language Design and Implementation (PLDI), 2019. URL: https://doi.org/10.1145/3314221.3314622.
  36. Victor Magron, George Constantinides, and Alastair Donaldson. Certified Roundoff Error Bounds Using Semidefinite Programming. ACM Transactions on Mathematical Software, 43(4), 2017. URL: https://doi.org/10.1145/3015465.
  37. Rupak Majumdar, Indranil Saha, and Majid Zamani. Synthesis of Minimal-Error Control Software. In International Conference on Embedded Software (EMSOFT), 2012. URL: https://doi.org/10.1145/2380356.2380380.
  38. Adolfo Anta Martinez, Rupak Majumdar, Indranil Saha, and Paulo Tabuada. Automatic Verification of Control System Implementations. In International Conference on Embedded software (EMSOFT), 2010. URL: https://doi.org/10.1145/1879021.1879024.
  39. David Menendez, Santosh Nagarakatte, and Aarti Gupta. Alive-FP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM. In Static Analysis Symposium (SAS), 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_16.
  40. Ramon E. Moore, R. Baker Kearfott, and Michael J. Cloud. Introduction to Interval Analysis. Society for Industrial and Applied Mathematics, 2009. URL: https://doi.org/10.1137/1.9780898717716.
  41. Mariano M. Moscato, Laura Titolo, Aaron Dutle, and César A. Muñoz. Automatic Estimation of Verified Floating-Point Round-Off Errors via Static Analysis. In Computer Safety, Reliability, and Security (SAFECOMP), 2017. URL: https://doi.org/10.1007/978-3-319-66266-4_14.
  42. Andres Nötzli and Fraser Brown. LifeJacket: Verifying Precise Floating-Point Optimizations in LLVM. In International Workshop on State Of the Art in Program Analysis (SOAP), 2016. URL: https://doi.org/10.1145/2931021.2931024.
  43. Scott Owens, Magnus O Myreen, Ramana Kumar, and Yong Kiam Tan. Functional Big-Step Semantics. In European Symposium on Programming (ESOP), 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_23.
  44. Pavel Panchekha, Alex Sanchez-Stern, James R Wilcox, and Zachary Tatlock. Automatically Improving Accuracy for Floating Point Expressions. In Conference on Programming Language Design and Implementation (PLDI), 2015. URL: https://doi.org/10.1145/2737924.2737959.
  45. A. Pnueli, M. Siegel, and E. Singerman. Translation Validation. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1998. URL: https://doi.org/10.1007/BFb0054170.
  46. Johannes Aman Pohjola, Henrik Rostedt, and Magnus O. Myreen. Characteristic Formulae for Liveness Properties of Non-terminating CakeML Programs. In Interactive Theorem Proving (ITP), 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.32.
  47. Markus Püschel, José M F Moura, Bryan Singer, Jianxin Xiong, Jeremy R Johnson, David A Padua, Manuela M Veloso, and Robert W Johnson. Spiral - A Generator for Platform-Adapted Libraries of Signal Processing Algorithms. International Journal of High Performance Computing Applications, 18(1), 2004. Google Scholar
  48. Tahina Ramananandro, Paul Mountcastle, Benoît Meister, and Richard Lethin. A Unified Coq Framework for Verifying C Programs with Floating-Point Computations. In Certified Programs and Proofs (CPP), 2016. URL: https://doi.org/10.1145/2854065.2854066.
  49. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages, 5, 2019. URL: https://doi.org/10.1561/2500000045.
  50. Cindy Rubio-González, Cuong Nguyen, Hong Diep Nguyen, James Demmel, William Kahan, Koushik Sen, David H. Bailey, Costin Iancu, and David Hough. Precimonious: Tuning Assistant for Floating-Point Precision. In International Conference for High Performance Computing, Networking, Storage and Analysis (SC), 2013. URL: https://doi.org/10.1145/2503210.2503296.
  51. Hanan Samet. Proving the Correctness of Heuristically Optimized Code. Communications of the ACM, 21(7), 1978. URL: https://doi.org/10.1145/359545.359569.
  52. Eric Schkufza, Rahul Sharma, and Alex Aiken. Stochastic Optimization of Floating-point Programs with Tunable Precision. In Programming Language Design and Implementation (PLDI), 2014. URL: https://doi.org/10.1145/2594291.2594302.
  53. Konrad Slind and Michael Norrish. A Brief Overview of HOL4. In International Conference on Theorem Proving in Higher Order Logics (TPHOL), 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  54. Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, and Ganesh Gopalakrishnan. Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions. In International Symposium on Formal Methods (FM), 2015. URL: https://doi.org/10.1007/978-3-319-19249-9_33.
  55. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The Verified CakeML Compiler Backend. Journal of Functional Programming, 29, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  56. Laura Titolo, Marco A Feliú, Mariano Moscato, and César A Munoz. An Abstract Interpretation Framework for the Round-off Error Analysis of Floating-Point Programs. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2018. URL: https://doi.org/10.1007/978-3-319-73721-8_24.
  57. Linus Torvalds. What is acceptable for -ffast-math?, 2001. URL: https://gcc.gnu.org/legacy-ml/gcc/2001-07/msg02150.html.
  58. Vadim Zaliva. HELIX: From Math to Verified Code. PhD thesis, Carnegie Mellon University, 2020. Google Scholar
  59. Jianzhou Zhao, Santosh Nagarakatte, Milo MK Martin, and Steve Zdancewic. Formalizing the LLVM Intermediate Representation for Verified Program Transformations. In Principles of Programming Languages (POPL), 2012. URL: https://doi.org/10.1145/2103656.2103709.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact