Alastair F. Donaldson

We present WGSLsmith, a tool for randomised testing of compilers for the WebGPU Shading Language (WGSL). Under the WebGPU API---now supported by all three major browsers---GPU programs are written in the WebGPU Shading Language (WGSL), and every implementation ships a WGSL compiler that validates shaders and translates them to platform-specific code. Because shaders may come from untrusted websites, these compilers can be exercised by arbitrary web pages, making them a security-critical target for testing. WGSLsmith generates random shaders to find compiler crashes and cross-implementation mismatches. We describe its architecture and usage, and how we have broadened its language feature coverage to keep up to date with the evolving WGSL specification and support features absent from the original design. We report on a campaign that uncovered 12 bugs (all confirmed, 8 fixed) in various parts of the WebGPU stack, and evaluate the thoroughness of WGSLsmith via coverage analysis.

We present repair-driven greybox fuzzing, a new approach to greybox fuzzing that combines the strengths of unstructured, byte-level input mutation and grammar-guided input generation. By increasing input diversity while preserving input validity, repair-driven fuzzing promises to improve bug-finding ability for systems under test such as programming language interpreters that consume highly structured inputs. Our idea is to first mutate an input using a standard byte-level mutator, typically leading to an invalid input, and then repair the input using a grammar. Aggressively breaking and then repairing an input provides an effective way to reach parts of the input space that would be left unexplored by both byte-level and idiomatic grammar-based mutations. We put this idea into practice via RepairFuzz, a new greybox fuzzer based on AFL++, leveraging the byte level mutations of AFL++ and using the CPCT+ error recovery algorithm for input repair. We present experiments applying RepairFuzz to six SUTs covering four programming language input formats (Lua, PHP, JavaScript and Ruby), and present an experimental comparison with AFL++, Grammarinator and Nautilus, the state-of-the-art in standard greybox fuzzing and grammar-guided fuzzing. Our evaluation shows that RepairFuzz was able to find 13 confirmed bugs that were previously unknown, including 9 that were not found by AFL++, Grammarinator or Nautilus. Further, RepairFuzz yields absolute increases in code coverage for several SUTs and substantial complementary code coverage across all.

The WebGPU programming model brings general-purpose GPU programming to the web, allowing untrusted JavaScript to issue parallel workloads to client GPUs. To ensure reliability, WebGPU mandates uniformity analysis —a static check that rejects programs that could cause barrier divergence , a GPU control-flow error that can hang execution and require OS-level recovery. While traditional GPU models treat barrier divergence as undefined behaviour, WebGPU’s need for safety and reliability makes this unacceptable. We present the first comprehensive formal and practical study of uniformity analysis in WebGPU, identifying four key issues and making corresponding contributions: (1) Lack of definition: The analysis currently defines non-uniform programs only as those it rejects, without an independent notion of barrier divergence. We provide an operational semantics for TinyWGSL, a core calculus of the WebGPU Shading Language (WGSL), developed in consultation with WGSL specification editors and implementers. This semantics rigorously defines barrier divergence in the context of WGSL for the first time. (2) Complex specification: The current description of uniformity analysis in WGSL is lengthy and imprecise. We reformulate it via concise formal rules for TinyWGSL and argue their soundness with respect to our semantics. (3) Lack of soundness and precision: Using our semantics, we expose soundness and precision flaws in the analysis as presented in the WGSL specification. In response, we have proposed four significant changes to the specification (all accepted). (4) Testing difficulty: The complex, semi-formal definition of uniformity in the WGSL specification makes it hard to test implementations. We mechanise uniformity analysis in Alloy and use Alloy’s test generation to stress-test the Chromium implementation, revealing specification–implementation discrepancies and a bug in the Chromium implementation. Overall, our work resolves an important GPU programming problem (rigorously defining barrier divergence), brings an interesting new analysis to the attention of the PL community, and demonstrates the impact of applying formal PL techniques to an important industrial language specification.

Transactions are a key feature of database systems and isolation levels specify the behavior of concurrently executing transactions. Ensuring the correctness of isolation levels is crucial. Recently, many isolation anomalies have been found in production database systems. Checkers can be used to validate that a particular execution history conforms to a desired isolation level. However, state-of-the-art checkers cannot handle predicate operations, which are both common in real-world workloads and essential for distinguishing between the repeatable read and serializable isolation levels. In this work, we address this issue by proposing two techniques for efficient white-box checking. Our key idea is to use information, that is, easily provided by database systems to efficiently check the isolation level of a given execution history. We present the version certificate recovery technique and its associated checker Emme . Version certificate recovery is a method of recovering the version order and each operation’s version set from the database system under test. To minimise execution time, we also propose the expected serialization order technique, along with its associated checker Enne , which obviates the need to define and recover a version certificate for many serializable concurrency control protocols. We have implemented version certificate recovery for three widely used database systems—PostgreSQL, CockroachDB, and TiDB. We demonstrate that Emme is 1.2–3.6× faster than Elle, a state-of-the-art checker. When paired with the expected serialization order technique, Enne obtains a further speedup of 34–430× when checking execution histories containing predicate operations. We show that our approaches can identify invalid execution histories that cannot be detected by Elle and also show that they can find realistic bugs purposely introduced by an engineer. Finally, we create a new checker, King Cobra , by modifying Cobra, an existing black-box checker, in order to conduct an ablation study to evaluate how the performance of a black-box checker changes when provided with varying degrees of ordering information. By doing so, we highlight the fundamental role that ordering information plays in the execution time of an isolation level checker and explore the limits that this places on a truly black-box checker.

We present the concept of a question neighbourhood for systematically evaluating instruction-tuned large language models (LLMs) for code generation via a new benchmark, Turbulence. Turbulence consists of a large set of natural language question templates, each of which is a programming problem, parameterised so that it can be asked in many different forms. Each question template has an associated test oracle that judges whether a code solution returned by an LLM is correct. Thus, from a single question template, it is possible to ask an LLM a neighbourhood of very similar programming questions, and assess the correctness of the result returned for each question. This allows gaps in an LLM’s code generation abilities to be identified, including anomalies where the LLM correctly solves many questions in a neighbourhood but fails for particular parameter instantiations. We present experiments against 22 state-of-the-art proprietary and open-source LLMs, each at two temperature configurations. Our evaluation is based on three complementary scores: accuracy score, correctness-potential score, and consistent-correctness score. Our findings show that, across the board, Turbulence is able to reveal cases where LLMs do not behave in a correct and consistent manner, highlighting gaps in their reasoning ability. This goes beyond merely highlighting that LLMs sometimes produce wrong code (which is no surprise): by systematically identifying cases where LLMs are able to solve some problems in a neighbourhood but do not manage to generalise to solve the whole neighbourhood, our method provides detailed insight into the behavioural characteristics of current code-generating LLMs. We present data and examples that shed light on the kinds of mistakes that LLMs make when they return incorrect code results.