Sökning: onr:"swepub:oai:research.chalmers.se:62e27fbe-5913-4ee0-9e2e-a9c824cd97a2" >
Verified Compilatio...
Verified Compilation and Optimization of Floating-Point Programs in CakeML
-
- Becker, Heiko (författare)
- Max Planck Gesellschaft zur Förderung der Wissenschaften e.V. (MPG),Max Planck Society for the Advancement of Science (MPG)
-
- Rabe, Robert (författare)
- Technische Universität München (TUM),Technical University of Munich (TUM)
-
- Darulova, Eva (författare)
- Uppsala universitet,Datalogi
-
visa fler...
-
- Myreen, Magnus, 1983 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Tatlock, Zachary (författare)
- University of Washington
-
- Kumar, R. (författare)
- Google DeepMind
-
- Tan, Yong Kiam (författare)
- Carnegie Mellon University (CMU)
-
- Fox, Anthony C. J. (författare)
- ARM Limited
-
visa färre...
-
Max Planck Gesellschaft zur Förderung der Wissenschaften eV. (MPG) Technische Universität München (TUM) (creator_code:org_t)
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022
- 2022
- Engelska.
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - : Schloss Dagstuhl - Leibniz-Zentrum für Informatik. - 1868-8969. ; 222
- Relaterad länk:
-
https://doi.org/10.4...
-
visa fler...
-
https://uu.diva-port... (primary) (Raw object)
-
https://research.cha...
-
https://doi.org/10.4...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Datorsystem (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Computer Systems (hsv//eng)
Nyckelord
- compiler optimization
- compiler verification
- floating-point arithmetic
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas