> ## Documentation Index
> Fetch the complete documentation index at: https://docs.theformalera.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Races and overflows, without a GPU

> Four kernels with schedule- and shape-dependent defects, caught on a machine with no visible GPU in 5.7 s.

Some GPU bugs only appear on some shapes, some inputs, or some schedules. This run verifies four such kernels with `CUDA_VISIBLE_DEVICES=''`, so no GPU is visible:

```text theme={"system"}
$ python -c 'import torch; print("GPUs visible:", torch.cuda.device_count())'
GPUs visible: 0
$ time theformalera verify kernels/unsafe_samples.py
 kernel                       spec node                 configs   result    level / id     time
 ──────────────────────────────────────────────────────────────────────────────────────────────
 silu_mul_fp16_exp            layers[*].mlp.act             0/1   FAILED    F-0005         24ms
 silu_mul_int32_index         layers[*].mlp.act             0/1   FAILED    F-0006         56ms
 rmsnorm_unmasked_store       layers[*].input_norm          0/1   FAILED    F-0007         2.1s
 residual_overlapping_tiles   layers[*].attn_residual       0/1   FAILED    F-0008         2.6s

0 passed · 4 failed · 0 unknown        run `theformalera explain F-0005`

real	0m5.734s
```

![With zero GPUs visible, theformalera verify fails all four kernels in 5.7 seconds; explain shows an int32 overflow for T=61682 and a write-write conflict](https://mintcdn.com/n-a-24de7f09/RKvaTncjzKh3Uq1K/images/screenshots/case3-unsafe-overflow-no-gpu.png?fit=max\&auto=format\&n=RKvaTncjzKh3Uq1K\&q=85\&s=9f54af298df3972aedadd04d2b5c60b5)

| Kernel | Defect | Verdict |
| - | - | - |
| `silu_mul_fp16_exp` | Sigmoid as `e^g / (1 + e^g)` with `e^g` cast to fp16: `e^g` is infinite for `g > 11.09`, and inf / inf is NaN | OVERFLOW, 24 ms |
| `silu_mul_int32_index` | `row * (2 * I)` in int32 wraps for long prefills | OVERFLOW, 56 ms; `correct only when T <= 61681` |
| `rmsnorm_unmasked_store` | The store is not masked: lanes 5120–8191 write into the next row, racing the program that owns it | UNSAFE, 2.1 s |
| `residual_overlapping_tiles` | Tiles advance by `BLOCK - 64` but are `BLOCK` wide: neighbouring programs write the same 64 elements | UNSAFE, 2.6 s |

```text theme={"system"}
$ theformalera explain F-0006
F-0006  OVERFLOW  silu_mul_int32_index -> Qwen/Qwen3.8-27B@1.0:layers[*].mlp.act
failing configs    1 of 1
witness            T=61682                  int32 overflow of `%g` for T=61682
correct only when  T <= 61681
```

```text theme={"system"}
$ theformalera explain F-0008
F-0008  UNSAFE  residual_overlapping_tiles -> Qwen/Qwen3.8-27B@1.0:layers[*].attn_residual
failing configs    1 of 1
witness (minimal)  T=1                      write-write conflict on `Y` at element offset 960 (program (1, 0, 0)):
                   address already written by program 0
```

## How they are found

* **Integer overflow** is checked with an SMT solver over the **whole** shape domain, not by sampling. That is how the exact boundary `T = 61682` comes out.
* **Float overflow** uses interval analysis over the declared value domain (bf16 activations, `|x| ≤ 65504`).
* **Races and out-of-bounds accesses** are found by an instrumented interpreter that records every address every program touches. A race shows up as two programs writing the same address, deterministically, whatever the schedule.

On a GPU, the unmasked store produces correct or wrong output depending on which program happens to run last. On a CPU, the verifier reports it every time.


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.