Skip to main content
The kernel is paged decode attention for the 16 Gated Attention layers of Qwen3.8-27B: one program per (sequence, query head), keys and values read page by page through the block table (page size 16), with an online softmax. It counts pages like this:
kernels/attn_decode.py
It should round up. The tokens of a partial last page are never read.

​
The differential test passes

Random bf16 inputs on an RTX 4090, compared with a float64 PyTorch reference at the conventional lengths:
pytest output: four differential tests pass at sequence lengths 128, 512, 1024 and 2048
Every length is a multiple of 16, so the bug never triggers. Other lengths do trigger it: seq_len = 1 gives NaN, 17 gives an error of 0.73, 100 gives 0.20. And seq_len = 2047 still passes allclose: one missing token in 2047 stays inside the tolerance.

​
The verifier rejects it, on a CPU, in 2.5 s

theformalera verify reports FAILED F-0001, and explain shows the witnesses, the failing region seq_len % 16 == 0 and the suspect line
correct only when seq_len % 16 == 0 explains why the tests passed. The suspect line names the expression to change and the expected one.

​
And the repro confirms it on the GPU

The generated repro script prints a max abs diff of 0.426 for seq_len 17 and nan for seq_len 1

​
What to take away

  • A test that samples inputs can only show the bug on the inputs it samples. The verifier searches the whole shape domain and reports the failing region.
  • No GPU is needed to find the bug, only to look at it.
  • After the fix (tl.cdiv(seq_len, PAGE_SIZE)) the counterexample is gone. The kernel is UNKNOWN rather than PROVED, because paged online-softmax proofs are not wired in yet. See Limitations.