Module Sarek_execute.Execute

V2 Vector argument type - supports automatic transfers and length expansion. This is the main type-safe way to pass arguments to kernels.

Convert vector_arg list to exec_arg array (new typed interface). Creates EXEC_VECTOR wrappers for vectors.

Retrieve device buffer for a vector on a specific device.

Returns a first-class module containing the device buffer's pointer, size, and binding function. The buffer must exist (typically created by a prior transfer).

• parameter v

  Vector to get buffer from

• parameter dev

  Device the buffer should be allocated on

• returns

  Device buffer module

• raises Transfer_failed

  if vector has no buffer on this device

Transfer all V2 Vector args to device

Expand vector args to run_source_arg format.

• parameter inject_lengths

  If true (default), auto-inject vector length as RSA_Vector_Length after each buffer. This matches Sarek-generated kernels which expect (ptr, len) pairs. Set to false for external kernels with different signatures.

The injected length is tagged RSA_Vector_Length, not RSA_Int32, so backends can tell it apart from a genuine caller-supplied scalar that happens to immediately follow a buffer (which is exactly what a ~inject_lengths:false caller can pass) - see Framework_sig.run_source_arg.

Launch-time argument check

The Vec constructor of vector_arg is existential (Vec : ('a, 'b) Vector.t -> vector_arg), so a vector's element type is ERASED the moment it enters an ~args list. No OCaml type constraint on the generated kernel closure can therefore catch passing a float32 vector where the kernel declared a float16 vector — the mismatch happens on a path where the types are already gone. Executed on gfx1100: such a launch compiled clean and read/wrote 2N bytes of a 4N-byte buffer, producing 1 2 0 0 for input 1 2 3 4, with the Native path catching it only by accident.

The IR is the one place where the DECLARED parameters and the SUPPLIED arguments meet, so the check lives here, and it covers every element type.

ARITY IS CHECKED FIRST, and is an error rather than a precondition for the rest. An earlier version ran the per-argument checks only if the counts matched, which made a wrong count silently disable every other check — the conservatism was also a bypass. Worse, a SHORT argument list is a memory-safety problem in its own right and independent of f16: both Cuda_api.Kernel.launch and Hip_api.Kernel.launch size the kernel-argument array with CArray.make (ptr void) (List.length args) and hand cuLaunchKernel / hipModuleLaunchKernel a bare CArray.start params with NO count (the trailing extra pointer is NULL). The driver then reads as many entries as the COMPILED signature declares, so a short list makes it read past the end of that array and dereference whatever it finds as a parameter — for a pointer parameter, an arbitrary device address. Rejecting the arity here is what keeps that unreachable.

Element types are compared exactly where the runtime kind has an IR counterpart. Where it does not, the check does NOT silently pass: it falls back to comparing PHYSICAL ELEMENT WIDTHS, which is the property that actually matters for buffer striding. That closes the wildcard: Vector.Char holds 1-byte elements while source char lowers to TInt32, so a Char vector is accessed through a 4-byte int*. (That lowering is PRE-EXISTING — Sarek_lower_ir.elttype_of_typ mapped TReg Char -> Ir.TInt32 before this branch — and is NOT fixed here; the check simply refuses to be the thing that hides it.)

Still conservative where it must be: a Custom (record/variant) element is nominal and both sides derive it from the same registered layout, so its element comparison is skipped deliberately rather than by omission.

Byte width of an IR element type, when it is a scalar. None for aggregates (whose width comes from the registered layout, not from this table).

IR element type a SCALAR launch argument is tagged with on the host. Int and Int32 denote the same 32-bit slot. None for Vec, which is handled by the vector arms.

This tag is exactly what decides how many bytes the launch writes into the argument slot, so it is the host side of the same width contract the vector check enforces — see check_launch_args.

Render a non-permitting verdict and raise it as a Backend_error.

Shared by check_device_capabilities and check_interpreter_capabilities so the two launch gates cannot drift into describing the same refusal differently — which is a real hazard here, since backlog-154 was two gates disagreeing about the same kernel.

Refuse a launch whose kernel needs a wide element type the target device does not provide (#142).

WHY THIS IS A LAUNCH GATE AND NOT A CODEGEN REFUSAL. These are Sarek_capability.kind.Device_optional capabilities: kind_needs_device Device_optional = true, and Framework_sig.generate_source takes no device, so codegen is structurally the wrong place to ask. The device is first in scope here, next to check_launch_args.

WHAT IT REPLACES. Nothing — that is the defect. Before #142 an int64 kernel on Vulkan reached vkCreateShaderModule with SPIR-V declaring OpCapability Int64 and no shaderInt64 enabled on the logical device. On an RX 7900 XTX (RADV, Mesa 26.1.4-arch3.1) that is not a crash and not a wrong answer: results are correct and the violation is visible only under VK_LAYER_KHRONOS_validation (VUID-VkShaderModuleCreateInfo-pCode-08740). Silent undefined behaviour on the driver that happens to cope is exactly the failure mode a capability model exists to convert into a diagnostic.

Routed through Sarek_capability.permits rather than a membership test so an Sarek_capability.verdict.Unknown verdict refuses instead of falling through to permitted.

The launch gate for run_interpreter_vectors (backlog-154).

run_interpreter_vectors applied check_launch_args and NOT check_device_capabilities, so the interpreter — the cross-backend numeric oracle — was the one execution path with no capability gate on it. The asymmetry was observable: in one run of test_coopmat_integer_e2e on this workstation, check_device_capabilities printed launch gate refuses on CPU Interpreter (Sequential) for the same kernel run_interpreter_vectors then evaluated to 65536 bit-exact results.

Note what could NOT be done about that: calling check_device_capabilities here. It needs a Device.t, this entry point has none by design, and — the substantive half — the interpreter's Framework_sig.capabilities says coopmat = None, which means "not probed", which refuses. Wiring the device gate in would have taken the oracle offline rather than closed a hole. The bypass was load-bearing, which is why the fix is a capability answer for the interpreter and not a call to someone else's.

Sarek_interp_capability is that answer, and it lives beside the evaluator that justifies it. See its interface for the argument about what an interpreter should advertise.

Execute a kernel on a device using the unified dispatch mechanism.

• parameter device

  Target device

• parameter name

  Kernel name

• parameter ir

  Sarek IR kernel (lazy, only forced for JIT backends)

• parameter native_fn

  Pre-compiled native function (for Direct backends)

• parameter block

  Block dimensions

• parameter grid

  Grid dimensions

• parameter shared_mem

  Shared memory size in bytes (default 0)

• parameter args

  Kernel arguments as vector_arg list

• raises Execution_error

  if execution fails

Mark vectors as stale on CPU after kernel execution.

After a kernel modifies vector data on a device, we need to track that the CPU-side data is now stale. This ensures future CPU reads will trigger a device→CPU transfer.

Special cases:

• Native backend: No-op (uses zero-copy shared memory, no staleness)
• JIT backends: Always mark stale (Transfer module handles zero-copy checks)
• OpenCL CPU: Mark stale for custom types (scalar types use zero-copy)

• parameter args

  Arguments that may contain vectors

• parameter dev

  Device that just executed the kernel

Convert a V2 Vector to interpreter value array.

Converts vectors of primitive types (int32, float32, etc.) to the interpreter's runtime value representation. Custom types are converted using registered type helpers from Sarek_type_helpers.

This enables the interpreter backend to execute kernels on CPU without requiring GPU infrastructure.

• parameter vec

  Input vector of any type

• returns

  Array of interpreter values matching vector contents

Copy interpreter value array back to V2 Vector.

After interpreter execution, this function copies the runtime values back into the typed vector representation. Performs type checking and conversion for each element.

• parameter arr

  Array of interpreter runtime values

• parameter vec

  Destination vector (must match type of values)

Run kernel via interpreter with V2 Vectors. Note: Interpreter works with IR params directly - one arg per param. Vectors map to ArgArray (length is intrinsic to array).

Execute a kernel with V2 Vectors. Auto-transfers, dispatches to backend.

This is the main execution entry point for Sarek-generated kernels. It performs the complete execution pipeline:

1. **Transfer**: Move vectors to device (no-op for CPU backends) 2. **Dispatch**: Call appropriate backend's execution method 3. **Mark stale**: Update vector location tracking

The function automatically handles differences between execution models:

• JIT backends: Generate source, compile, launch
• Direct (Native): Call pre-compiled OCaml function
• Custom (Interpreter): Walk IR and evaluate expressions

• parameter device

  Target device (determines backend)

• parameter ir

  Sarek IR kernel definition

• parameter args

  Kernel arguments (vectors and scalars)

• parameter block

  Thread block dimensions (e.g., (256, 1, 1))

• parameter grid

  Grid dimensions (e.g., (4, 1, 1))

• parameter shared_mem

  Optional shared memory size in bytes (default: 0)

• raises Execute_error

  on validation or execution failure

Sync all V2 Vector outputs back to CPU

Create 1D grid and block dimensions

Create 2D grid and block dimensions

Create 3D grid and block dimensions

Calculate grid size for a given problem size and block size

Calculate 1D grid dimensions for a problem size

Re-export source language type

Check if a device supports a given source language.

Different backends support different source languages:

• CUDA: CUDA source (.cu), PTX
• OpenCL: OpenCL source (.cl)
• Vulkan: SPIR-V, GLSL source (.comp, .glsl)
• Native/Interpreter: None (not JIT backends)

• parameter dev

  Device to check

• parameter lang

  Source language to query

• returns

  true if device can compile and execute this language

Execute an external kernel from source code.

This function allows running pre-written GPU kernels (CUDA, OpenCL, PTX) directly without going through the Sarek DSL.

• parameter device

  Target device

• parameter source

  Kernel source code as string

• parameter lang

  Source language (CUDA_Source, OpenCL_Source, PTX)

• parameter kernel_name

  Name of the kernel function in the source

• parameter block

  Block dimensions

• parameter grid

  Grid dimensions

• parameter shared_mem

  Shared memory size in bytes (default 0)

• parameter inject_lengths

  If true (default), auto-inject vector length as Int32 after each buffer argument. Sarek-generated kernels expect (ptr, len) pairs. Set to false for external kernels that don't follow this convention.

• parameter args

  Kernel arguments as vector_arg list

• raises Execution_error

  if device doesn't support the source language

Load kernel source from a file

Detect source language from file extension

Execute an external kernel from a file.

Loads pre-written GPU kernel source from a file and executes it. Useful for integrating hand-optimized kernels or using features not yet supported by the Sarek PPX.

Source language is auto-detected from file extension:

• .cu → CUDA source
• .cl → OpenCL source
• .ptx → PTX assembly
• .spv → SPIR-V binary
• .comp / .glsl → GLSL compute shader

Example:

  (* Execute hand-written CUDA kernel *)
  Execute.run_source_file
    ~device:(Device.get_default ())
    ~path:"kernels/optimized_matmul.cu"
    ~kernel_name:"matmul_kernel"
    ~block:(16, 16, 1)
    ~grid:(64, 64, 1)
    [Vec a; Vec b; Vec c; Int32 1024l]

• parameter device

  Target device

• parameter path

  Path to kernel source file

• parameter kernel_name

  Name of kernel function in source

• parameter block

  Block dimensions

• parameter grid

  Grid dimensions

• parameter shared_mem

  Optional shared memory in bytes

• parameter inject_lengths

  If true (default), inject vector lengths after buffer args

• parameter args

  Kernel arguments

• raises Invalid_file

  if file extension is not recognized

• raises Execute_error

  if compilation or execution fails