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")

ebnf & parser of PTX from sdk 13.4

Observing raw data from previous part we can conclude that many (17) new attributes were inserted in middle of indices table thereby shifting the indices. And even worse - they were inserted in many arbitrary places. So instead of patching long-suffering script iptx.pl I made its clone iptx3.pl (DRY, yeah)

After some brute-forcing & RE I was able to identify 130 attributes masks - so still unknown 8. Given that at least 6 of them describe semantics of instruction - actually only 2 indices currently unknown:

• 13:5 for spdecompress
• 17:0 for tensormap.replace
  

EBNF

5246 lines vs 4460 from old version

Intrinsics

I wrote script to compare them. No new instrinsics but 3 were removed:

• __cuda_sm20_div_rn_ftz_f32
• __cuda_sm20_div_rn_f32
• __cuda_sm20_div_rn_noftz_f32_slowpath
  

See raw data in files ptx_intr.txt & ptx134_intr.txt

Expanded macros

Data

Seems that all newly added PTX instructions actually implemented as macros and expanding to calls of __nv_ptx_builtin_ocg_XXX. Unfortunately I was unable to find those functions inside ptxas, and in RT kernels too. Some (like fabricXXX) described here

 

However we always can generate ptx and examine what it actually compiles into:
__HIR0X1C0.8.U2.2TO4.X4 R0, R8, R8, UR4 ;

It's funny that sample for spdecompress from official doc doesn't even compile. And for trace.marks too. I wonder — has even one of the many morons on Twitter, who keep posting this document as if it were the official nvidia assembler manual, actually tried verifying anything in it?

Parser

New data from iptx3.pl -C