一句话：为 SPIR-V 结构化控制流建立形式模型，据此修正规范、校验工具，并用模型引导的模糊测试发现 20 个编译器缺陷。
本文报告了将轻量级形式化方法应用于工业标准 GPU 中间表示 SPIR-V 的经验，重点重构其结构化控制流的定义。作者给出的形式模型首先揭示了 SPIR-V 规范中控制流定义存在的多处歧义与不必要的复杂性；随后与规范作者合作推动修订，最新版规范已采纳这套重新定义的控制流规则。作者还用该模型交叉校验支持 SPIR-V 的开发者工具与一致性测试套件，在提升工具与测试质量的同时也改进了模型本身。最后，他们提出一种由形式模型驱动的编译器模糊测试新方法，用于检测误编译缺陷，并在 Google、Khronos Group、Intel 与 Mozilla 的 SPIR-V 编译器中发现了 20 个此前未知的独立缺陷。该工作展示了形式化建模与分析技术对工业标准语言设计与实现的切实影响。
We describe our experiences successfully applying lightweight formal methods to substantially improve and reformulate an important part of Standard Portable Intermediate Representation SPIRV, an industry-standard language for GPU computing. The formal model that we present has allowed us to (1) identify several ambiguities and needless complexities in the way that structured control flow was defined in the SPIRV specification; (2) interact with the authors of the SPIRV specification to rectify these problems; (3) validate the developer tools and conformance test suites that support the SPIRV language by cross-checking them against our formal model, improving the tools, test suites, and our models in the process; and (4) develop a novel method for fuzzing SPIRV compilers to detect miscompilation bugs that leverages our formal model. The latest release of the SPIRV specification incorporates the revised set of control-flow definitions that have arisen from our work. Furthermore, our novel compiler-fuzzing technique has led to the discovery of twenty distinct, previously unknown bugs in SPIRV compilers from Google, the Khronos Group, Intel, and Mozilla. Our work showcases the practical impact that formal modelling and analysis techniques can have on the design and implementation of industry-standard programming languages.
@article{paperbot2078,
title = {Taking Back Control in an Intermediate Representation for GPU Computing},
author = {Vasileios Klimis and Jack Clark and Alan Baker and David Neto and John Wickerson and Alastair F. Donaldson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571253}
}