This page is generated from docs/SURFACE.toml at docs-build time; edit that file, not this page. test/host/surface.jl machine-checks the inventory against the form registry, the typed-wrapper-only rules, and the wrapper registry.
Every PTX ISA 9.4 instruction family (§9.7.1–§9.7.21) has an explicit disposition, so textual expressibility is never mistaken for reviewed coverage. The four statuses:
- strict — closed, reviewed schemas and/or typed wrappers; an unreviewed spelling fails loudly before reaching LLVM.
- generic — the chain default renders the form under a reviewed
FORMS contract (purity/convergence/brackets/return promises). - raw-only — no
FORMS entry or wrapper exists; the explicit ptx"..."raw escape hatch (maximally conservative contract) is the only route, and the entry's note states its evidence boundary. - out-of-scope — deliberately unsupported: no contract, no wrapper, and raw use is unsanctioned (unsound or structurally inexpressible as a single inline-asm call).
A status describes binding, not proof. Evidence climbs a ladder: spelled (the form renders) → assembles (ptxas accepts it, the ptxas/ tier) → executes (a live device runs it, the gpu/ tier) → numerically validated (its results are checked against a reference). Entries marked verify carry an unresolved question — see their notes.
| Section | Opcodes | Status | Notes |
|---|
| §9.7.1 | add, sub, mul, mad, mul24, mad24, sad, div, rem, abs, neg, min, max, popc, clz, brev, bfe, bfi, szext, dp4a, dp2a, clmad | 🔵 generic | Pure per-lane ALU under the generic trailing-dtype rule; the add/sub/mul/mad/div/abs/neg/min/max heads also own the floating-point (§9.7.3), half (§9.7.4), and mixed-precision (§9.7.5) variants. |
| §9.7.1 | bfind, fns, bmsk | 🟠 raw-only | Unregistered pending review: bfind's destination is always .u32 regardless of source width, so the trailing-type heuristic misreads its .u64 forms (loud ptxas reject, never a miscompile); fns and bmsk raw-render correctly and simply await a reviewed FORMS entry. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.2 | addc, subc, madc | 🟢 strict | Implicit CC.CF cannot cross an LLVM inline-asm call boundary: chain AND raw are rejected by the semantic guard; typed wrappers expose the flag explicitly or fuse the operation. The add.cc/sub.cc/mad.cc spellings live under the §9.7.1 heads and hit the same guard. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.3 | fma, copysign, rcp, sqrt, rsqrt, sin, cos, lg2, ex2, tanh | 🔵 generic | Pure per-lane FP under the generic trailing-dtype rule; add/sub/mul/mad/div/abs/neg/min/max heads are owned by the §9.7.1 entry and cover the FP forms. |
| §9.7.3.1 | testp | 🔵 generic | Pure per-lane FP property test; the tail names the SOURCE type and the destination is a predicate, so the whole opcode is audited in the structured-result ledger (12 op×type forms, no legal _ sink) instead of trailing-type inference. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.4 | — | 🔵 generic | No distinct opcode heads: add/sub/mul/fma/neg/abs/min/max/tanh/ex2 f16/f16x2/bf16 forms flow through the §9.7.1/§9.7.3 entries' FORMS contracts. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.5 | — | 🔵 generic | No distinct opcode heads: mixed-precision add/sub/fma forms flow through the §9.7.1/§9.7.3 entries' FORMS contracts. The PTX ISA 9.4 packed additions (f32x2/f16x2/bf16x2 add/sub/mul/fma, sm_107f) are deferred: their two-type tails end in an operand type, so they need audited scalar-result schemas before any chain spelling is admitted. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.6 | — | 🟠 raw-only | New family in PTX ISA 9.4: FP8/FP6/FP4 x4 packed add/sub/mul/fma (sm100a/sm103a). No distinct opcode heads — the add/sub/mul/fma heads are owned by §9.7.1/§9.7.3, but their FORMS contracts must not be extended to these dtype.atype tails without review (tail names an operand type, not the result); raw-only until the packed forms get audited two-type schemas. ptxas cannot assemble ISA 9.4 until a CUDA 13.4+ compiler artifact ships. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.7 | setp, selp | 🔵 generic | selp is pure trailing-dtype; setp's scalar/grouped predicate ABI is audited in the structured-result ledger. |
| §9.7.7 | set, slct | 🟠 raw-only | Deliberately unregistered (forms.jl header): set's dtype.stype and slct's dtype.ctype tails end in an operand type, so raw misreads the destination class whenever dtype and the tail differ (loud ptxas reject) — stays raw-only until given grammar-aware entries. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.8 | — | 🔵 generic | No distinct opcode heads: f16 set/setp forms share the §9.7.6 entries (same tail-grammar caveat for set). |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.9 | and, or, xor, not, lop3, shf, shl, shr | 🔵 generic | Pure per-lane bit ops; lop3's optional predicate-destination group is audited in the structured-result ledger. |
| §9.7.9.5 | cnot | 🟠 raw-only | Plain C-style logical negation; raw renders a correct scalar form, unregistered simply because nothing needed it yet. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.10.3 | mov | 🔵 generic | Generic scalar mov plus special-register reads (sreg"..."); mov.b128 pack/unpack is the audited B128 carrier bridge. |
| §9.7.10.6 | shfl | 🟢 strict | Convergent; plain d-destination forms are chain-generic, but the d|p grouped destination is typed-wrapper-only (the :pred selector rule) and the deprecated non-sync shfl (§9.7.9.5) is not blessed. |
| §9.7.10.7 | prmt | 🔵 generic | Pure byte-permute under the generic rule. |
| §9.7.10.8 | ld, ldu, st | 🔵 generic | Bracketed memory ops (st is a sink: the dtype tail names the value written); covers ld.global.nc, st.async (§9.7.9.12), and st.bulk (§9.7.9.14); vector and .b128 forms are audited in their ledgers, and vec_ldst typed wrappers cover the tuple API. |
| §9.7.10.15 | multimem | 🔵 generic | Multicast ld_reduce/st/red plus multimem.st.async (§9.7.9.13), multimem.red.async (§9.7.14.8), and multimem.cp bulk forms; st/red/cp prefixes are sink overrides. |
| §9.7.10.16 | prefetch | 🔵 generic | Bracketed cache-prefetch hint. |
| §9.7.10.16 | prefetchu | 🟠 raw-only | Uniform-cache prefetch; raw renders the correct no-result bracketed form, unregistered because nothing needed it yet. |
| §9.7.10.17 | applypriority | 🔵 generic | Bracketed eviction-priority hint. |
| §9.7.10.20 | discard | 🔵 generic | Bracketed cache-discard hint. |
| §9.7.10.21 | createpolicy | 🟠 raw-only | Cache-policy handle creation; raw renders the correct scalar .b64 destination, unregistered because nothing needed it yet. |
| §9.7.10.22 | isspacep | 🔵 generic | Pure per-lane state-space window query; the predicate destination and UNbracketed dual-width (u32/u64) address operand are audited in the structured-result ledger (8 space forms, no legal _ sink). |
| §9.7.10.23 | cvta | 🔵 generic | Address-space cast under the generic rule (pure: no memory access). |
| §9.7.10.24 | cvt | 🔵 generic | Destination is the penultimate type token (audited in inferrettype); source carriers for ordinary cvt and cvt.pack (§9.7.10.25) come from the closed cvt ledger, with exact wrappers for the microfloat/stochastic forms. PTX ISA 9.4 additions (ue5m3x2, scaled::n1::ue8m0, .pzo/.rz widenings; sm107f) are spelled-only until a CUDA 13.4+ ptxas ships; the n1 scale factor is physically b8, carried as b16 (no i8 constraint) — exact b8-bridging wrappers are deferred to hardware validation. |
| §9.7.10.26 | mapa | 🔵 generic | Cluster CTA address mapping — a pure address computation held at :observable (undeletable, but no memory clobber; PTX 9.4 §9.7.10.13), matching the typed wrapper's rendering; typed wrappers handle the shared::cluster addrspace bookkeeping. |
| §9.7.10.27 | getctarank | 🔵 generic | Cluster CTA-rank query (observable cross-CTA visibility, hence not pure). |
| §9.7.10.28 | cp | 🟢 strict | cp.async and the bulk/tensor forms are chain-renderable under sink overrides (the terminal type token is an operand descriptor), cp.async.bulk.prefetch.tensor is typed-wrapper-only (rank-dependent coordinate vectors plus a paired cache-hint operand), and the TMA wrappers own the tensor-copy API. The whole cp.async.bulk.tensor/prefetch wrapper family is single-route asm — the former tier-2 intrinsic route was demoted (observable async effects; the argmem-widen A/B on B200 showed the conservative clobber is codegen-free) — making the notation WYSIWYG: cluster cta_group::2 renders after the rank like the pre-existing shared::cta residue (ptxas accepts both orders). |
| §9.7.10.29 | tensormap | 🔵 generic | Sink (the type tail names the replaced field); the head also covers tensormap.cp_fenceproxy (§9.7.14.17); the tensormap PROXY FENCES live under the fence head and are typed-wrapper-only. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.11 | fabric | 🟢 strict | Hand-written asm wrappers (submit/wait/tryget/tryput, PTX 9.3 sm100+): the two-register CFT handle operand has no chain-default rendering, so :fabric is deliberately NOT in FORMS; tryred/trypullred and the cpmask/counted::bytes put forms are deferred. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.12 | tex, tld4, txq, istypep | ⚪ out-of-scope | Opaque texref/sampler operands and grouped vector destinations are inexpressible as a single scalar-constraint asm call; graphics-oriented surface not targeted by PTX.jl. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.13 | suld, sust, sured, suq | ⚪ out-of-scope | Opaque surfref operands and grouped vector destinations, same boundary as §9.7.11; not targeted by PTX.jl. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.14 | ret, exit | 🔵 generic | Terminal sinks with observable effects (sideeffect + clobber); no operands, so the generic contract fits. |
| §9.7.14 | bra, brx, call | ⚪ out-of-scope | Control transfer cannot cross an LLVM inline-asm call boundary (labels/targets are invisible to the compiler); Julia control flow is the supported route. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.15.1 | bar, barrier | 🔵 generic | Convergent collectives; covers bar.warp.sync (§9.7.14.2) and barrier.cluster (§9.7.14.3); bar.red returns while bar.sync's tail is an id, and intrinsic-backed wrappers cover the common forms. |
| §9.7.15.4 | membar | 🔵 generic | Legacy memory barrier; sideeffect + clobber, no operands. |
| §9.7.15.4 | fence | 🟢 strict | Ordinary fence forms are chain-generic, but the tensormap::generic proxy fences are typed-wrapper-only (direction-specific acquire/release ABIs, exact scope set, ISA-fixed 128-byte acquire range); intrinsic/core-IR wrappers cover the common scoped fences. |
| §9.7.15.5 | atom | 🔵 generic | Bracketed read-modify-write returning the old value; 128-bit forms are audited in the B128 ledger. |
| §9.7.15.6 | red | 🔵 generic | Sink reduction (the type tail names the value written); covers red.async (§9.7.14.7). |
| §9.7.15.10 | vote | 🔵 generic | Convergent; the deprecated non-sync vote (§9.7.14.9) shares the head and the same conservative contract. |
| §9.7.15.11 | match | 🔵 generic | Convergent; the match.all d|p grouped destination is audited in the structured-result ledger. |
| §9.7.15.12 | activemask | 🔵 generic | Convergent by contract so the optimizer can never duplicate or merge it across divergence (the classic miscompile class). |
| §9.7.15.13 | redux | 🔵 generic | Convergent warp reduction under the generic rule. |
| §9.7.15.14 | griddepcontrol | 🔵 generic | Grid-dependency control; sideeffect + clobber, no operands. |
| §9.7.15.15 | elect | 🔵 generic | Convergent; the d|p grouped destination is audited in the structured-result ledger. |
| §9.7.15.16 | mbarrier | 🟢 strict | Every mbarrier chain is gated by the closed §9.7.15.16 grammar/ABI ledger (the terminal .b64 is never a result type; destinations span sink/state/pred/count/report groups); the family is single-route asm — the former tier-2 intrinsic forms were demoted — and MBarriers/Pipelines build on the wrappers. |
| §9.7.15.18 | clusterlaunchcontrol | 🔵 generic | trycancel is a sink with two mandatory address operands (dedicated override + schema); querycancel (§9.7.14.19) .b128 forms are audited in the B128 ledger. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.16.4 | wmma | ⚪ out-of-scope | Legacy wmma.load/store/mma fragment API superseded by mma.sync; shape-dependent fragment groups are inexpressible in chain/raw, and no wrapper is planned. |
| §9.7.16.5 | mma | 🟢 strict | Typed-wrapper-only (shape-dependent grouped fragment operands and results); covers mma.sync dense, block-scaled, .sp/.sp::ordered_metadata sparse, and the b1 forms via generated wrapper families. Contract is convergent + :pure — register-only compute, warp-collective. |
| §9.7.16.5.15 | ldmatrix | 🟢 strict | Typed-wrapper-only: shape/count-dependent grouped results (two registers per matrix for m16n16) and format-specific arity. The PTX ISA 9.4 sign-extending .s8.s4 m8n16 forms (sm_90a + 100f/110f/120f families) are asm-tier, spelled-only until a CUDA 13.4+ ptxas ships. |
| §9.7.16.5.16 | stmatrix | 🔵 generic | Convergent bracketed sink; x1/x2/x4 source groups are covered by typed wrappers, and the FORMS contract keeps chain spellings conservative. |
| §9.7.16.5.17 | movmatrix | 🟠 raw-only | Single-register warp transpose; raw renders the correct convergent scalar form, unregistered because nothing needed it yet. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.17 | wgmma | 🟢 strict | wgmma.mmaasync (dense and .sp) is typed-wrapper-only (shape-dependent tied accumulator groups and matrix descriptors); wgmma.fence/commitgroup/wait_group share the head under the convergent FORMS contract. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.18 | tcgen05 | 🟢 strict | Typed-wrapper-only: one head spans address destinations, register vectors, sinks, fences, and matrix descriptors (alloc/dealloc, ld/st grids, cp, mma dense/sp/ws/mx, commit, fences). The management verbs (alloc/dealloc/relinquishallocpermit/commit/cp), the waits, and the PTX ISA 9.4 additions (.exclusive alloc/dealloc, commit multicast::cluster::{16b,32b} and syncrestrict::shared::read::mma::a — spelled-only until a ptxas that accepts ISA 9.4 ships) are single-route asm, as are ld.red (no upstream intrinsics; ISA target floor sm103f/sm110a — no sm100 support) and the block-scale mma family, dense and sp (sp with the mxf4 kinds is a-variant-exclusive per the §9.7.18.10 support list); ld/st, shift, and non-block-scale dense/sp/ws mma lower via tier-2 intrinsics. Not wrapped: the ISA 9.4 sm_107f additions ti16, collector::b outside the ws family, and decompress::lut::b (gated on the 9.4-GA defect recheck) — the pre-9.4 surface is complete up to the deliberately out-of-scope generic-AS forms. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.19 | stacksave, stackrestore, alloca | ⚪ out-of-scope | Mutating the stack pointer behind LLVM's back inside compiler-managed frames is unsound; Julia/LLVM own stack allocation. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.20 | vadd, vsub, vabsdiff, vmin, vmax, vshl, vshr, vmad, vset, vadd2, vsub2, vavrg2, vabsdiff2, vmin2, vmax2, vset2, vadd4, vsub4, vavrg4, vabsdiff4, vmin4, vmax4, vset4 | ⚪ out-of-scope | Legacy scalar/SIMD video ALU (emulated on modern targets); optional secondary-operation suffixes defeat the trailing-dtype rule and nothing motivates review. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.21 | brkpt, nanosleep, pmevent, trap, setmaxnreg | 🔵 generic | Observable side effects, conservative contracts (nanosleep/pmevent tails name operands; setmaxnreg is convergent and requires .reqntid via minthreads to take effect). |
The gpu/hopper and gpu/blackwell runtime tiers run in no CI lane; their evidence comes from manual cloud sessions recorded in test/EVIDENCE.toml (the test manifest prints these records — and what has changed since the recorded tree — whenever it skips a tier). Dates matter: a record older than the tree under test is spelled/assembles evidence only.
| Tier | Evidence | Last validated | Device | Tree | Suite |
|---|
gpu/hopper (cc==9.0) | manual | 2026-07-30 | NVIDIA H100 PCIe (CC 9.0) | 30e1d4d | 97465 |
gpu/blackwell (cc==10|cc==11) | manual | 2026-07-30 | B300 SXM6 AC (CC 10.3) | ecbc00e | 98144 |
gpu (cc>=7.0 floors up to cc==12.1) | ci-continuous | — | GB10 (CC 12.1 / sm_121a), self-hosted CI runner | — | — |