Show HN: Cuq – Formal Verification of Rust GPU Kernels
4 months ago
- #formal verification
- #Rust
- #GPU programming
- Cuq是一个框架，通过将Rust的MIR（中级中间表示）翻译成Coq并与PTX内存模型关联，来形式化验证Rust GPU内核的语义。
- 尽管Rust GPU代码能够编译为PTX或SPIR-V，但目前尚不存在其形式化语义。
- 该项目旨在为MIR的一个子集定义机械化操作语义，并证明在编译到PTX时内存模型的正确性。
- 关键目标包括验证内核级属性，例如避免发散屏障同步以及符合PTX一致性模型。
- 该框架提供了一个原型工具链，用于将Rust-CUDA内核转换为Coq术语并与PTX证明接口。
- 未来扩展可能会纳入Rust的所有权和生命周期推理，以实现安全性和正确性的端到端证明。