Rake
GPU profiles
Rake doesn't have a GPU compiler, runtime or device-artifact verifier yet, because CPU coverage and native C interoperation come first. In this design, the hardware schedules warps while Rake controls the algorithm's lane mapping, keeps temporaries in registers where the profile requires it, and makes memory and synchronisation costs explicit. The first backend will target NVIDIA PTX and verify an ahead-of-time cubin.
Racks and lanes
A CPU rack occupies one vector register, whereas a GPU rack will span a specified warp, wave or subgroup, with each invocation holding one lane's value, as in NVIDIA's SIMT model. A hidden loop that processes every rack element inside one invocation breaks the profile's rules.
| Property | Physical CPU profile | Proposed NVIDIA profile |
|---|---|---|
| Rack | one vector register | one 32-thread warp |
| Lane | a register component | a value held by one thread |
| Uniform | one scalar broadcast into the rack | one value shared by the warp |
| Tine | a vector mask | a predicate for each thread |
| Lane exchange | vector shuffle or reduction | explicit warp collective |
| Physical registers | allocated by Rake | allocated by NVIDIA, then checked in the cubin |
| Scheduling | Rake's instruction sequence, executed by the CPU | NVIDIA's instruction schedule and hardware warp scheduling |
Partial masks are legitimate program choices, and Rake can't make arbitrary inputs keep every lane active. It can tell uniform control from lane-varying control, though, and refuse serialization introduced by the compiler.
Matrix products, formats and fused regions
A GPU has two kinds of arithmetic unit. Its CUDA cores do ordinary arithmetic on one value per lane, while its tensor cores multiply whole tiles of two matrices at once, many times faster, and do nothing else. Most of an inference workload's arithmetic is matrix multiplication, so where those products run decides how fast the program is. The GPU profiles carry Rake's vectorisation rule over to these units with three checks on the compiled kernel.
A matrix product runs on the tensor cores. If the profile can't lower one to
tensor-core instructions, compilation fails, and a slow { ... } block is the
explicit place for a matrix product on the CUDA cores, such as a convolution
too small to fill a tile.
A declared number format runs as itself. Each tensor-core instruction takes particular formats, from 4-bit NVFP4 to TF32, and an engine without a kernel for a format can quietly widen it, running an FP8 product as BF16, or fall back from a fused attention kernel to a slower one. Rake rejects a format the profile has no instruction for. It warns when a narrower format at the same speed would hold every value exactly, such as BF16 weights declared as TF32.
A fused region is one kernel, and the values between its operations stay in registers and shared memory. Norms, activations and softmax are limited by memory traffic more than arithmetic, so writing each intermediate result out to device memory and reading it back, as an eager framework does with one kernel per operation, costs more than the operations themselves. The verifier checks the cubin for spills and for device-memory traffic inside the region, and rejects the kernel if it finds either.
First profile: NVIDIA PTX
The proposed profile, nvidia-ptx-sm120a, fixes PTX ISA
8.7,
sm_120a, 64-bit addressing and a 32-lane rack, and initially supports only
that SM architecture. It targets sm_120a because PTX 8.7 provides the
block-scaled and 4- and 6-bit forms of mma only for that architecture-specific
target. It uses CUDA
12.8.1,
with the exact tool binaries pinned by hash. Other architectures and
operations need a checked profile extension, and the compiler will report an
unsupported construct's source location, profile and failed obligation.
| Area | Initial support |
|---|---|
| Values | f32 lane values and predicates, 32-bit integer indices and 64-bit device addresses. Uniformity is tracked separately |
| Arithmetic | binary32 add, subtract, multiply, divide, square root, explicit FMA, ordered comparisons and selection. Divide and square root require correctly rounded forms |
| Floating point | round to nearest, ties to even, with subnormals preserved. Explicit FMA has one rounding. Fused regions may contract under published rules. No implicit fast-math |
| Masks | source through/sweep priority, no inactive memory effects, safe operands or verified predication for partial arithmetic |
| Collectives | broadcast, static shuffle, ballot and ordered float reductions/scans through published warp-shuffle sequences. Participation and reduction order are explicit |
| Memory | typed structure-of-arrays global loads/stores, with alignment, count and lane-to-address mapping. Tails suppress out-of-bounds accesses |
| Control | uniform bounds and source traversal control are permitted. Pure fused regions forbid calls and hidden lane loops |
| Matrix products | warp-level mma in each form sm_120a provides: block-scaled NVFP4 and MXFP4 (kind::mxf4nvf4), FP4, FP6 and FP8 in any pairing (kind::mxf8f6f4), INT8, FP16, BF16 and TF32, with FP32 accumulation |
| Initial exclusions | shared-memory collectives, atomics, dynamic allocation, recursion, device callbacks, scatter and unsupported numerical functions |
Every launched warp will contain 32 invocations. Padding invocations stay present until the required collectives finish, supplying neutral operands for inactive data lanes, and never touch out-of-bounds records. Every participant reaches the same collective with the same membership mask. Execution never relies on implicit lockstep between threads, so the checker will reject reads from unavailable shuffle sources, and any collective when it can't establish which lanes take part.
Compilation and final-code verification
Rake source and GPU lane contract
-> checked IR: uniformity, masks and memory effects
-> inspectable PTX 8.7 for sm_120a
-> pinned ptxas: ahead-of-time cubin
-> nvdisasm and cuobjdump: instructions, control flow and resources
-> Rake's sm_120a artifact verifier
-> exact verified cubin loaded by the runtime
NVIDIA owns final instruction selection, physical register allocation and
instruction scheduling on this virtual profile, so Rake verifies the
resulting artifact instead. Using NVIDIA's
binary utilities,
the verifier will inspect every reachable instruction and control-flow path,
relate register and data flow to the profile's lane, mask, memory and
collective rules, and check the LOCAL and STACK resource counts. It
rejects unknown instructions, opaque helper paths and unexplained loops,
and rejects the artifact whenever the evidence is insufficient. Designated pure regions forbid
spills, reloads, calls and hidden serial lane loops, while explicit address
and traversal work has separate obligations.
Artifact identity and runtime boundary
Verification will bind the exact cubin and kernel hashes to the source, profile, compiler revision, PTX hash, toolchain binaries and flags, target SM, verifier version and launch/parameter ABI, and runtime evidence also records the device and driver. A driver or runtime change requires refreshed compatibility checks and execution evidence. The runtime will load only those verified bytes, and refuse PTX JIT fallback or a rebuild with different flags.
The host interface is a separate C ABI for loading a verified artifact and launching a kernel with an explicit CUDA context, stream and versioned parameter layout. Column arguments will be device addresses with counts and alignment requirements, and the caller owns allocation, lifetimes, stream ordering and synchronisation, and launch errors stay visible to it. CUDA supplies the execution interface, while Rake source compiles directly to PTX.
Guarantees and measurements
| Compilation or artifact verification | Execution and measurement |
|---|---|
| lanes map to threads, without a hidden serial lane loop | enough independent warps to use the device |
| matrix products on tensor-core instructions, in their declared formats | how fully the tensor cores are kept busy |
| one kernel per fused region, with its intermediate values kept on chip | memory bandwidth achieved between regions |
| permitted predicates, control flow and collective participation | input-dependent inactive lanes |
| no forbidden spills, reloads or helpers in checked regions | achieved occupancy and whether another register policy is faster |
| parameter layout and lane-to-address pattern | memory transactions, caches and transfer overhead |
| numerical semantics and explicit synchronisation scopes | elapsed time and application throughput |
More registers per thread can leave room for fewer resident warps, as NVIDIA's register and occupancy discussion explains. A strict no-spill profile will still reject a forbidden spill when another policy might run faster, and a relaxed resource policy will get a profile of its own.
Verification tests
Independent numerical and CPU reference results will check lane mapping, mask priority, tails, collectives and floating-point edge cases, including empty data, partial warps, missing participants and unavailable shuffle sources. Negative fixtures will give the verifier each forbidden pattern, including incorrect address patterns and unexpected divergent control, and it refuses them even when a resource summary looks acceptable. Artifact checks will alter bytes, architecture, flags and launch metadata, so verification can't silently carry over to a different kernel.
Later portable and physical profiles
A later SPIR-V/Vulkan
profile, such as vulkan-subgroup32 or vulkan-subgroup64, will span a rack
across a required
subgroup width rather
than a large OpTypeVector inside one invocation. Each will specify its
SPIR-V and Vulkan versions, memory model, numerical modes, operations and
collective participation, and pipeline creation will reject incompatible
devices. Physical resource verification needs the driver-generated
executable, and Vulkan's optional
pipeline executable properties extension
may expose it. Rake refuses certification without enough final-code evidence,
and binds that evidence to the module, pipeline state, device, driver and
verifier.
A physical profile for a sufficiently documented ISA, such as one in AMD's architecture documentation, would let Rake own selection, allocation and scheduling as well as verification.
Rake and other languages compares this design with ISPC's gangs and Bend 2's fork–join tasks.