Scaling up Roundoff Analysis of Functional Data Structure Programs
Floating-point arithmetic is counter-intuitive due to inherent rounding errors that potentially occur at every arithmetic operation. A selection of automated tools now exists to ensure correctness of floating-point programs by computing guaranteed bounds on rounding errors at the end of a computation, but these tools effectively consider only straight-line programs over scalar variables. Much of numerical codes, however, use data structures such as lists, arrays or matrices and loops over these. To analyze such programs today, all data structure operations need to be unrolled, manually or by the analyzer, reducing the analysis to straight-line code, ultimately limiting the analyzers’ scalability.
We present the first rounding error analysis for numerical programs written over vectors and matrices that leverages the data structure information to speed up the analysis. We facilitate this with our functional domain-specific input language that we design based on a new set of numerical benchmarks that we collect from a variety of domains. Our DSL explicitly carries semantic information that is useful for avoiding duplicate and thus unnecessary analysis steps, as well as enabling abstractions for further speed-ups. Compared to unrolling-based approaches in state-of-the-art tools, our analysis retains adequate accuracy and is able to analyze more benchmarks or is significantly faster, and particularly scales better for larger programs.
Mon 23 OctDisplayed time zone: Lisbon change
14:00 - 15:30 | |||
14:00 30mTalk | Error Invariants for Fault Localization via Abstract Interpretation SAS 2023 Aleksandar S. Dimovski Mother Teresa University, Skopje Pre-print File Attached | ||
14:30 30mTalk | Error Localization for Sequential Effect Systems SAS 2023 Link to publication Pre-print | ||
15:00 30mTalk | Scaling up Roundoff Analysis of Functional Data Structure Programs SAS 2023 Pre-print |