18.3.1. CPU, single-threaded — the universal baseline and the oracle🔗

Instantiate the model at the scalar executable carrier (α := Float). The kind overlay erases by .magnitude to the bare floating-point program of Step 4's payoff; every intermediate lives in a register, so the arithmetic intensity per work-item is maximal and the kernel is compute-bound on one core. This strategy is unconditional: it runs any science model, including those whose interleaving of I/O and computation, data-dependent iteration, or irregular memory access makes efficient parallelism genuinely hard — the cases where the later strategies do not apply. It is also the oracle: because it is the same erased kernel, its per-pixel result is the reference the parallel and GPU strategies are checked against, bit for bit. The cost is that it uses a single core.

18.3.2. CPU, multi-threaded — coarse-grained task parallelism🔗

Keep the scalar carrier and split the row-independent (pixel) axis into contiguous slices, running the whole kernel on each slice on its own dedicated Lean Task. The parallelism is Lean's own task construct — no external threading library, no OpenMP shim — and it is coarse-grained: one task per slice runs the entire op-chain, so the compute-per-fork is maximal and per-operation fork/join overhead is nil. This is exact whenever the work-items are independent (which the per-pixel retrieval is), and it scales toward the core count when the model has good arithmetic intensity — enough compute per work-item that the cores are kept busy rather than starved on memory bandwidth or throttled by task overhead. A model with poor intensity, or one whose items are not independent, sees little benefit here and is better served by the single-threaded baseline. This strategy is the deployment layer's runSharded.

18.3.3. GPU, eager — one pre-compiled kernel per operation🔗

Instantiate the model at TorchLean's batched device carrier (α := CudaT). Each NumCarrier operation on this carrier is a single pre-compiled CUDA kernel, launched by a foreign-function call, that reads its operand buffers from device memory and writes one output buffer back. Running the write-once source at this carrier therefore issues a sequence of device kernel launches, one per arithmetic operation of the model, and the GPU parallelizes within each launch — one thread per pixel per operation.

It is worth being exact about what is not happening here, because it is a common confusion: this is not an intermediate representation being interpreted on the GPU, and no IR is involved at all. The Lean-level operation sequence directly drives a sequence of hand-written device kernels through the foreign-function boundary — eager, operation-at-a-time dispatch, the device analogue of running the scalar kernel one statement at a time. There is no on-device program, no fused kernel, and nothing that walks a graph at run time.

This strategy is automatic in the strongest sense — the very same write-once source runs on the GPU with no GPU code written — and it wins substantially when the pixel batch is large, because each launch amortizes over the whole batch. Its ceiling is set by memory bandwidth: every intermediate of the model is materialized as a full device buffer and round-tripped through DRAM, so the workload is memory-bound and its arithmetic intensity — arithmetic performed per byte moved — sits far below the device's roofline (for the SMAP–NISAR AVS fit, an intensity of roughly 0.17 against an ideal near 13.75, an ~80× gap). The device spends its time moving buffers, not computing. This is the current production GPU path.

18.3.4. Fused forms — a targeted middle ground🔗

Between dispatching every operation eagerly and compiling the whole model there is a targeted lever: a fused form. On the eager carrier a single composed sub-expression of the model — say a two-way attenuation exp(c · x · y) — is several kernel launches and as many DRAM round-trips, one per operation. A fused form replaces that one recurring shape with a single kernel the carrier provides directly, computing the composition in one pass with its intermediates in registers. Crucially the fused form is a refinement of the composition, not an approximation of it: it is required to be bit-identical to the NumCarrier expression it stands in for — same operations, same association — so substituting it changes only how fast the shape is computed, never what it computes. Where a carrier offers no fused form for a shape, the model simply falls back to the plain composition; the write-once source is unchanged either way.

This lever is domain-neutral and extensible. The forms are named by their mathematical shape, not by any application: the first is the scaled product exponential exp(c · x · y), of which a soil-moisture vegetation attenuation exp(−2 · b · ndvi) and a Beer–Lambert two-way extinction exp(−2 · κ · ℓ) are instances — the domain reading lives downstream, in the science model that supplies the coefficient. Further forms — an affine exponent exp(a + c · x) (Arrhenius, log-linear models), a Gaussian exp(−γ · x²) (radial-basis kernels), a numerically-stable logSumExp, a reciprocal square root — drop in the same way, each earned by a specific hot path rather than added speculatively.

A fused form is the special case of the general fusion the next strategy performs. The megakernel compiles the whole model into one kernel; a fused form hand-collapses one named shape within an otherwise eager execution. It is the right tool when a single sub-expression dominates and the rest of the model is content to run eagerly, or as the concrete kernel a compiled path targets for that shape. The same discipline governs both: a fused form is trusted because it is a refinement of its composed spec, exactly as the megakernel is trusted because it is proved faithful to the recorded model.

18.3.5. Vocabulary extensions — tabulated data as a declared capability🔗

A fused form refines a shape the base vocabulary can already compose. Some operations are not like that: a look-up into tabulated data is a data-dependent gather, and the branchless carrier vocabulary deliberately has no indexing to compose it from — the exclusion that makes every model above lower to one straight-line kernel. When a model genuinely needs a table (a tabulated transfer function, a calibration curve), the honest move is not to smuggle the gather in but to declare it: a vocabulary-extension class whose single operation is piecewise-linear interpolation into a named, layered, uniform-abscissa table. Unlike a fused form it has no composed fallback — a model that uses it says so in its type, so the dependence on tabulated data is visible exactly where the write-once discipline wants it: in the instance context.

The extension keeps every leg of the discipline. Its reference semantics is one small function — clamp, floor, linear interpolation, the uniform-grid analogue of the operational interpolator — which is simultaneously the scalar oracle, the value a recording stores (recorder-faithful by construction), and the meaning the interpreter assigns a recorded fetch. On the device it is realised by texture hardware: the table lives in a layered texture bound once, fetched through the GPU's dedicated texture cache — a table of tens of kilobytes is simply resident there, so per-fetch traffic effectively vanishes. One boundary must be stated rather than wished away: the texture unit's hardware interpolation uses a low-precision fixed-point blend weight, so the hardware-filtered mode is a tolerance-bounded accelerator, never bit-reproducible; the point-fetch mode — two exact texel reads and an explicit, contraction-blocked lerp — is the bit-reproducible twin of the reference, and it is the mode every bit-exact claim quantifies over. The split is fixed at generation time, not discovered in production. Two further consequences come for free: the table's name rides in the recorded node, so common-subexpression elimination distinguishes fetches into different tables with no change to its key; and because texture hardware interpolates only uniform coordinates, an inverse table over a non-uniform abscissa must first be inverted and resampled host-side — a one-time, measured, controllable approximation that belongs to the model's accuracy budget, stated next to the table's own discretization bias.

18.3.6. GPU, megakernel-compiled — Lean → recorded IR → CUDA source🔗

The remaining headroom is recovered by compiling the model rather than dispatching it operation-by-operation. Because the write-once kernel is branchless — the NumCarrier guarantee — the same source, instantiated at a recording carrier, does not compute a number: it records its own elementwise operation graph. That graph is common-subexpression-eliminated to its DAG of distinct sub-expressions and emitted as a single fused CUDA __global__ kernel: one thread per pixel, the whole model held in registers, with device memory touched only for the model's actual inputs and outputs. This is a genuine ahead-of-time compilation — from the Lean source, through a recorded intermediate representation, to CUDA C source text — and, again, not an interpreter: the generated kernel is ordinary compiled CUDA, with no graph walked at run time.

The trade the previous strategy could not make is now available: with every intermediate kept in a register instead of round-tripped to DRAM, the workload moves from memory-bound to compute-bound, and its arithmetic intensity rises above the roofline knee — as close to the device's peak as the science allows. The cost is a precondition: the model must have favourable AI properties — branchless (guaranteed) and register-fittable, since the register pressure of the fused kernel bounds how much of the model can be held live at once (a very large model is fused per-step and looped on the device, rather than fused whole). This is why the strategy is not universal in the way the single-threaded baseline is: it buys the roofline in exchange for a structural demand on the model.

Two properties make this more than a code generator. First, it is verified: the recorded graph is proved — sorry-free, over all inputs, by the tape's forward-value faithfulness — to compute exactly the source kernel, so the generated kernel is faithful to the model by a theorem, not by a tested diff. Second, it is bit-controllable: compiled with fused-multiply-add contraction disabled and no re-association, the megakernel is bit-identical to the eager device path, because fusion changes only where an intermediate lives (a register versus DRAM), never the arithmetic performed — the speedup is pure memory-traffic elimination, orthogonal to the numerics. (Enabling contraction trades that exact identity for additional speed and a more-accurate-but-different result, a separate, quantified step.)

18.3.7. Recording carriers are deferred — share loop-carried state or the graph explodes🔗

The megakernel strategy carries one authoring hazard worth stating on its own, because it is a property of the recording carrier rather than of any model. That carrier is deferred: a recorded value is a thunk that re-emits its sub-graph on every reference, not a memoized handle to an already-emitted node. Reusing an intermediate therefore records it again — and an iterated computation reuses its loop-carried state on every step. A fixed-point sweep whose accumulator appears k times in the body, composed to depth d, records on the order of k^{d} copies of the first step before common-subexpression elimination can collapse them. CSE dedups the result, but the recorder must first build that intermediate, so a deep, reuse-heavy fold can exhaust memory at elaboration time even though the final DAG — and every carrier's actual arithmetic — is small.

The discipline is the recording-time analogue of the megakernel's own fuse one step, loop the device shape: record one step and materialize the loop-carried state to a single node between steps, so the next step references it as one shared leaf instead of re-recording the entire prior step. Materialization is semantics-preserving — the shared node computes the same value — so the recording stays bit-for-bit the same kernel; only its cost of being recorded changes, from exponential to linear in the step count. This is invisible at the scalar, threaded, and eager-GPU carriers, where a value is just a number or a buffer and reuse is free; it surfaces only when the same write-once source is run at the deferred recording carrier, and it is a general hazard for any science model with an unrolled iteration recorded that way — not a quirk of one retrieval. It was found and fixed in exactly that setting: an eight-sweep loss-coupling fixed point in the SMAP–NISAR closed-form Stage-3 retrieval, its accumulator reused several times per sweep, unrolled past a hundred gigabytes at elaboration until the fold was threaded to share its accumulator per sweep — after which the same recording completed in seconds, the generated kernel unchanged.

18.3.8. Right-sizing the deployment — the memory shape is computed, the platform is asked🔗

Choosing a strategy is only half of a deployment decision; the other half is a number — how many task-shards the multi-threaded strategy forks, or how many pixels a device batch carries. Both are bounded by memory before they are bounded by compute: the eager device carrier materializes a full buffer per live intermediate, and the sharded CPU path holds every concurrent slice at once. And the bound is a property of this model on this machine, so a hand-set constant is wrong somewhere — cores idle on the large host, or an out-of-memory kill on the confined worker. The calculus therefore treats sizing the way it treats everything else in this chapter: the model's memory shape is computed, from the same recording that already proves faithfulness and computes arithmetic intensity; the platform is asked what it will actually grant; and a small solver combines the two — with an explicit operator override that wins verbatim when someone knows better.

The model half is computed, not cited — the same standard the intensity accounting set. Memory use is affine in the pixel count for every strategy, bytes(P) = fixed + perElement · P, and the per-element term falls out of the recorded DAG per strategy. For the fused megakernel it is exact: inputs plus outputs, four bytes each — every intermediate is a register — with a bound table charged once per launch. For the eager carrier it is the peak count of simultaneously-live buffers when the DAG is evaluated in tape order, each buffer freed after its last consumer: one pass recovers every node's last use, one walk takes the running peak (maxLiveNodes, reported beside the intensity numbers by the same aiReport), and the sharded CPU path adds its host marshaling columns on top. One honesty clause belongs here: the eager number is a lower bound, because "freed promptly after its last consumer" is what a garbage-collected finalizer approaches rather than guarantees, and a driver that loops a recorded step holds its carry across iterations. So the static shape is the prior — what makes a freshly authored model safely sizable before it has ever run — and a measured probe of a real block (allocator peak on the device, child peak memory on the host) is the authority that calibrates it.

The platform half is asked with its provenance kept, because the budget that matters is the one enforcement reads. A confined process is killed at its cgroup limit, not at the host's advertised available memory — a container capped at 28 GiB on a host reporting 62 GiB is the observed norm on shared worker queues — so the budget query asks cgroup v2 first (the process's own cgroup, minimum over its ancestors), falls back to cgroup v1, and only then to the host's own figure, every answer labeled with its source so the log records which limit the sizing believed. Core counts get the same discipline: the scheduler's affinity mask intersected with the cgroup CPU quota, never the raw host core count. On the device the query is the CUDA free-memory figure, taken after the carrier's warm-up — the context's fixed tax is then already netted out of it, which is one fixed overhead nobody has to specify.

Two solver shapes close the loop, because the two knobs constrain differently. Task-sharding partitions one resident tile among concurrent shards, so the variable term is invariant in the shard count and only a per-shard fixed cost scales with it — and when the resident term alone exceeds the budget, no shard count fits, and the solver says exactly that (shrink the tile, not the count) instead of clamping to a plausible-looking answer. Block-concurrency — a fixed block size, choosing how many run at once — divides the remaining headroom by the per-worker cost. Either way the decision is announced on one line with every term and its source, so an out-of-memory kill or an inexplicably idle machine is diagnosable from the log alone; and the validation suite pins the peak-residency walk on hand-computed live-set structures and the capacity parsers on captured platform records, so the shapes are checked facts under the same CI as the parity theorems.

18.3.9. The through-line🔗

The four strategies are one source. The single-threaded baseline runs anything and is the oracle; the multi-threaded and both GPU strategies trade a structural demand on the model — independence and good arithmetic intensity, and for the megakernel, register-fittability — for progressively more of the hardware's peak. What licenses the automatic parallelization and fusion of the latter three is not a heroic compiler analysis but the NumCarrier discipline itself: a model that typechecks against it is already branchless and fusible, so "go fast, automatically" is earned at authoring time by the same type that made "write once, correctly" true. The performance is a corollary of the specification, not a second, hand-written artifact that must be kept in step with it. And the deployment's size is earned the same way: the recording that licenses fusion also yields the model's memory shape, so how much of the spectrum a given machine can sustain is computed from the same single source — asked of the platform at run time, never tuned into the model.