Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode
summary
RLibm generates correctly rounded elementary functions and this work builds two ways to avoid costly rounding-mode switches: round-to-zero emulation replaces additions and multiplications with error‑free‑transformation checks and a small adjustment to force round‑toward‑zero, while rounding‑invariant input bounds uses interval arithmetic through polynomial generation to bound all rounding‑mode outcomes. Implementations (up to 32‑bit targets) are proven correct, available as artifacts, and deliver about 1.5× and 2.3× speedups respectively.
AI-written summary · about
chapters (15)
- 0:00RLBM project introduction
- 1:25Correctly rounded math libraries
- 3:09Using results as oracles
- 4:12Generating polynomials via LP
- 4:33Round to odd for multi-rep
- 5:14Rounding mode switch overhead
- 6:17Rounding invariant outputs
- 8:23Custom addition for round to zero
- 10:28Rounding invariant input bounds
- 11:11Polynomial outputs as intervals
- 13:38Tighter constraints for correctness
- 14:41Validating new implementations
- 15:25Performance improvements
- 16:50New methods and trade-offs
- 17:32Q&A
related talks
26mGenerating Correctly Rounded Math Libraries for New Floating Point Variants
22mOne Polynomial Approximation to Produce Correctly Rounded Results of an Elementa
58mFrom Formal Verification to Correctly Rounded Math Libraries
58mPortable floating-point calculations
10mCorrectly Rounded Dot Products under Round-to-Odd
20mImplementation and Synthesis of Math Library Functions
14mFPL: Fast Presburger Arithmetic through Transprecision
19mPorting SLEEF to RISC-V