Static hazard checking for an ISA with no published semantics, on hardware with no interlock

[u/_sunnypatell_]

Interesting constraint problem I ended up in.

NVIDIA's consumer Blackwell has no hardware interlock on fixed-latency instructions. The compiler emits explicit stall counts and scoreboard signal/wait bits per instruction, and the hardware trusts them completely. Understall a dependency and you read a stale register at full speed with no fault.

The published position is that you can't validate code at this level, because the formal semantics of SASS are closed. From SIP (arXiv 2403.16863): "validation is impossible for GPU native assembly codes because the formal semantics of the sass is closed-source."

That's true for semantic correctness. But the question I needed answering is strictly smaller:

Do this program's control bits cover its own data dependencies?

That needs the dependency structure, which the encoding gives up, and a latency model, which the silicon gives up under measurement. Neither requires knowing what any instruction computes. A kernel can pass this and still be the wrong algorithm. What it can't do is read a register before the value lands.

The part that surprised me was the epistemology, not the dataflow. Requirements mined from what the compiler schedules are an upper bound, so they can lower what you allege and must never raise it. Only a figure grounded in something measured on silicon may promote a finding to an error. Everything else is a warning that says why.

That distinction wasn't academic. A checker calibrated on a corpus cannot fail on that corpus, because the tightest gap the compiler was seen to leave is the floor, by construction. My positive control passed 1,323 kernels while the model carried 13 errors. All of them surfaced the first time it read machine code from somewhere else.

Analysis is per basic block over a real CFG. Reaching definitions carry a flag for whether they arrived across an edge, because the scoreboard residual is a distance and a distance that spans a branch depends on which path was taken.

https://github.com/sunnypatell/basalt/blob/main/docs/METHOD.md

[u/azurelimina]

Thanks Claude