Document Open Access Logo

Verified Compilation and Optimization of Floating-Point Programs in CakeML (Artifact)

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

PDF
Thumbnail PDF

Artifact Description

DARTS.8.2.10.pdf
  • Filesize: 484 kB
  • 2 pages

Document Identifiers

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.

Cite AsGet 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 (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DARTS.8.2.10

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy

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 document describes the artifact for 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.

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

Related Article

  • 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), LIPIcs, Vol. 222, pp. 1:1-1:28, 2022. https://doi.org/10.4230/LIPIcs.ECOOP.2022.1
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact