The 2023 POPL paper 'Taking Back Control in an Intermediate Representation for GPU Computing' formalised SPIR-V's structured control flow in the Alloy modelling language, used the model to cross-check Khronos's official validator (spirv-val) and the Vulkan Conformance Test Suite, and introduced 'CFG fleshing' — turning randomly generated skeleton control-flow graphs into self-checking SPIR-V programs whose recorded execution paths expose compiler bugs (20 found across production implementations, and the paper's 'structural dominance' definition was adopted into the SPIR-V specification). The paper itself listed three avenues for future work. The avenue of formalising further SPIR-V aspects — above all its scoped, relaxed memory model — remains open; the avenue of fleshing strategies incorporating thread-barrier synchronisation remains open beyond the artifact's simple same-path barriers; and the avenue of applying CFG fleshing to other CFG-based IRs has been substantially advanced for decompilers by FuzzFlesh (ECOOP 2025), which explicitly left general-purpose compilers as future work. This problem asks the solver to close the surviving open core: (C1) a mechanised, cross-checked formalisation of the SPIR-V/Vulkan memory model; (C2) fleshing strategies for barrier-synchronised, genuinely divergent threads with sound oracles and deadlock-freedom; and (C3) an evidence-backed determination of whether CFG fleshing can effectively test compilers for other CFG-based representations, of which general-purpose compilers are the identified open core. Each component is to be resolved either by substantiated results or by a rigorous infeasibility argument.

Background

GPU computing and SPIR-V. Modern GPUs are programmed through shader and compute languages (GLSL, HLSL, WGSL, OpenCL C) whose source is compiled to SPIR-V (Standard Portable Intermediate Representation - V), the industry-standard intermediate representation (IR — the compiler-internal program form between source language and machine code) defined by the Khronos Group. SPIR-V modules are consumed by Vulkan and WebGPU implementations: vendor drivers (NVIDIA, AMD, Intel), the open-source Mesa stack, and translators such as SPIRV-Cross, Naga, and DXC. Bugs in these SPIR-V consumers — crashes and, worse, miscompilations (silently producing wrong results) — affect every application built on these APIs.

Structured control flow and the 2023 POPL paper. Unlike most IRs, SPIR-V does not permit arbitrary control flow: every conditional branch and loop must carry a 'merge' instruction (OpSelectionMerge or OpLoopMerge) declaring where diverged control re-converges; validity of these constructs was defined in the specification via dominance (block A dominates B if every path from the program entry to B passes through A) plus ad-hoc side conditions. The paper by Klimis, Clark, Baker, Neto, Wickerson, and Donaldson (POPL 2023) formalised these rules as an Alloy model — Alloy being a declarative modelling language whose Analyzer performs bounded, SAT-based search for model instances — capturing control-flow-graph (CFG) validity in 26 predicates. It introduced 'structural dominance' (a strengthening of dominance under which the merge structure forces reconvergence at the declared merge block), redefined the specification's rules on that basis, and this redefinition was adopted into the official SPIR-V specification, version 1.6 revision 2. The model was cross-checked against spirv-val (Khronos's official SPIR-V validator) and the Vulkan Conformance Test Suite (CTS — Khronos's official suite of tests that conformant implementations must pass), exposing disagreements in both directions, and the model can generate both valid and invalid example modules.

CFG fleshing. The same paper introduced a compiler-fuzzing technique called control-flow-graph fleshing. A 'skeleton' CFG satisfying the model's validity constraints is generated by the Alloy Analyzer; 'fleshing' then turns the skeleton into an executable, self-checking SPIR-V program: each conditional branch reads one element of an input 'directions' array to decide which way to go, and every basic block appends its identifier to an output array, so the program records the path actually executed. A host-side oracle (the mechanism that decides pass/fail without a reference implementation) compares the recorded path against the path dictated by the program's source-level semantics; any mismatch is a miscompilation, and any crash is a crash bug. Three modes were evaluated: basic (via loads/stores), phi-based (via phi instructions — the static single assignment, SSA, mechanism that selects a value according to which predecessor block executed), and independent-paths (distinct threads of a workgroup — the group of GPU threads that share a barrier — following distinct paths). A months-long campaign applied these modes to 400 skeletons mined from the Vulkan CTS and 2,499 Alloy-generated skeletons, and found 20 bugs (8 miscompilations, 12 crashes) across Mesa, SwiftShader, MoltenVK, an NVIDIA driver, SPIRV-Cross, Naga, and DXC.

Barriers and the memory model — the two aspects left open. (a) Synchronisation: OpControlBarrier forces all threads of a workgroup to wait until every thread has arrived; if threads reach a barrier different numbers of times ('barrier divergence'), execution can hang. The static check that rejects programs that could cause this, uniformity analysis, is an active research topic (the WebGPU standard mandates it, and its first comprehensive formal treatment appeared only in 2026). (b) Memory: the SPIR-V/Vulkan memory model is a scoped, relaxed memory model: its prose rules combine happens-before ordering (the partial order established by synchronisation and other ordered operations) with memory scopes (device, workgroup, subgroup, invocation — the visibility range an operation is guaranteed to) and storage classes. Unlike the structured-control-flow rules, these rules have, to date, no mechanised formalisation.

Post-2023 landscape. FuzzFlesh (ECOOP 2025, Gorzynski and Donaldson) transferred CFG-based program generation — explicitly inspired by the SPIR-V work — to testing decompilers (tools that recover source-like code from binaries) for Java bytecode, .NET assembly, and x86, finding 12 bugs; it states that its implementation is unlikely to find bugs in mainstream compilers without further work, because compilers decline to optimise very complex control flow. Ratte (ASPLOS 2025) fuzzes MLIR (a framework for defining compiler IR 'dialects') for miscompilations using composable semantics rather than fleshing. The WGSL uniformity analysis work (2026) gives the WebGPU shading language an operational semantics and formal uniformity rules in the formalise-and-cross-check style, and SIMT-Step (2026) gives an operational semantics for GPU subgroup (warp) execution, mechanised in the TLA+ formal specification language; neither formalises the SPIR-V/Vulkan memory model nor generates fleshed tests. DarthShader (2024) fuzzes WebGPU shader translators by combining intermediate-representation and abstract-syntax-tree mutations with generated and imported shader seeds — a different technique from fleshing. The 2023 artifact itself ships simple barrier support (barriers only along a single common path, or on distinct paths constrained to execute every barrier block an identical number of times), which the paper's evaluated campaign modes did not use.

Problem Statement

Objective. The 2023 POPL paper established a three-step methodology for a chosen aspect of SPIR-V: (i) formalise it in a machine-checkable model; (ii) cross-check the model against official tooling — the validator spirv-val and the Vulkan Conformance Test Suite (CTS) — and feed discrepancies back into the specification; and (iii) use the model to drive CFG fleshing, a randomised, self-checking fuzzing campaign against production compilers. It applied this methodology to structured control flow. The problem is to extend the methodology to the aspects the paper left open.

C1. Memory-model formalisation and cross-checking. Provide a mechanised formalisation of the SPIR-V/Vulkan memory model — the scoped, relaxed memory semantics specified in prose in the Vulkan and SPIR-V specifications, combining happens-before ordering, memory scopes (device, workgroup, subgroup, invocation), storage classes, and atomic memory ordering semantics — in a machine-checkable formalism of the solver's choice (a bounded model finder in the spirit of the original Alloy model, or a proof-assistant or model-checker formalisation, for example in Alloy, Isabelle/HOL, Coq/ROCq, or TLA+ — all being tools that check claims mechanically rather than by prose argument). The formalisation must be precise enough to distinguish valid from invalid executions and to generate example programs (litmus tests — small programs designed to expose whether particular reorderings or visibility behaviours are allowed), and must be cross-checked against official artefacts of the ecosystem: spirv-val's rules for memory-model instructions where applicable, the Vulkan CTS memory-model tests, and the behaviour of reference implementations on generated litmus tests. Deliver a systematic account of agreements and disagreements, documenting genuine errors or ambiguities in the specification or tooling, reproducing for the memory model what the 2023 work achieved for structured control flow.

C2. Barrier-aware fleshing. Extend CFG fleshing with genuinely synchronisation-aware strategies: generation of self-checking SPIR-V programs in which threads of a workgroup execute barrier-synchronised but genuinely divergent control flow. This must go beyond the artifact's existing constrained forms, in which barriers appear only along a single common path, or on distinct paths restricted to execute every barrier block an identical number of loop iterations. Required elements: (a) a generation strategy for per-thread paths whose loop-iteration counts at barriers are controlled rather than merely constrained equal, so that tests exercise interesting synchronisation-dependent control flow; (b) an argument that the runtime path-recording oracle remains sound once synchronisation introduces shared state that couples thread executions; (c) an argument for deadlock-freedom (absence of barrier divergence) of generated programs, or a deliberate, validated exploration of barrier-divergent programs against implementations whose semantics give barrier divergence defined meaning; and (d) an evaluation of the strategies against production SPIR-V compilers, documenting any miscompilations and crashes found.

C3. Fleshing for general-purpose compilers. Determine, with evidence, whether CFG fleshing is effective as a means for finding bugs in compilers for other CFG-based representations, following the source paper's future-work avenue; FuzzFlesh (ECOOP 2025) substantially investigated the decompiler instance, leaving general-purpose compilers — compilers whose optimisation passes transform control flow — and any other CFG-based IR compilers not covered by FuzzFlesh as the surviving open core. FuzzFlesh transferred the technique to decompilers and identified the central obstacle for compilers: programs with overly complex control flow may simply not be optimised, so tests must be complex enough to engage control-flow optimisation passes yet simple enough that optimisation is still attempted. The determination must establish, with evidence, whether CFG fleshing is effective for these compilers and by what generation-and-oracle designs.

Resolution boundary. Each of C1, C2, and C3 is to be resolved either positively — for C1, a mechanised formalisation cross-checked against official artefacts with a systematic account of agreements and disagreements, and for C2 and C3, generated tests demonstrated against production compilers with documented miscompilations or crashes — or negatively, by a rigorous impossibility or boundary argument commensurate with the full scope of the component (for example, a proof that no sound path-recording oracle exists for a well-defined class of barrier-aware programs that covers the synchronised, divergent control flow targeted by C2, a formal demonstration that the memory model's semantics cannot be usefully expressed in any machine-checkable formalism of the kinds C1 admits, or an exhaustive-generation negative result over a precisely delineated program space for the compiler instance of C3). The remaining open core of C3 is the general-purpose-compiler instance, and the open core of C2 is barrier-aware fleshing of genuinely divergent synchronised threads; the decompiler instance is already substantially covered by FuzzFlesh. The three components are scientifically interdependent — C1's formalisation is the natural semantic backdrop for C2's oracle-soundness argument, and C2 and C3 are two instances of the same generation-plus-oracle design question — and together they define the single objective: extending the model-cross-check-flesh methodology beyond structured control flow.

References

  1. Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, Alastair F. Donaldson. Taking Back Control in an Intermediate Representation for GPU Computing. Proceedings of the ACM on Programming Languages, 7(POPL), pages 1740-1769, 2023 (POPL 2023). DOI: 10.1145/3571253. https://doi.org/10.1145/3571253 (open access, CC-BY 4.0; author-hosted full text: https://www.doc.ic.ac.uk/~afd/papers/2023/POPL.pdf)
  2. Vasileios Klimis, Jack Clark, Alan Baker, David Neto, John Wickerson, Alastair F. Donaldson. Artifact for 'Taking Back Control in an Intermediate Representation for GPU Computing' (POPL 2023). Zenodo, published 2022-10-05. DOI: 10.5281/zenodo.7152484. https://doi.org/10.5281/zenodo.7152484 — https://zenodo.org/records/7152484
  3. mc-imperial/spirv-control-flow — 'Formal modelling of SPIR-V control flow using Alloy', the source repository of the POPL 2023 artifact, including the Alloy model (AlloyModel/StructuredDominanceCFG.als) and the fleshing implementation (fleshing/fleshout.py). https://github.com/mc-imperial/spirv-control-flow
  4. Amber Gorzynski, Alastair F. Donaldson. FuzzFlesh: Randomised Testing of Decompilers via Control Flow Graph-Based Program Generation. 39th European Conference on Object-Oriented Programming (ECOOP 2025), LIPIcs vol. 333, pages 13:1-13:26, 2025. DOI: 10.4230/LIPIcs.ECOOP.2025.13. https://doi.org/10.4230/LIPIcs.ECOOP.2025.13 — full text: https://drops.dagstuhl.de/storage/00lipics/lipics-vol333-ecoop2025/html/LIPIcs.ECOOP.2025.13/LIPIcs.ECOOP.2025.13.html
  5. Pingshi Yu, Nicolas Wu, Alastair F. Donaldson. Ratte: Fuzzing for Miscompilations in Multi-Level Compilers Using Composable Semantics. Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2 (ASPLOS 2025), pages 966-981, 2025. DOI: 10.1145/3676641.3716270. https://doi.org/10.1145/3676641.3716270
  6. Pingshi Yu. Reasoning about MLIR Semantics through Effects and Handlers. ISSTA 2023 (NIER track), pages 1552-1554, 2023. DOI: 10.1145/3597926.3605239. https://doi.org/10.1145/3597926.3605239
  7. James Lee-Jones, John Wickerson, Alastair F. Donaldson. Uniformity Analysis in the WebGPU Shading Language. Proceedings of the ACM on Programming Languages, 10(PLDI), pages 2109-2133, 2026 (PLDI 2026). DOI: 10.1145/3808331. https://doi.org/10.1145/3808331
  8. Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen. SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior. Proceedings of the ACM on Programming Languages, 10(PLDI), pages 1253-1277, 2026 (PLDI 2026). DOI: 10.1145/3808297. https://doi.org/10.1145/3808297
  9. Lukas Bernhard, Nico Schiller, Moritz Schloegel, Nils Bars, Thorsten Holz. DarthShader: Fuzzing WebGPU Shader Translators & Compilers. arXiv:2409.01824, 2024; published at ACM CCS 2024, pages 690-704. arXiv: https://arxiv.org/abs/2409.01824 — DOI: 10.1145/3658644.3690209. https://doi.org/10.1145/3658644.3690209
  10. Vasileios Klimis, Avner Bensoussan, Elena Chachkarova, Karine Even-Mendoza, Sophie Fortz, Connor Lenihan. Shaking Up Quantum Simulators with Fuzzing and Rigour. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), pages 1400-1428, 2025 (OOPSLA 2025); tool named FuzzQ. DOI: 10.1145/3763100. https://doi.org/10.1145/3763100
  11. Vasileios Klimis, Alastair F. Donaldson, Viktor Vafeiadis, John Wickerson, Azalea Raad. Challenges in Empirically Testing Memory Persistency Models. NIER track, ICSE 2024, pages 82-86, 2024. DOI: 10.1145/3639476.3639765. https://doi.org/10.1145/3639476.3639765
  12. Hugo Devillers, Matthias Kurtenacher, Richard Membarth, Stefan Lemme, Michael Kenzel, Ömercan Yazici, Philipp Slusallek. No More Shading Languages: Compiling C++ to Vulkan Shaders. High Performance Graphics 2025 (HPG 2025), Eurographics Association. DOI: 10.2312/hpg.20251167. https://doi.org/10.2312/hpg.20251167 — https://diglib.eg.org/handle/10.2312/hpg.20251167
  13. Vasileios Klimis. Shouting at Memory: Where Did My Write Go? (Pearl/Brave New Idea). 39th European Conference on Object-Oriented Programming (ECOOP 2025), LIPIcs vol. 333, pages 41:1-41:26, 2025. DOI: 10.4230/LIPIcs.ECOOP.2025.41. https://doi.org/10.4230/LIPIcs.ECOOP.2025.41