一句话：将 PTX 与 Vulkan 一致性模型集成到 Dartagnan，实现首个可分析真实 GPU 代码的多模型验证工具，并发现原模型两处缺陷。
CPU 系统的一致性保证经过三十余年研究已有较扎实的理解，而 GPU 在这方面仍明显不足。随着通用 GPU 编程的流行，Nvidia 与 Khronos 分别形式化了 PTX 和 Vulkan 一致性模型，为程序正确性问题提供了精确答案，但这些模型难以被普通开发者解读，现有工具支持也不充分。本文的工作是把 PTX 与 Vulkan 一致性模型翻译并集成进验证工具 Dartagnan，使其成为首个能够分析真实 GPU 代码、且同时支持多种 GPU 一致性模型的分析工具。在验证翻译后的模型过程中，作者还发现了原始 PTX 与 Vulkan 一致性模型中存在的两个缺陷，说明该统一分析路径既能提升工具可用性，也有助于检验工业模型本身。
After more than 30 years of research, there is a solid understanding of the consistency guarantees given by CPU systems. Unfortunately, the same is not yet true for GPUs. The growing popularity of general purpose GPU programming has been a call for action which industry players like Nvidia and Khronos have answered by formalizing their Ptx and Vulkan consistency models. These models give precise answers to questions about program's correctness. However, interpreting them still requires a level of expertise that escapes most developers, and the current tool support is insufficient. To remedy this, we translated and integrated the Ptx and Vulkan models into the Dartagnan verification tool. This makes Dartagnan the first analysis tool for multiple GPU consistency models that can analyze real GPU code. During the validation of the translated models, we discovered two bugs in the original Ptx and Vulkan consistency models.