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.