混合精度矩阵乘法的 SMT 形式化：针对三个代际 Tensor Core 的建模

许多近期计算加速器提供非标准（例如降低精度）算术运算以提高浮点矩阵乘法的性能。不幸的是，这些加速器的属性并不广为人知，且缺乏对其行为的充分描述。这使得超出原始供应商的工具构建者难以正确针对或模拟硬件，或让算法设计者对自己的代码充满信心。为了填补这一差距，先前的研究通过手动构建的测试来探测这些单元的行为。此类测试繁琐且难以设计，且随着加速器的演进需要重复的手动工作。我们为 Nvidia 的 Volta、Turing 和 Ampere GPU 的 Tensor Core 提供了形式化模型。我们确定了特定属性——舍入模式、精度和累加顺序——驱动这些核心的行为。我们对这些属性进行形式化建模，然后使用该形式化模型自动生成能说明不同机器差异的判别输入。我们的结果确认了先前 tensor core 研究的许多发现，但也识别出一些细微的不一致。特别是，Nvidia 的机器并不像之前报告的那样使用 round-to-zero 进行累加，其 5 项累加器需要 3 个额外的进位位才能实现完全精度。使用我们的形式化模型，我们分析了两个现有的算法，这些算法使用半精度 tensor core 来加速带有误差校正的单精度乘法。我们的分析表明，较新设计为在某些输入下比第一个算法更不准确。