浮点数清理器 (FpSan)

FpSan 是一种编译器插桩模式，它将选定的浮点 Triton IR 运算重写为基于整数位模式的确定性“载荷代数”(payload algebra)。它的目标不是近似 IEEE 浮点算术。相反，它保留了特定的代数结构，使得在清理后的语义下符号等价的内核能够保持一致，同时错误的重写、错误的运算数、错误的数据流或缺失的同步往往会扰动结果。

这使得 FpSan 主要成为一种内核检查工具。当您更关心内核是否保留了预期的符号计算，而非其在特定输入上的确切 IEEE 结果时，它特别有用。

概括来说，FpSan 会：

• 将浮点位模式映射到整数载荷域

• 用整数域重写替代受支持的浮点运算，以精确保留特定的恒等式

• 将结果载荷映射回浮点位模式，以便流水线的其余部分可以继续运行

启用 FpSan

在进行编译或运行之前启用 FpSan 以进行插桩。

从 Python 启用

import triton

triton.knobs.compilation.instrumentation_mode = "fpsan"
# compile and run kernels here
triton.knobs.compilation.instrumentation_mode = ""

从 Shell 启用

TRITON_INSTRUMENTATION_MODE=fpsan python your_script.py

注意事项

• FpSan 是一项编译器功能，因此不适用于解释器模式。

• 在 AMD 平台上，后端目前仅为 gfx942、gfx950 和 gfx1250 启用 FpSan。

如何使用

使用 FpSan 最有效的方法是在相同的 FpSan 模式下比较两个内核，或同一个内核的两个版本。典型用途包括：

• 比较优化后的内核与简单的参考内核

• 比较融合内核与非融合组合

• 比较数学上应等价的两个调度变体

• 检查累加器选择、谓词或 TMEM 流水线是否保留了预期的载荷流

FpSan 的结果只能与其它 FpSan 结果进行比较，不能与普通的浮点输出进行比较。

载荷模型

对于每个浮点宽度 w，FpSan 定义了浮点位模式与 w 位整数载荷之间的双射；算术运算按 2^w 取模。

概念上：

• embed(x) 将浮点位模式映射为整数载荷

• unembed(u) 将整数载荷映射回浮点位模式

• 清理后的浮点运算实现为 unembed(F(embed(...)))

嵌入的选择是经过深思熟虑的，以保证一些重要的常量保持稳定：

• embed(+0.0) = 0

• embed(+1.0) = 1

• embed(-1.0) = 全 1

这些固定点使得诸如 x + 0 = x 和 x * 1 = x 等恒等式在 FpSan 下能自然成立。

FpSan 保留的内容

FpSan 保留了每次重写所选载荷代数中的精确恒等式。最重要的包括：

• 环恒等式（用于加法、减法、乘法、FMA 和点积类累加）

• 针对 exp 和 exp2 的选定指数恒等式（详情见下文）

• 针对 sin 和 cos 的三角恒等式

• 通过类型转换、加载、存储和复制保留载荷相等性

• 为尚无更丰富代数模型的一元函数提供确定性的运算区分标签

这正是 FpSan 对内核检查具有价值的原因：如果两个内核在所保留的属性下应是相同的符号计算，它们就应产生相同的载荷。这建立在一个（普遍认为成立的）超验数论猜想即 Schanuel 猜想的基础上。FpSan 的作者之一有一篇[博文](https://cp4space.hatsya.com/2026/05/03/schanuels-conjecture-and-the-semantics-of-fpsan/)，从数学角度解释了 FpSan 背后的理论。

FpSan 不保留的内容

FpSan 不是 IEEE 模拟器。

特别地，请不要依赖它进行：

• 真实的浮点排序、舍入、NaN 传播、无穷大、次正规数或异常处理

• 针对 log、sqrt、erf、floor、ceil、rsqrt 及类似带标签一元运算的真实超验语义

• 预期的浮点位模式（例如用于在浮点数和整数之间进行 bitcast 的内核）

当某个属性对您的检查很重要时，正确的问题是：“这个属性在特定运算族的载荷重写中被保留了吗？”

常用算术运算

加、减、乘

支持的操作：

• x + y

• x - y

• x * y

重写：

• 对嵌入的载荷进行加、减或乘，然后将结果取消嵌入 (unembed)

精确保留的属性：

• x + 0 = x

• x - 0 = x

• x - x = 0

• x * 1 = x

• 加法和乘法的结合律与交换律

• 乘法对加法的分配律

重要提示：

• 这是模 2^w 的环算术，而非 IEEE 算术。

最小值和最大值

支持的操作：

• tl.minimum(x, y)

• tl.maximum(x, y)

• Triton 代码中的 min(x, y) 和 max(x, y)

重写：

• 在载荷上执行有符号整数的 min 或 max

精确保留的属性：

• 幂等性：min(x, x) = x 且 max(x, x) = x

• 交换律

• 结合律

重要提示：

• 排序方式是载荷的有符号整数顺序，而非 IEEE 浮点顺序。

• 不模拟 NaN 处理和精确的带符号零契约。

除法

支持的操作：

• x / y

重写：

• x / y 变为 embed(x) * inv(embed(y))，然后进行 unembed

其中 inv 为：

• 奇数载荷的真模逆元

• 偶数载荷的保持奇偶性的对合 (involution)

精确保留的属性：

• x / 1 = x

• 1 / (1 / x) = x

• 对于奇数载荷，常规模逆元法则成立

重要提示：

• 对于所有载荷，不保证 x / x = 1。

• 除以零不会产生 IEEE 无穷大或陷阱。

• 选择此重写是为了代数检查，而非数值真实性。

取余

支持的操作：

• x % y

重写：

• 在通过 den | 1 强制分母为奇数后，对载荷执行有符号整数取余

精确保留的属性：

• 相同的输入产生相同的清理后取余载荷

重要提示：

• 不模拟真实浮点取余语义。

• 分母为零会被有意映射到一个安全的奇数载荷，而不是触发陷阱。

FMA

支持的操作：

• tl.fma(a, b, c)

重写：

• 载荷算术中的 a * b + c

精确保留的属性：

• 与清理后的展开式（mul 紧接着 add）精确一致

• 在载荷环中 fma(a, b, c) = a*b + c

重要提示：

• 没有特殊的融合舍入行为。

一元数学运算

exp2

支持的操作：

• tl.exp2(x)

重写：

• 载荷空间中由固定奇数生成元的模幂运算

精确保留的属性：

• exp2(x + y) = exp2(x) * exp2(y)

• exp2(0) = 1

• exp2(-x) = 1.0 / exp2(x)

exp

支持的操作：

• tl.exp(x)

重写：

• exp(x) 在载荷空间中实现为 exp2(x * rcp_log2)

精确保留的属性：

• exp 在将输入乘以一个固定的内部载荷常量后，使用与 exp2 相同的载荷空间构建方式

sin 和 cos

支持的操作：

• tl.sin(x)

• tl.cos(x)

重写：

• 为了保留下述恒等式而选择的确定性载荷空间重写

精确保留的属性：

• sin(x + y) = sin(x) * cos(y) + cos(x) * sin(y)

• sin(x - y) = sin(x) * cos(y) - cos(x) * sin(y)

• cos(x + y) = cos(x) * cos(y) - sin(x) * sin(y)

• cos(x - y) = cos(x) * cos(y) + sin(x) * sin(y)

• cos(x)^2 + sin(x)^2 = 1

重要提示：

• 这些不是 IEEE 三角函数值；它们是为了保留上述角度恒等式而选择的载荷函数。

带标签的一元运算

支持的操作：

• tl.log(x)

• tl.log2(x)

• tl.sqrt(x)

• tl.rsqrt(x)

• tl.erf(x)

• tl.floor(x)

• tl.ceil(x)

• 精确平方根变体

重写：

• 可逆载荷标签：乘以一个奇数常量，与运算特定的哈希异或，然后再乘以另一个常量

精确保留的属性：

• 对于相同的运算，保留载荷相等性：如果载荷空间中 x == y，则 op(x) == op(y)

• 不同的受支持一元运算获得不同的标签

重要提示：

• 这些重写刻意不保留诸如 sqrt(x)^2 = x 或 log(x*y) = log(x) + log(y) 等真实的数学恒等式。

类型转换与格式转换

浮点到浮点转换

支持的操作：

• 使用 x.to(dtype) 在浮点类型之间转换张量

• 隐式浮点宽化和窄化转换

重写：

• 载荷空间中的有符号整数扩展或截断，随后进行 unembed

精确保留的属性：

• 0、+1 和 -1 在转换中保持稳定

• 载荷域中的符号扩展行为

• 截断会丢弃高位载荷位

• 先向上转换再向下转换是恒等映射

重要提示：

• 这保留了载荷结构，而非 IEEE 转换语义。

• 相同宽度的浮点类型之间的转换不模拟任何精度或范围损失，因此，例如在 fpsan 下 fn(a.to(tl.float16)).to(tl.bfloat16) == fn(a) (对于任何 bfloat16 的 a)。

压缩 fp4 转换

重写：

• 从源字节张量解包低位和高位半字节 (nibble)

• 重塑并重新排序它们

• 将每个解包的半字节直接解释为目标浮点宽度的载荷

精确保留的属性：

• 压缩 fp4 存储的确定性解包

• 精确保留解包后的半字节载荷

重要提示：

• 这并非真正的 fp4 数值解码。

• 缩放点积路径也对 e2m1 重复使用了相同的原始载荷解释。

纯外部逐元素运算

支持的操作：

• 当且仅当满足以下所有条件时，对 tl.extern_elementwise 执行操作：

  • 该运算是 pure (纯函数) 的

  • 结果类型是浮点类

  • 至少有一个运算数

  • 每个运算数都是数值型的

重写：

• 根据参数索引循环移位每个运算数的载荷

• 对移位后的载荷求和

• 将结果与符号名称的稳定哈希值异或

• 取消嵌入

精确保留的属性：

• 对所有运算数及运算数顺序的确定性依赖

• 不同外部符号之间的确定性区分

• 支持混合浮点和整数运算数；浮点运算数被嵌入，整数运算数在进行有符号转换为结果宽度后直接使用

重要提示：

• 这是一个结构标签，而非外部函数的数值模型。

Gluon MMA 和张量内存

支持的 Gluon 操作包括：

• mma_v2

• warpgroup_mma 和 warpgroup_mma_wait

• tcgen05_mma 和 tcgen05_mma_scaled

• tcgen05_copy 和 tcgen05_commit

• allocate_tensor_memory

• 张量内存描述符方法，例如 load、load_min、load_max、store、slice、index 和 _reinterpret

• AMD mfma、mfma_scaled、wmma、wmma_scaled 和 scaled_upcast

重写：

• 在载荷空间中执行乘加累加

• 在张量内存加载、存储、复制和视图操作中保留载荷位

• 使累加器选择和谓词行为在结构上可见

精确保留的属性：

• 载荷环上的精确矩阵乘法代数

• 与清理后的标量乘加展开式精确一致

• 与所提供的累加器的累加被保留为载荷加法

• 张量内存操作在流水线中保留载荷流

重要提示：

• Scaled MMA 保留了清理器对低精度运算数和缩放因子的载荷处理，而非精确的硬件格式数值解码。

• 张量内存操作保留载荷数据流；它们不能使 FpSan 替代竞态或同步检查。

• 目前 fpsan 在所有 NVIDIA 硬件以及 AMD gfx942、gfx950 和 gfx1250 上受支持。

检查的实践指南

FpSan 非常适合用于检查：

• 两个内核是否实现了相同的保留代数

• 融合内核是否保持了预期的数据流

• 谓词或累加器选择逻辑的连接是否正确

• 张量内存或 warp 专用流水线是否保留了载荷流

FpSan 不适合用于检查：

• IEEE 边界情况

• 真实的超验函数精度

• NaN 或无穷大行为

• 低精度格式的硬件格式解码语义

简而言之，依靠 FpSan 进行结构保留的内核验证，依靠普通数值测试进行 IEEE 行为验证。