Scaling up Roundoff Analysis of Functional Data Structure Programs

on YouTube ↗32m

" summary

Claims a method that analyzes floating-point roundoff for loops over vectors and matrices by grouping elements by value ranges and analyzing each group once. Implements a prototype called DS tool, open source and integrated with Daisy, that evaluates 10,000–700,000-iteration benchmarks (1–1,000 ops/iter), runs median ~24× faster than a leading loop analyzer and up to 260× faster on others, with error bounds of the same order and some cases trading 2.3× less accuracy for 31× speed. once-per-range evaluation data-structure abstraction DS tool

AI-written summary · about

" chapters (21)

1. 0:00Roundoff error analysis intro
2. 1:49Loops over data structures challenges
3. 3:59Functional spec of loops and DS
4. 6:30Designing the functional domain-specific language
5. 10:08DS abstraction for analysis
6. 13:02DSL + abstractions for analysis
7. 14:09Non-numerical ops in analysis
8. 15:11Arithmetic ops and filters special cases
9. 16:35Binary ops and matrix multiplication
10. 17:37Accumulators and propagation limits
11. 18:41Fold ops optimization for scale
12. 20:07Benchmark setup and collection
13. 21:53DS tool vs state-of-the-art
14. 23:22DS abstraction impact on performance
15. 24:25Optimized folds vs unrolling
16. 25:49Key takeaways and tool availability
17. 26:52Q&A on floating-point semantics
18. 28:18Infinite loops and filters handling
19. 29:03Grouping criteria in abstractions
20. 30:51Extending to unbounded finite DS
21. 32:18Closing remarks