🚀 如果形式化验证能让 GPU kernel 既更安全又更快，会怎样？

介绍 SentryWard——一个面向 GPU kernel 的开源形式化验证器。👁⚡ https://t.co/CZYsi7wfuu

你能信任 AI 生成的 GPU Kernel 吗？SentryWard 来了

作者： Mengdi Wu · Sreeram Vennam · Stephen Mell · Advay Kadam · Ziwei Zhou · Xinhao Cheng · Oded Padon · Zhihao Jia

我们分析了来自热门库的 85 个 GPU kernel，发现其中 32 个存在潜在的数据竞争、同步 bug 或资源生命周期违规。

随着 AI 编码代理越来越多地生成和优化 GPU kernel，确保其正确性正成为一项关键挑战。

现代 GPU kernel 使用异步内存传输、tensor core 和复杂的同步原语来最大化性能。一个缺失的 barrier 或一个顺序错误的异步操作，就可能导致静默的数据损坏、死锁或崩溃。

棘手的地方在于：这些 bug 可能隐藏在极少被触发的执行调度中。 一个 GPU kernel 可能通过 100,000 个测试，但在并发操作以不同顺序执行时，仍然产生错误结果或死锁。

🧿 介绍 SentryWard：一个开源的 GPU kernel 形式化验证工具。

与传统测试（采样执行调度）不同，SentryWard 在给定的配置和硬件模型下，从数学上推理所有可能的执行调度。

它可以自动验证：

✅ 同步安全性： 检测错误的 barrier 使用和潜在死锁。

✅ 数据竞争自由： 证明对全局内存、共享内存和 tensor 内存的并发访问顺序正确。

✅ 资源生命周期安全性： 捕获对已释放的 tensor 内存或 barrier 的非法访问。

✅ 数学正确性： 证明与 PyTorch 参考实现的等价性。

SentryWard 分析编译后的 NVIDIA PTX，并支持高级 GPU 特性，包括 TMA、异步 tensor-core 操作和 mbarrier。

⚡ 令人意外的是，形式化验证还能让 GPU kernel 更快！

我们发现，无论是 AI 代理还是人类专家，在编写 warp-specialized kernel 时都倾向于过度保守，引入了不必要的同步和等待，从而限制了性能。

SentryWard 将此转化为一个优化机会。

与其盲目移除同步并祈祷测试依然通过，我们可以系统地移除等待，然后形式化验证修改后的 kernel 是否仍然无竞争且正确。 如果验证成功，就保留该优化；否则，恢复同步操作。

我们在 NVIDIA B200 GPU 上的结果：

🔥 在特定输入配置下，我们评估的 kernel 中 42% 的同步操作可以安全移除（https://sentryward.io/results/）。

🔥 kernel 速度最高提升 1.4 倍，仅仅通过移除不必要的等待，而无需改变底层计算。

这展示了形式化验证的一个强大新角色：不仅能证明 GPU kernel 的正确性，还能支持那些原本风险太高的激进性能优化。

🚀 迈向全自动、经过验证的 GPU Kernel 优化

我们的愿景是实现一个全自动的 GPU 性能优化工作流：

AI 代理 → 生成 Kernel → 形式化验证 → 修复与优化 → 循环迭代

AI 代理可以积极地探索 kernel 优化方案，包括移除不必要的同步，而 SentryWard 则形式化验证生成的 kernel 在指定配置和模型假设下保持正确。

形式化验证可以将 GPU kernel 优化从试错转变为一个系统化的、正确性驱动的过程。

随着 AI 代理使 GPU kernel 生成越来越触手可及，我们相信形式化验证将成为 GPU 编程工作流中不可或缺的一部分。

不要只是测试你的 GPU kernel。证明它们正确，并让它们更快。

🔬 博客： https://sentryward.io/blog/

💻 代码： https://github.com/gpu-verifier/sentryward

📊 结果： https://sentryward.io/results/

▶️ 演示： https://sentryward.io/demo/