v5.0.1

kernelcheck 5.0.1 corrects figures and claims that an independent end-to-end verification of 5.0.0 found wrong, each checked again here before it changed. The verification reproduced the rest: a full rerun of campaign c1 matched the artifact byte for byte, nine mutants rebuilt matched every recorded field, and the web port's parity held. The kernels are unchanged.

Three of the twelve mutants that 3.0.0 argued equivalent are not. guard_past/gemm/32, guard_past/gemm/38 and guard_past/transpose/30 each add a pass to a tile loop, and for a dimension from 2147483617 to 2147483647, which the contract allows, that pass computes a tile offset of 67108864 * 32 in int. Run on the loops' arithmetic with -fsanitize=signed-integer-overflow, each mutant overflows at 2147483617 and at INT_MAX and no original does; wrapped, the offset is -2147483648, every guard of the pass holds, and the pass reads 2^31 elements before a view, the two tile-row mutants writing there too. guard_past/gemm/38's argument also held that a fused multiply-add never makes an accumulator -0; built against the model with m = n = 1 and products of -2^-100 and 2^-100, which underflow, the original gives -0 at k = 32 and 64 and the mutant +0. The pre-registered definition of equivalence stands, so the three become fuzzer blind spots of a sixth kind, shapes past 2^31 - 32, which no campaign reaches, since shapes stop at 2^24 and such a case needs buffers of 8 GiB or more, and which no unit test reaches either. The evaluation therefore counts 159 real defects, 9 equivalent and 3 contract-equivalent mutants: the fuzzer detected 144 of the 159 in m1 and 156 in m1-v4, and the unit tests 130 in m1. Both artifacts' classification files carry the change with the former arguments, the summaries and the tables mutant by mutant follow, and a new unit test holds gemm's exact zero sums to the sign their evaluation order gives, which shows guard_past/gemm/38's -0 against the model though not its overflow.

Two corrections concern how the figures are read. m1-v4 repeated two evaluations after the host stalled, and the pre-registration has no rule for a repeat; under the rule as written, identity/softmax/34's first attempt, in which four unrelated unit tests timed out, counts as detected by the unit tests, so in m1-v4 they detect 131 and the fuzzer alone 25, with the repeat's 130 and 26 kept beside them as a disclosed deviation. And m1-v4 measures the fixes of 4.0.0 on the very mutants whose misses they were written for, so its 156 of 159 is in-sample and cannot measure detection of defects nobody has seen; the documents and the page now say so wherever the figure appears. docs/campaign.md now states what the repository can and cannot show about when c1 first ran: the pre-registration commit precedes the results commit by 8 minutes, the commit the artifact records is read when its summary is written, and a whole run fits in that window.

The model's documentation claimed more than the model does. A barrier is identified by its call site, so threads that reach one __syncthreads() inside a helper from both branches of a divergent if are not reported; a read of unwritten shared memory is not reported itself, only filled with a NaN that shows where it reaches a checked output; shared memory is not bounds-checked; and no race is detected as such, only a result that an order the model runs changes. The README, docs/execution-model.md and the page now say this. This release also carries the hardening merged after 5.0.0: a barrier is identified by a static tag at each lexical expansion, so two calls on one line or inside nested macros are told apart; each newly executed mutant records its runner's digest and build manifest, and an evaluation refuses to resume under a different plan, campaign or driver; the class counts of the three warp helper mutants in both summaries now add up across kernels; and the page labels a shrink that ran out of budget as best-found and recovers from a failed worker or data load. Smaller fixes: a relative mutant work directory made every unit test run record no tests, because ctest writes its report relative to the build directory, and it is now resolved first; the page bundles the m1-v4 traces once instead of twice, handing the worker the minimal cases it checks; and its evidence links point at the corrected documents.

As in every release, nothing has run on a GPU: every result comes from the CPU execution model, in C++ or in the port. 219 kernel and model tests, 173 fuzzer tests, and in web/ 928 self checks and the parity check at this commit.

v5.0.0

kernelcheck 5.0.0 puts the execution model in the browser. web/ is a page that runs a TypeScript port of the CPU execution model, the six kernels with their launchers, the reference implementations, the input data, campaign generation with its extras, the canary, finite-fill and tight checks and the shrinker, in a Web Worker. It is the CPU model ported, not a GPU and not a recording: each simulated thread is a generator that yields at every __syncthreads() and warp shuffle to a port of the C++ scheduler, with its ready queue, its seeded block permutation and thread draws, 32-lane warps with every mask fault, barrier divergence, float4 alignment checks, shared memory poisoned before each block, buffers fenced at their pages, and float32 arithmetic through Math.fround with the fused multiply-add emulated to one rounding. Each of the 171 seeded mutants of m1 is a one-site switch in the port next to the line it rewrites in the CUDA source, and the self check requires every id to appear exactly once.

The port is checked against the C++ build rather than trusted. kc_fuzz_runner gained an --outputs mode that prints, for each case, the bits of its inputs, of the output its target left and of the reference, with its result through all three checks. It wrote those for 34 fixture cases covering every kernel and path, and CI's fuzz jobs write them again on Linux and macOS and compare them with the committed ones. The port reproduces the inputs and references bit for bit and every output of transpose, rmsnorm, gemm, row_sum and inclusive_scan; softmax goes through the host expf in C++ and Math.exp in the port, which round differently for a small fraction of arguments, so its outputs are held to within 4 ulp, and 41 of the 22162 differ, by at most 2 (glibc's expf and Apple's differ in the same way, on 44 of 44324 softmax outputs and references). Two NaNs compare equal unless one carries the canary, since the NaN an invalid operation produces is positive on arm64 and negative on x86-64, in both languages. C++ builds of 19 of the seeded mutants, swapped into a scratch tree one at a time, wrote the outputs of 32 more cases, among them the wrong sums of a racing reduction and the partial outputs of launches that fault, and the port leaves the same bits on 54933 of their 54935 output elements, the other two softmax's. Beyond the fixtures, the port draws the 96 cases of the smoke campaign and gives each its recorded class, gives the first failing case and the minimal case of every one of the 162 shrinks of m1-v4 the class the C++ runner recorded under its mutant, and runs all 162 shrinks again with its own shrinker: 5857 candidate cases, every one in the same order with the same class, each shrink ending at the recorded minimal case, on arm64 and on the x86-64 runners alike.

The page's fuzz panel lets a visitor pick a kernel and a seeded mutant, labelled as the planted defect it is, run the cases of campaign c2 in the order m1-v4 ran them, and watch the first failing case shrink step by step beside the trace the C++ runner recorded, with the trigger condition, and then run the kernel as it is on the same cases. The page also runs the fixtures and the 162 minimal cases in the visitor's browser. The measured results are read at build time from results/ by a script whose drift check runs in CI: c1's 60000 cases with none failing, m1 and m1-v4 with 144 and then all 156 of the real defects detected by the fuzzer and 130 by the unit tests, the 15 equivalent and contract-equivalent mutants, the width counts by the rule and by root cause (20 and 18, then 23 and 22) and the table by operator. A self check recomputes every figure the page states from the artifacts without going through the page's copy, regenerating the 30000 cases the two evaluations ran to test the width rule. The web CI job type-checks, runs the self check, bundles the page within a weight budget, runs the parity check and drives the production bundle in headless Chrome at 1440 and 390 px, failing on a console error, a request off the origin or a horizontal overflow, fuzzing a seeded mutant to its recorded minimal case and running the in-browser parity check.

As in every release, nothing has run on a GPU: every result comes from the CPU execution model, in C++ or in the port, and the device build is compiled and linked by nvcc in CI only. 216 kernel and model tests, 73 fuzzer tests, and in web/ 926 self checks and the parity check at this commit.

Correction (2026-09-29, v5.0.1): the measured results are 144 and then 156 of 159 real defects, the second in-sample, the unit tests 130 and 131 (130 with the repeated evaluation), and 9 equivalent and 3 contract-equivalent mutants; the page and the documents also narrow what the model reports (see v5.0.1).

v4.0.0

kernelcheck 4.0.0 closes the blind spots that the seeded mutant evaluation of 3.0.0 found in the fuzzer, and measures the result on the same mutants. m1 had missed 12 real defects of five kinds, and each kind is fixed in its own commit. Every case is now checked three times, stopping at the first failure: with the NaN canary as before, with every buffer filled with the finite value 2^100 instead, which a fmaxf, a comparison or a value computed from the canary cannot hide, and in a tight placement where each buffer ends on a page boundary with at most three elements of slack, so that a read past a view faults even when its value is thrown away, while every view keeps its alignment and so every kernel its code path. A campaign file can now add extras drawn from a second stream of each case, which leave every case they do not touch exactly as before: tall shapes past the 65535 tiles a grid may have in y, where transpose and gemm loop over their tile rows; a distribution of values from -128 down to just above -2^21, for softmax rows whose maximum lies far below zero; and non-finite rows that are masks of -inf at a high rate, as attention masks are. Both implementations of the input data, the runner's and the Python one, gained the new distribution and the mask and still agree bit for bit, and each new check has a planted defect in the fuzzer's own tests that only it detects.

The rerun m1-v4 was pre-registered before it ran, with the same 171 seeded mutants of the v1.0.0 kernels, the same 2000 finite and 500 non-finite cases for each kernel a mutant changes, and the same shrink budget; the cases come from campaign c2, which is c1 with the extras, and the timeout per case is three times c1's because a case now runs up to three checks. The unmutated kernels passed every one of the 15000 control cases through all three checks. The fuzzer detected 156 of the 171 mutants, against 144 in m1: every one of the 156 real defects, with no mutant lost, and none of the 12 equivalent and 3 contract-equivalent ones, which stay undetected as they must. The tight placement caught the seven discarded reads, the finite fill the two that the canary had hidden, the tall shapes the missing barrier in transpose's tile-row loop, the negative data the softmax maximum that started at zero and the masked rows the online sum that started at one. The unit tests still detect 130, so the fuzzer now catches 26 mutants they miss and they catch none it misses, and by root cause 22 of its detections trigger only when a width is not a multiple of 32. Two evaluations were repeated after the host stalled, a test discovery timeout and four unrelated unit tests killed after 1042 seconds, and their first attempts are kept in the artifact.

The runner also builds with nvcc now. Its device build copies each checked buffer, guards included, into device memory, launches the kernel there and copies everything back, so the same checks judge what the kernel left on the device; the cuda-compile CI job compiles and links it against the CUDA runtime with toolkits 12.9.1 and 13.4.1 and starts it with --version, which touches no GPU. docs/fuzzing.md describes how to run a campaign with it on a machine that has one. It has not been run on a GPU by this repository, and as before every result here comes from the CPU build under the execution model, with no timing figure published. 216 kernel and model tests and 72 fuzzer tests at this commit.

Correction (2026-09-29, v5.0.1): with three mutants argued equivalent reclassified as real defects past the fuzzer's shape limits, m1-v4's fuzzer detected 156 of 159 real defects, not all 156, an in-sample figure since the fixes were written for these mutants' misses; under the rules as pre-registered the unit tests detect 131 and the fuzzer alone 25 (130 and 26 with the repeated evaluation).

v3.0.0

kernelcheck 3.0.0 measures what the differential fuzzer of 2.0.0 can see. Campaign c1 found nothing in the v1.0.0 kernels, and a result of zero says as much about the fuzzer as about the kernels, so this release plants defects on purpose and counts how many are caught. docs/mutants.md and mutants/m1.json were committed before any mutant was generated, built or run, and fix twelve mutation operators (an off-by-one past or short of a bounds guard, a dropped tail loop, a removed __syncthreads, a narrowed shuffle mask, a shuffle loop over half a warp, a stride used as a width and a width used as a stride, a weakened condition for rmsnorm's float4 path, a wrong reduction identity, a tile or block count that rounds down, and a dropped in-place update), the rule that applies them to the v1.0.0 kernel sources one site at a time, how equivalent mutants are identified, the fuzz budget and seed, and what counts as detection. The generator reads only source text, applies each operator's regular expressions line by line inside kernel and device function bodies (or anywhere, for the launcher arithmetic), and makes one mutant per site: 171 of them across the six kernels and the warp helpers. Every one is a seeded defect in a scratch copy of the sources; none is in the kernels and none is a finding.

Each mutant was built in its own scratch tree, run against the 216 unit tests of v1.0.0 under the default and a seeded random schedule, and fuzzed with the first 2000 finite and 500 non-finite cases of c1 for every kernel it changes, the same cases for every mutant of a kernel and all of them passing on the unmutated kernels; the first failing case of each kernel was shrunk with c1's shrinker. The unmutated sources, run first as a control, passed every test and all 15000 cases. None of the mutants was stillborn and none compiled to the control's object code. The unit tests detected 130, the fuzzer 144: 128 both, 16 only the fuzzer, 2 only the unit tests and 25 neither. Of the 25, 12 are argued equivalent and 3 change only rounding within the bounds docs/testing.md derives, so of the 156 real defects the fuzzer caught 144 and the unit tests 130. The fuzzer's own catches are mostly layouts the unit tests never combine, such as a single misaligned buffer on rmsnorm's float4 path or input and output rows with different strides, and reads past a view long enough to reach the fence. By the pre-registered rule 20 of the fuzzer's detections trigger only when a width is not a multiple of 32; by root cause 18 do, the other two needing data that the wide distribution only produces on short rows.

The 12 real defects the fuzzer missed name its blind spots, in five kinds: reads outside an input view whose values are discarded, which the 1024-element guards absorb; a NaN canary that fmaxf drops or that arithmetic reproduces, so a write of it outside a view looks untouched; shapes past the grid's limit of 65535 tiles in y, which the unit tests reach and c1 does not; long softmax rows whose maximum is far below zero; and long runs of -inf with a finite maximum, as an attention mask makes. results/m1-v1.0.0/classification.json carries the argument for every mutant the fuzzer missed, and docs/mutants-m1.md lists all 171 with their detections, minimal cases and the properties every failing case shares. As before, every result comes from the CPU build under the execution model; nothing has run on a GPU, and no timing figure is published. 216 kernel and model tests and 64 fuzzer tests at this commit.

Correction (2026-09-29, v5.0.1): three of the 12 mutants argued equivalent (guard_past gemm 32, gemm 38 and transpose 30) are real defects past the fuzzer's shape limits, so 9 are equivalent and there are 159 real defects, of which the fuzzer caught 144 and the unit tests 130, not 156 (docs/mutants.md, Corrections of 2026-09-29).

v2.0.0

kernelcheck 2.0.0 adds the differential fuzz tester the repository is named for. kcfuzz, a Python package under fuzz/, generates cases for the six kernels: each dimension drawn on its own, half the time from boundary values (1, 2, 3, every power of two and every multiple of 32 up to the limit with their neighbours) and half uniformly; a row stride and an offset for every buffer, including padded strides that are not multiples of four and offsets that break 16-byte alignment; data from four distributions (uniform, normal, small integers, wide magnitudes from 2^-20 to 2^21) with -inf, +inf and NaN confined to a separately labelled class; and an execution model schedule of block order, thread order and seed. kc_fuzz_runner, a C++ executable of the same CMake build, runs one case at a time: it draws the inputs itself from a specification precise enough for another implementation to reproduce every bit, places every buffer in checked memory (whole pages fenced by 256 MiB of inaccessible address space, filled with a NaN canary everywhere but the logical input elements, so that a read outside a view carries the canary into the output, a write outside an output view or an unwritten element is found after the launch, and a far stray access ends the case's process), runs the kernel and the reference, and compares every output element under the bounds of docs/testing.md, with an allowance for subnormal softmax results and a cap on the softmax row range that the unit test data never needed. Every case runs in a process forked for it alone, so a crash is recorded with its signal, a hang as a timeout, and no case can affect the next. A failing case is shrunk toward a minimal one, each dimension through the boundary values, strides toward contiguous, offsets toward zero, data toward simple values, with the schedule held fixed, and minimal cases are grouped by kernel, failure class and triggering shape feature. The fuzzer is tested against planted defects in runner/planted.cu (a dropped tail, a wrong stride, a misaligned float4 load, an early return before a barrier, a half-warp shuffle mask, an unwritten last element, a write into padding, a write to an input, a crash and a hang), each of which it must detect and shrink to its known minimal case, and against the reference target, on which every generated case must pass.

Campaign c1 was pre-registered: campaigns/c1.json (seed 0x6b633266757a7a31, 8000 finite and 2000 non-finite cases per kernel, shrink budget 300, 20 seconds per case) was committed together with docs/campaign.md, which fixes how a failure is counted and how distinct defects are decided by root cause, before any case had run against the kernels, and neither file changed afterwards. The campaign then ran against the v1.0.0 kernel sources unmodified, with the artifact recording the sha256 of every kernel file. It found nothing: 60000 cases ran, 0 failed, 0 distinct minimal cases resulted. Every case returned ok under every schedule drawn, left every guard, padding gap and input untouched, wrote every output element and stayed within its bound; the largest ratio of error to bound over all passing elements was 0.396 for gemm and 0.219 for softmax, where the bound is twice the first-order worst case. docs/findings.md records the result, what it does and does not say, and how a finding would have been recorded; the regression corpus is empty and there are no expected failures. Every result comes from the CPU build with the kernels under the execution model; nothing has run on a GPU, and no timing figure is published.

CI gains a fuzz job on Linux x86-64 with GCC and on macOS arm64 with Apple clang that builds the runner with warnings as errors, lints and tests the fuzzer, and runs the fixed-seed smoke campaign of 96 cases against the kernels, requiring every case's class to match the recorded results/smoke/expected.json. 216 kernel and model tests and 53 fuzzer tests at this commit.

Correction (2026-09-29, v5.0.1): that no case ran against the kernels before c1 was pre-registered is the author's statement, not something the artifact shows: the repository shows only that the pre-registration commit precedes the results by 8 minutes, and the artifact's commit is read when its summary is written (docs/campaign.md).

v1.0.0

kernelcheck 1.0.0 is a library of six CUDA C++ kernels of the kind a model runtime needs: a transpose through a 32 by 32 shared memory tile padded against bank conflicts, a row softmax with one warp per row and shuffle reductions that keeps rows of up to 1024 columns in registers and takes an online pass for longer ones, an RMS normalisation that reads and writes float4 wherever every row and the weight vector are 16-byte aligned, a GEMM that walks k in 32 by 32 shared memory tiles, a row sum reduced in shared memory and finished with shuffles, and an inclusive row scan built from warp scans with block aggregation. Each launcher accepts any positive shape, row strides of at least the row length and views at any offset into larger buffers, and its header states that contract together with the kernel's launch configuration and evaluation order.

The same kernel text builds two ways. Under nvcc it compiles for the device: CI compiles every kernel and launcher for sm_80 and sm_90 with CUDA 12.9.1 and 13.4.1 in the official nvidia/cuda devel containers, with nvcc, ptxas and host compiler warnings as errors, and ptxas reports no stack frame and no spilled register for any of the 23 kernel instantiations on either architecture. Nothing in this release has been executed on a GPU. Under any other compiler the kernels compile as C++ against a CPU execution model that gives each simulated thread its own stack, switched by a short aarch64 or x86-64 routine, makes __syncthreads a barrier that every thread of the block must reach at the same call, runs the shuffle, vote and syncwarp primitives over 32-lane warps with the PTX source lane rules and their mask requirements, fills shared memory with NaN poison before every block, checks the alignment of every float4 load and store, and runs blocks and threads in order, in reverse or in an order drawn from a seed. A divergent barrier, a bad warp mask or a misaligned vector access stops the launch with a message naming the threads, lanes and call sites instead of hanging, and docs/execution-model.md lists what the model does not capture, from its sequentially consistent memory and one-block-at-a-time execution to its use of the host's floating point library.

The tests hold each kernel to a double-accumulating reference on fixed tables of model-sized shapes, in a contiguous layout and in a padded one whose rows start on 4-byte boundaries, inside buffers fenced with a NaN sentinel so that a write outside the output view or any change to an input fails the test. Transpose must match bit for bit; the other kernels are held to twice the first-order rounding error bound of their own evaluation order, derived in docs/testing.md. Transpose and GEMM also run a matrix of 2097153 rows, past the 65535 blocks a grid may have in y, softmax is checked on rows holding -inf, +inf and NaN on both of its paths, and every kernel must produce identical bits under five block and thread orders. The execution model is tested separately with toy kernels in tests/emu that exit before a barrier, split a warp's masks, read shared memory nobody wrote, load a float4 from a misaligned address and reduce without a barrier; that last one gives 15 distinct sums over 18 interleavings while its synchronised twin gives the exact 32896 under all of them. CI runs the suite with GCC 13.3 and Clang 18.1 on Linux x86-64 and with Apple clang on macOS arm64, once in the default order and once in a seeded random order. 216 tests at this commit.

Correction (2026-09-29, v5.0.1): a divergent barrier is reported when threads wait at different barrier call sites or exit before one; a single __syncthreads() inside a helper reached from both branches of a divergent if is one site and is not reported (docs/execution-model.md).