Module Sarek_coopmat

Cooperative matrix: the DEVICE-facing half.

Every type and value of Sarek_coopmat_types is re-exported here by include module type of, with its type equalities intact, so Sarek_coopmat.fragment, Sarek_coopmat.Uint8 and the rest mean exactly what they meant before slice 3 split the module. Read Sarek_coopmat_types's interface for the vocabulary and the design rationale behind it.

What is defined HERE is the part that consults Sarek_capability, and it is separated for a mechanical reason as much as a conceptual one: the IR names a fragment, Sarek_capability depends on the IR, and a vocabulary that also depended on Sarek_capability would close a module cycle.

include module type of struct include Sarek_coopmat_types end

What this module deliberately does NOT do

It does not emit code, and it does not decide accuracy. regime classifies a configuration into the two acceptance regimes of the design document's §1.6, but it does not admit anything: the device verdict and the accuracy policy (Sarek_coopmat.verdict, Sarek_coopmat.policy_verdict) do. The emitters are GLSL (integer configurations), CUDA/HIP (specs/coopmat-hip-wmma.md) and Metal (specs/coopmat-metal-simdgroup.md); nothing in the DSL produces a fragment, so a cooperative-matrix kernel is built as IR.

Why the type admits integers

§8 of the design document, adopted as binding by §7 slice 4b. Twelve of the fourteen configurations the local RX 7900 XTX advertises are integer; SPV_KHR_cooperative_matrix states that integer accumulation is exact at the precision of the result type; so those configurations are deliverable under Sarek's EXISTING strict accuracy contract, with no relaxation, no allowlist and no opt-in. accumulation_is_exact is where that distinction is computed rather than asserted in prose. Retrofitting integer component types after an f16-only fragment type had shipped would be a wide, invasive change; admitting them now costs one variant group and one predicate.

Component types

type component_type = Sarek_coopmat_types.component_type =
  1. | Float16
  2. | BFloat16
    (*

    bfloat16 operand (specs/matrix-pattern-rewrite.md). A BFloat16 fragment is loaded from a float32 buffer, each element rounded to bfloat16 (round to nearest even): exact for values already representable. Lowered on HIP gfx11 only.

    *)
  3. | Float32
  4. | Uint8
  5. | Sint8
  6. | Uint32
  7. | Sint32

The element type of one matrix operand or result.

The float half is the two configurations that need the relaxed contract; the integer half is the twelve that do not. Closed on what has been MEASURED to exist on a device this project can reach — the Vulkan set of docs/design/f16-relaxed-accuracy.md §4 — plus BFloat16, added with its measurement on HIP gfx11 (specs/matrix-pattern-rewrite.md). Metal's 8x8 bfloat simdgroup_matrix (§7 slice 6) is still unmeasured and not lowered.

val component_name : component_type -> string

Stable lowercase rendering: "f16", "bf16", "f32", "u8", "s8", "u32", "s32". Matches the column headings of the design document's §4 table and the ctype function of tools/probes/vulkan_coopmat_probe.c, so a probe line and a Sarek diagnostic can be compared by eye.

val component_bits : component_type -> int

Width in bits.

val component_is_integer : component_type -> bool

Whether the component type is an integer type.

Load-bearing rather than cosmetic: it is what accumulation_is_exact reads, and therefore what decides whether a configuration falls under the strict contract or needs the relaxation.

Scope

type scope = Sarek_coopmat_types.scope =
  1. | Subgroup
  2. | Workgroup
  3. | Device_scope
  4. | Queue_family

The set of invocations that cooperate to hold one matrix.

All fourteen configurations measured locally are Subgroup scope, and Metal's simdgroup_matrix is a SIMD-group (i.e. subgroup) construct too, so Subgroup is the only scope any planned backend can currently produce. The other three are modelled because Sarek_capability's lesson is that a value you cannot represent becomes a value you silently permit: a device reporting Workgroup scope must come back as an unrecognised-but-named scope, not be quietly rewritten to Subgroup.

val scope_name : scope -> string

Shapes

type shape = Sarek_coopmat_types.shape = {
  1. m : int;
  2. n : int;
  3. k : int;
}

A m x n x k multiply-add shape: A is m x k, B is k x n, and C and the result are m x n.

A record of three ints rather than a closed variant of the shapes seen so far, because §7 slice 4b makes non-hard-coded dimensions binding: Vulkan measured 16x16x16 and Metal measured 8x8x8, and 8x8 is the ONLY size MSL offers, so a type that could only spell 16x16x16 would already be wrong for a backend whose numbers are in the same document.

val shape_name : shape -> string

Configurations

type config = Sarek_coopmat_types.config = {
  1. cfg_shape : shape;
  2. cfg_a : component_type;
  3. cfg_b : component_type;
  4. cfg_c : component_type;
  5. cfg_result : component_type;
  6. cfg_saturating : bool;
  7. cfg_scope : scope;
}

One multiply-add configuration a device advertises: D = A x B + C.

cfg_saturating is Vulkan's saturatingAccumulation — integer accumulation that clamps instead of wrapping. It is a separate field rather than a component type because it is a property of the OPERATION, not of any operand: the local device advertises the same s8 x s8 -> s32 element types both with it and without it, and those are two distinct configurations that compute different functions.

val config_name : config -> string

A one-line rendering, e.g. "16x16x16 f16*f16+f32->f32 subgroup". Appears in diagnostics.

Accuracy regime — the §8 discriminator

val accumulation_is_exact : config -> bool

Is the accumulation of this configuration exact?

True exactly when the addend and result component types are both integer. SPV_KHR_cooperative_matrix states that integer accumulation is performed at the precision of the result type and is exact, so such a configuration computes the same function as the interpreter and lands under Sarek's existing strict contract. Every float configuration is false: the specification leaves the ORDER of the k + 1 additions to the implementation, which is a freedom no closed-form model can pin down (design document §5.1).

type accuracy_regime = Sarek_coopmat_types.accuracy_regime =
  1. | Strict
  2. | Relaxed_bounded

The two acceptance regimes of docs/design/f16-relaxed-accuracy.md §1.6.

Strict means bit-identity with the interpreter is still promised. Relaxed_bounded means only the derived error bound of §5.2 holds, which §6.1 makes an explicit opt-in rather than a diagnostic.

val regime : config -> accuracy_regime
val regime_name : accuracy_regime -> string

What a device provides

type device_support = Sarek_coopmat_types.device_support = {
  1. ds_configs : config list;
  2. ds_robust_buffer_access : bool;
    (*

    Vulkan cooperativeMatrixRobustBufferAccess: whether out-of-bounds cooperative-matrix loads and stores are bounds-checked.

    *)
  3. ds_subgroup_size : int;
    (*

    Invocations per subgroup, as the device reports it — NOT a constant. Measured 64 on the RX 7900 XTX under radv / Mesa 26.1.4-arch3.1, where Vulkan_plugin_base had been hard-coding 32.

    *)
  4. ds_advertised_count : int;
    (*

    How many configurations the DEVICE reported, including any this build could not represent and therefore dropped from ds_configs.

    Kept because dropping an unrepresentable configuration is the safe direction (it can only cause a refusal) but it is also SILENT, and a silent drop hid a real defect once: a wrong VkComponentTypeKHR enumerant table turned fourteen advertised configurations into six plausible-looking wrong ones. The equality ds_advertised_count = List.length ds_configs is the check that catches it, and it is hardware-independent — unlike any assertion about which configurations a particular GPU offers.

    *)
  5. ds_evidence : string;
    (*

    How the probe decided, in one sentence a refusal can quote: the backend's rule and the device facts it read (e.g. the Vulkan extension and feature bits, or the HIP gfx family and warp size). Sarek_coopmat.device_lacks_config puts it in the refusal, so a refused launch says WHY this device, on this backend, offers no configuration — the backends decide by different rules and a single backend's wording would mislead on the others.

    *)
}

A device's cooperative-matrix support, as probed.

ds_subgroup_size is here rather than left to the caller because a subgroup-scope fragment's storage is distributed across exactly that many invocations, so it is part of the calling convention and not an unrelated device statistic. See components_per_invocation.

val config_matches : shape:shape -> a:component_type -> b:component_type -> c:component_type -> result:component_type -> config -> bool

config_matches ~shape ~a ~b ~c ~result cfg compares the DIMENSIONS and the four component types, and deliberately NOT cfg_saturating or cfg_scope.

Those two are what separates configurations that this predicate is used to group: the local device advertises the same s8 x s8 -> s32 element types both saturating and not, and they compute different functions. Callers that need an exact match (verdict) test them explicitly on top; callers that are searching (find_config) rank them. Folding them in here would make the two behaviours indistinguishable at the call site.

val find_config : support:device_support option -> shape:shape -> a:component_type -> b:component_type -> c:component_type -> result:component_type -> config option

find_config ~support ~a ~b ~c ~result ~shape returns the first advertised configuration matching those component types and that shape, preferring a non-saturating one. None when the device was not probed or advertises no such configuration.

The fragment type (slice 4b)

type use = Sarek_coopmat_types.use =
  1. | Matrix_a
  2. | Matrix_b
  3. | Accumulator

Which operand of D = A x B + C a fragment holds.

Accumulator covers both C and the result D, which are the same shape and the same component type in every configuration measured, and which SPIR-V and MSL both give a single fragment role.

val use_name : use -> string
type layout = Sarek_coopmat_types.layout =
  1. | Row_major
  2. | Col_major

How a matrix is laid out in the buffer a fragment is loaded from or stored to, with index the buffer position of element (0, 0) and stride the distance between consecutive rows (Row_major: element (r, c) is at index + r * stride + c) or consecutive columns (Col_major: element (r, c) is at index + c * stride + r).

A memory property of one load or store, not of the fragment: the same fragment may be loaded from a row-major buffer and stored to a column-major one.

val layout_name : layout -> string
type fragment = Sarek_coopmat_types.fragment = {
  1. frag_use : use;
  2. frag_shape : shape;
  3. frag_component : component_type;
  4. frag_scope : scope;
}

A cooperative-matrix fragment: the DSL-side value one invocation holds a slice of.

It is NOT a per-invocation array. A fragment is a subgroup-cooperative value: the whole subgroup collectively holds rows x columns components, each invocation holding components_per_invocation of them at an implementation-defined position. That indeterminate position is why a fragment must not be indexable from the DSL, and it is the reason this type exists at all rather than the DSL using an array.

val fragment_dims : fragment -> int * int

fragment_dims f is (rows, columns), derived from use and the shape: A is m x k, B is k x n, and an accumulator is m x n. Derived rather than stored so a fragment cannot be built claiming a size its shape does not have.

val fragment_components : fragment -> int

Total components in the whole fragment, i.e. rows * columns.

val fragments_of_config : config -> fragment * fragment * fragment * fragment

The fragments a configuration operates on: (a, b, c, result).

The subgroup calling convention

val components_per_invocation : subgroup_size:int -> fragment -> (int, string) Stdlib.result

components_per_invocation ~subgroup_size f is how many components of f each invocation of the cooperating subgroup holds.

Error when subgroup_size does not divide fragment_components, which is a real constraint and not a defensive check: a 16x16 fragment over a 64-wide subgroup is 4 components per invocation, and the same fragment over a 24-wide subgroup has no distribution at all. It returns a result rather than raising because it is the check a codegen slice must perform BEFORE emitting anything, and it is the check a device query must survive when a driver reports a subgroup size the configuration cannot be laid out over.

The value itself is deliberately NOT a promise about WHICH components an invocation holds. That mapping is implementation-defined in both SPIR-V and MSL; only the count is portable.

val config_fits_subgroup : subgroup_size:int -> config -> bool

config_fits_subgroup ~subgroup_size cfg is true when every one of the four fragments of cfg can be distributed over a subgroup of that size.

val verdict : support:device_support option -> config -> Sarek_capability.verdict

verdict ~support cfg judges a requested configuration against a device.

support = None yields Sarek_capability.verdict.Unknown, which Sarek_capability.permits refuses. That is the reason this takes an option and the reason Framework_sig.capabilities stores an option: an empty configuration list and an unprobed device are different facts, and only one of them is evidence.

The gate must be keyed on the feature, not on the configuration list, and this is measured rather than argued. On this workstation vkGetPhysicalDeviceCooperativeMatrixPropertiesKHR returns VK_SUCCESS and FOURTEEN configurations for the Raphael iGPU — a device that does not advertise VK_KHR_cooperative_matrix and whose cooperativeMatrix feature reads false. A probe that populated ds_configs from that call without first checking the extension would report the iGPU as fully capable, and this verdict would say Available for a device that cannot run the instruction. The Vulkan probe therefore leaves ds_configs empty unless the extension is advertised AND the feature is true; see sarek-vulkan/Vulkan_api_device.ml.

val device_lacks_config : ?evidence:string -> config -> Sarek_capability.t

The Sarek_capability.kind.Device_optional record for a device that provides no cooperative-matrix support at all, or none matching the request. evidence is the probe's device_support.ds_evidence; verdict passes it, so the refusal says which backend rule refused this device.

val fragment_verdict : support:device_support option -> fragment -> Sarek_capability.verdict

fragment_verdict ~support f: does the device offer any configuration one of whose four fragments is f? A kernel that declares, loads or stores a fragment without ever multiplying still needs the device's per-lane layout for it, so the launch gate asks this for every fragment as well as verdict for every multiply-add. None support is Unknown.

The accuracy policy (docs/design/f16-relaxed-accuracy.md §6.1)

A float configuration is Relaxed_bounded: the hardware chooses the order of the additions, so its result is within a derived bound of the exact value but not bit-identical to the interpreter. The owner's decision of 2026-07-27 is that such a deviation needs an EXPLICIT opt-in and that the launch fails without it; these three values are that opt-in.

val accept_relaxed_accumulation : reason:string -> unit

accept_relaxed_accumulation ~reason admits the float configurations that have a derived bound (f16 * f16 + f32 -> f32 and bf16 * bf16 + f32 -> f32; the latter also needs accept_operand_rounding) for the rest of the process. One-way: there is no withdrawal, so a capability check that has passed stays valid. The first non-empty reason is kept.

  • raises Invalid_argument

    if reason is empty or blank.

val relaxed_accumulation_reason : unit -> string option

The reason recorded by accept_relaxed_accumulation at process scope, if it was called. Like the other *_reason () readers of this module it does not see Kernel-scoped grants: the verdicts take a budget (policy_verdict_for).

Operand rounding (specs/matrix-pattern-rewrite.md)

A float32 matrix product computed on matrix units must first round its operands to a narrower type. That is a larger deviation than the accumulation order accept_relaxed_accumulation admits, so it has its own opt-in, per precision: accepting one does not accept another — for the matrix rewrite. A hand-built BFloat16 configuration is admitted by either Operands_bf16 or Operands_bf16x3, since the configuration cannot tell a split term from a plain rounded operand. Operands_bf16x3 splits each operand into three bfloat16 terms (x = hi + mid + lo) and keeps the six products of order at most two, for near-float32 accuracy. Process-wide and one-way, like accept_relaxed_accumulation.

type operand_precision = Sarek_policy.operand_precision =
  1. | Operands_f16
  2. | Operands_bf16
  3. | Operands_bf16x3
val operand_precision_name : operand_precision -> string
val accept_operand_rounding : precision:operand_precision -> reason:string -> unit
  • raises Invalid_argument

    if reason is empty or blank.

val operand_rounding_reason : operand_precision -> string option

The reason recorded for that precision, if it was accepted.

Automatic float rewrite (specs/matrix-pattern-dynamic.md)

Execute.run_vectors can rewrite a program's OWN float GEMM-shaped kernels onto matrix units, without the program having asked for matrix units. That is a separate decision from accepting the accuracy deviation: the accuracy opt-ins (accept_relaxed_accumulation, accept_operand_rounding) admit matrix-unit configurations for code that asks for them explicitly (Sarek_gemm.Coopmat, Sarek_matrix.run); they do NOT enable the automatic rewrite. The automatic float rewrite happens only when this opt-in AND the accuracy opt-ins required for the configuration were all given. Granting one never enables more than it names. int32 (exact) products are rewritten automatically without any opt-in.

This opt-in has no environment variable, like the accuracy opt-ins: it is a statement in the program's source. Process-wide, one-way, thread-safe.

val accept_automatic_float_rewrite : reason:string -> unit

accept_automatic_float_rewrite ~reason: the first non-empty reason is kept; later calls are no-ops.

  • raises Invalid_argument

    if reason is empty or blank.

val automatic_float_rewrite_reason : unit -> string option

The reason recorded by accept_automatic_float_rewrite, if it was called.

val policy_verdict : config -> Sarek_capability.verdict

policy_verdict cfg judges the accuracy regime, independently of any device:

  • configurations whose four component types are all integer are Available (strict: exact accumulation);
  • f16 * f16 + f32 -> f32 is Available after accept_relaxed_accumulation;
  • bf16 * bf16 + f32 -> f32 is Available after accept_relaxed_accumulation AND accept_operand_rounding for Operands_bf16 or Operands_bf16x3 (its load rounds float32 operands);
  • every other configuration with a float component is Unavailable (no derived bound, §5.4). A refusal is a Sarek_capability.kind.Policy record naming the missing call. The launch gate and the interpreter apply it after the device verdict.

policy_verdict_for budget cfg: policy_verdict against the grants of budget (pure). policy_verdict cfg is policy_verdict_for (Sarek_policy.budget ~kernels:[]) cfg, the process grants only, for a caller with no kernel; a caller that knows the kernel passes Sarek_policy.budget ~kernels:[name] so that a Kernel-scoped Accumulation_order or Operand_rounding grant is honoured for that kernel only (the launch gate, the interpreter).

val policy_decision_for : Sarek_policy.Budget.t -> config -> Sarek_policy.decision

policy_decision_for budget cfg: the same judgement as a decision for the explain report. Refused names the missing capability (the cap_name of the refusal); Applied says Exact_by_construction for an integer configuration and otherwise Granted with the grants it rests on (Accumulation_order, and the operand rounding of a bf16 operand) and their reasons.