一句话:首次系统评测混合精度调优工具,量化健全静态分析与不健全动态方法在性能收益与精度保证间的权衡。
数值程序常在资源受限硬件上重复执行,降低计算精度是提升性能的有效手段,但会引入舍入误差。混合精度调优在保证整体误差可接受的前提下,为部分变量与算符分配尽可能低的精度。现有工具用健全静态分析或动态采样来验证优化后程序的精度。本文首次对浮点程序的混合精度调优工具进行综合评测,定量比较健全静态方法与不健全动态方法,衡量性能收益、优化潜力与精度健全性保证之间的权衡,即“健全性的代价”。基于 FPBench 基准的实验推翻了“动态优化器总能生成更快程序”的常见看法:对小型直线数值程序,加入 regime inference 的健全工具能匹敌甚至优于动态方法,同时提供形式化正确性保证,代价是优化时间增加;而独立的健全工具过于保守,精度约束紧时尤甚;动态工具对不同目标始终有效,但超出最大允许误差最多达 9 个数量级。
Numerical code is often executed repetitively and on hardware with limited resources, which makes it a perfect target for optimizations. One of the most effective ways to boost performance—especially in terms of runtime—is by reducing the precision of computations. However, low precision can introduce significant rounding errors, potentially compromising the correctness of results. Mixed-precision tuning addresses this trade-off by assigning the lowest possible precision to a subset of variables and arithmetic operations in the program while ensuring that the overall error remains within acceptable bounds. State-of-the-art tools validate the accuracy of optimized programs using either sound static analysis or dynamic sampling. While sound methods are often considered safer but overly conservative, and dynamic methods are more aggressive and potentially more effective, the question remains: how do these approaches compare in practice? In this paper, we present the first comprehensive evaluation of existing mixed-precision tuning tools for floating-point programs, offering a quantitative comparison between sound static and (unsound) dynamic approaches. We measure the trade-offs between performance gains, utilizing optimization potential, and the soundness guarantees on the accuracy—what we refer to as the cost of soundness . Our experiments on the standard FPBench benchmark suite challenge the common belief that dynamic optimizers consistently generate faster programs. In fact, for small straight-line numerical programs, we find that sound tools enhanced with regime inference match or outperform dynamic ones, while providing formal correctness guarantees, albeit at the cost of increased optimization time. Standalone sound tools, however, are overly conservative, especially when accuracy constraints are tight; whereas dynamic tools are consistently effective for different targets, but exceed the maximum allowed error by up to 9 orders of magnitude.