Visible to the public Scalable yet Rigorous Floating-Point Error Analysis

TitleScalable yet Rigorous Floating-Point Error Analysis
Publication TypeConference Paper
Year of Publication2020
AuthorsDas, Arnab, Briggs, Ian, Gopalakrishnan, Ganesh, Krishnamoorthy, Sriram, Panchekha, Pavel
Conference NameSC20: International Conference for High Performance Computing, Networking, Storage and Analysis
Keywordsabstraction, Algorithmic Differentiation, compositionality, Error analysis, floating-point arithmetic, High performance computing, numerical analysis, Optimization, Predictive Metrics, pubcrawl, Resiliency, Resource management, Round-off error, Scalability, Scalable Analysis, scalable verification, symbolic execution, Tools
AbstractAutomated techniques for rigorous floating-point round-off error analysis are a prerequisite to placing important activities in HPC such as precision allocation, verification, and code optimization on a formal footing. Yet existing techniques cannot provide tight bounds for expressions beyond a few dozen operators-barely enough for HPC. In this work, we offer an approach embedded in a new tool called SATIHE that scales error analysis by four orders of magnitude compared to today's best-of-class tools. We explain how three key ideas underlying SATIHE helps it attain such scale: path strength reduction, bound optimization, and abstraction. SATIHE provides tight bounds and rigorous guarantees on significantly larger expressions with well over a hundred thousand operators, covering important examples including FFT, matrix multiplication, and PDE stencils.
Citation Keydas_scalable_2020