Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909781297463296 |
|---|---|
| author | Tekriwal, Mohit Sarracino, John |
| author_facet | Tekriwal, Mohit Sarracino, John |
| contents | Scientific computing programs often undergo aggressive compiler optimization to achieve high performance and efficient resource utilization. While performance is critical, we also need to ensure that these optimizations are correct. In this paper, we focus on a specific class of optimizations, floating-point optimizations, notably due to fast math, at the LLVM IR level. We present a preliminary work, which leverages the Verified LLVM framework in the Rocq theorem prover, to prove the correctness of Fused-Multiply-Add (FMA) optimization for a basic block implementing the arithmetic expression $a * b + c$ . We then propose ways to extend this preliminary results by adding more program features and fast math floating-point optimizations. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_09019 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs Tekriwal, Mohit Sarracino, John Programming Languages Scientific computing programs often undergo aggressive compiler optimization to achieve high performance and efficient resource utilization. While performance is critical, we also need to ensure that these optimizations are correct. In this paper, we focus on a specific class of optimizations, floating-point optimizations, notably due to fast math, at the LLVM IR level. We present a preliminary work, which leverages the Verified LLVM framework in the Rocq theorem prover, to prove the correctness of Fused-Multiply-Add (FMA) optimization for a basic block implementing the arithmetic expression $a * b + c$ . We then propose ways to extend this preliminary results by adding more program features and fast math floating-point optimizations. |
| title | Towards Verified Compilation of Floating-point Optimization in Scientific Computing Programs |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2509.09019 |