发表机构
University of Washington; Intel; University of Pennsylvania（华盛顿大学; 英特尔; 宾夕法尼亚大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种判定双重舍入正确性的精确条件，并基于此开发MPFX数字库，其性能显著优于MPFR，与SoftFloat相当，并用于高效模拟硬件。
AI 中文摘要
数字库在软件中实现数字格式及其算术运算，用于模拟硬件，从而使硬件行为可复现，进而可验证且更易于设计。然而，现代机器学习加速器难以模拟，因为它们越来越多地使用现有数字库不支持的专业数字格式。使用传统方法扩展这些库成本高昂：每种操作、格式和舍入模式的组合通常需要专门的实现。一种更简单的方法是双重舍入——先以更高精度计算，再重新舍入——这样，一个高精度内核就可以服务于多种格式，但双重舍入仅在特定情况下被证明是正确的。我们给出了一个精确的、可高效检查的判定条件，用于确定在多种格式和舍入模式下双重舍入何时正确。我们的结果基于一种新颖的抽象数字格式，它统一了定点表示和浮点表示，将双重舍入的正确性归结为格式包含问题：一种格式的每个值是否都能在另一种格式中表示。我们在Lean 4中机械化验证了这些结果。此外，我们提出了一种格式推断算法，给定一个操作序列，该算法用保证包含其结果的数字格式来界定每个表达式。我们将这些见解应用于两个方面。首先，我们提出了MPFX，一个正确舍入的多精度数字库，它利用正确的双重舍入来高效模拟多种数字格式。MPFX的正确舍入操作比MPFR快达11倍（平均6.05倍），并且在相同精度下与SoftFloat相当——速度在0.46倍到1.63倍之间（平均0.94倍）。其次，在一个案例研究中，我们使用SoftFloat和MPFX的原语实现了硬件规范的软件模拟；MPFX版本快达13.5倍。
英文摘要
Number libraries, which implement number formats and their arithmetic in software, are used to simulate hardware, making hardware behavior reproducible and thus verifiable and easier to design. However, modern machine learning accelerators are difficult to simulate, as they increasingly use specialized number formats that existing number libraries do not support. It is costly to extend these libraries using traditional methods: each combination of operation, format, and rounding mode typically requires a bespoke implementation. An easier way is to double round---compute at higher precision, then re-round---so that one high-precision kernel serves many formats, but double rounding is only known to be correct in select cases. We give a precise, efficiently checkable characterization of when double rounding is correct across many formats and rounding modes. Our result rests on a novel abstract number format that unifies fixed- and floating-point representations, reducing the correctness of double rounding to format containment: whether every value of one format is representable in another. We mechanized these results in Lean 4. In addition, we introduce a format inference algorithm that, given a sequence of operations, bounds each expression by a number format guaranteed to contain its result. We apply these insights in two ways. First, we present MPFX, a correctly-rounded, multi-precision number library that exploits correct double rounding to efficiently simulate many number formats. MPFX's correctly-rounded operations are up to 11x (mean: 6.05x) faster than MPFR's, and competitive with SoftFloat's---between 0.46x and 1.63x as fast (mean: 0.94x)---at the same precision. Second, in a case study, we implement a software simulation of a hardware specification using both SoftFloat and MPFX's primitives; the MPFX version is up to 13.5x faster.
