一句话：对 NVIDIA PTX 内存模型进行公理化建模、Alloy 测试与 Coq 机器验证，证明其可作为 CUDA 等语言的可靠编译目标。
本文首次对 NVIDIA PTX 虚拟 ISA 的官方内存一致性模型进行形式化分析。PTX 是弱序模型，提供带作用域的同步原语，但不要求无数据竞争，因此规则更复杂。作者将公开文档的英文规范改写为公理化模型，给出类似 OpenCL 的作用域 C++ 模型到 PTX 的同步原语映射，并用 Alloy 关系建模工具测试映射正确性；随后在 Coq 中编译模型与映射，对任意规模程序证明映射的可靠性。分析表明，新一代 PTX 内存模型尽管此前世代存在问题，仍可作为 CUDA 等 GPU 编程语言的可靠编译目标。
This paper presents the first formal analysis of the official memory consistency model for the NVIDIA PTX virtual ISA. Like other GPU memory models, the PTX memory model is weakly ordered but provides scoped synchronization primitives that enable GPU program threads to communicate through memory. However, unlike some competing GPU memory models, PTX does not require data race freedom, and this results in PTX using a fundamentally different (and more complicated) set of rules in its memory model. As such, PTX has a clear need for a rigorous and reliable memory model testing and analysis infrastructure. We break our formal analysis of the PTX memory model into multiple steps that collectively demonstrate its rigor and validity. First, we adapt the English language specification from the public PTX documentation into a formal axiomatic model. Second, we derive an up-to-date presentation of an OpenCL-like scoped C++ model and develop a mapping from the synchronization primitives of that scoped C++ model onto PTX. Third, we use the Alloy relational modeling tool to empirically test the correctness of the mapping. Finally, we compile the model and mapping into Coq and build a full machine-checked proof that the mapping is sound for programs of any size. Our analysis demonstrates that in spite of issues in previous generations, the new NVIDIA PTX memory model is suitable as a sound compilation target for GPU programming languages such as CUDA.