sbinabdullah opened a new pull request, #19978:
URL: https://github.com/apache/tvm/pull/19978

   ## Summary
   
   The "tighter bounds using modular set" fast path in 
`ConstIntBoundAnalyzer`'s `Mod`/`FloorMod` visitors normalizes the modular-set 
base with `base % modulus` instead of `base % gcd(coeff, modulus)`. When the 
base is not already smaller than the gcd, this produces an **invalid bound with 
`min_value > max_value`**.
   
   Example (free `int64` n):
   
   ```python
   analyzer.const_int_bound((n * 320 + 255) % 256)
   # before: ConstIntBound(min_value=255, max_value=191)   <- min > max
   # after:  ConstIntBound(min_value=63,  max_value=255)
   ```
   
   The true value set is `{63, 127, 191, 255}`: since `gcd(320, 256) = 64`, the 
dividend satisfies `a == 255 == 63 (mod 64)`, so `floormod(a, 256)` can only 
take values `63 + 64k`.
   
   ## Why it matters (miscompilation, not just precision)
   
   The invalid bound makes `Analyzer::CanProve(..., kSymbolicBound)` "prove" 
the bounds predicate of imperfect dynamic loop splits. For example, after 
`sch.fuse()` of `T.grid(n, 5, 64)` and `sch.split(..., factors=[None, 256])`, 
the predicate
   
   ```
   bx*256 + tx < n*320
   ```
   
   was deemed provable (the symbolic-bound path reduces it to 
`const_int_bound((n*320 + 255) % 256 - 254).min_value >= 1`, which the broken 
`[255, 191]` bound satisfies), so `split()` silently **dropped the `T.where` 
predicate**. Any kernel scheduled through dlight `gpu.Fallback` with a dynamic 
fused extent then ran without an out-of-bounds guard.
   
   Downstream, this corrupted the paged-KV cache on WebGPU: the unguarded 
`tir_kv_cache_transpose_append` kernel's excess threads read `position_map` 
past `ntoken` (zero-initialized memory returns `0`, not the `-1` sentinel) and 
overwrote page 0 / slot 0 of the KV cache with stale data on every decode, 
breaking multi-sequence decoding.
   
   ## Fix
   
   Normalize the residue modulo the gcd:
   
   - `FloorMod` (divisor > 0): result is in `{r, r + g, ..., modulus - g + r}` 
with `r = base % g` normalized to `[0, g)`.
   - Truncated `Mod`: same set on the non-negative side; when the dividend can 
be negative, mirror the residue set (`r' = (g - r) % g`) on the negative side.
   
   ## Testing
   
   - New regression cases in `tests/python/arith/test_arith_const_int_bound.py` 
(`TestModBoundWithModularSet`) covering the floormod case above, the truncmod 
mixed-sign / non-negative-dividend cases, and the original `base = 0` example 
from the code comment.
   - `tests/python/arith` passes (964 passed); `tests/python/s_tir/schedule -k 
"split or fuse"` and `tests/python/s_tir/dlight` pass.
   - Verified end-to-end that `sch.fuse` + imperfect `sch.split` on a dynamic 
extent emits the `T.where` bounds predicate again, and that the recompiled 
WebGPU kernel contains the bounds guard.
   


-- 
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

To unsubscribe, e-mail: [email protected]

For queries about this service, please contact Infrastructure at:
[email protected]


---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]

Reply via email to