{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:13Z","timestamp":1750220053965,"version":"3.41.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>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.  \nThe 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.  \nThe 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.<\/jats:p>","DOI":"10.1145\/3571253","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"1740-1769","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Taking Back Control in an Intermediate Representation for GPU Computing"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3173-8636","authenticated-orcid":false,"given":"Vasileios","family":"Klimis","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3886-7657","authenticated-orcid":false,"given":"Jack","family":"Clark","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0178-1983","authenticated-orcid":false,"given":"Alan","family":"Baker","sequence":"additional","affiliation":[{"name":"Google, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4326-5896","authenticated-orcid":false,"given":"David","family":"Neto","sequence":"additional","affiliation":[{"name":"Google, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6735-5533","authenticated-orcid":false,"given":"John","family":"Wickerson","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7448-7961","authenticated-orcid":false,"given":"Alastair F.","family":"Donaldson","sequence":"additional","affiliation":[{"name":"Imperial College London, UK \/ Google, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Ullman","author":"Aho Alfred V.","year":"2007","unstructured":"Alfred V. Aho , Monica S. Lam , Ravi Sethi , and Jeffrey D . Ullman . 2007 . Compilers, Principles, Techniques & Tools, Second Edition. Pearson . Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2007. Compilers, Principles, Techniques & Tools, Second Edition. Pearson."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694391"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.1993.394061"},{"key":"e_1_2_1_4_1","unstructured":"Apple. 2022. Metal Shading Language.  https:\/\/developer.apple.com\/metal\/ \t\t\t\t  Apple. 2022. Metal Shading Language.  https:\/\/developer.apple.com\/metal\/"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0019410"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837637"},{"key":"e_1_2_1_7_1","unstructured":"Sean Baxter. 2020. Khronos Group forum post: Clarify meaning of merge block. https:\/\/community.khronos.org\/t\/clarify-meaning-of-merge-block\/106006 \t\t\t\t  Sean Baxter. 2020. Khronos Group forum post: Clarify meaning of merge block. https:\/\/community.khronos.org\/t\/clarify-meaning-of-merge-block\/106006"},{"key":"e_1_2_1_8_1","unstructured":"Sean Baxter. 2021. Tweet about SPIR-V control flow. https:\/\/twitter.com\/seanbax\/status\/1348780718797807622 \t\t\t\t  Sean Baxter. 2021. Tweet about SPIR-V control flow. https:\/\/twitter.com\/seanbax\/status\/1348780718797807622"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3363562"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_16"},{"key":"e_1_2_1_12_1","unstructured":"David Neto. 2022. SPIR-V samples for WebGPU.  https:\/\/github.com\/dneto0\/spirv-samples \t\t\t\t  David Neto. 2022. SPIR-V samples for WebGPU.  https:\/\/github.com\/dneto0\/spirv-samples"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133917"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454092"},{"key":"e_1_2_1_15_1","unstructured":"Jason Ekstrand. 2022. In defense of NIR. https:\/\/www.jlekstrand.net\/jason\/blog\/2022\/01\/in-defense-of-nir\/ \t\t\t\t  Jason Ekstrand. 2022. In defense of NIR. https:\/\/www.jlekstrand.net\/jason\/blog\/2022\/01\/in-defense-of-nir\/"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701618"},{"volume-title":"Advanced Metaprogramming in Classic C++","author":"Gennaro Davide Di","key":"e_1_2_1_17_1","unstructured":"Davide Di Gennaro . 2015. Advanced Metaprogramming in Classic C++ . Apress . Davide Di Gennaro. 2015. Advanced Metaprogramming in Classic C++. Apress."},{"key":"e_1_2_1_18_1","unstructured":"Google. 2022. Amber Repository.  https:\/\/github.com\/google\/amber \t\t\t\t  Google. 2022. Amber Repository.  https:\/\/github.com\/google\/amber"},{"key":"e_1_2_1_19_1","unstructured":"Google. 2022. ANGLE - Almost Native Graphics Layer Engine.  https:\/\/chromium.googlesource.com\/angle\/angle \t\t\t\t  Google. 2022. ANGLE - Almost Native Graphics Layer Engine.  https:\/\/chromium.googlesource.com\/angle\/angle"},{"key":"e_1_2_1_20_1","unstructured":"Google. 2022. The clspv project.  https:\/\/github.com\/google\/clspv \t\t\t\t  Google. 2022. The clspv project.  https:\/\/github.com\/google\/clspv"},{"key":"e_1_2_1_21_1","unstructured":"Google. 2022. Dawn a WebGPU implementation.  https:\/\/dawn.googlesource.com\/dawn \t\t\t\t  Google. 2022. Dawn a WebGPU implementation.  https:\/\/dawn.googlesource.com\/dawn"},{"key":"e_1_2_1_22_1","unstructured":"Google. 2022. SwiftShader CPU-based Vulkan Implementation.  https:\/\/swiftshader.googlesource.com\/SwiftShader \t\t\t\t  Google. 2022. SwiftShader CPU-based Vulkan Implementation.  https:\/\/swiftshader.googlesource.com\/SwiftShader"},{"key":"e_1_2_1_23_1","unstructured":"Google. 2022. The Tint project.  https:\/\/dawn.googlesource.com\/tint \t\t\t\t  Google. 2022. The Tint project.  https:\/\/dawn.googlesource.com\/tint"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_16"},{"key":"e_1_2_1_25_1","volume-title":"Platform","volume":"01","year":"2020","unstructured":"Intel. 2020 . Intel Iris Plus Graphics and UHD Graphics Open Source, Programmer\u2019s Reference Manual For the 2019 10th Generation Intel Core Processors based on the \u201cIce Lake \u201d Platform , Volume 2a. https:\/\/ 01 .org\/sites\/default\/files\/documentation\/intel-gfx-prm-osrc-icllp-vol02a-commandreference-instructions_2.pdf Intel. 2020. Intel Iris Plus Graphics and UHD Graphics Open Source, Programmer\u2019s Reference Manual For the 2019 10th Generation Intel Core Processors based on the \u201cIce Lake\u201d Platform, Volume 2a. https:\/\/01.org\/sites\/default\/files\/documentation\/intel-gfx-prm-osrc-icllp-vol02a-commandreference-instructions_2.pdf"},{"key":"e_1_2_1_26_1","unstructured":"Intel. 2022. Mesa 3D Graphics Stack Repository.  https:\/\/gitlab.freedesktop.org\/mesa\/mesa \t\t\t\t  Intel. 2022. Mesa 3D Graphics Stack Repository.  https:\/\/gitlab.freedesktop.org\/mesa\/mesa"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485497"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34117-5_1"},{"key":"e_1_2_1_30_1","unstructured":"Khronos Group. 2014. SPIR Specification Version 1.2.  https:\/\/www.khronos.org\/registry\/SPIR\/specs\/spir_spec-1.2.pdf \t\t\t\t  Khronos Group. 2014. SPIR Specification Version 1.2.  https:\/\/www.khronos.org\/registry\/SPIR\/specs\/spir_spec-1.2.pdf"},{"key":"e_1_2_1_31_1","unstructured":"Khronos Group. 2017. SPIR-V Specification Version 1.0 Revision 12. https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/1.0\/SPIRV.html \t\t\t\t  Khronos Group. 2017. SPIR-V Specification Version 1.0 Revision 12. https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/1.0\/SPIRV.html"},{"key":"e_1_2_1_32_1","unstructured":"Khronos Group. 2019. The OpenGL Shading Language Version 4.60.7.  https:\/\/www.khronos.org\/registry\/OpenGL\/specs\/gl\/GLSLangSpec.4.60.pdf \t\t\t\t  Khronos Group. 2019. The OpenGL Shading Language Version 4.60.7.  https:\/\/www.khronos.org\/registry\/OpenGL\/specs\/gl\/GLSLangSpec.4.60.pdf"},{"key":"e_1_2_1_33_1","unstructured":"Khronos Group. 2022. A complete registry of all official SPIR-V specifications. https:\/\/www.khronos.org\/registry\/SPIR-V\/ \t\t\t\t  Khronos Group. 2022. A complete registry of all official SPIR-V specifications. https:\/\/www.khronos.org\/registry\/SPIR-V\/"},{"key":"e_1_2_1_34_1","unstructured":"Khronos Group. 2022. glslang GitHub repository.  https:\/\/github.com\/KhronosGroup\/glslang \t\t\t\t  Khronos Group. 2022. glslang GitHub repository.  https:\/\/github.com\/KhronosGroup\/glslang"},{"key":"e_1_2_1_35_1","unstructured":"Khronos Group. 2022. Khronos Vulkan OpenGL and OpenGL ES conformance tests.  https:\/\/github.com\/KhronosGroup\/VK-GL-CTS \t\t\t\t  Khronos Group. 2022. Khronos Vulkan OpenGL and OpenGL ES conformance tests.  https:\/\/github.com\/KhronosGroup\/VK-GL-CTS"},{"key":"e_1_2_1_36_1","unstructured":"Khronos Group. 2022. MoltenVK a Vulkan Portability Implementation.  https:\/\/github.com\/KhronosGroup\/MoltenVK \t\t\t\t  Khronos Group. 2022. MoltenVK a Vulkan Portability Implementation.  https:\/\/github.com\/KhronosGroup\/MoltenVK"},{"key":"e_1_2_1_37_1","unstructured":"Khronos Group. 2022. OpenCL-Docs.  https:\/\/github.com\/KhronosGroup\/OpenCL-Docs \t\t\t\t  Khronos Group. 2022. OpenCL-Docs.  https:\/\/github.com\/KhronosGroup\/OpenCL-Docs"},{"key":"e_1_2_1_38_1","unstructured":"Khronos Group. 2022. SPIR-V Specification Version 1.6 Revision 1 Unified. https:\/\/web.archive.org\/web\/20220613184046\/https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/unified1\/SPIRV.pdf Also cited as . \t\t\t\t  Khronos Group. 2022. SPIR-V Specification Version 1.6 Revision 1 Unified. https:\/\/web.archive.org\/web\/20220613184046\/https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/unified1\/SPIRV.pdf Also cited as ."},{"key":"e_1_2_1_39_1","unstructured":"Khronos Group. 2022. SPIR-V Specification Version 1.6 Revision 2 Unified. https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/unified1\/SPIRV.html Also cited as . \t\t\t\t  Khronos Group. 2022. SPIR-V Specification Version 1.6 Revision 2 Unified. https:\/\/www.khronos.org\/registry\/SPIR-V\/specs\/unified1\/SPIRV.html Also cited as ."},{"key":"e_1_2_1_40_1","unstructured":"Khronos Group. 2022. SPIRV-Cross Repository.  https:\/\/github.com\/KhronosGroup\/SPIRV-Crosss \t\t\t\t  Khronos Group. 2022. SPIRV-Cross Repository.  https:\/\/github.com\/KhronosGroup\/SPIRV-Crosss"},{"key":"e_1_2_1_41_1","unstructured":"Khronos Group. 2022. SPIRV-Tools Repository including spirv-opt and spirv-val.  https:\/\/github.com\/KhronosGroup\/SPIRV-Tools \t\t\t\t  Khronos Group. 2022. SPIRV-Tools Repository including spirv-opt and spirv-val.  https:\/\/github.com\/KhronosGroup\/SPIRV-Tools"},{"key":"e_1_2_1_42_1","unstructured":"Khronos Group. 2022. Vulkan 1.3 - A Specification (with all registered Vulkan extensions).  https:\/\/www.khronos.org\/registry\/vulkan\/specs\/1.3-extensions\/html\/vkspec.html \t\t\t\t  Khronos Group. 2022. Vulkan 1.3 - A Specification (with all registered Vulkan extensions).  https:\/\/www.khronos.org\/registry\/vulkan\/specs\/1.3-extensions\/html\/vkspec.html"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7152484"},{"key":"e_1_2_1_44_1","volume-title":"Donaldson","author":"Klimis Vasileios","year":"2022","unstructured":"Vasileios Klimis , Jack Clark , John Wickerson , and Alastair F . Donaldson . 2022 . Repository containing SPIR-V control flow Alloy model and fuzzer.. https:\/\/github.com\/mc-imperial\/spirv-control-flow Vasileios Klimis, Jack Clark, John Wickerson, and Alastair F. Donaldson. 2022. Repository containing SPIR-V control flow Alloy model and fuzzer.. https:\/\/github.com\/mc-imperial\/spirv-control-flow"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737986"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_2_1_48_1","unstructured":"LLVM Compiler Infrastructure. 2022. LLVM Language Reference Manual.  https:\/\/llvm.org\/docs\/LangRef.html \t\t\t\t  LLVM Compiler Infrastructure. 2022. LLVM Language Reference Manual.  https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304043"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037723"},{"key":"e_1_2_1_51_1","volume-title":"Automatic Unbounded Verification of Alloy Specifications with Prover9. CoRR, abs\/1209.5773","author":"Macedo Nuno","year":"2012","unstructured":"Nuno Macedo and Alcino Cunha . 2012. Automatic Unbounded Verification of Alloy Specifications with Prover9. CoRR, abs\/1209.5773 ( 2012 ), 17 pages. arXiv:1209.5773. arxiv:1209.5773 Nuno Macedo and Alcino Cunha. 2012. Automatic Unbounded Verification of Alloy Specifications with Prover9. CoRR, abs\/1209.5773 (2012), 17 pages. arXiv:1209.5773. arxiv:1209.5773"},{"key":"e_1_2_1_52_1","unstructured":"Dzmitry Malyshau. 2021. Horrors of SPIR-V. http:\/\/kvark.github.io\/spirv\/2021\/05\/01\/spirv-horrors.html \t\t\t\t  Dzmitry Malyshau. 2021. Horrors of SPIR-V. http:\/\/kvark.github.io\/spirv\/2021\/05\/01\/spirv-horrors.html"},{"key":"e_1_2_1_53_1","unstructured":"Microsoft. 2019. Reference for HLSL.  https:\/\/docs.microsoft.com\/en-us\/windows\/win32\/direct3dhlsl\/dx-graphics-hlsl-reference \t\t\t\t  Microsoft. 2019. Reference for HLSL.  https:\/\/docs.microsoft.com\/en-us\/windows\/win32\/direct3dhlsl\/dx-graphics-hlsl-reference"},{"key":"e_1_2_1_54_1","unstructured":"Microsoft. 2022. DirectX Shader Compiler Repository.  https:\/\/github.com\/microsoft\/DirectXShaderCompiler \t\t\t\t  Microsoft. 2022. DirectX Shader Compiler Repository.  https:\/\/github.com\/microsoft\/DirectXShaderCompiler"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjtsldm.7.91"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371079"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360561"},{"key":"e_1_2_1_59_1","unstructured":"Philip Rebohle. 2022. DXVK.  https:\/\/github.com\/doitsujin\/dxvk\/ \t\t\t\t  Philip Rebohle. 2022. DXVK.  https:\/\/github.com\/doitsujin\/dxvk\/"},{"key":"e_1_2_1_60_1","unstructured":"Rust Graphics Mages. 2022. The Naga project.  https:\/\/github.com\/gfx-rs\/naga \t\t\t\t  Rust Graphics Mages. 2022. The Naga project.  https:\/\/github.com\/gfx-rs\/naga"},{"key":"e_1_2_1_61_1","unstructured":"Mark Segal and Kurt Akeley. 2022. OpenGL 4.6 Core Profile.  https:\/\/www.khronos.org\/registry\/OpenGL\/specs\/gl\/glspec46.core.pdf \t\t\t\t  Mark Segal and Kurt Akeley. 2022. OpenGL 4.6 Core Profile.  https:\/\/www.khronos.org\/registry\/OpenGL\/specs\/gl\/glspec46.core.pdf"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485508"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268577"},{"key":"e_1_2_1_64_1","unstructured":"W3C. 2022. WebGPU Shading Language W3C Working Draft.  https:\/\/www.w3.org\/TR\/WGSL\/ \t\t\t\t  W3C. 2022. WebGPU Shading Language W3C Working Draft.  https:\/\/www.w3.org\/TR\/WGSL\/"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2998503"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009838"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062379"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571253","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571253","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":68,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571253"],"URL":"https:\/\/doi.org\/10.1145\/3571253","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}