TIRx Metal reduction lowering

The bridge proves a semantic FP32 row reduction before assigning it to one or more SIMD groups and deriving worker-private storage. This is a target realization of execution-first TileIR, not a warp-specific DSL.

This page owns the mapping, proof, resource and intrinsic contracts. Performance measurements and regressions are maintained separately in Metal reduction measurements.

The lowering first proves semantics and ownership, then searches legal execution maps. Private and shared storage are consequences of that map, not execution levels in the source language.

1. The frontend stays execution-first

The optimization needs no warp-specific DSL object and leaks no mma_team-style hardware role into an ordinary reduction. This is the complete source for a row softmax:

auto definition = tile_kernel(
    "softmax",
    [](TensorView<const float, 2> input,
       TensorView<float, 2> output) {
        auto rows = axis("rows", input.extent<0>());
        auto one = axis("one", 1);
        auto columns = axis("columns", input.extent<1>());

        for (auto &nest : parallel(shape(rows))) {
            auto origin = coord(nest.index(), 0);
            auto value = input[origin, shape(one, columns)];
            auto shifted =
                exp(value - reduce(value, columns, maximum));
            output(origin, shape(one, columns))
                .store(shifted / reduce(shifted, columns, add));
        }
    });

The syntax preserves the language decisions made elsewhere:

• parallel(shape(rows)) defines independent logical row programs. It does not choose threads, warps, SIMD groups or memory.

• nest.index() is a logical execution coordinate, not a memory access.

• input[origin, shape(...)] loads a Tile; output(...).store(...) makes the memory effect explicit.

• reduce is a semantic algebraic region/library operation. It can become a serial fold, tree or target collective only under its numerical contract.

• exp, subtraction and division remain Tile-level elementwise operations.

Cross-entropy needs no loss-specific primitive. It composes the same semantic reductions with a guarded indirect Tile operation:

auto definition = tile_kernel(
    "cross_entropy",
    [](TensorView<const float, 2> logits,
       TensorView<const int64_t, 1> labels,
       TensorView<float, 1> losses) {
        auto rows = axis("rows", logits.extent<0>());
        auto one = axis("one", 1);
        auto columns = axis("columns", logits.extent<1>());

        for (auto &nest : parallel(shape(rows))) {
            auto origin = coord(nest.index(), 0);
            auto row = logits[origin, shape(one, columns)];
            auto label = labels[coord(nest.index()), shape(one)];
            auto peak = reduce(row, columns, maximum);
            auto total = reduce(exp(row - peak), columns, add);
            auto selected = gather(row, label, columns);
            losses(coord(nest.index()), shape(one))
                .store(log(total) + peak - selected);
        }
    });

gather remains a general Tile-level library operation. The lowering derives its guarded Tensor access from the input view; neither the source hierarchy nor the primitive names a subgroup, thread or memory level.

The compile option metal_subgroup_reductions enables a candidate family, not numerical permission. Each reduction carries its resolved ReductionPolicy: unordered_tree by default, with explicit ordered_tree, fold_left or fold_right restrictions. The current striped emitter requires unordered-tree permission and a compatible body; an ordered tree or fold stays ordered. The Metal Runtime enables the candidate family automatically when it can establish device capability and noalias and no explicit TIRx configuration was provided. Standalone bridge clients still declare those contracts. Richer accuracy/exception/deterministic-tree policies remain unimplemented.

Order restrictions also constrain the final machine compiler. Luisa Runtime disables global fast math for a kernel containing an ordered reduction; its TIRx source artifact carries requires_precise_math. TVM’s own Metal runtime requires the separately versioned precise-math extension: stock TVM hardcodes fast math on. Missing support is an explicit compile error, not a tolerance change or CPU fallback. Another unordered reduction in the same kernel may still use a collective.

Reductions inside composed groups

The same per-operation permission check also applies to a closed reduction Tile inside an already bound cooperative group, including pipeline iterations with other element and matrix phases. It does not require the complete program to match the whole-row realization.

For a group of T threads, this bounded realization assigns each reduced output to one 32-lane subgroup:

subgroup = thread / 32; lane = thread % 32
output   = batch * (T / 32) + subgroup
element  = chunk * 32 + lane

Each lane folds its stripe; all lanes in the active subgroup enter simd_sum, simd_max or simd_min. Missing elements contribute the identity, and only the subgroup leader publishes the result. The output-tail guard is subgroup-uniform. The enclosing group mapper supplies the publication fence before a later phase consumes shared results.

The matcher reuses the canonical FP32 add/max/min, scalar carry and identity checks. Output dimensions may form a rectangular nest; the reduced axis need not be the last memory dimension. Tests exercise both axis positions, extent one, ragged widths, pipeline state and more outputs than resident subgroups. The ordinary ordered realization remains when the candidate option is off or the group is not a whole number of subgroups.

The group workload analysis reuses the emitter’s exact policy/body matcher. For its reference binding it counts one complete subgroup per independent collective output, capped by the target thread limit. It no longer mistakes a scalar reduction result for only one lane of available work. Explicit thread overrides remain authoritative and can select a serial fallback.

This first composed candidate uses one subgroup per output. It is not the whole-row planner’s multi-subgroup/cached-stripe algorithm, and the group cost model does not yet price its phase-specific reduction service demand. Emitting an intrinsic alone is therefore not evidence of a speedup; see the separate performance results for the retained negative screens.

The same logical row program can be remapped without changing its Tensor views. Conversely, several memory resources can be accessed by one execution level without reversing the hierarchy.

2. Where the optimization lives

The path is intentionally split by responsibility:

C++ Tile DSL
  -> mutable, typed Candidate TileIR
  -> shared structural TileIR-to-TIRx export
  -> target-independent TIRx simplification / semantic annotations
  -> Metal subgroup reduction proof + finite planner
  -> standard scheduled TIRx (thread bindings, buffers, barriers, intrinsics)
  -> TVMx Metal code generation
  -> backend kernel/binary
  -> Runtime shader handle
  -> stream launch

Candidate TileIR remains the thin, transformable semantic layer. The Metal mapper is a bridge-local target realization; it does not force subgroup details into TileIR or manufacture a general Machine TileIR before one is needed. GroupPlan is an inspectable decision record containing threads, programs, subgroup factor, storage, synchronization and cost facts.

The implementation uses TVMx’s C++ TIRx API directly. It emits no Python and introduces no MLIR dependency. Reduction recognition is structural and typed. The strings simd_sum, simd_max and simd_min appear only at the final Metal intrinsic ABI boundary; operation selection is not performed by comparing arbitrary operation names.

The same scheduled TIRx can be compiled by the standalone TVM route or extracted as a typed DeviceArtifact for the ordinary Luisa Metal Runtime. Backend compilation and launch ownership remain outside the bridge.

Warp and SIMD-group intrinsics in the generated code

The Metal path uses simd_sum, simd_max and simd_min. They are present in emitted MSL, not merely listed as future planner capabilities. Each worker first accumulates its own ordered stripe; the intrinsic then combines the 32 lanes of its SIMD group. For a single-group program, the result is already available to every lane and no threadgroup scratch or barrier is needed.

With S > 1 cooperating SIMD groups, each group’s lane zero writes one partial to shared memory. One threadgroup barrier makes those partials visible. Every participating SIMD group then performs a second collective over the S partials, padding unused lanes with the reducer’s identity. For sum, the generated structure is equivalent to:

float partial = simd_sum(local_sum);
if (lane == 0) { shared_partials[program_base + simd_group] = partial; }
threadgroup_barrier(mem_flags::mem_threadgroup);
float total = simd_sum(lane < S ? shared_partials[program_base + lane] : 0.0f);

program_base is zero for a one-program group. With explicit cooperating program packing it is packed_program * S, isolating each program’s partials while all physical threads participate in the same barrier.

The second collective is replicated across participating groups so subsequent distributed consumers have the result without an additional broadcast barrier. This implementation uses the native collective rather than an explicit shuffle-down loop. It does not currently need ballot, match or scan intrinsics; using more intrinsics is not itself an optimization objective. Generated MSL does not by itself prove a particular final machine-instruction sequence.

The scope is the admitted Metal FP32 add/max/min family. The explicit metal_subgroup_reductions option only enables candidates; the local policy must permit their reassociation and permutation. Disabled or unproved automatic cases retain the reference path, and an unrealizable explicit subgroup binding is rejected. This is not a claim that the CPU, CUDA or arbitrary reducer path has the same collective optimization.

The implementation is ReductionProgramMapper::_reduction in reduction.cpp. The execution tests check the generated intrinsic names, one-/multi-group barrier/storage counts, numerical outputs and disabled/fallback behavior.

3. Semantic domain and fail-closed admission

Let a root logical parallel region contain P > 0 independent programs. Its body may contain reduction regions r in R and independent Tile-element domains d in D. A reduction has a static positive extent N_r, FP32 state, identity z_r, associative operation op_r and pure contribution expression f_r(e). An element domain has a static count I_d.

The current mapper admits only the following bounded subset:

Requirement	Checked fact
Target and binding	Metal target, 32-lane subgroup, outermost automatic or explicit subgroup root
Kernel ABI	noalias arguments; read-only forwarding is re-proved before use
Reduction type	FP32 add, maximum or minimum
Canonical state	one local scalar carry, exact identity, one update, no extra observation
Contribution	pure typed expression; no carry/temporary escape or unknown call effect
Control	static unit-step serial source loop; no conditional containing the reduction
Execution nesting	no nested logical parallel inside the mapped program
Global effects	stores occur only inside a distributed independent-element domain
Distributed private storage	every nonscalar local buffer with distributed stores has compact row-major accesses proved equal to the current worker owner
Guarded input views	every delayed source is immutable; each lazy consumer path proves its temporary and source indices in bounds
Manual resources	only compatible private constraints; unsupported placement rejects the path
Dynamic control	no while, break, continue, return, assert or opaque Tile primitive

The structural exporter attaches a reducer-kind marker only after matching the Candidate TileIR update. The Metal pass does not trust the marker by itself: it rechecks the exact initializer, allocation, loop, update, operands, effects and types in current TIRx. Every marked reduction must match exactly. An explicit subgroup binding that cannot be realized is an error; automatic binding may fall back to the reference path.

The option permits a floating-point tree order. The saved tests use finite inputs and compare against an FP64 oracle within recorded tolerances. Complete NaN payload, signed-zero and deterministic bitwise policies for max/min/add remain future typed numerical contracts, not properties inferred from the current performance tests.

4. Execution mapping algebra

For a candidate using S cooperating SIMD groups per logical program, define

L = 32                         lanes per SIMD group
W = L * S                      workers per logical program
q = floor(thread / W)          program coordinate within a group
w = thread mod W               worker coordinate within a program
s = floor(w / L)               SIMD-group coordinate within a program
l = w mod L                    lane coordinate

The planner considers every integer S from 1 through min(32, floor(target_max_threads/32)), restricted by shared/private capacity and the explicit search budget. Non-power-of-two widths are legal. The 32-subgroup algorithmic bound comes from the second collective: one lane reads each subgroup’s partial. It is not a universal schedule space.

4.1 One SIMD group per program: spatial packing

When S = 1 wins under automatic planning, a threadgroup can contain Q independent logical programs, where

1 <= Q <= min(P, 8, floor(max_threads / 32))
blocks = ceil_div(P, Q)
threadgroup_threads = 32 * Q

p = block * Q + q
e = 32 * chunk + lane

The final partial group is guarded by p < P. Each subgroup executes one program and no shared partial is needed. Packing amortizes threadgroup setup without inventing an order or dependence between the source parallel instances.

For example, P=17, N=257 chooses one subgroup per program but reports a 256-thread group: eight independent row programs are packed into its eight subgroups. reduction_subgroups_per_program=1 distinguishes this from one row using all 256 workers.

4.2 Several SIMD groups per program: cooperative striping

When S > 1, automatic packing retains one logical program per threadgroup:

blocks = P
threadgroup_threads = W
p = block
e = W * chunk + w

Each worker folds its strided elements into a private scalar. A reduction then uses this uniform protocol:

worker-local serial fold
  -> simd_{sum|max|min} in every subgroup
  -> lane 0 writes shared partial[r, s]
  -> one threadgroup barrier
  -> lanes l < S read partial[r, l], other lanes use the identity
  -> uniform simd_{sum|max|min}
  -> every worker receives the program result

The first collective must execute uniformly; placing it under lane == 0 would be invalid. Only the shared write is lane-zero conditional. The second collective also executes uniformly, so subsequent replicated element domains can consume the result without a hidden cross-subgroup race.

The shared footprint is exactly

shared_bytes(S) = |R| * S * sizeof(float),  when S > 1
shared_bytes(1) = 0.

The emitted barrier count is recorded as a static site count, not a dynamic execution count. Cooperating subgroups report independent_subgroups=false; the existing barrier-elision proof cannot misclassify them as independent programs.

4.3 Explicit packing of cooperating programs

An explicit reduction_programs_per_group=Q>1 can also pack programs that each use S>1 SIMD groups. Collaboration within one program and packing independent programs are separate factors; neither is a memory hierarchy.

T = 32 * S * Q                 total physical threads per group
W = 32 * S                     workers cooperating on one program
q = floor(thread / W)          packed program coordinate
w = thread mod W               worker coordinate within that program
s = floor(w / 32), l = w % 32   local subgroup and lane coordinates
p = block * Q + q              logical program coordinate before loop min
partial[r, q*S + s]            shared slot written by local subgroup s
blocks = ceil_div(P, Q)         P is the logical program count

one physical threadgroup, Q=2, S=2
  program q=0                   program q=1
    subgroup 0 -> partial[0]      subgroup 0 -> partial[2]
    subgroup 1 -> partial[1]      subgroup 1 -> partial[3]
  ------------------ one uniform group barrier ------------------
    read partial[0:2]             read partial[2:4]
    both groups get result 0      both groups get result 1

Shared storage grows to |R| * Q * S * sizeof(float). Worker-private stripes are still derived from W, not T; packing does not give a worker twice the private capacity or another program’s elements. An exact thread request fixes T and must be divisible by 32*Q. Without one, the bounded solver searches fitting cooperating widths for that explicit Q. Thread, shared-memory and private-state checks are applied before cost ranking.

For a partial final group, a whole-program if (p<P) would put the group barrier under divergent control. Instead, inactive programs replay the last valid row (min(p,P-1), plus the original loop minimum) and suppress only external stores. Their input addresses remain valid even for guarded, data-dependent gathers; they still perform reads and arithmetic. Active programs retain unique element coverage and store ownership.

This requires an additional conservative proof: reduction-containing enclosing loops must have constant minimum, unit extent and unit serial step. Repeated or dynamic enclosing loops are rejected, including fully packed cases: scratch reuse across iterations needs a read-before-next-write fence proof. A packed tail also rejects any external buffer observed both read and written, under the existing noalias and pure-effect admission checks. Replay must not race with a valid program’s writes. Unknown proofs decline this realization.

The automatic Q=0 option keeps the established candidate family; it does not begin choosing cooperating packed groups. The fixed packing replay finds substantial regressions as well as two narrow gains, so the extension remains explicit/JIT-only, without a new default or fitted coefficient.

4.4 Coverage and ancestry

For every distributed domain of count N, the default V=1 mapper enumerates

chunk in [0, ceil_div(N, W))
e = W * chunk + w
execute iff e < N.

e is unflattened into the domain’s named logical axes using their original mixed-radix order. The root program coordinate p and every ancestor coordinate are substituted independently of memory indexing. Therefore the mapping covers each (p,e) exactly once and preserves the ancestor execution prefix used by Tensor origins.

The optional PlannerOptions::reduction_lane_elements generalizes this to blocked-cyclic ownership without changing program ancestry:

e = (W * chunk + w) * V + v,  0 <= v < V,  V in {1,2,4,8}
private_slot = chunk * V + v
inverse: v=e%V, w=(e/V)%W, chunk=e/(W*V)

The inverse establishes unique coverage, while the existing ownership audit requires producers and consumers to refer to the same logical element before either is remapped. The maximum private allocation becomes floor(N/(W*V))*V + min(N%(W*V), V). Only the partial final pack carries a bounds predicate; no invalid load/store is speculatively evaluated. V changes the worker-local FP32 recurrence and requires the existing reduction-tree permission, unlike ordered stripe unrolling. It is not a vector-instruction promise. The layout and GPU/E2E evidence records the generic implementation, resource checks and frozen replay.

This is the concrete instance of the more general relationship

ancestor execution coordinates + local element coordinate
    --layout correspondence--> logical Tensor coordinate
    --Tensor layout-----------> physical address.

The execution map changes the producer of the local element coordinate; it does not reinterpret the Tensor layout.

5. Logical Tile materialization to physical worker storage

Softmax exposes the key execution/memory separation. The logical expression

auto shifted = exp(value - reduce(value, columns, maximum));
output(...).store(shifted / reduce(shifted, columns, add));

has two consumers, so the shared structural lowering preserves shifted as one logical definition. By default the same rule applies to every pure multi-consumer Tile, independent of whether the opcode is exp, add or sub. Before execution mapping that logical object has N elements. Naively allocating it after distributing rows but before distributing elements creates N private values per worker.

At V=1 the subgroup mapper may replace logical T[N] with worker-private T_worker[ceil_div(N,W)] (the generalized V-dependent bound is above), but only after proving all of the following:

1. the object is a compiler-owned local FP32 materialization with one allocation and one defining store;

2. its expression is pure and does not read or expose the object recursively;

3. it has at least one load and no opaque pointer/variable escape;

4. for every store and load in its enclosing loop domain, flatten(indices) == owner_coordinate is provable; and

5. the owner coordinate is the same distributed logical element e used by that domain or reduction.

After mapping, the physical slot is chunk = floor(e / W). A fixed, permuted, cross-element or escaping access with an unknown owner proof cannot use this substitution. The independent distributed-local audit then either proves the uncompacted private allocation safe or declines the complete subgroup map; it is never silently redirected to another worker’s slot.

For width 4096 with exactly 256 workers, each worker owns only 16 FP32 values. Auto-layout tests independently enumerate the current objective and check the private stripe required by the chosen width, while rejecting the old per-thread [4096] form. This is a resource-planning result, not a new source-level Memory declaration. Explicit manual Memory remains for deliberate expert placement and still requires explicit .store().

5.1 Shared SSA is not a physical allocation decision

Fused residual LayerNorm makes the distinction observable:

auto combined = X[origin, shape(one, columns)] +
                residual[origin, shape(one, columns)];
auto mean = reduce(combined, columns, add) / width;
auto centered = combined - mean;
auto variance = reduce(centered * centered, columns, add) / width;
Y(origin, shape(one, columns))
    .store(centered / sqrt(variance + 1e-5f));

combined and centered each have several consumers. Cloning their producer expressions makes generated Metal load every X and residual element four times. Preserving the two SSA definitions does not require two source-level Memory declarations. The Metal mapper proves element ownership and realizes them as two worker stripes, so each input element is loaded once.

Structural lower(function) defaults to SharedTileMaterialization::PRESERVE because erasing sharing is irreversible and deprives later analyses of a legal choice. EXPENSIVE_ONLY is retained as an explicit lowering/JIT candidate: it preserves shared transcendental Tiles but recomputes cheap arithmetic. Neither mode changes TileIR semantics. On the measured M1 Max, Metal selects PRESERVE; LLVM CPU selects EXPENSIVE_ONLY. This is precisely why the decision belongs to target planning rather than the C++ DSL.

Worker stripes also have an explicit software-state bound:

stripe_scalars(S) = sum[t in materialized Tiles]
                    ceil_div(elements(t), 32*S)
stripe_scalars(S) <= max_reduction_striped_scalars_per_worker = 64.

The value is a compiler-created storage budget, not a claim about allocated hardware registers. A backend may scalarize or spill it. A candidate above the bound is rejected before code generation instead of silently creating an unbounded private array. At residual LayerNorm width 4096, 32- and 64-thread maps would require 256 and 128 scalars per worker and are rejected; 128/256 threads require 64/32 and remain legal.

Reduction factorization changes participants and local slots. The semantic contribution set, grouping map, identity and merge contract remain intact.

5.2 Guarded immutable views and dynamic gather

Cross-entropy revealed another ownership case. Before mapping, a logical row snapshot can legally be consumed both as V[e] by reductions and as V[label] by a guarded gather. Mechanically distributing its initialization while retaining a private V[N] per worker is invalid:

worker w initializes only private_w.V[e(w)]
worker 0 later reads private_0.V[label]

Unless label == e(0), that read does not observe the logical snapshot. The first prototype did exactly this and failed six of seven cross-entropy rows; the reductions themselves were correct.

The view analysis is now path-sensitive for pure lazy if_then_else calls. For a target-buffer load under path predicate G, every index bound must be proved from the loop domain, contained syntactically in G, or follow from G. Under the independent noalias/effect proof, substitution preserves the lazy source guard and produces:

selected = ite(0 <= label && label < N,
               global_logits[row, label], 0)

The logical snapshot allocation disappears; reductions and gather read the same immutable Tensor directly. Conditions, address expressions and fill values remain lazy. An unguarded memory-dependent index is still unknown, as are predicates outside the supported pure Boolean fragment.

This optimization is not the correctness firewall. A separate whole-program audit examines every nonscalar local buffer that has a distributed store. It requires one allocation, compact storage and flatten(access_indices) == owner_coordinate for every observed load and distributed store. The current proof intentionally rejects otherwise safe but unrecognized permutations. Automatic execution then falls back to the reference map; an explicit subgroup request reports that it is unrealizable.

Forwarding is a profitable realization; the distributed-local audit is the independent fail-closed correctness boundary.

6. Cost model and finite solver

Legality is decided before profitability. Let D be the independent element domains, R the reductions, I_d and N_r their counts, S the candidate subgroups per program, W=32S, and Q the separately searched packed-program count (automatic Q>1 only for S=1; explicit Q can also use cooperating groups). At V=1 the bootstrap score is

rounds(S) = sum[d in D] ceil_div(I_d, W)
          + sum[r in R] ceil_div(N_r, W)

score(S, Q) = alpha * rounds(S)
         + beta  * |R| * S
         + gamma / Q

alpha = 1, beta = 2, gamma = 16.

For non-default consecutive-worker width V, each ceil_div(N,W) becomes floor(N/(W*V))*V + min(N%(W*V),V), the maximum live scalar work per worker. The resource bound uses the same layout-dependent expression, and backend policies receive V explicitly. This accounts for tail ownership but does not model vector issue, coalescing or reduced active-group concurrency.

Policies also receive physical group count ceil_div(programs,Q), total useful scalar elements summed over these separate domains, and useful lane work elements/(rounds*W). These immutable facts do not assert measured occupancy. Device thread capacity is now queried by the benchmark adapter, instead of inheriting TVM’s 256-thread target default. The algorithm’s 32-partial collective bound remains independent of that device limit.

Each independent domain is rounded separately. Combining their total before ceil_div would underprice separate softmax passes at a tail width.

The three terms represent worker stripe rounds, SIMD collective work and amortized program/threadgroup setup. They are dimensionless priors, not measured instructions, occupancy or nanoseconds. Ties retain the smaller S.

The v1 score currently treats every scalar round alike. It does not yet count global loads duplicated by recomputation, expression depth, or the different service costs of local stripe access. The residual LayerNorm policy search therefore exposes up to 43.66% model regret on this finite candidate set. This is recorded as a model defect; correctness-checked staged/JIT measurement is the selection authority until those features are calibrated.

Before scoring, a candidate is rejected if it violates any of:

S <= min(32, floor(target_max_threads / 32))
threadgroup_threads <= target_max_threads
shared_bytes(S, Q) <= target_shared_memory
stripe_scalars(S) <= max_reduction_striped_scalars_per_worker
enumerated_widths <= max_thread_candidates
finite, nonnegative coefficients
supported exact thread constraint, when present.

There are at most 39 unconstrained automatic (S,Q) candidates (eight Q choices for S=1, 31 wider single-program choices), so exhaustive enumeration is clearer and more exact than integer programming or simulated annealing here. Those methods become relevant only when later planners jointly choose tile factorizations, layouts, atoms, storage versions and pipeline schedules over a much larger discrete space.

threads_per_group=0 means automatic choice. A nonzero value is an exact JIT constraint and must be a legal multiple of 32. Without an exact packing request it fixes cooperating workers per program, retaining the original interface. reduction_programs_per_group>1 instead explicitly fixes Q; any simultaneous thread request must equal 32*S*Q for a supported S. Constraints are never silently clamped or reinterpreted.

The optional service policy prices packed-tail replay reads for all ceil_div(P,Q)*Q cooperating program slots, but global writes only for the P active programs. Payload facts per program remain useful work, not padded launch totals. The analytic prior has no such service term and currently rewards packing’s setup amortization without its occupancy/synchronization costs; the fixed packing measurements expose that limitation.

The bridge now exposes a backend-owned cost-policy interface and bounded ordered stripe unrolling. See the implemented policy and search contract. The JIT harness can search --tune-reduction-packing, --tune-reduction-unroll and --tune-reduction-lane-elements alongside exact thread widths. The original model remains an uncalibrated prior; it does not price the unrolling choice or V’s hardware issue behavior. Host-wall throughput remains the default tuning objective; explicit --tuning-metric gpu-control instead requires the no-counter Metal command-buffer metric. Both objectives remeasure the winner and retain GPU and E2E scopes separately in frozen replay reports.

6.1 Plans selected in the original 20-case run

The historical launch-plan table now lives with the measurements that produced it. It is not the current automatic schedule contract: later shared-SSA preservation, target-width and resource policies change the candidate facts. This link retains the original section anchor without duplicating experiment data in the lowering reference.

7. Staged/JIT tuning is the outer authority

The analytic solver chooses among physical maps for one captured shape. It does not require a single universal capture. A staged outer tuner can simply compile several concrete parameterizations:

uv run --no-project --python 3.13 --with torch --with numpy python \
  scripts/benchmark/tile_torch/run.py \
  --native cmake-build-tirx/bin/benchmark_tile_tirx \
  --output NEW_EMPTY_DIRECTORY \
  --backends metal --operations rmsnorm \
  --metal-subgroup-reductions \
  --tune-group-threads '32,64,128,256' \
  --samples 9 --sample-ms 60 --warmup-ms 100

For every width, the runner recaptures/JIT-compiles the ordinary host configuration, validates the complete output, and retains failed candidates. It selects by native throughput only among valid trials, then recaptures, recompiles, validates and measures the winner again. The published row is that fresh measurement, not the optimistic search minimum. Candidate order rotates across shapes and a finite compile budget rejects oversized products.

This cleanly separates three questions:

Layer	Role	Authority
Semantic proof	Is a tree/distribution legal?	compiler; never timing
Analytic cost model	Which legal maps should be shortlisted/defaulted?	replaceable target prior
Staged/JIT measurement	Which concrete valid candidate is fastest here?	correctness-checked measurement

Measured data may calibrate alpha, beta, gamma or a richer device profile. It must never make an illegal candidate legal.

Materialization is another ordinary staged dimension:

uv run --no-project --python 3.13 --with torch --with numpy python \
  scripts/benchmark/tile_torch/run.py \
  --native cmake-build-tirx/bin/benchmark_tile_tirx \
  --output NEW_EMPTY_DIRECTORY \
  --backends metal --operations residual_layernorm \
  --metal-subgroup-reductions \
  --tune-shared-tile-materializations preserve,expensive-only

The runner includes this choice in the finite Cartesian product with tile, pipeline and execution-width candidates, enforces the global JIT budget, retains failed candidates, and recompiles/revalidates the measured winner. There is no capture-once super-kernel.

8. Correctness and structural verification

The regression suite checks both generated structure and actual hardware results:

• option/target/noalias contracts, the raw bridge’s conservative candidate default, and Luisa Runtime’s capability-resolved automatic selection;

• row sums at widths 127, 257, 1024 and 4096, including expected one/one/four/eight-group plans;

• softmax at 3×4096, requiring two reductions, an independently enumerated minimum-cost width, the corresponding exact private stripe, simd_max, simd_sum, and every output element against FP64;

• LayerNorm at 3×4096, requiring two reductions and checking all 12,288 affine outputs against an independent FP64 mean/variance formula; the test independently checks the selected compact stripe for its shared cheap arithmetic Tile;

• 14 additional V=1/4 softmax layouts, automatic and exact widths 96/160/224/288/512/1024 on a capable device, ragged domains, both collectives, complete outputs, every legal candidate reaching the backend policy and rejection of insufficient search budgets;

• canonical multi-consumer arithmetic under both PRESERVE and EXPENSIVE_ONLY, proving that the first retains the SSA boundary and the second is a real recomputation candidate;

• cross-entropy at 7×4096, including two collectives, a guarded dynamic label gather, absence of the private [4096] input snapshot, and every loss against a stable FP64 log-sum-exp formula;

• an explicitly materialized derived-logits negative case, which must decline subgroup mapping because its gather crosses private worker ownership;

• a CPU structural pair showing that an unguarded memory-dependent consumer index retains its snapshot while the same index under a complete lazy bounds guard is safely forwarded;

• minimum and maximum together at 7×1024;

• uniform first collectives and guarded tails in generated Metal;

• 36 cooperating-packing configurations for sum, softmax, no-affine LayerNorm and paired min/max, including non-power-of-two widths, cached/ragged inputs, a 1024-thread group, automatic width selection and sentinel guard rows;

• six raw-IR packing admission cases: direct/unit-wrapper success and repeated, row-varying, read/write-tail and over-limit rejection, with a typed check that the accepted group fence is not nested under a conditional;

• CPU fallback behavior and unchanged reference paths; and

• benchmark/replay metadata, policy preservation, cooperating-subgroup facts and staged/JIT winner revalidation, including materialization policy.

Executed counts, historical checkpoints and remaining worktree failures belong to the validation record. The cooperating-packing measurements link the latest full CTest log, independent audit and retained negative results. The contracts above describe required coverage, not a claim that every current worktree or target passes all tests.