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 36 PTX ISA 9.4 packed add/sub/mul/fma forms have closed scalar-result schemas for their destination and source type tails: f32x2 uses UInt64, f16x2/bf16x2 use UInt32. Target floor is sm107f (or higher in the same family); assembly is tested when the managed compiler supports ISA 9.4. Runtime evidence on sm107 hardware remains pending. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.6 | — | 🔵 generic | PTX ISA 9.4 alternate packed add/sub/mul/fma have 896 canonical scalar-result schemas and seven exact documented postfix-satfinite compatibility forms. Results use UInt32; compact e2m1x4 inputs use UInt16, while padded e2m1p4x4 and the other x4 formats use UInt32. Restricted to sm100a and sm103a; every form is assembled with stored results when the managed compiler supports ISA 9.4. Runtime execution on those targets remains unverified. |
| 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 | 🔵 generic | Closed scalar-result grammar for 1152 general, 1960 half/BF16, and 32 PTX 9.4 packed integer set forms. Destination and source carriers, Boolean predicate inputs, and legal comparison/ftz prefixes are explicit. Packed integer forms require the sm_107f family and have complete offline assembly coverage; execution on that family remains unverified. |
| §9.7.7 | slct | 🟠 raw-only | Deliberately unregistered: slct has a dtype.ctype tail whose final type describes the condition input. It needs a reviewed destination/source grammar before joining the registered surface. |
| Section | Opcodes | Status | Notes |
|---|
| §9.7.8 | — | 🔵 generic | No distinct opcode heads: half/BF16 set and setp share the section 9.7.7 opcode entries. The scalar-result ledger fixes numeric set results; the structured-result ledger fixes scalar/grouped setp predicates. |
| 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 (ptx"%..."); mov.b128 is audited in the B128 ledger (UInt128 carrier on the q constraint). |
| §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. Scalar ld{.global}.type.proxy::readonly reads its result type before the trailing proxy, with host, assembly, and numeric coverage. |
| §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 | 🟢 strict | Bracketed eviction-priority hint; the scalar form and the PTX ISA 9.4 applypriority.async.bulk form are chain-renderable under a sink override (the eviction priority is the terminal token, not a dtype). applypriority.async.bulk.tensor (§9.7.10.19) is typed-wrapper-only in the TMA wrappers. |
| §9.7.10.18 | — | 🔵 generic | No distinct opcode head: applypriority.async.bulk{.global}.bulk_group.L2::evict_normal [a], size (PTX ISA 9.4, sm107f family) renders through the §9.7.10.17 entry's sink override; assembled at sm107f when the managed compiler supports ISA 9.4. |
| §9.7.10.19 | — | 🟢 strict | No distinct opcode head: the tensor eviction hint (PTX ISA 9.4, sm_107f family) is typed-wrapper-only under the §9.7.10.17 entry. Wrapped: tile ranks 1d-5d, base im2col ranks 3d-5d with N-2 offsets, and tile ranks with the global-address and attribute overrides. Not wrapped: tile::gather4 and the im2col::w modes. |
| §9.7.10.20 | discard | 🔵 generic | Bracketed cache-discard hint. |
| §9.7.10.21 | createpolicy | 🟠 raw-only | Cache-policy handle creation; ordinary raw forms render a scalar .b64 destination. The PTX 9.4 range.fabric form needs a composite [endpoint, offset] operand and has no reviewed binding. |
| §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) have source-carrier coverage and sm107f assembly coverage (test/ptxas/cvtimmediate_carriers.jl); numeric validation needs CC 10.7 hardware. Stochastic .rs rejects .pzo. The n1 scale factor and the e2m1x2 destination/source are physically b8: the chain render bridges the UInt16 carrier through a block-local .b8 register. |
| §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 ctagroup::2 renders after the rank like the pre-existing shared::cta residue (ptxas accepts both orders). PTX ISA 9.4 (sm107f family) wrapped inventory: .multicast::cluster::{16b,32b} on the cluster loads (with and without ctagroup::2); the six .reportmechanism spellings on both load directions (no multicast or ::32b); .override::globaladdress alone and with the rank-determined .overrideattribute on both load directions (no multicast or ::32b), the tile store, the tile reduce (all eight redOps), the tile prefetch, and the tile eviction hint; .im2colnooffs and .im2colnooffs::w on the store and reduce directions (3d-5d); .L2::evictlast on the tile and base-im2col prefetches; plus the pre-9.4 cp.reduce.async.bulk.tensor tile forms. Not wrapped: report×override crosses, report/override with ctagroup::2, .L2::cachehint on copies or with overrides/evictlast, tile::gather4 and im2col::w modes. Assembly evidence at sm107f/sm107a only; no runtime evidence. The chain cp.async.bulk ::16b/::32b/report and cp.async.bulk.prefetch .L2::evict_last spellings render under the sink override. |
| §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. |
| §9.7.10.30 | spcompress | 🟢 strict | Typed-wrapper-only (PTX 9.4, sm107a): the dense input, kept-element, and index vectors are qualifier-dependent b32 register groups with two leading grouped destinations, so the chain cannot render them. The closed 28-form grid ({b8,b16} x {b2,b4} x x1..x64) is asm-tier without a sideeffect marker (register-only, :pure) and early-clobber outputs; spcompressdesc packs the Table 38 descriptor. Assembled at sm107a and rejected at sm107f/sm100a; no runtime evidence (needs sm107a hardware). |
| §9.7.10.31 | spdecompress | 🟢 strict | Typed-wrapper-only (PTX 9.4, sm107a): the index, compressed, and dense vectors are qualifier-dependent b32 register groups with a leading grouped destination. The 143 admitted (elemsize, idxsize, sp::S:T, num) tuples follow the five ISA validity conditions (S·elemsize <= 32, .b2 indexes T <= 4, output 32..4096 bits, register cap); asm-tier without a sideeffect marker (register-only, :pure) and early-clobber outputs. Assembled at sm107a and rejected at sm107f/sm100a; no runtime evidence (needs sm_107a hardware). |
| 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. PTX 9.4 tensor get/put/red, tryatom, and cache-policy operands remain unimplemented. The deferred trypullred.sync form requires a literal full-warp member mask. |
| 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. PTX 9.4 alias acquire/release.sys and async::generic release.syncrestrict::shared::cluster::read.cluster have host and sm90 assembly coverage. The cluster-read fence is non-cumulative; assembly does not establish concurrent runtime ordering. |
| §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 (sm90a + 100f/110f/120f families) are asm-tier, assembled at sm90a/sm100f/sm120f/sm121a and executed on GB10 (test/gpu/ldmatrixdecompression.jl). |
| §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, assembled at their target floors in test/ptxas/blackwell.jl; runtime evidence needs sm107 hardware) 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. The sm107a ld{.red}.spcompress family (72 asm forms, 2:4 row compression on 32x32b loads; test/host/tcgen05ldst.jl) is single-route asm. The ISA 9.4 sm107f mma additions — .kind::ti16 (dense/sp/ws), .collector::b::* on the float and block-scale family kinds, and .decompress::lut::b on f8f6f4/mxf8f6f4.block32 — are single-route asm (no upstream intrinsics), assembled at sm107f/sm107a in test/ptxas/tcgen05mma.jl; the descriptor builders expose the sm107f wide-K, scale-layout, 15-bit field, and lut segment encodings behind explicit keywords and pin ti16 transpose to zero where the ISA tables contradict each other. 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-09-14 | NVIDIA B200 (CC 10.0) | 435fb84 | 238075 |
gpu (cc>=7.0 floors up to cc==12.1) | ci-continuous | — | GB10 (CC 12.1 / sm_121a), self-hosted CI runner | — | — |