Module Sarek_interp.Sarek_ir_interp_eval

val positional_field_index : string -> int option

Positional tuple-field index for a synthesized _tup_* record: "_0" -> Some 0, "_12" -> Some 12, any other name -> None. Used to resolve tuple-element field access without a record-registry entry.

val coopmat_subgroup_size : int

Lanes per cooperative-matrix subgroup. 32, the CUDA/Metal width and the tile width of the kernels in this repository. A device with a wider subgroup (wave64) corresponds to two interpreter subgroups; that is only visible to a kernel in which two interpreter subgroups touch the same tile, which is a data race on a 32-wide device and not a supported program.

val linear_thread_id : Sarek_ir_interp_value.thread_state -> int

Linear invocation index within the block (x fastest).

val coopmat_is_leader : Sarek_ir_interp_value.thread_state -> bool

The lowest lane of its subgroup: the one that executes a cooperative-matrix operation on the subgroup's behalf.

val coopmat_key : Sarek_ir_interp_value.thread_state -> 'a -> int * 'a

The fragment-table key of name as seen by the subgroup of state.

val coopmat_element : layout:Sarek_coopmat_types.layout -> base:int -> stride:int -> int -> int -> int

The buffer position of element (r, c) of a fragment loaded from or stored to base with stride in layout (Sarek_ir_types.CM_load).

val eval_intrinsic : Sarek_ir_interp_value.thread_state -> string list -> string -> Sarek_ir_interp_value.value list -> Sarek_ir_interp_value.value

Main intrinsic dispatcher - tries each category in order

eval_intrinsic for a call that may need the block's shared table: the warp operations exchange through it. Everything else is path-dispatched as before.

val eval_intrinsic_by_type : string list -> string -> Sarek_ir_interp_value.value list -> Sarek_ir_interp_value.value

Try type-specific intrinsics based on path

val eval_registered_intrinsic : string list -> string -> Sarek_ir_interp_value.value list -> Sarek_ir_interp_value.value

An intrinsic with no built-in entry: run the host implementation that let%sarek_intrinsic registered for it (any library's, sarek's stdlib or a downstream one), converting each argument to its DECLARED type. Raises Unknown_intrinsic when nothing is registered, which is the case for a signature with a non-scalar type.

Expression Evaluation

Array expression evaluation

Record and variant expression evaluation

Control flow expression evaluation

Cast and intrinsic expression evaluation

Main expression evaluator - dispatches to specialized handlers

val get_array : Sarek_ir_interp_value.env -> string -> Sarek_ir_interp_value.value array

Statement Execution

Cooperative matrix — backlog-62 slice 3

The interpreter is the ORACLE every backend is checked against, so this is not a courtesy implementation: test_coopmat_integer_e2e (GLSL) and test_coopmat_hip_e2e (HIP) compare the backends' output against these numbers bit for bit, and a skip here would let a coopmat kernel "agree" with an interpreter that never computed the product.

Each operation is executed ONCE PER SUBGROUP, by the subgroup's lowest lane (coopmat_is_leader), on a whole-matrix fragment owned by the subgroup (coopmat_key); the other lanes' statements are no-ops. Running it in every invocation would not be equivalent to the device: in-place D = A*B + D would accumulate once per lane. See Sarek_ir_interp_value.env.coopmats for the model and its assumptions (dynamically uniform arguments, every lane reaching the operation).

Integer configurations are a strict oracle: the specification states integer accumulation is exact at the precision of the result type.

The one float configuration with a derived bound — f16 * f16 + f32 -> f32 — is evaluated only after Sarek_coopmat.accept_relaxed_accumulation, and in ONE FIXED ORDER: acc := C[m][n], then for k = 0 .. K-1, acc := fl32 (acc + A[m][k] * B[k][n]). The product of two binary16 values is exact in binary32, so the only rounding is the addition's. The hardware chooses its own order, so this is one admissible member of the bounded set (docs/design/f16-relaxed-accuracy.md §5.2), not a value a device must equal; tests compare both against the exact result under the bound. Every other float configuration is refused (Sarek_coopmat.policy_verdict).

val to_bfloat16 : float -> float

Round a binary32 value to bfloat16 (round to nearest, ties to even), the result kept as a binary32 value. NaN stays NaN.

Convert a buffer element to the declared component type.

For the 8-bit operand types this is what makes the interpreter a faithful oracle rather than merely a plausible one: a value loaded into a u8 fragment from a buffer holding 300 is 44 on the device, and an oracle that kept 300 would disagree with correct hardware. For f16 it is the round-to-nearest-even narrowing the device performs (the identity on a float16 buffer).

val coopmat_refuse_policy : Sarek_ir_interp_value.env -> Sarek_coopmat_types.config -> unit

Kernel Execution

type parked = (unit, unit) Stdlib.Effect.Deep.continuation * bool

A parked thread: its continuation, and whether it waits on a block-wide barrier (as opposed to a warp barrier).

val thread_handler : parked option array -> int Stdlib.ref -> int -> (unit, unit) Stdlib.Effect.Deep.handler

The effect handler of thread tid: a barrier parks the thread in waiting; finishing counts it in num_completed.

val check_barrier_can_release : parked option array -> num_completed:int -> unit

A block-wide barrier releases only when EVERY thread of the block has arrived. After a round of execution each thread is either parked or finished, so a block barrier with parked threads AND finished ones can never release: the finished threads will not arrive. Threads parked on a warp barrier prove nothing about the rest of the block.

val run_block : Sarek_ir_interp_value.env -> Sarek_ir_types.stmt -> (int * int * int) -> (int * int * int) -> (int * int * int) -> unit

Run all threads in a block with BSP barrier synchronization

val run_grid_sequential : Sarek_ir_interp_value.env -> Sarek_ir_types.stmt -> (int * int * int) -> (int * int * int) -> unit

Run all blocks in a grid (sequential)