Module Spoc_framework.Framework_sig

Common Types

type dims = {
  1. x : int;
  2. y : int;
  3. z : int;
}

3D dimensions for grid and block

val dims_1d : int -> dims
val dims_2d : int -> int -> dims
val dims_3d : int -> int -> int -> dims
type capabilities = {
  1. max_threads_per_block : int;
  2. max_block_dims : int * int * int;
  3. max_grid_dims : int * int * int;
  4. shared_mem_per_block : int;
  5. total_global_mem : int64;
  6. compute_capability : int * int;
    (*

    (major, minor) for CUDA, (0,0) for OpenCL

    *)
  7. device_features : Sarek_ir_analysis.feature list;
    (*

    The wide element types this DEVICE provides, as the same vocabulary Sarek_ir_analysis.kernel_uses asks a kernel for. The pairing is the point: a kernel says what it REQUIRES, this says what the device PROVIDES, and a launch gate is one List.mem rather than a per-width boolean added to this record every time a width is.

    Replaces the former supports_fp64 : bool (#142). It was a single boolean for a question that already had three answers — fp64, f16 and int64 — and the missing one had teeth: an int64 kernel reached vkCreateShaderModule declaring OpCapability Int64 against a logical device that had never enabled shaderInt64, because nothing in this record could express the int64 half of the question. Read it through Sarek_capability.permits, never by testing membership directly: an unprobed device must not fall into the permitted bucket.

    Spoc_core.Device.allows_fp64 and allows_int64 are the derived accessors, so this stays the single source and the two cannot drift.

    *)
  8. coopmat : Sarek_coopmat.device_support option;
    (*

    The cooperative-matrix (tensor-core) configurations this DEVICE advertises, or None when the backend does not probe for them (backlog-62 slice 2).

    An OPTION rather than a plain list, for the same reason Sarek_capability.device_verdict takes one: an empty list and an unprobed device are different facts, and collapsing them makes "advertises nothing" indistinguishable from "nobody asked". Only the first is evidence. Sarek_coopmat.verdict maps None to Sarek_capability.verdict.Unknown, which does not permit.

    Read it through Sarek_coopmat.verdict or Sarek_coopmat.find_config, never by matching on the list directly.

    *)
  9. supports_atomics : bool;
  10. warp_size : int;
    (*

    Invocations that execute in lockstep — CUDA warp, AMD wavefront, Vulkan/Metal subgroup. Load-bearing for cooperative matrices, whose fragments are distributed across exactly this many invocations (Sarek_coopmat.components_per_invocation), so a wrong value here is a wrong ABI rather than a wrong statistic. The Vulkan backend now reports VkPhysicalDeviceSubgroupProperties.subgroupSize instead of a hard-coded 32; on the RX 7900 XTX under radv / Mesa 26.1.4-arch3.1 that is 64.

    *)
  11. max_registers_per_block : int;
  12. clock_rate_khz : int;
  13. multiprocessor_count : int;
  14. is_cpu : bool;
    (*

    True for CPU devices - enables zero-copy optimization

    *)
}

Device capabilities - queried from hardware

type device = {
  1. id : int;
    (*

    Global device ID (0, 1, 2...)

    *)
  2. backend_id : int;
    (*

    ID within the backend (0, 1...)

    *)
  3. name : string;
    (*

    Human-readable device name

    *)
  4. framework : string;
    (*

    Backend name: "CUDA", "OpenCL", "Vulkan", "Native"

    *)
  5. capabilities : capabilities;
}

Device representation - SDK layer type shared across all backends

Plugin Module Signature

module type S = sig ... end

Minimal framework signature for plugin registration. Used by Framework_registry for basic plugin management.

type execution_model =
  1. | JIT
  2. | Direct
  3. | Custom

Execution model for backends.

  • JIT: Generate source code at runtime, compile with GPU compiler (CUDA, OpenCL)
  • Direct: Execute pre-compiled OCaml functions directly (Native CPU)
  • Custom: Full control over compilation pipeline (LLVM, SPIR-V, future)
type source_lang =
  1. | CUDA_Source
    (*

    CUDA C/C++ source (.cu)

    *)
  2. | OpenCL_Source
    (*

    OpenCL C source (.cl)

    *)
  3. | PTX
    (*

    NVIDIA PTX assembly

    *)
  4. | SPIR_V
    (*

    SPIR-V binary

    *)
  5. | GLSL_Source
    (*

    Vulkan GLSL compute shader

    *)

Source language for external kernels

type kargs = ..

Extensible type for backend-specific kernel arguments. Each backend extends this type with its own variant. This allows type-safe passing of kernel args across the framework boundary with typed witnesses.

type kargs +=
  1. | No_kargs

Placeholder kargs for testing - not associated with any backend

type run_source_arg =
  1. | RSA_Buffer of {
    1. binder : kargs -> int -> unit;
      (*

      Binds buffer to kernel arg

      *)
    2. length : int;
      (*

      Vector length for generated kernels

      *)
    }
  2. | RSA_Vector_Length of int32
    (*

    Auto-injected vector length (see Execute.expand_to_run_source_args ~inject_lengths), distinguished from a genuine caller-supplied RSA_Int32 so backends that derive lengths from the bound buffer itself (e.g. Vulkan) can drop it without relying on its position in the argument list - "immediately after a buffer" is not a safe test, since ~inject_lengths:false callers can put a real RSA_Int32 there instead. Backends that need the length as an ordinary scalar kernel argument (CUDA/Metal/OpenCL) treat this identically to RSA_Int32.

    *)
  3. | RSA_Int32 of int32
  4. | RSA_Int64 of int64
  5. | RSA_Float32 of float
  6. | RSA_Float64 of float

Argument type for run_source. Buffer binder receives typed kargs.

type convergence =
  1. | Uniform
  2. | Divergent
  3. | Sync

Convergence behavior of an intrinsic.

  • Uniform: All threads in warp/wavefront compute same value
  • Divergent: Threads may compute different values
  • Sync: Intrinsic contains synchronization (barrier)
module type INTRINSIC_REGISTRY = sig ... end

Intrinsic registry interface for backend-specific intrinsics. Note: The actual intrinsic_impl type is defined in each backend's intrinsic registry module to avoid circular dependencies with Sarek_ir.

type exec_arg = Typed_value.exec_arg =
  1. | EA_Int32 of int32
  2. | EA_Int64 of int64
  3. | EA_Float32 of float
  4. | EA_Float64 of float
  5. | EA_Scalar : (module Typed_value.SCALAR_TYPE with type t = 'a) * 'a -> exec_arg
  6. | EA_Composite : (module Typed_value.COMPOSITE_TYPE with type t = 'a) * 'a -> exec_arg
  7. | EA_Vec of (module Typed_value.EXEC_VECTOR)

Re-export typed value types for convenience

module type BACKEND = sig ... end

Extended backend signature for Phase 4 unified execution. Adds execution model discrimination and IR-based code generation.

module type PLUGIN_BASE = sig ... end

Low-level backend implementation interface shared by the CUDA, OpenCL, and Metal plugin-base modules. This is the device/memory/stream/event/kernel core that each backend's *_plugin_base.ml implements directly on top of its FFI bindings; the full BACKEND interface (source generation, direct execution, intrinsics, external-kernel execution, kargs wrapping) is assembled on top of it in each backend's *_plugin.ml.