notes on PTX verification

I recently read article called "Formalizing PTX in Lean to Prove GPU Kernel Correctness". All you need for hype - gpu, ptx, lean for the Navier-Stokes equations

As is customary in such cases, there is no code, however paper contains remarkable phrase:

The interpreter implements 81 instruction forms

Just some numbers: ptxas from sdk 13.1 has has 270 unique instructions in 1420 forms, from sdk 13.4 - 291 instructions in 1669 forms. How do I know this? Well

So they covered in best case 81 / 270 = 30% of all PTX instructions, and now they’ll be shouting loudly all over the internet "software solved", "all your code belongs to us", "your entire career is now a $20/month subscription" and the rest of the obligatory misanthropic repertoire

Ok, let's examine some real projects in this field - I mean you even can check their source code

SentyWard

Parser is just blood from eyes and it is absolutely impossible to figure out which instructions and attributes it can recognize. Executor doesn't look even slightly better but from numerous

if (op == "shl"

if (In(op, {"shr", "div", "rem"})


at least we can estimate that its support of PTX is incomplete

volta

function parse_opcode looks terrible, but at least we can estimate number of supported PTX instructions: ~160 / 270 = 60%. Twice as much, but it's not enough for hype because there's no lean

cuKLEE

Strictly speaking, it can only parse PTX inline asm, and as you can see it also understands very limited number of instructions

Conclusion

There are no verification tools with full support of PTX - mainly bcs evil nvidia refuses to publish formal PTX spec (and instead of fixing bugs in official documentation prefers to release something with name "nsight-perf-sdk-for-ai")