Cost_model (arrayjit.Ir.Cost

type node_footprint = {

fp_read_bytes : int;
(*
Distinct cells read (including accumulation reads) times byte width.
*)
fp_write_bytes : int;
(*
Distinct cells written times byte width.
*)
fp_rmw_bytes : int;
(*
The subset of fp_write_bytes written by read-modify-write accumulations (a_rmw).
*)
fp_approx : bool;
(*
true when any contributing count is an upper bound rather than exact (see the module contract for the causes).
*)

}

val sexp_of_node_footprint : node_footprint -> Sexplib0.Sexp.t

type summary = {

per_node : (Tnode.t * node_footprint) list;
(*
In first-access program order.
*)
read_bytes : int;
(*
Sum of fp_read_bytes over per_node.
*)
write_bytes : int;
(*
Sum of fp_write_bytes over per_node.
*)
flops : int;
(*
Whole-kernel arithmetic-op count (loop extents times per-statement ops).
*)
flops_approx : bool;
(*
true when guarded (If) code contributed (guards-taken bound), or a short-circuiting form was charged in full while executing only in part — a Where whose arms carry any inline cost (only one arm's expression executes), a gated right operand with nonzero inline cost (gh-ocannl-578). A cost residing in a hoisted Local_scope body executes unconditionally — every renderer emits scope definitions before the statement's expression — so it is charged exactly and never flags (gh-ocannl-637).
*)
opaque : bool;
(*
true when the code contains Staged_compilation or merge-buffer reads: some traffic and ops are invisible to the analysis, so counts may UNDER-estimate.
*)

}

val sexp_of_summary : summary -> Sexplib0.Sexp.t

val analyze : Low_level.t -> summary

The whole-kernel extraction: footprints from Low_level.affine_accesses image cardinalities, op counts from a loop-nest walk. Input is typically post-optimize code — the analysis charges whatever materialization the code actually performs, so virtual/inlined nodes never appear and recomputation is charged as ops, not bytes.

val total_bytes : summary -> int

read_bytes + write_bytes: the "bytes moved" denominator of arithmetic intensity — an accumulation's cells are charged once in each direction.

val arithmetic_intensity : summary -> float

FLOPs per byte moved, flops / max 1 (total_bytes).

val footprint_approximate : summary -> bool

true when any per-node footprint is an upper bound rather than exact (fp_approx) — the byte counts over-approximate while the op count may still be exact.

type floor = {

fr_flops : int;
fr_bytes : int;
fr_exact : bool;

}

Lower bounds on arithmetic work and compulsory traffic — the dual extraction (gh-ocannl-514 phase 3), for bounding every completion of a partial placement vector where analyze upper-bounds one concrete candidate. fr_exact is false when some flooring occurred (a guarded body, a non-exact access image counted at its lower bound, opaque code): the floor is then sound but not tight.

val sexp_of_floor : floor -> Sexplib0.Sexp.t

val completion_floor : 
  ?open_placement:(Tnode.t -> bool) ->
  Low_level.t ->
  floor

The floor of the roofline legs over placement completions, with every approximation biased down — the exact dual of analyze's contract:

fr_flops: guarded (If) bodies count zero (guards-never-taken, dual to guards-taken); the short-circuiting forms count only their certain part — Where its condition plus the cheaper arm's inline work (rendered as ?:), And/Or the left operand's (rendered as &&/||), both sides' hoisted scope bodies in either case (they execute regardless, gh-ocannl-637), the Arg1/Arg2 projections only the selected operand (the discarded one is never rendered, hoisted definitions included); opaque code counts zero (an under-count is sound in this direction); Tile_mma keeps the lane-cooperative attribution, exact when the lane binding is in scope. Statements producing an open_placement node — the Set family and Tile_mma with an open accumulator — count zero: an inline completion instantiates the producer only at surviving consumer sites, possibly fewer cells than the setter loop covers, so "recomputation only adds ops" does not hold and the producer's whole effect attributes to the open placement. Call this on the all-materialized specialization of the decision surface, where every open node's work sits in its own producer statement.
fr_bytes: per node and direction, the sum of the exact images when they are pairwise provably disjoint (a disjoint union attains its sum — both extractions then agree, gh-ocannl-578), otherwise the largest exact image (a union is at least its largest member — dual to the upper extraction's capped sum; a second nonzero contribution then marks the floor loose); a certain access whose image is not exact — an overlapping window's s*o + d*k, a dynamic gather's or a vector run's known coordinates — counts Affine.image_cardinality_lb of its coordinate view (gh-ocannl-1601), at most its true image; guarded, dead-loop-enclosed, conditionally-evaluated (a Where arm's or an And/Or right operand's inline read — not a hoisted scope body's) and open-producer-operand accesses contribute zero — their execution is not certain in every completion. So does an accumulation's read of its own cell (the read at the position its read-modify-write statement writes): a privatizing completion accumulates in a register and stores the target once (gh-ocannl-1601). Nodes with open_placement contribute zero.

Committing a placement decision is re-evaluation with the narrowed open_placement: the suppression sets only shrink, so the floor is monotone in refinement — the property that lets a bound prune as commitments accumulate. (An incremental per-node delta cannot be sound in isolation: a Materialize commitment also makes its producer's operations and operand reads certain, not just the node's own traffic.) Committing to Inline tightens nothing for now: a nonzero recompute floor needs lower-bound multiplicity metrics, deferred until the driver proves the need.

A max (fr_flops/peak_flops) (fr_bytes/peak_bandwidth) roofline over these floors (roofline_seconds) lower-bounds every completion — the two legs' minima need not be simultaneously achievable for the max of the two to be sound.

val approximate : summary -> bool

flops_approx || footprint_approximate: some count is an upper bound rather than exact. Such counts are still upper bounds (unlike under opaque), but a candidate whose guards mostly fail can carry counts far above the work it performs — quantities derived from an approximate count (achieved throughput, the roofline bound vs. a measurement) are not evidence about the hardware. Exactness is per leg: op counts (flops_approx) and byte counts (footprint_approximate) go approximate independently.

val roofline_seconds : 
  ?peak_flops:float ->
  ?peak_memory_bandwidth:float ->
  flops:int ->
  bytes:int ->
  unit ->
  float option

The roofline lower-bound time: max (flops/peak_flops) (bytes/peak_memory_bandwidth) over the envelope constants present (peak_flops in FLOP/s, peak_memory_bandwidth in bytes/s — the advisory Backend_intf.hardware_limits fields); None when neither is given. Monotone: raising either constant never increases the bound. A lower bound only up to the model's upper-bound byte/op counts — rank with it, do not predict.

The ranking score (gh-ocannl-1253)

analyze charges distinct cells under a perfect cache: that is what makes it a lower bound, and what scores an untiled contraction exactly at its roofline floor however often its operands are re-read from DRAM — the branch-and-bound over the tiling families then fathoms every sketch. The ranking score is the second, separate quantity the untimed choosers rank by (Autotune.model_default, the auto seeding gate of Autotune.seeded_default). The bound is unchanged and keeps serving pruning, pre-filtering, the agreement check and calibration rows; putting a cache model into it would raise BOUND VIOLATION whenever a kernel hits in cache.

Contract:

Global reads are REQUESTED per block: the cells one block touches — its Grid loops standing still, Affine.fiber_cardinality over the remaining loop box, capped by the node — times the number of blocks (the product of the enclosing Grid extents). An untiled weight gradient under a Grid row and a wg-thread Workgroup requests M·N·K·elt·(1 + 1/wg); a bm × bn blocktile M·N·K·elt·(1/bm + 1/bn). Reuse within a block is free (it is what the block's shared tiles and L1 are for); reuse across blocks is what is priced. Global means neither Local nor workgroup-shared (global_in): staged tiles and thread-private scratch keep their distinct-cell charge. Per node, the requested bytes are never below analyze's distinct read bytes.
Serial re-reads of a one-block nest (gh-ocannl-1633). A nest with no Grid loop is one block, so the per-block charge alone requests only its distinct cells, and a serial kernel's sketches could at best tie it. Given a capacity, and only where that nest's bytes exceed it, a global read is also re-requested once per iteration of each enclosing Serial loop it is invariant along (no known coordinate of its map mentions the loop) whose one iteration — that loop and every loop outside it standing still — touches more global read bytes than the capacity (each node's accesses summed, capped at the node; the whole capped at the nest's bytes). A loop whose iteration fits keeps the read cached: the untiled i, j, k matmul re-reads B[k, j] once per i where a row of A and all of B do not fit, not A[i, k] once per j, and no accumulator once per k. Re-reads are therefore charged only in a spilling nest, at the DRAM rate. Point-in-time boundary: one cache level; invariant loops only (overlap along a loop the map mentions, a window's, counts as kept); reads the map does not describe (whole-node, Concat, dynamic, uninterpretable) keep their distinct charge; and a multi-block nest's serial loops within a block re-read nothing. Without a capacity (the calibration's sweep, cc and Metal at their shipped constants) the charge is exactly the per-block one. The working set is unchanged.
Two tiers (the wave decision of 2026-10-18 on the measured HIP boxes, where cache-served re-reads ran at 1.5–2.8 TB/s against 235–261 GB/s from DRAM). Past capacity — the working set, per-block bytes times the blocks resident at once (max_resident_threads over the kernel's launch block, Low_level.launch_dims, at most the blocks; all blocks when no residency is given), the largest over the kernel's launch nests, exceeding cache_capacity_bytes — the requested bytes are charged at the DRAM rate (below). Within it (or with no capacity), they are charged at cache_bandwidth beside the distinct bytes at the DRAM rate, whichever leg is longer; with no cache bandwidth either, the memory leg is the distinct bytes at the DRAM rate — with no reuse extraction and no DRAM rate, exactly the roofline. A cache bandwidth below the DRAM rate is read as the DRAM rate.
Its own rates (gh-ocannl-1442). The bound divides by ceilings (peak_flops, peak_memory_bandwidth: class ceilings, so that no kernel beats its bound); the score divides by what kernels achieve. dram_bandwidth (the STREAM-achieved DRAM rate) prices the DRAM tier and the distinct bytes; issue_rate (the effective scalar operation rate of a register-blocktiled kernel, its staging included) prices the scalar operations, while the Tile_mma work the backend accepts (the caller's mma_flops, accepted_tile_mma_flops) is priced at mma_rate (below): a scalar rate never prices work on the matrix units. Tile-MMA work not counted there — declined by a layout or by the backend's hook, so its scalar fallback runs, or not classified at all — is priced as scalar work. Each rate reads as at most its ceiling, and as the ceiling when not given, so a device without them scores exactly as before.
Memory space (gh-ocannl-1442). Under the per-block model (a reuse extraction given), the bytes of the nodes the kernel touches outside global memory (reuse.ru_scratch: staged workgroup tiles and thread-private scratch) are off the DRAM leg. Their cost is carried by the fitted issue rate — an empirical approximation that holds for the staging geometry the rate was fitted on, not a model of copies, barriers or shared-memory gathers. Without a reuse extraction they keep the roofline's charge.
Tile-MMA rate and device gathers (gh-ocannl-1495). Accepted tile-MMA work is priced at mma_rate, the effective rate the staged tensorized kernels of a site achieve, read as at most peak_flops and as it when not given. The per-lane operand gathers those statements issue straight from device memory (the caller's device_gathers, device_operand_gathers) add their count over device_gather_rate to the compute leg, at the Tile_mma contexts' fill under a launch model; no rate, no term. That is what operand staging buys: at the gh-ocannl-1190 fp8 site on rog the staged leaves ran 2.3x faster than the unstaged ones, which every score before tied. Shared-memory gathers, ldmatrix and whole-fragment loads are not priced (their cost is in the fitted mma_rate), nor bank conflicts, swizzle arithmetic or barriers, and the two plain/swizzled twins of a staged geometry still tie exactly. Several Tile_mma contexts in one kernel share their class's harmonic fill, as the accepted work does.
Launch fill (gh-ocannl-1479). Given a fill_model and the kernel's launch_contexts, the scalar work is priced at the issue rate times its contexts' fill (context_fill): per parallel context, its operations over its fill, summed. Serial loops (a plain leaf's batch loops) multiply work but add no parallelism; Grid and Workgroup loops add parallelism, not work. Tile-MMA work takes the fill of the Tile_mma statements' contexts: accepted work at mma_rate, declined work (its scalar fallback) at the issue rate. The saturating thread count is fitted on scalar kernels; for the matrix units it is uncalibrated, and the blocks-over-multiprocessors factor is what orders a plain tensorized leaf against its bgrid twin. Without a fill model the compute leg is exactly as before. A launch-shape proxy, not an occupancy model: no registers, shared memory, wave quantization, or the block a wider sibling nest allocates.
Memory transactions (gh-ocannl-1600). Given the kernel's memory_transactions and a transaction_rate (sectors/s), the excess sector transactions of its global accesses -- per launch block, the sectors touched beyond the compact count for the same distinct bytes, each context's over its fill under a launch model -- add their count over the rate to the compute leg: a strided access's replays occupy the issuing multiprocessor. That is what orders a layout whose lanes read contiguous cells against a twin whose lanes stride, which every term above ties (same work, launch and footprints). A fitted relative term: alignment is assumed, L1 serves a sector across the block's lane groups and a lane's innermost run; other L1/L2 reuse of an over-fetched sector is in the fitted rate; bank conflicts are not modeled. No rate, or no excess: the leg is exactly as before. And the kernel's occupancy, given a workgroup capacity per multiprocessor: the compute leg over the fraction of a multiprocessor's thread slots its resident blocks fill -- what orders a deep-K staged tile (16-64 KiB of workgroup memory per block) against its shallow twin on HIP's RDNA parts, measured. Registers are not modeled, nor the launch size (the fill's).
Never below the bound: the memory leg is at least the distinct bytes at the peak_memory_bandwidth ceiling, and the compute leg at least the operations at the peak_flops ceiling (a fill is at most 1), so ranking_seconds is at least roofline_seconds over analyze's counts — and therefore at least any roofline over completion_floor. Monotone: raising the capacity, the cache bandwidth, the issue rate, the DRAM rate, the tile-MMA rate, the device-gather rate or the transaction rate never raises the score; raising the fill model's multiprocessors or saturating threads never lowers it.

Writes, op counts and the opacity flag are analyze's.

type reuse = {

ru_requested : (Tnode.t * int) list;
(*
Per global node read, in first-access order: the bytes its reads request under per-block caching — blocks times per-block cells times byte width, summed over its read accesses, NOT capped by the node's size (re-reads are the point) — plus, given a capacity, a one-block nest's serial re-reads (gh-ocannl-1633).
*)
ru_working_set_bytes : int;
(*
The largest over the kernel's launch nests of per-block global read bytes times resident blocks.
*)
ru_scratch : Tnode.t list;
(*
The nodes the kernel reads or writes that are not global (is_global false: workgroup tiles, thread-private scratch), in first-access order — the bytes the score keeps off the DRAM leg.
*)

}

val sexp_of_reuse : reuse -> Sexplib0.Sexp.t

val global_in : Low_level.optimized -> Tnode.t -> bool

Whether a node lives in global memory under the specialization's placements: neither Local (thread-private scratch, Tnode.Placements.is_local_peek) nor a workgroup-shared tile.

val reuse_traffic : 
  ?cache_capacity_bytes:int ->
  ?max_resident_threads:int ->
  is_global:(Tnode.t -> bool) ->
  Low_level.t ->
  reuse

The per-block read charge and working set of one kernel (see the section contract). Given cache_capacity_bytes, the charge includes the serial re-reads of a one-block nest that spills it (gh-ocannl-1633); without it, the per-block charge alone.

val requested_bytes : summary -> reuse -> int

total_bytes with each global node's read bytes raised to its requested bytes: all the traffic a kernel moves through the memory hierarchy when every cross-block re-read is a request. Never below total_bytes.

val spills : ?cache_capacity_bytes:int -> reuse -> bool

Whether the working set exceeds the capacity (false without one).

type launch_context = {

lc_blocks : int;
lc_threads : int;
lc_tile_mma : bool;
lc_ops : int;

}

One op-carrying parallel context of a kernel (gh-ocannl-1479): the statements whose enclosing Grid loop extents multiply to lc_blocks and enclosing Workgroup / Workgroup_reduce extents to lc_threads, split by whether they are Tile_mma statements, and their operations — analyze's census (one walk), attributed per statement: a hoisted Local_scope body counts in its hoisting statement's context.

val sexp_of_launch_context : launch_context -> Sexplib0.Sexp.t

val launch_contexts : Low_level.t -> launch_context list

In first-reported order, one entry per distinct context; contexts with no operations (zero nests, copies) are absent. The lc_ops sum to analyze's flops.

type fill_model = {

fm_multiprocessors : int;
fm_fill_threads : int;

}

The device's launch shape as the score reads it: fm_multiprocessors multiprocessors, each saturating its scalar issue at fm_fill_threads threads — a fitted constant (tools/calibrate_issue_rate.exe), not the physical residency.

val sexp_of_fill_model : fill_model -> Sexplib0.Sexp.t

val context_fill : fill_model -> blocks:int -> threads:int -> float

min 1 (B * min T t / (P * t)): the fraction of the device's saturated issue a launch of B blocks of T threads reaches, each block counting at most one multiprocessor's saturating share. Positive, at most 1.

val launch_fill : fill_model -> launch_context list -> float

The scalar contexts' work-weighted harmonic fill: total scalar operations over the sum of each context's operations divided by its fill. 1 without scalar work. A diagnostic: the score sums per context.

type transaction_context = {

tx_blocks : int;
tx_threads : int;
tx_excess : float;
(*
The excess sector transactions of the context's global accesses over the compact count for the same distinct bytes, per launch block and summed over every execution: zero for a fully coalesced access. Residue-averaged, hence fractional.
*)
tx_uncovered : int;
(*
How many of those accesses had an Unknown coordinate (a dynamic axis, a Concat) and were counted one sector per active lane: an estimate, not exact evidence.
*)

}

gh-ocannl-1600: the memory transactions of one parallel context of a kernel -- the global accesses whose enclosing Grid loop extents multiply to tx_blocks and enclosing Workgroup / Workgroup_reduce extents to tx_threads.

val sexp_of_transaction_context : transaction_context -> Sexplib0.Sexp.t

val transaction_sector_bytes : int

The counting unit, 32 bytes: the sector an NVIDIA L1 tags, and the smallest request the supported AMD and Apple parts serve. A fitted transaction rate is per sector of this size.

val memory_transactions : 
  ?sector:int ->
  lane_width:int ->
  is_global:(Tnode.t -> bool) ->
  Low_level.t ->
  transaction_context list

The excess memory transactions of one kernel, per parallel context in first-access order (contexts with no global access are absent). The sectors are the ones the kernel's launch block touches together (slot .x fastest): its lane groups, lane_width consecutive threads each, share what L1 serves (gh-ocannl-1661's partitioned copies: two warps reading the halves of the same sectors carry no excess); lane_width sizes the run window and the estimate of an uncovered access. sector (default transaction_sector_bytes) is the counting unit. Activity follows each access's own workgroup loops (a lane outside one is idle), a slot the access has no loop of is a broadcast, a lane's innermost run (the serial loops inside every hardware loop, while a lane group's footprint over them is at most 8 KiB) is one footprint with its block's (L1 serves the next iteration), the other symbols stand at their base with the base averaged over its sector residues, guards are taken, buffers start sector-aligned, Tile_mma statements and non-global nodes are left out (is_global, as reuse_traffic).

val occupancy : 
  workgroup_bytes:int ->
  block_threads:int ->
  threads_per_mp:int ->
  bytes_per_mp:int ->
  float

gh-ocannl-1600: theoretical occupancy, the occupancy calculator's with registers left out: the blocks of block_threads threads declaring workgroup_bytes workgroup-shared bytes that one multiprocessor of threads_per_mp thread slots and bytes_per_mp workgroup bytes keeps resident -- min (bytes_per_mp / workgroup_bytes) (threads_per_mp / block_threads), at least one -- times block_threads, over threads_per_mp. Positive, at most 1. Not a launch-size reading: a grid too small to fill the resident slots is the launch fill's to price.

val filled_transactions : 
  ?fill_model:fill_model ->
  transaction_context list ->
  float

The excess transactions as the compute leg divides them by the transaction rate: each context's over its context_fill under a fill model, the plain sum without one.

val ranking_seconds_of : 
  ?peak_flops:float ->
  ?peak_memory_bandwidth:float ->
  ?cache_capacity_bytes:int ->
  ?cache_bandwidth:float ->
  ?issue_rate:float ->
  ?dram_bandwidth:float ->
  ?mma_rate:float ->
  ?mma_flops:int ->
  ?device_gathers:int ->
  ?device_gather_rate:float ->
  ?launch:(fill_model * launch_context list) ->
  ?transactions:transaction_context list ->
  ?transaction_rate:float ->
  ?occupancy:float ->
  summary ->
  reuse option ->
  float option

The ranking score of one kernel from its extractions: the larger of the compute leg and the two-tier memory leg (section contract; None for the reuse means no per-block charge, the roofline). Bandwidths in bytes/s, the issue and tile-MMA rates in operations/s. mma_flops (default 0) is the summary's tile-MMA work the backend accepts (accepted_tile_mma_flops), capped at its operations; device_gathers (default 0) its accepted statements' per-lane device gathers (device_operand_gathers), priced at device_gather_rate (gathers/s). launch is the device's fill model and the kernel's launch_contexts (absent: no launch fill). transactions (default none) are the kernel's memory_transactions, their filled_transactions priced at transaction_rate (sectors/s) and added to the compute leg (gh-ocannl-1600): without a rate, or without an excess, the leg is exactly as before. occupancy (default none) is the kernel's occupancy: below 1, the compute leg is divided by it; absent or 1, unchanged. None when neither peak is given.

val ranking_legs_of : 
  ?peak_flops:float ->
  ?peak_memory_bandwidth:float ->
  ?cache_capacity_bytes:int ->
  ?cache_bandwidth:float ->
  ?issue_rate:float ->
  ?dram_bandwidth:float ->
  ?mma_rate:float ->
  ?mma_flops:int ->
  ?device_gathers:int ->
  ?device_gather_rate:float ->
  ?launch:(fill_model * launch_context list) ->
  ?transactions:transaction_context list ->
  ?transaction_rate:float ->
  ?occupancy:float ->
  summary ->
  reuse option ->
  float option * float option

The two legs ranking_seconds_of takes the larger of: (compute, memory) in seconds, each None when its peak is not given. For reports that explain a score (Autotune.model_explain).

val ranking_mma_terms : 
  ?mma_flops:int ->
  ?device_gathers:int ->
  ?launch:(fill_model * launch_context list) ->
  summary ->
  float * float

The accepted tile-MMA work and the device gathers as the compute leg divides them by their rates (gh-ocannl-1495): each over its Tile_mma contexts' fill under a launch model, as counted without one. For reports and for fitting the two rates (benchmarks/gh1442_agreement.py --fit-mma).

val ranking_seconds : 
  ?peak_flops:float ->
  ?peak_memory_bandwidth:float ->
  ?cache_capacity_bytes:int ->
  ?cache_bandwidth:float ->
  ?issue_rate:float ->
  ?dram_bandwidth:float ->
  ?mma_rate:float ->
  ?mma_flops:int ->
  ?device_gathers:int ->
  ?device_gather_rate:float ->
  ?fill_model:fill_model ->
  ?transaction_rate:float ->
  ?lane_width:int ->
  ?max_resident_threads:int ->
  is_global:(Tnode.t -> bool) ->
  Low_level.t ->
  float option

ranking_seconds_of over analyze, launch_contexts when a fill model is given, and, when a capacity or a cache bandwidth is given, reuse_traffic; with both a transaction rate and a lane width, memory_transactions. A ranking score, not a runtime prediction — and, unlike roofline_seconds, not a lower bound either.

Tile-MMA operand loads (gh-ocannl-1254)

Not a priced term and not part of any score (only its device-gather part is, device_operand_gathers): a count the untimed choosers break exact ranking ties with (Autotune.model_default's family search, through Schedule_space.search's tie_break). Twins that differ only in a staged tile's physical layout — the plain and Swizzle_b128 staged fp8 twins of gh-ocannl-1190 — touch the same cells with the same operations, so analyze and the ranking score tie them; what differs is how a lane brings each operand tile into registers, which the backend's load rule decides (Backend_intf.codegen_capabilities.mma_operand_loads, the rule its emission applies).

Each Tile_mma operand is classified, in the statement's emission scope, from its place — workgroup-shared, per-thread (Local) or device, and its optimized.swizzled layout — by that rule. The count, per execution of the statement (the enclosing loop extents over its lane extent), is per lane: an ldmatrix operand costs one instruction per lane_bytes it delivers to each lane — 16 for a, CUDA's emitted .x4 form, and 8 for b, its .x2 form — a fragment the arm loads whole (wmma's and rocWMMA's load_matrix_sync, Metal's simdgroup_load) one load, a gathered one one load per element (fp8 gathers bytes, the 16-bit arms 16-bit halves, f32 32-bit words) — counted per intrinsic fragment of the arm's own tile, with the reloads its loop nest repeats (Backend_intf.mma_fragments), since ties fall between geometries too. Only a backend that describes its arms counts at all (CUDA, Metal and HIP; gh-ocannl-1456). A statement whose accumulator the schedule marked in optimized.simdgroup_fragments is counted in the fragment scope where the backend's hook accepts it there as an update-only call, and every other statement per statement where the hook accepts it with its destination's own place (mma_accepts, the hook itself); a statement the hook declines both ways has no count.

type operand_load =

| Ldmatrix of {
1. lane_bytes : int;
}
(*
A warp-cooperative matrix load (ldmatrix on CUDA) delivering lane_bytes to each lane per instruction.
*)
| Fragment_load
(*
A whole fragment loaded by one cooperative call (CUDA's wmma load_matrix_sync).
*)
| Gather of {
1. elt_bytes : int;
}
(*
Per-lane gathers of elt_bytes-wide elements.
*)

val sexp_of_operand_load : operand_load -> Sexplib0.Sexp.t

val equal_operand_load : operand_load -> operand_load -> bool

val operand_place : 
  Low_level.optimized ->
  Tnode.t ->
  Backend_intf.mma_operand_place

A Tile_mma operand's space and layout as the renderer classifies them: workgroup-shared when the schedule placed the node there, per-thread when its placement is Local, device otherwise; `Swizzled_b128 for a Swizzle_b128 entry of optimized.swizzled.

val statement_operand_loads : 
  Backend_intf.mma_fragments ->
  ldmatrix:(bool * bool) ->
  a_prec:Ops.prec ->
  b_prec:Ops.prec ->
  lanes:int ->
  m:int ->
  n:int ->
  k:int ->
  (int * int) option

The per-lane load instructions ONE execution of an accepted m x n x k statement issues for its a and b operands, under an arm's fragment structure and its ldmatrix answer for each operand (Backend_intf.codegen_capabilities.mma_operand_loads) — the per-statement term operand_load_count sums over executions. None where the arm's tile does not divide the extents. Exposed so a backend's description can be checked against the loop nest its hook renders (test/operations/mma_format_arm_tables, gh-ocannl-1456).

type load_count =

| No_tile_mma
(*
The code has no Tile_mma: not zero loads — it loads its operands by paths this count does not see — but nothing to count.
*)
| Undescribed
(*
Some statement the backend does not describe, or whose extents its arm's tile does not divide: a partial count would order candidates by the part it sees.
*)
| Loads of int

val sexp_of_load_count : load_count -> Sexplib0.Sexp.t

val equal_load_count : load_count -> load_count -> bool

val combine_load_counts : load_count list -> load_count

Several kernels' counts as one candidate's: Undescribed if any is, else the sum of the Loads (No_tile_mma when there are none).

val accepted_tile_mma_flops : 
  operand_accepts:
    (d_prec:Ops.prec ->
      a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      ta:bool ->
      tb:bool ->
      m:int ->
      n:int ->
      k:int ->
      fragment_target:(int * Backend_intf.mma_operand_place) option ->
      d:(int * Backend_intf.mma_operand_place) ->
      a:(int * Backend_intf.mma_operand_place) ->
      b:(int * Backend_intf.mma_operand_place) ->
      bool) ->
  Low_level.optimized ->
  int

The Tile_mma work that runs on the matrix units (gh-ocannl-1442): 2*m*n*k per execution of each statement whose emission the renderer's layouts and the backend's hook (operand_accepts, Backend_intf.codegen_capabilities.mma_accepts) accept, in either scope, exactly as operand_load_count decides it — the same walk, counted per lane group like analyze. A declined statement renders its scalar fallback and counts zero here, and so does a Tile_mma the statement walk does not reach (one in a Local_scope body), whose work analyze still counts: the ranking score prices both as scalar work.

val operand_load_count : 
  operand_accepts:
    (d_prec:Ops.prec ->
      a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      ta:bool ->
      tb:bool ->
      m:int ->
      n:int ->
      k:int ->
      fragment_target:(int * Backend_intf.mma_operand_place) option ->
      d:(int * Backend_intf.mma_operand_place) ->
      a:(int * Backend_intf.mma_operand_place) ->
      b:(int * Backend_intf.mma_operand_place) ->
      bool) ->
  operand_fragments:
    (a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      d_prec:Ops.prec ->
      scope:Backend_intf.mma_emission_scope ->
      Backend_intf.mma_fragments option) ->
  operand_loads:
    (a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      d_prec:Ops.prec ->
      scope:Backend_intf.mma_emission_scope ->
      ta:bool ->
      tb:bool ->
      a:Backend_intf.mma_operand_place ->
      b:Backend_intf.mma_operand_place ->
      bool * bool) ->
  Low_level.optimized ->
  load_count

The per-lane load instructions of every Tile_mma operand, summed over the statements' executions (see the section contract), under a backend's load rule (operand_loads, its mma_operand_loads) and fragment structure (operand_fragments, its mma_operand_fragments), for the statements its hook accepts (operand_accepts, its mma_accepts: a declined statement is Undescribed); load_count says when there is nothing, or nothing complete, to count.

val device_operand_gathers : 
  operand_accepts:
    (d_prec:Ops.prec ->
      a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      ta:bool ->
      tb:bool ->
      m:int ->
      n:int ->
      k:int ->
      fragment_target:(int * Backend_intf.mma_operand_place) option ->
      d:(int * Backend_intf.mma_operand_place) ->
      a:(int * Backend_intf.mma_operand_place) ->
      b:(int * Backend_intf.mma_operand_place) ->
      bool) ->
  operand_fragments:
    (a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      d_prec:Ops.prec ->
      scope:Backend_intf.mma_emission_scope ->
      Backend_intf.mma_fragments option) ->
  operand_loads:
    (a_prec:Ops.prec ->
      b_prec:Ops.prec ->
      d_prec:Ops.prec ->
      scope:Backend_intf.mma_emission_scope ->
      ta:bool ->
      tb:bool ->
      a:Backend_intf.mma_operand_place ->
      b:Backend_intf.mma_operand_place ->
      bool * bool) ->
  Low_level.optimized ->
  int

The part of operand_load_count the ranking score prices (gh-ocannl-1495): the per-lane load instructions of the operands an accepted statement GATHERS element by element (Gather, never Ldmatrix or Fragment_load) from a `Device place, summed over executions in the same unit. A declined statement, or one whose arm is undescribed, adds nothing (the score then prices it as before); so does a staged operand (workgroup-shared or per-thread). Zero for code with no Tile_mma.

The cost of one inlined computation (gh-ocannl-637 Part 2, gh-ocannl-1011)

The cost model's account of what a node costs to recompute at ONE read site — the flops and bytes of one instantiation of its computation, with the exactness the extraction tracks. The reader's multiplicity stays outside, as in the virtualizer's traced proxy (inline_reduction_extent × read multiplicity × inline_fanin); these queries replace the extent × fan-in factor with the modeled arithmetic, and Low_level.recompute_pricer feeds them to the flip-candidate ordering (gh-ocannl-555), the memory-budget planner and, through fa_recompute_cost, footprint-scoped materialization (gh-ocannl-616).

What is priced is code, not a rewrite of it: the inliner's own instantiation of the node's computations at a synthetic read site, after the pipeline the emitted code receives (Low_level.instantiate_at_synthetic_read). The guards the inliner emits (a multi-setter node's per-component range guards and selects, a diagonal producer's consistency guards, a unit-solved affine position's range guard and the loop it keeps), the lane-extract form of a packed-uniform producer, a scope retracted to a read, the simplifier's collapses and the CSE are all in that code, so their cost — and whether each leg is exact — is analyze's verdict on it: a guarded arm with inline work makes the op count a guards-taken bound there as everywhere, a read under a guard's arm makes the byte count one, and a component whose work hoists or whose arm only reads keeps the op count exact.

The exactness contract: a count is exact for the most general in-bounds reader — per axis a fresh index spanning the axis. What a particular reader does on top of that — folding arithmetic once a constant stands for an index, binding an affine position structurally where the generic reader's unit solving keeps a loop, collapsing a loop over a sub-image, or sharing one instantiation between sibling statements through hoist_cross_statement_cse — only LOWERS what executes, so a modeled count times a read multiplicity is an upper bound in the same sense the traced proxy's is; the reader's side of the account stays outside these queries.

type recompute = {

rc_flops : int;
(*
Operations of one instantiation.
*)
rc_bytes : int;
(*
Bytes one instantiation reads from nodes other than the computed one — its own cells are a scope local once inlined. Distinct cells within the instantiation's code.
*)
rc_flops_approx : bool;
(*
The op count is an upper bound rather than exact (analyze's flops_approx): a guarded arm with inline work, charged guards-taken. Low_level.recompute_pricer prices only operations, so this flag alone decides whether it returns a count.
*)
rc_bytes_approx : bool;
(*
The byte count is an upper bound (analyze's per-node footprint flags): notably a read under a guard's arm, of which one executes per read. Exactness is per leg, as in summary.
*)
rc_opaque : bool;
(*
Opaque code: the counts may under-estimate.
*)

}

val sexp_of_recompute : recompute -> Sexplib0.Sexp.t

val instantiation_cost : 
  ?static_indices:Indexing.static_symbol list ->
  ?placements:Tnode.Placements.t ->
  self:Tnode.t ->
  (Indexing.axis_index array option * Low_level.t) list ->
  recompute option

One read of a node whose computations are given (an optimize_ctx.computations entry, newest first): analyze over Low_level.instantiate_at_synthetic_read's code, the node's own traffic excluded. placements (default: empty) is the lineage the read is instantiated against — it decides which nested scopes the pipeline retracts to reads and whether a packed-uniform producer's counter can serve the lane-extract form; static_indices are the routine's. None when the inliner refuses the read.

val recompute_cost : 
  ?static_indices:Indexing.static_symbol list ->
  Low_level.optimize_ctx ->
  Tnode.t ->
  recompute option

One read of a node the lineage stored computations for, through instantiation_cost under the lineage's placements; None for a node with none. Nested virtual producers need no expansion: a stored computation carries every producer inlined when it was stored as a nested scope, exactly what a read replays, and a producer read that stayed a read is a read in the emitted code too. The flip-candidate pricer (Low_level.recompute_pricer) reaches the same instantiation through the world specialize_proc hands it per node — including, for a node a heuristic cap materialized, the computations the virtualizer's own walk stores once the node is not materialized. Memoized per lineage: partially apply to the context once per compile.

val tile_mma_macs_per_update : int

How many multiply-accumulates of a Tile_mma fork_join_updates charges as one scalar update (16: on cc a Tile_mma renders as a register-tiled vector micro-kernel; gh-ocannl-1564).

val fork_join_updates : cap:int -> Low_level.t -> int

Scalar updates one run of the statement performs, saturating at cap: one per executed store or register update, loop extents multiplying, Local_scope bodies counted (an apparently single store may carry a whole reduction), a whole-node Zero_out its cells, an If guards-taken, a Tile_mma its MACs over tile_mma_macs_per_update; Staged_compilation, barriers and Scan_loop read as cap. The one count both CPU fork/join judgments use (gh-ocannl-1458): the renderer's launch floor (C_syntax, config cc_grid_min_updates) and the default CPU annotator's per-dispatch gate (Schedule.default_cpu, config cpu_schedule_min_work) -- so at equal thresholds the annotator never retypes a loop the renderer would decline. A decline heuristic in machine-independent units, not a runtime prediction: arithmetic inside a store's expression is not charged.

module Calibration : sig ... end

The calibration TSV schema (config autotune_calibration_file, gh-ocannl-491 task 4) and the envelope fitter over it (gh-ocannl-514 phase 0): one row per timed candidate, the model's inputs and roofline score next to the measured time. This module is the schema's single owner — rows are emitted through to_line (by Autotune) and read back through of_line (by tools/fit_envelope.exe), so writer and reader cannot drift apart.