ptxsim: a PTX interpreter and verification toolkit for the NVPTX compiler backend

ptxsim executes NVIDIA PTX on any CPU, with no GPU and no CUDA driver. It is used here as the execution engine for three ways of verifying LLVM's NVPTX backend (the open-source compiler path from LLVM IR to PTX):

1. Differential fuzzing. A random generator produces LLVM IR kernels that are free of undefined behaviour. Each one is compiled to PTX by 7 different pipelines (O0–O3, Os, sm_70, sm_86), every PTX file is executed in ptxsim, and the outputs are compared.
2. Automatic test-case reduction. Any mismatch is shrunk to a minimal program by delta debugging over the generator's AST.
3. SMT translation validation (Alive2-style). Two compilations of the same kernel are executed symbolically and Z3 is asked whether any input makes them differ. It either proves equivalence or produces a concrete counterexample, which ptxsim then replays to rule out a modelling bug.

 irgen.py ──► LLVM IR (16 kernels) ──► NVPTX backend × 7 pipelines ──► PTX ──► ptxsim (C++) ──► per-kernel hash
 (UB-free,       O0 O1 O2 O3 Os                                        │     memcheck / racecheck / synccheck
  swarm)         O3/sm_70  O2/sm_86                                    ▼
                                                     mismatch ──► reduce.py (ddmin on AST) ──► 1-line repro
 tv.py: symbolic PTX executor → Z3:  O0 ≡ O3 ?   unsat = proof   sat = counterexample ──► replayed in ptxsim

ptxsim (src/ptxsim.cpp, ~1.2k lines of C++17)

• Execution model: Volta-style independent thread scheduling.
  • Every thread has its own program counter and runs until it reaches a warp-synchronous instruction.
  • shfl.sync (up/down/bfly/idx, with clamp and segment-mask semantics from the PTX ISA) and vote.sync (ballot/any/all/uni) fire once every lane in the membermask has arrived.
  • bar.sync releases once every live thread in the CTA has arrived.
• Memory: global, shared, local (the per-thread stack) and param state spaces, with generic addressing through cvta / cvta.to.
• Instruction subset: integer and f32/f64 arithmetic, mul.hi/.wide, mad, div/rem, and the clamped PTX shift semantics. Also setp with .and/.or/.xor, selp, popc, clz, brev, prmt, bfe, shf (funnel), min/max/sad, cvt, vector ld/st, and predication.
• Built-in checks, similar to compute-sanitizer:
  • out-of-bounds accesses in every state space
  • shared-memory data races between barriers
  • deadlocks, e.g. __syncthreads in divergent code
  • shuffles that read a lane outside the membermask, and exited lanes named in a mask
  • reads of uninitialised registers
  • operand type errors: the module is rejected, as ptxas does
• Self-tests: the hand-written PTX kernels from cuda-compiler-verify give the same results as on an A100. That includes rejecting the deliberately ill-typed module.

The fuzzer (fuzz/)

Generated kernels are integer-only and free of undefined behaviour and poison by construction:

• Divisions are guarded with select.
• Shift amounts are masked to 0–31.
• No nsw/nuw flags are used.
• Shared memory follows a write-own-slot / barrier / read-neighbour / barrier pattern.
• shfl.sync and vote.sync are emitted only where the generator can prove all 32 lanes are converged. That rules out thread-dependent branches and data-dependent loops, whose bounds are re-evaluated only by the lanes still looping.

Each kernel enables a random subset of 12 features (swarm testing, Groce et al. ISSTA'12).

Results (Apple-silicon MacBook, 10 cores; clean 15-minute campaign)

Kernels generated, each compiled under 7 pipelines	47,392 (20,734 NVPTX compilations, 331,744 simulated kernel launches of 512 threads, 66M lines of generated PTX)
Throughput	≈ 3,100 kernels/min on 8 worker processes
Distinct PTX opcodes exercised	129
Mismatches after the simulator fixes below	0
Planted miscompilation (off-by-one magic constant in division-by-constant lowering)	caught in 54% of the batches where it was planted (115/213); every report isolated the injected build, and the reducer shrank one report from 310 AST nodes to v2 |= v3 / 641u in 25 tests

An earlier 20-minute run reported 112 mismatches in 7 batches. These were an artifact: I rebuilt ptxsim mid-campaign, so those batches mixed two binaries. Re-checking all 112 with a single binary gave 0 differences, and the campaign above was run without touching the binary.

Bugs found. Both were in the simulator; each was reduced automatically to a one-line kernel and is now a regression test:

1. 16-bit mul.hi with a negative immediate.
   • LLVM's known-bits analysis proved v5 % 1000 fits in 16 bits, so it lowered the following % 10 with 16-bit magic-number division: mul.hi.u16 %rs2, %rs1, -13107.
   • The simulator handled only 32- and 64-bit mul.hi, and did not truncate the immediate.
   • Reduced repro: for (i<2) v5 *= (v5 % 1000) % 10; (250 → 5 AST nodes in 32 tests).
2. Sign-extending sub-word loads.
   • At O0, LLVM lowered v1 >> 24 (arithmetic) to a load of the top byte with ld.s8.
   • The simulator truncated the result to 8 bits instead of sign-extending it into the 32-bit register.
   • Reduced repro: v4 *= (v1 >>s 24); (132 → 4 AST nodes in 21 tests).

One observation that is not a bug. At O2, LLVM speculates guarded integer divisions: it computes rem.s32 with a possibly-zero divisor and then discards the result. This is legal in PTX, where division by zero does not trap and only yields an unspecified value, even though it would be undefined behaviour in LLVM IR. The sanitizer counts these instead of reporting them.

Translation validation

tv.py symbolically executes PTX:

• Branches with symbolic conditions fork the path.
• Loads through selp-selected stack pointers at O0 are split per case.
• Results are merged into ITE terms, and Z3 checks O0(x) ≠ O3(x) for all inputs x and all thread ids.

query	result
v0 = (v2 >>s (sel(v5 >u tid, v1, v3) & 31)) ^ v0, O0 vs O3	proved equivalent for all inputs
v2 |= v3 / 641 with the planted bug, O2 vs O2_injected	counterexample found in < 1 s (thread 0, concrete input words); replaying it in ptxsim reproduced exactly the same two differing outputs
64 random loop-free kernels (40 single-statement + 24 multi-statement), O0 vs O3	7 proved equivalent, 0 counterexamples, 56 solver timeouts (10–15 s), 1 unsupported
the same kernels with the planted bug, O2 vs O2_injected	10 of 14 caught, each with a counterexample confirmed by ptxsim replay; 4 timeouts

The model was validated against ptxsim. Its first SAT result was spurious: the O0 code loads through a selp.b64 pointer, which the model did not handle. Replay caught this automatically. It is why every counterexample is replayed: two independent implementations of PTX semantics check each other.

Usage

make                                    # build/ptxsim
make test                               # self-tests + regression tests
build/ptxsim selftest ptx               # hand-written PTX: vadd, warp_reduce, invalid-module rejection
python3 fuzz/campaign.py --minutes 10 --out campaigns/main
python3 fuzz/campaign.py --minutes 2 --inject-bug --out campaigns/selftest
python3 fuzz/reduce.py --seed <kernel seed> --a O0 --b O2
python3 fuzz/tv.py --count 25           # translation validation O0 vs O3

Requirements: a C++17 compiler, Python 3.9+, llvmlite (bundles LLVM with the NVPTX backend), z3-solver.

Limitations

• PTX subset: it covers what LLVM emits for integer kernels plus basic f32/f64 arithmetic. There are no textures, atomics, tensor-core (mma) instructions, or floating-point transcendentals.
• Data races: threads in a CTA are scheduled run-until-block, so the outcome of a racy program can differ from hardware. Races are reported, not reproduced.
• Translation validation scope: loop-free, thread-local kernels only. Division- and multiplication-heavy formulas often reach the solver timeout ("unknown").
• LLVM version: the NVPTX backend is LLVM 14, the version bundled by llvmlite.