ACL2 邂逅 GPU：在 ACL2 中形式化基于 CUDA 的可并行全源最短路径算法

随着图形处理器（GPU）能力的提升和 GPU 开发环境的成熟，开发人员越来越多地利用 GPU 来卸载主机 CPU 上数值密集且可并行的计算任务。现代 GPU 拥有数百个核心，并提供双精度浮点运算甚至有限递归等编程便利。然而，从 CPU 到 GPU 的转变引发了一个问题：我们如何知道这些新的基于 GPU 的算法是正确的？为了探索这一新的验证前沿，我们在 ACL2 中对一个可并行的加权图全源最短路径（APSP）算法进行了形式化，该算法最初使用 NVIDIA 的 CUDA 语言编写。ACL2 规范使用单线程对象（stobj）和尾递归编写，因为 stobj 与尾递归的组合能够从命令式编程语言进行最直接的翻译，并在 ACL2 内部生成高效、可扩展的可执行规范。APSP 算法的 ACL2 版本可以处理数百万个顶点和边，几乎不产生垃圾回收，其执行速度是用 C 语言编写的主机版 APSP 的六分之一，对于定理证明器而言这是一个非常可观的结果。除了形式化 APSP 算法（其核心使用 Dijkstra 最短路径算法）外，我们还提供了原始 APSP 代码所缺乏的功能，即最短路径恢复。路径恢复是通过一个实现后进先出（LIFO）栈的辅助 ACL2 stobj 完成的，并已证明其正确性。作为实验的结论，我们将 APSP 内核的 ACL2 版本移植回 C 语言，导致性能下降不到 5%；此外还进行了部分反向移植到 CUDA，出乎意料地带来了轻微的性能提升。