Sarek_ir_cuda (sarek.Sarek_codegen.Sarek_ir

module Codegen_error : sig ... end

Local error module — same raised exception as the package-level Cuda_error.

module Dispatch = Sarek_ir_intrinsic_dispatch

val bad_arity : string -> int -> int -> 'a

Raise a located invalid-argument-count error (atomic-arity helper for the shared Dispatch.emit_atomic).

type state = {

variants : (string * (string * Sarek_ir_types.elttype list) list) list;

}

Everything one run of generate_with_types needs to know that is not reachable from the IR node it is currently emitting. It is a VALUE threaded through the emit functions, not module state, and that is the whole point of backlog-185/200: the field below used to be a module-level ref, so a second generation — on another domain, or simply a later one after Sarek_transpile had written it — read the first one's value.

variants is the kernel's own kern_variants, read by the SMatch/EMatch arms to recover a constructor's payload types. Derived from the kernel, so it could be re-derived at each use site; it is carried here because that is where the ref it replaces was read from.

It is the ONLY field. A mid-refactor draft also carried the framework tag, threaded in as ?framework so a caller could pick the registry spelling; that was dropped once it was clear every caller passed this backend its own name. The record survives the shrink deliberately — a one-field record is the honest shape for "one run's state", and the next thing that needs threading has somewhere to go.

val state : Sarek_ir_types.kernel -> state

The state for emitting k.

Type Mapping

val mangle_name : string -> string

val cuda_type_of_elttype : Sarek_ir_types.elttype -> string

Map Sarek IR element type to CUDA C type string

val cuda_param_type : Sarek_ir_types.elttype -> string

Map Sarek IR element type to CUDA C type for kernel parameters

Thread Intrinsics

val cuda_thread_intrinsic : string -> string

Expression Generation

val gen_expr : 'a -> Stdlib.Buffer.t -> Sarek_ir_types.expr -> unit

val gen_binop : Sarek_ir_types.binop -> string

val gen_unop : Sarek_ir_types.unop -> string

val cuda_backend : 'a -> Sarek_ir_types.expr Dispatch.spec

L-value Generation

val gen_lvalue : 'a -> Stdlib.Buffer.t -> Sarek_ir_types.lvalue -> unit

Statement Generation

val gen_stmt : 
  state ->
  Stdlib.Buffer.t ->
  string ->
  Sarek_ir_types.stmt ->
  unit

val gen_record_assign : 
  state ->
  Stdlib.Buffer.t ->
  string ->
  Sarek_ir_types.lvalue ->
  (string * Sarek_ir_types.expr) list ->
  unit

Helper: Generate record field assignment

val gen_match_case : 
  state ->
  Stdlib.Buffer.t ->
  string ->
  string ->
  Sarek_ir_types.pattern ->
  Sarek_ir_types.stmt ->
  unit

Helper: Generate switch case for pattern match

val gen_array_decl : 
  state ->
  Stdlib.Buffer.t ->
  Sarek_ir_types.var ->
  Sarek_ir_types.elttype ->
  Sarek_ir_types.expr ->
  Sarek_ir_types.memspace ->
  unit

Helper: Generate array declaration for SLet with EArrayCreate

Declaration Generation

val gen_param : Stdlib.Buffer.t -> Sarek_ir_types.decl -> unit

val gen_local : 'a -> Stdlib.Buffer.t -> string -> Sarek_ir_types.decl -> unit

Helper Function Generation

val gen_helper_func : 
  state ->
  Stdlib.Buffer.t ->
  Sarek_ir_types.helper_func ->
  unit

Generate a device helper function

Kernel Generation

val cuda_header : string

Generate the CUDA kernel header

val cuda_fp16_include : string

f16 feature declaration, emitted only for kernels that actually use f16 — the same conditional-emission discipline the OpenCL/GLSL backends apply to fp64 via Sarek_ir_analysis.kernel_uses_float64. Kernels without f16 are byte-identical to before.

The guard is NOT decoration. This generator is shared verbatim by the HIP backend (sarek-hip/Hip_shared.ml), and the two toolchains disagree:

CUDA needs #include <cuda_fp16.h> for __half and __float2half. Emitting the include is NECESSARY but not by itself SUFFICIENT under nvrtc: nvrtc is a library, not a driver, so it has no default include path and __half is not one of its builtins. Without an explicit --include-path the very include below fails with NVRTC_ERROR_COMPILATION / "could not open source file \"cuda_fp16.h\" (no directories in search list)". Supplying that path is Cuda_nvrtc.cuda_include_paths' job; nvcc, by contrast, adds the toolkit include directory itself.
HIP compiles through hiprtc, which pre-provides __half, half and __float2half with no include at all, and which cannot resolve ANY f16 header — neither cuda_fp16.h nor hip/hip_fp16.h exists on its search path. Emitting an unconditional include therefore breaks every HIP f16 kernel. Verified empirically against hiprtc on gfx1100: bare __half + __float2half compile; both include forms fail with "file not found"; this negative guard compiles.

__HIP__ / __HIP_PLATFORM_AMD__ are both defined under hiprtc (also verified), so the include is skipped there and taken on CUDA.

val sarek_f32_barrier_decl : string

An optimisation barrier that forces an f32 value to be MATERIALISED as a correctly-rounded binary32 register before it is consumed.

WHY THIS EXISTS. Sarek's f16 surface promises that arithmetic happens in f32 and that narrowing to binary16 is a separate, explicit, round-to-nearest-even step — that is what makes the device agree with the interpreter bit-for-bit. The AMDGPU backend breaks that promise: it fuses a narrowing into the operation that feeds it. Measured on gfx1100 for __float2half((float)__float2half((float)inp[tid] * 1.1f) + 1000.0f):

v_fma_mixlo_f16 v0, v0, s2, 0 <- f32 multiply AND the narrowing, fused v_add_f16_e32 v0.l, 0x63d0, v0.l <- the f32 ADD demoted to binary16

Both fusions skip a mandated rounding. The first is what made x = 5.68359375 return 1006.5 on HIP where the interpreter, the native path and the host reference all return 1006.0: the fused form rounds the EXACT product once to binary16 instead of rounding to f32 first, and the exact product sits just above a binary16 tie that the correctly-rounded f32 value sits exactly on.

Both halves are individually CORRECT — verified in isolation: the device's f32 product is bit-identical to the host's (0x40c81000), and the device's f32->f16 narrowing is round-to-nearest-even on exact ties in both directions and on negatives. The defect is purely the FUSION.

WHY A BARRIER AND NOT A FLAG. Verified at ISA level, the emitted code is byte-identical under -ffp-contract=off, =on and =fast, and under #pragma clang fp contract(off): this is an AMDGPU ISel combine that the standard FP-contraction controls do not reach. -ffp-contract=off is still set on the hiprtc path (see Hip_rtc.base_options) because it DOES fix ordinary f32 a*b+c contraction, but it is necessary-not-sufficient and does nothing for this pattern.

COST. The asm volatile constraint pins the value in a register and clobbers nothing, so it costs no memory traffic — ScratchSize stays 0. A volatile local also works but spills to scratch, which is why it is not used. The price is the un-fused instruction count: 6 VALU ops instead of 2 per f16 round-trip. Paid only inside kernels that actually narrow to f16 — the declaration is emitted only under kernel_uses_float16.

NVIDIA BRANCH: DELIBERATELY EMPTY, and that is a statement about NVIDIA, not an oversight. The non-HIP branch previously carried a PTX-flavoured asm volatile("" : "+f"(x)). AT A NARROWING it bought nothing, and it was removed because a call site reading sarek_f32_barrier(...) on the CUDA path advertised a protection that did not exist — the gap between assumed and actual FP semantics is exactly what produced this bug class.

Measured for this file's current output on CUDA 13.3 (nvcc/ptxas/nvdisasm V13.3.73, host-side, no NVIDIA device) for sm_75, sm_80, sm_86, sm_89, sm_90, sm_100, sm_120 and sm_121: cmp on the cubin says byte-identical on all eight, and the arithmetic stream stays HADD2.F32 / FMUL / F2FP.F16.F32 / HADD2.F32 / FADD / F2FP.F16.F32 — the f32 multiply and the f32 add both intact and the narrowings separate — with the asm and without it.

WHY, precisely. The first version of this note got it wrong twice, and both corrections matter to anyone reusing this function:

NVVM does NOT erase the block. The barriered PTX keeps the // begin/end inline asm marker pair and allocates more virtual registers (%f<9> against %f<5>). What it contributes is ZERO PTX INSTRUCTIONS, so ptxas receives an identical instruction stream either way — which makes the identical cubins structural, not a 13.3 accident.
The barrier is NOT inert in general. On out[i] = sarek_f32_barrier(a[i]*b[i]) + c[i] it IS a real NVVM-level contraction barrier: mul.f32+add.f32 with it, fma.rn.f32 without. Measured at sm_90. But ptxas -O1 and above RE-CONTRACT that back to FFMA under the default -fmad=true (-O0 and --fmad=false do not), so the cubins are byte-identical there too.

CONSEQUENCE, and it is a trap: do NOT reach for sarek_f32_barrier to fix the caller-side df64 contraction hazard on NVIDIA. It protects the PTX and ptxas undoes it. Sarek_df64's mul_rn works because an fma cannot be fused a second time — a property of the instruction, not of a barrier.

At the f16 narrowing there is nothing for either level to fuse in the first place: NVIDIA has no fused multiply-and-convert-to-f16 instruction, which is why the emitted code is unchanged there under every flag tried.

WHAT ACTUALLY HOLDS THE GUARANTEE ON NVIDIA: ptxas declines to absorb cvt.rn.f16.f32 into the operation feeding it — hand-written PTX with no inline asm at all gives the same unfused SASS. That is a property of the assembler, not of anything Sarek emits, so it is machine-checked rather than assumed: sarek-cuda/test/test_cuda_f16_sass.ml walks generated CUDA -> nvrtc -> PTX -> ptxas -> cubin -> nvdisasm -> SASS on every architecture the local ptxas knows and fails if the discipline breaks. See docs/fp-contraction-policy.md and docs/optimization/cuda-f16-fusion-sass-audit.md. NO f16 kernel has been EXECUTED on NVIDIA hardware; the claim is a machine-code claim.

WHY THE GUARD NAMES THE PLATFORM AND NOT THE LANGUAGE (backlog #146). The guard is defined(__HIP_PLATFORM_AMD__) alone. It used to be defined(__HIP__) || defined(__HIP_PLATFORM_AMD__), and the second form reads as though it admits HIP compiled for an NVIDIA target, where "+v" is not a valid constraint. Measured on this host, ROCm 7.2.53211:

hiprtc predefines BOTH __HIP__ and __HIP_PLATFORM_AMD__, and neither __HIP_PLATFORM_NVIDIA__ nor the legacy __HIP_PLATFORM_HCC__. All three candidate guards select the AMD arm and compile the "+v" asm — checked with #error in the other arm, so "it compiled" proves which arm was taken. Evidence: EXECUTED (hiprtc).
hip/hip_common.h auto-enables __HIP_PLATFORM_AMD__ whenever __clang__ && __HIP__, and auto-enables __HIP_PLATFORM_NVIDIA__ only for __NVCC__ or clang-CUDA WITHOUT __HIP__. hip/linker_types.h then hard-#errors unless exactly one platform macro is set. So under HIP's own headers __HIP__ IMPLIES the AMD platform: the removed disjunct was redundant, not load-bearing, and the NVIDIA-target-with-__HIP__ configuration those headers describe cannot arise. Evidence: BY-CONSTRUCTION (the shipped headers).
Both ROCm clang 22.0.0git and upstream clang 22.1.6 refuse -x hip --offload-arch=sm_61 outright ("unsupported HIP gpu architecture"), so that configuration is not reachable with either compiler on this host either. Evidence: EXECUTED.
"+v" IS invalid on NVPTX, independently of HIP: clang rejects asm volatile("" : "+v"(x)) for --target=nvptx64-nvidia-cuda with "invalid output constraint '+v' in asm", and accepts "+f". Evidence: EXECUTED. This is the part that was previously inferred from the constraint vocabulary alone.

So this is a CLARITY change, not a bug fix: no reachable configuration was mis-served by the old guard. It is made because the asm is AMD-ISA-specific and the guard should say so — __HIP__ is a LANGUAGE predicate that constrains no target — and because the redundant disjunct has now twice led a reader to conclude the barrier ships to NVPTX. STILL UNVERIFIED: ROCm older than the 4.x rename, where __HIP_PLATFORM_HCC__ was the platform macro; no such toolchain exists here. If one is ever in play the AMD arm would be skipped and the f16 discipline would fail silently, which is the one direction this file cares about — test_f16_barrier_is_amd_scoped pins the guard so the change cannot happen unnoticed.

val cuda_header_for : Sarek_ir_types.kernel -> string

Prefix for a kernel's generated source: the f16 include (only when the kernel uses f16) followed by the standard header.

val generate_with_types : 
  types:(string * (string * Sarek_ir_types.elttype) list) list ->
  Sarek_ir_types.kernel ->
  string

Generate CUDA source with custom type definitions.

Registry lookups are made under the constant tag "CUDA". An earlier draft of backlog-185/200 threaded a ?framework argument here so a caller could override it; it was dropped, because every caller passed this backend its own name — exactly the value the constant already is — and the one consumer that would have distinguished them, SNative, now refuses outright.

val generate : Sarek_ir_types.kernel -> string

Generate complete CUDA source for a kernel.

A special case of generate_with_types with the kernel's OWN type declarations, which is the only thing every production caller ever passed: ~types has exactly the type of the kern_types field (Sarek_ir_types.kernel), so the parameter was redundant with the record it travels in. This used to be a separate 30-80 line copy of the emit sequence that silently omitted record typedefs, variant typedefs and the kernel's variants — source referencing an undeclared struct, with no error. Delegating keeps one emit path per backend.