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

The auto-injected vector length. Kernels index with int32, and Int32.of_int WRAPS silently above Int32.max_int — a 2^31-element vector would reach the kernel with a negative length. Refused instead (FR-018).

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.

Portable half of pragma ["sarek.max_threads N"]: refuse, before any backend sees the launch, a block whose thread count exceeds the declared bound. Applies to every backend, Native and Interpreter included, so the mistake is the same Sarek error everywhere rather than a driver failure on some of them. A kernel without a bound is never refused here.

The warp width a kernel will run on, on device. A hardware device reports its own; Native and the interpreter simulate one, whose width is read at launch time (Sarek_warp.simulated_width) because it is the test hook of the parity tests and is not frozen into the device's capabilities.

Refuse a launch whose kernel shuffles and whose block is not a whole number of warps (docs/plans/warp-shuffle-intake-2026-10-17.md, decision D3). The lanes of a partial warp would read sources that do not exist, which is undefined on CUDA, HIP and Metal; the rule is the same on every backend (Native and the interpreter included) so the mistake is one Sarek error everywhere. Kernels without a shuffle are never refused here. The error is Execute_error.error.Invalid_dimensions, the one check_launch_bounds raises for the sibling sarek.max_threads rule.

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.

Drop every memoised launch preparation: the next launch of every kernel re-runs its device capability check and regenerates its source. Needed only after replacing an intrinsic or type implementation that already-launched kernels use; backend cache clears and device teardown call it already.

check_device_capabilities, performed once per (IR, device id, physical capabilities record). A refusal raises every time.

B.generate_source, performed once per (IR, backend, block, soa_params). Every hit returns the same physical string, which also lets the backend's Compile_cache.make_key memo skip its digests. None and exceptions are not memoised.

Validate a launch on stream for device BEFORE anything is transferred: the stream must belong to device, and a JIT backend must implement stream launches — a launch the caller ordered on a stream must never run on the default queue instead. Direct/Custom backends (Native, Interpreter) execute synchronously, which satisfies any stream ordering.

Control and statistics of the launch window.

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

• parameter stream

  Enqueue the launch on this stream instead of the default one (HIP, CUDA); the call may return before the kernel has run, and the argument vectors stay rooted until the stream or a later event completes. On Metal the launch is enqueued on the stream's own command queue (host access to its buffers waits for it); on Native/Interpreter it is synchronous. Refused with Feature_not_supported on other JIT backends, and with Invalid_argument when the stream belongs to another device. The capability check and, on JIT backends, source generation are done once per physical IR and reused by later launches (see the launch-preparation memo above and clear_launch_cache); argument checks run every time. Without ~stream, a JIT launch on a backend whose launch window is enabled (HIP, OpenCL, Vulkan, CUDA and Metal by default) is deferred until the next synchronisation point and may be fused with independent launches (Window, specs/launch-window.md). Its checks and source generation still run in this call, but a device compilation or driver launch failure is raised by the call that flushes the window.

• 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, like the other JIT backends (a host-pointer buffer from Host_ptr_buffer is read back through map/unmap)

• 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 stream

  Launch on this stream (see run). Auto-transfers of the arguments still happen synchronously before the launch; vectors already resident (e.g. device-only ones) cost nothing.

• 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

run_vectors that also returns what ran: the kernel as given, or a matrix-unit rewrite of it (Matrix_specialise). precision chooses the operand rounding of a float32 product (it must have been accepted). ~explicit:true is an explicit request, like Sarek_matrix.run: float products need the accuracy opt-ins only (not Sarek_coopmat.accept_automatic_float_rewrite), and the interpreter is rewritten too.

Launch ir on device. When ir is a matrix product that matrix units can compute under the current restrictions and accuracy opt-ins, the rewritten kernel runs instead, writing exactly the same outputs (specs/matrix-pattern-dynamic.md).

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